My Take on SVA Usage with UVM

For verifying complex temporal behavior, SystemVerilog assertions (SVAs) are unmatched. They provide a powerful way to specify signal relationships over time and to validate that these requirements hold. One limitation of SVAs is that they can only be used in static constructs (module, interface or checker). Since modern verification is class based, this leads to segregation between the assertions and the testbench. There have been many papers written about how to bring these two parts of the verification environment closer together, particularly when using UVM.


This is a companion discussion topic for the original entry at https://verificationgentleman.netlify.app/2015/09/06/my-take-on-sva-usage-with-uvm.html

Can you please give sample test example to work with?
it will be a great help.

You can download the code here: http://sourceforge.net/p/verificationgentlemanblog/code/ci/default/tree/sva_usage_in_uvm/

Hi, While using virtual interface get inside test to use $assertoff - questa runs into following error
runtime “Illegal virtual interface dereference”

As mentioned in the post, this doesn’t generally work, hence the need to put more effort into disabling the assertion.

Yeah, If I call assertoff from top module of tb , it’s working fine. Thanks

Apologies for the necro posting, but I’ve bumped recently into this article while I was searching how to mix information captured through a transaction (say some packet has been observed on an interface) and passing it on as a precondition for an assertion.

Say you have are monitoring a USB packet and when you receive two consecutive ones you want to check if after a given amount of clocks a signal is asserted.

In the example here you use the is_pipelined signal from the agent as a configuration.

How would you go about using transactions as preconditions for assertions?

The is_pipelined configuration field in the example is something more “static”. In your case, you want to use the fact that you got a USB packet as a trigger for the assertion. You probably want to pulse a signal whenever you’d like to trigger your check and use that in the assertion. You could probably implement the “got two USB packets” part in the class based TB and then just drive a saw_two_usb_packets signal high for one cycle. The you can use it in SVA: assert property (saw_two_usb_packets |-> ....