SVA and clock domain crossing

In reply to henrsol:

The property is used twice, as_ifFullNotEmpty and as_ifEmptyNotFull.

This is a personal preference, but inline assertions (instead of using properties with arguments) are easier to read, and review. That assertion is not that complex that it calls for using arguments, an opinion, of course.

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?

I am not a software developer, but UVM is just a set of libraries and routines. When the simulator includes it, I presume that it occupies memory. I just did a test of that model with and without UVM package, and I saw a difference of about 70 MB on my PC. The simulation slowdown would be when calling the routines. I don’t believe that `uvm_error is much work intensive than a $display; you most likely would not see it.

on the necessity of the cover property statement

The cover statement for properties is not needed since Questa gives you the same info anyway.
The results of coverage statement for a property contain:
 Number of times attempted
 Number of times succeeded
 Number of times succeeded because of vacuity

However, the cover sequence is useful to insure that you covered enough test sequences, for example
cv_full_and_push: cover sequence(@(posedge clk) first_match(fifo_full ##[1:$] push));
Results of coverage for a sequence include:
 Number of times attempted
 Number of times matched (each attempt can generate multiple matches). In addition, statement_or_null gets executed for every match. If there are multiple matches at the same time, the statement gets executed multiple times, one for each match.
Ben