Question on consecutive repetition operator for SVA properties/assertions

puranik.sunil · July 7, 2016, 2:00pm

Hi,
I have a question on SVA repetition operator as follows :

Considering following assertion


a1: assert property (@(posedge clk) a[+] |-> p); //same as  assert property (@(posedge clk) a[*1:$] |-> p)


This means a[*1] or a[*2] ..or  a[*n] |-> p. So  my understanding is that it will start multiple parallel threads of evaluation. Assuming n= 5 (simulation run for 5 clocks), does this mean at clk1, simulator starts 5 threads (a[*1] or a[*2].. or a[*5]); at clk2, it will start 4 parallel threads (a[*1] or a[*2].. or a[*4]), at clk2, it will start 3 parallel threads etc. So if n is large,  will it  load the simulator and  will the simulation speed  be slow? 
If there is a series aaa at beginning of some attempt, then p should hold in all three clocks. So this assertion would be equivalent to 
a2: assert property (@(posedge clk) a |-> p); In that case, will a2 execute faster than a1?
 Let me know if this understanding is  correct. 

2. What would a1: assert property (@(posedge clk) a[+]) would mean? Considering logic mentioned above, will this be same as assert property (@(posedge clk)a)? In that case, would the latter statement execute much faster?

It would be great help if someone can explain above questions
rgs,
-sunil

user49 · July 7, 2016, 5:47pm

See embedded comments

I have a question on SVA repetition operator as follows :

Considering following assertion

a1: assert property (@(posedge clk) a[+] |-> p); //same as  assert property (@(posedge clk) a[*1:$] |-> p)

This means a[*1] or a[*2] …or a[*n] |-> p. So my understanding is that it will start multiple parallel threads of evaluation.

[Ben]

YES to a[*1] or a[*2] …or a[*n] |-> p
In addition, for EACH attempt, for the assertion to succeed (or for the property to be true) each of those threads must be tested, and each of them must succeed vacuously or nonvacuously. For a nonvacuous success, at least one thread must be nonvacuous. If any of those threads fails, then the assertion for that attempt fails.
Yes, for EACH ATTEMPT multiple threads will be started.
The concept of Assertion states (includig attempts and outcomes is very very important. For your conveniece, I uploaded 3 pages from my SVA Handbook 4th Edition, 2016 ISBN 978-1518681448 in the link below
http://systemverilog.us/attempt.pdf
For emphasis on attempt, I am reiteratig the following from my book:
“Attempted: When the assertion is attempted at its leading clocking event, it is considered as a start event, represented as a blue square. In essence, an attempt is the start of an evaluation of an assertion (see 2.3.1 for more information on attempts). Assertion statements are started (attempted) at every leading clocking event, unless they are disabled or if they are turned off. If the attempt succeeds, one or more threads for that successful attempt are started, and those threads are independent from previous or future attempts. If the attempt fails, that assertion for that attempt is either vacuous if the property has an implication operator, or it fails if there is no implication in the property.”

Assuming n= 5 (simulation run for 5 clocks), does this mean at clk1, simulator starts 5 threads (a[*1] or a[*2]… or a[*5]); at clk2, it will start 4 parallel threads (a[*1] or a[*2]… or a[*4]), at clk2, it will start 3 parallel threads etc. So if n is large, will it load the simulator and will the simulation speed be slow?

**NO. What it means, as explained in above about “attempt” is that at clk1 simulator starts 5 threads (a[*1] or a[*2]… or a[*5]); [b]at clk2, it will start 5 new parallel threads (a[*1] or a[2]… or a[5]), at clk2, it will start 5 new parallel threads etc. EACH of those threads are independent of other previously started threads caused by previous successful attempts Again, for each attempt, all 5 threads must not fail, but can be vacuous. Thus if you have 4 vacuous passes and 1 nonvacuous pass, the assertion succeeds nonvacuously. Any attempt where a==0 is optimized by the simulator as vacuous because if a[*1]==0, then obviously, a[*2] would also be ==0.

If there is a series aaa at beginning of some attempt, then p should hold in all three clocks. So this assertion would be equivalent to
a2: assert property (@(posedge clk) a |-> p); In that case, will a2 execute faster than a1?


ap3: assert property (@(posedge clk) a[*1:3] |-> p);// IS DIFFERENT than 
ap1: assert property (@(posedge clk) a |-> p);

For a[*1:3] |-> p, for the property to be true, all threads for each attempt must be tested, and none of the threads can fail, as explained above.
NOTE: In this case, with first_match and optimization


ap3fm: assert property(first_match(a[*1:3]) |-> p);  
ap3fm_equivalent: assert property(a |-> p); // if a[*1]==0, then obviously, a[*2]==2 too!
// and no other match can occur
// If for each attempt, first "a" is ==1, then first_match(a[*1:3]) == that first "a"
// However, in the following case, the first_match has more significance
ap3ab: assert property(a[*1:3] ##1 b |-> p);  
ap3abfm: assert property(first_match(a[*1:3] ##1 b) |-> p);

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

SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
// For 10% discount, use code 45KJT5GN @ https://www.createspace.com/5810350
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

puranik.sunil · July 8, 2016, 2:30am

Hi Ben,
thanks a lot for detailed reply. Referring to the discussion above on series “aaa” my question was that if there assertion,

a1: assert property (@(posedge clk) a[*1:$] |-> p)

then for example, for input pattern aa in first two clocks, p has to be true in both the clocks for assertion to be true, for pattern aaa, p has to be true in all three clocks, for pattern aaaa, p has to be true in all 4 clocks… etc. Same holds for all n till end of simulation. so does it mean

a1: assert property (@(posedge clk) a[*1:$] |-> p)

is same as

a1: assert property (@(posedge clk) a |-> p)

In the discussion above,

ap3ab: assert property(a[*1:3] ##1 b |-> p);  
ap3abfm: assert property(first_match(a[*1:3] ##1 b) |-> p);

both these assertions are not same due to first_match. For ap3ab to succeed, all the threads in attempt need to succeed while in ap3abfm, one you get one match, assertion succeeds and others threads need not succeed. Is that correct?

Also if the assertion a1 is in initial block, it will start only one attempt at first clock. Is this understanding correct?

rgs,
-sunil

user49 · July 8, 2016, 3:26am

In reply to puranik.sunil@tcs.com:

Referring to the discussion above on series “aaa” my question was that if there assertion,

a1: assert property (@(posedge clk) a[*1:$] |-> p)

then for example, for input pattern aa (meaning a==1 ##1 a==1in first two clocks, p has to be true in both the clocks for assertion to be true, for pattern aaa, p has to be true in all three clocks, for pattern aaaa, p has to be true in all 4 clocks… etc. Same holds for all n till end of simulation.

[Ben] That part is correct. However, for a pattern like


attempt     m   n   k   t   y 
cycle       1   2   3   4   5 
a==         1   1   1   0   X  .  ..
p==         1   1   1   X   X    
assertion
4 attempt m S   A   A   P      // result for attempt m, thread 4 @ cycle 4 is vacuous true 
// Thus, since for cycle 1, 2, 3 a==1 and p==1 and all possible threads of the antecedent were exercised with no failure, the assertion is a pass.  NOTE: vacuous true is success. 
However, since you have at least one nonvacuous  true of the property, the property is a 
nonvacuous true and the assertion is a pass.  Once you have a zero in "a" like aaa!a  all other threads after that !a are vacuous passes. Notation
S== started 
A == active 
P == PASS
F == FAIL 
V == vacuous 
--------------------------------------------
CONSIDER THIS case
attempt     m   n   k   t   y 
cycle       1   2   3   4   5 
a==         1   1   1   0   X  .  ..
p==         1   1   0   X   X    
assertion
4 attempt m S   A   F   -      // result for attempt m, thread 3 @ cycle 3 is FAIL

so does it mean

a1: assert property (@(posedge clk) a[*1:$] |-> p)

is same as

a1: assert property (@(posedge clk) a |-> p)

NO. CONSIDER THIS case


attempt     m   n   k   t   y 
cycle       1   2   3   4   5 
a==         1   1   1   0   X  .  ..
p==         1   1   0   X   X    
assertion a[*1:$] |-> p)
4 attempt m S   A   F   -      // result for attempt m thread 3 @ cycle 3 is FAIL
--
assertion a |-> p
4 attempt m P  -------------
4 attempt n -  P ------------      
4 attempt k ---------F -------
4 attempt t ------------V      // vacuous true, vacuous result 
 // Remember that ALL threads of antecedent must be tested.  Simulator may optimize; e.g., for a[*1:$], any occurrence of a==0 means that all other occurrences are false.

In the discussion above,

ap3ab: assert property(a[*1:3] ##1 b |-> p);  
ap3abfm: assert property(first_match(a[*1:3] ##1 b) |-> p);

both these assertions are not same due to first_match. For ap3ab to succeed, all the threads in attempt need to succeed (vacuously or nonvacuouslys) while in ap3abfm, one you get one match, assertion succeeds and others threads need not succeed. Is that correct?

[Ben] correct, except that it is more correct to say that all other threads are not tested.

Also if the assertion a1 is in initial block, it will start only one attempt at first clock. Is this understanding correct?

[Ben] Correct.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
// For 10% discount, use code 45KJT5GN @ https://www.createspace.com/5810350
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

puranik.sunil · July 8, 2016, 6:23am

Hi Ben,

I am not clear about the following table you have given. According to the table, result for attempt m @ cycle 3 is a fail for assertion a[*1:] |-> p) and the result for assertion a |-> p for attempt k at cycle 3 is also a fail. For assertion a |-> p, attempt t @cycle 4 is vacuous pass but for assertion (a[*1:] |-> p) @cycle 4, for all threads of attempts m, n, k, t, a[*1:$] is not true so it should also be a vacuous pass. So that would mean both the assertions are equivalent. For case II @cylce 4 you have shown V, vacuous pass but for case I @cycle 4, you have just shown - as result. What does that mean? Can you please elaborate why result is not V for case I @cycle 4 and why Case I and Case II are not equivalent.

rgs,
-sunil


case I
attempt     m   n   k   t   y 
cycle       1   2   3   4   5 
a==         1   1   1   0   X  .  ..
p==         1   1   0   X   X    
assertion a[*1:$] |-> p)
4 attempt m S   A   F   -      // result for attempt m thread 3 @ cycle 3 is FAIL
--
Case II
assertion a |-> p
4 attempt m P  -------------
4 attempt n -  P ------------      
4 attempt k ---------F -------
4 attempt t ------------V      // vacuous true, vacuous result 
 // Remember that ALL threads of antecedent must be tested.  Simulator may optimize; e.g., for a[*1:$], any occurrence of a==0 means that all other occurrences are false.

user49 · July 8, 2016, 7:04am

In reply to puranik.sunil@tcs.com:

Hi Ben,
I am not clear about the following table you have given. According to the table, result for attempt m @ cycle 3 is a fail for assertion a[*1:] |-> p) and the result for assertion a |-> p for attempt k at cycle 3 is also a fail. For assertion a |-> p, attempt t @cycle 4 is vacuous pass but for assertion (a[*1:] |-> p) @cycle 4, for all threads of attempts m, n, k, t, a[*1:$] is not true so it should also be a vacuous pass. So that would mean both the assertions are equivalent. For case II @cylce 4 you have shown V, vacuous pass but for case I @cycle 4, you have just shown - as result. What does that mean? Can you please elaborate why result is not V for case I @cycle 4 and why Case I and Case II are not equivalent.
rgs,
-sunil


case I
attempt     m   n   k   t   y 
cycle       1   2   3   4   5 
a==         1   1   1   0   X  .  ..
p==         1   1   0   X   X    
assertion a[*1:$] |-> p)
4 attempt m S   A   F   -      // result for attempt m thread 3 @ cycle 3 is FAIL
--
Case II
assertion a |-> p
4 attempt m P  -------------
4 attempt n -  P ------------      
4 attempt k ---------F -------
4 attempt t ------------V      // vacuous true, vacuous result 
// Remember that ALL threads of antecedent must be tested.  Simulator may optimize; e.g., for a[*1:$], any occurrence of a==0 means that all other occurrences are false.