In reply to ben@SystemVerilog.us:
[Ben] Not sure as to why you needed to do this.
Seeing as the two clocks are asynchronous I needed to check that b would be low two ckB cycles after a rose on the ckA edge. Therefore, I needed to move the sampling of a in $rose(a) to a scheduling region after ‘Observed’, so that I could evaluate the change when it happens and not on the next ckA edge(possibly very slow relative to ckB). Failing to do this in some clever way, I merely moved the checking edge until after the change had resolved itself, while making sure that I also wanted to move the checking of the ckB events.
Thank you for your kind advice.
The property is used twice, as_ifFullNotEmpty and as_ifEmptyNotFull.
I have been feeling the lack of a proper way of reporting(my last project involved UVM), and I hadn’t thought to use only the reporting part of UVM. Does adding the whole UVM package, to an otherwise simple testbench, add any unwanted overhead? Is there a particular subset that one could import?
If you don’t mind, I’ll slip in another question: What are your thoughts on the necessity of the cover property statement. Questa seems to be able to count the number of activations of an assertion when this option(-assertion_debug?) is set, but this doesn’t seem as “loud” as a cover property. Right now I am doing it like this:
property pr_ifAnotBstable(a, b, ckA, ckB);
disable iff(arstWrite | arstRead)
@(posedge ckA) $rose(a) |->
@(posedge ckB) ##1 !b;
endproperty
as_ifEmptyNotFull: assert property
(pr_ifAnotBstable(fifoEmpty, fifoFull, ckReadDel, ckWriteDel))
else $error("Assertion failed");
cv_ifEmptyNotFull: cover property
(pr_ifAnotBstable(fifoEmpty, fifoFull, ckReadDel, ckWriteDel));
/Henrik