Understading assertions

SystemVerilog
,
1

How does the following two properties differ? or are they both same?

Ex1:
a ##1 b ##1 c;

Ex2:
a ##1 b |=> c;

2

First assertion becomes active everytime when ‘a’ becomes true (a == 1). Once the assertion is active (say at time t) then it checks for b==1 (at time t+1) and then c==1 (at time t+2) in the consecutive cycles.

Where as the second assertion becomes active only when a ##1 b is true i.e, if a==1 at time t and b==1 at time t+1 then assertion gets activated at t+1. Then it checks for c==1 in the next cycle (t+2).

i.e, for a scenario a=1 at t, b=0 at t+1 first assertion fails where as the second assertion wouldn’t even get activated and so a vacuous pass would be seen.

3

Ex1:
a ##1 b ##1 c;
Ex2:
a ##1 b |=> c;

Every assertion is attempted at every clocking event and a new thread is initiated until that assertion either succeeds (true or vacuous success), fails, or is cancelled.
In ex1, the assertion basically requires that at all cycles “a”, “b”, and “c” must be true. There is no vacuous success here because the property is a sequence.

In ex2, the sequence (a ##1 b) is the antecedent, and it too is started at every clocking event. However, if the antecedent fails, the assertion is considered vacuous (or true vacuously), meaning it is not an important case.

Assertions are never written as in ex1. For case 2, if the antecedent has multiple threads, you’ll need to add the first_match operator. Thus,

ap1: assert property( @(posedge clk) first_match( a ##[1:2]b) |=> c); 
 ap2: assert property( @(posedge clk) first_match(a ##1 b[*1:2]) |=> c;

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
4

In reply to S.P.Rajkumar.V:

Thanks Rajkumar

5

In reply to ben@SystemVerilog.us:

Hi Ben,

I need clarification from the below statement :
Every assertion is attempted at every clocking event and a new thread is initiated

Does this mean that at every clock event , a thread is created checking the assertion . If it succeeds/fails only then it starts a new thread from the start correct ?

6

In reply to diptishe:

In reply to ben@SystemVerilog.us:
Hi Ben,
I need clarification from the below statement :
Every assertion is attempted at every clocking event and a new thread is initiated
Does this mean that at every clock event , a thread is created checking the assertion . If it succeeds/fails only then it starts a new thread from the start correct ?

Deninetly see my paper: Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2

To answer your question,
Every assertion is attempted at every clocking event and a new thread is initiated
Yes, this is exactly what it means. At every clock event, a thread is created for that attempt to check the assertion. That first thread is the attempt. WIthin that 1st attempted thread, there could be other threads but they are all related to that attempted thread. That thread is totally independent from other attempted threads, and has no effect on future threads from other attempts. Its success or failure has notheing to do with other attempts.


initial forever #5 clk=!clk;  // new edge every 10ns 
ap_1: assert property(@(posedge clk) 
   a |=> ##[1:3] b); 
// Below is for explanation only, tools handle the assertions differently and that is proprietary 
// In my reference paper, I have a model for assertions that works and it explains the concepts of threads, 
// and the independence of each started (or attempted) assertions from other attempts. 
//
// @10ns "a" is attempted, and that is the 1st starting thread, called the attempt.
// If(a) then 3 new secondary threads are started
//  one for ##1 b, one for ##2 b, and one for ##3 b. 
// If the antecedent is a no match (sequence a==0), the result for that attempt is vacuity  
// 
// At 20ns #a is attempted, and that is the 1st starting thread, called the attempt.
// ...
// At 30ns #a is attempted, and that is the 1st starting thread, called the attempt.
// ...

Bottom line, every attempted thread has a life of its own. Its attempt is its birth, it lives as long as it can until it succeeds or dies (fail). It knows nothing about its past siblings (previous attempts) and has no effect on future siblings (future births).
It is not like a human family.
:)

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
    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
  4. Understanding the SVA Engine,
    https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
  5. https://verificationacademy.com/forums/announcements/free-book-component-design-example-…-step-step-process-using-vhdl-uart-vehicle