System verilog assertions- not htting criteria

Hi

How we can report an error if a particular assertion doesn’t hit even one time throughout simulation?

In reply to Naga:

Use the strong qualifier. At the end of the simulation you will see the report of the assertion failing. Thus:

 
ap_ab: assert properly(@(posedge clk) 
             a |-> strong( ##[1;$] b));

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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 978-1539769712
  • 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

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Thanks for your response Ben

If my left side one/antecedent itself doesn’t gets trigger then It won’t work right?

If ‘a’ is ‘0’ throughout simulation in your example, then I want to report with an error indicates Assertion has not triggered.

In reply to Naga:

Create in your TB an endofsim signal triggered a few cycles
before the $stop or $finish


bit endofsim;
bit a_occur;
always @(posedge clk)
 if(a) a_occur=1;
assert property(@ (posedge clk) 
     endofsim |-> strong(a_occur));


Ben systemverilog.us

In reply to ben@SystemVerilog.us:

I would create an additional assertion that says a must occur.

assert property(@(posedge clk) s_eventually a)
ap_ab: assert property(@(posedge clk) 
             a |-> strong( ##[1;$] b));

I’m assuming that these two properties could be combined into one, but I’m guessing this shows the requirements more clearly.

In reply to dave_59:

Thanks Dave, forgot about the s_eventually.
That is a better s/ cleaner olution.
Ben systemverilog.us

Can’t we use the followed operator instead of the overlapping operator ? #-#, #=#would fail if antecedent or precedent never fired in a run .

In reply to pkumar16:

Can’t we use the followed operator instead of the overlapping operator ? #-#, #=#would fail if antecedent or precedent never fired in a run .

The followed-by operator is a oroperty that contains a sequence followed by a property.
I don’t see how you would use this work here.

Dave_59 solution is the best using 2 assertions. There is nothing wrong in writing multiple small assertions; in fact, it is better to write multiple small assertions, with each one accomplishing a specific goal that trying to cram everything into one.

Engineers (me too) have this tendency of always searching for the “optimum” solution at all costs.
Let’s get practical!
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment