How does the following two properties differ? or are they both same?
Ex1:
a ##1 b ##1 c;
Ex2:
a ##1 b |=> c;
How does the following two properties differ? or are they both same?
Ex1:
a ##1 b ##1 c;
Ex2:
a ##1 b |=> c;
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.
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
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 ?
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.
// ...
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr