Assertions Understanding

SystemVerilog
1

Hello All,

I have a query in assertion understanding. Generally we say that Signal “a” is asserted. What does that mean? Does it mean the rising edge of signal “a” or it’s just the true case of signal “a”?

2

In reply to janudeep3:

I have a query in assertion understanding. Generally we say that Signal “a” is asserted. What does that mean? Does it mean the rising edge of signal “a” or it’s just the true case of signal “a”?

Every language has its own lingo.
As you may know, in an concurrent assertion statement, all variables (or signals) are sampled in the Preponed region, just before the clocking event. SystemVerilog assertions have 4 layers of definition: Boolean, sequence, property, and directive (e.g., assertm cover, etc). Thus, when you have an assertion like:

ap_ab: assert property(@(posedge clk)  a |=> b==1'b0);

If “a” evaluates to 1, it is an accepted lingo to say " ‘a’ is asserted", or “‘a’ is active”.
Since “a” is considered an expression, if a==1, it is considered “true”.

The rising edge (e.g., $rose(a)) is exaplined in 1800.
$rose returns true when the sampled value of a Boolean signal argument transition is true at the current cycle (i.e., least significant bit of the expression==1’b1) and FALSE in the previous cycle (i.e., was 0, X, or Z), with respect to the clock of its context, otherwise it returns FALSE. From my book, “The $rose function is useful to ensure that a triggering condition is edge sensitive (i.e., a new positive edge) rather than level sensitive, as sampled with a clocking event. Not using the $rose function in antecedents is a very common mistake because of potential assertion errors caused by overlapping. Assertion overlapping was briefly discussed in Section 1.3.3. With an asserted property, the verification tool will attempt the evaluation of the assertion at every leading clocking event of the assertion. This can create overlapping assertions that are monitoring the same set of signals during the same bus cycles. For example, the thread started in attempt n is concurrent with the thread started in attempt n+1. While such overlapping is very powerful, these overlapping assertions can lead to unexpected assertion failures.”

Other things that may be confusing about assertions:

  1. The result of a property is true or false
  2. Vacuity on true/false of a property is a characterization of the strength (or significance) of that result
  3. The PASS action block can be enabled on passes (vacuous or on nonvacuous) , based on assertion controls (e.g., $assertpasson/$assertpassoff)
  4. Another level of granularity is added for the vacuous pass action block with the $assertnonvacuouson, $assertnonvacuousoff
  5. Currently, the FAIL action block can be enabled on failures (vacuous or on nonvacuous) based on assertion controls (e.g., $assertfailon, $assertfailoff)
    Ben Cohen
    http://www.systemverilog.us/ ben@systemverilog.us
  • SystemVerilog Assertions 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 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