Unbounded delay range in Assertion Property

SystemVerilog
, ,
1

Hi,

If unbounded delay range is used in an assertion property, it will be checking till the end of simulation and it will not give a fail status at the end of test.
For example,
property p1;
@(posedge clk)
|-> ##[1:$] ;
endproperty

In the above example, if consequent doesn’t occur throughout the simulation, this assertion won’t give a FAIL.

Is there any way to get a fail status from this assertion before the simulation ends?
Note: Number of cycles the test runs may be varying.
Additional information: My TB has an ‘event’ that triggers just before some cycles the test ends.

I had a solution of asserting a flag at the start and deasserting after the consequent occurs; and at the ‘event’ checking for the flag through one more assertion, but this will increase the code as i have to write similar checks for all the flags in many assertions.

Regards,
Dilip

2

Qualify as strong sequences that have range delays or consecutive repetition operators (e.g., [*, [->, [= , and are consequents in an assertion. This is important when it is necessary to qualify an assertion as a failure if the consequent never terminates at the end of simulation. Example:


   ap_ab_recommend: assert property(@ (posedge clk)  a |-> strong([1:$] b)); // YES!!!
   ap_ab_weak:      assert property(@ (posedge clk)  a |-> ([1:$] b)); // !!!NO
   ap_abc_recommend: assert property(@ (posedge clk)  a |-> strong(b[*) ##1 c); // YES!!!
   ap_abc_weak:      assert property(@ (posedge clk)  a |-> (b[*) ##1 c); // !!!NO

In Questa, vsim has a switch named “-onfinish”. Specifying “-onfinish stop” on the vsim command line customizes the kernel shutdown behavior at the end of simulation when $finish() is exersized in the model (e.g., initial #4000 $finish();). Valid modes for " onfinish" include ask, stop, exit, final (Default: ask).

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
3

Hi Ben,

Is “strong” supported by all the tools? Is this recommended in LRM?

Regards,
Dilip

4

In reply to Dilip Bagadi:

I believe that it is supported, as the concept of “strong” was in the original 1800’2005.
I know that the major 3 vendors (Mentor, Cadence, Synopsys) do support it.
Ben

5

In reply to ben@SystemVerilog.us:

Thanks Ben!!!