The way how threading works in assertions

Hello,

Lets consider the following assertions:

my_prop1: assert property( a ##[2:] b |=> c ##[1:] d);
my_prop2: assert property( a ##[2:] b |=> c[*1:] ##1 d);

My questions are that:

  1. I know that infinite delay (##[2:]) will spawn infinite threads, likewise, will the infinite repetition (c[*1:]) spawn infinite threads too?
  2. If I modify my_prop1 to-- assert property( first_match(a ##[2:] b) |=> first_match(c ##[1:] d) );
    then can I get the assertion to complete/finish, ie, will it end up in a nonvacuos pass or fail?
  3. If I modify my_prop1 to – assert property( a ##2 b[->1] |=> c ##1 d[->1]);
    then my understanding is that the assertion can finish and be a pass/fail. Is this correct?
  4. If 3) is correct then, does that mean the goto repetition [->] doesnt spawn infinite threads?
    I read that goto repetition can expanded as, say if its b[->1] then this is equivalent to: !b[*0:] ##1 b. If this is correct then wont the [*0:] part in here spawn multiple threads. But I have seen that if I use goto instead of ##[1:$] will make the assertion complete and thereby it will either pass or fail.

Any clarifications for these questions are appreciated. Thanks

my_prop1: assert property( a ##[2:] b |=> c ##[1:] d);
my_prop2: assert property( a ##[2:] b |=> c[*1:] ##1 d);

  1. I know that infinite delay (##[2:]) will spawn infinite threads, likewise, will the infinite repetition (c[*1:]) spawn infinite threads too?[

YES. For example,

$rose(a) ##[1:5] b  // this sequence is equivalent to
  ($rose(a) ##[1] b) or ($rose(a) ##[2] b) or ...($rose(a) ##[5] b)  |->  ##3 c
// whether that sequence is in antecedent or consequent is irrelevant 

  1. If I modify my_prop1 to-- assert property( first_match(a ##[2:] b) |=> first_match(c ##[1:] d) );
    then can I get the assertion to complete/finish, ie, will it end up in a nonvacuos pass or fail?

SVA requires that each of the threads of that antecedent with a range or a repeat statement, must be tested with its appropriate consequent. Thus,

    $rose(a) ##[1:5] b |->  ##3 c;  // is equivalent to
  ($rose(a) ##[1] b) or ($rose(a) ##[2] b) or ...($rose(a) ##[5] b)  |->  ##3 c;
// This ORing in the antecedent creates multiple threads, something like: 
  ($rose(a) ##[1] b |->  ##3 c) and  // separate thread 
  ($rose(a) ##[2] b |->  ##3 c) and  // separate thread 
  ..
  ($rose(a) ##[5] b |->  ##3 c);     // last thread 
 

Conclusion: An assertion with an antecedent that has an infinite delay of the form (a ##[1:$} b |-> some_prperty;
can NEVERsucceed because for success (true or vacuous) ALL POSSIBLE HREADS MUST BE TESTED. It can however FAIL. A first_match(antecedent_sequence) in the antecedent constrains the antecedent to one antecedent that does not cause the property to be vacuous (assuming the consequent is a sequence).

  1. If I modify my_prop1 to – assert property( a ##2 b[->1] |=> c ##1 d[->1]);
    then my understanding is that the assertion can finish and be a pass/fail. Is this correct?

That is correct. Since, as you mentioned, b[->1] is equivalent to: !b[*0:$] ##1 b.

  1. If 3) is correct then, does that mean the goto repetition [->] doesn’t spawn infinite threads?
    I read that goto repetition can expanded as, say if its b[->1] then this is equivalent to: !b[*0:] ##1 b. If this is correct then wont the [*0:] part in here spawn multiple threads. But I have seen that if I use goto instead of ##[1:$] will make the assertion complete and thereby it will either pass or fail.

Consider

ap_rpt: assert property(@ (posedge clk) 
   $rose(a) ##1 !b[*0:$] ##1 b|=> c);  
//Assume that after the $rose(a),   
//  at ##1 b==0, (!b[*0] ##1 b) is a NO match, expected the sequence (b) 
//  at ##2 b==0, (!b[*1] ##1 b) is a NO match, expected the sequence (!b ##1 b)  
//  at ##3 b==1, (!b[*2] ##1 b) IS match, got the sequence (!b ##1 !b ##1 b)  
//  at ##4 b==1, (!b[*3] ##1 b) is a NO match, expected the sequence (!b ##1 !b ##1 !b ##1b)   
// !b[*3] is a no match because the b sequence was "0011, on the 3rd cycle for the b test 
//  "b" was 1. for (!b[*3] ##1 b to match, we need b sequence to be "0001" 
// From there on, no future sequences qill match because "b" was a '1' in a past sequence.
// THUS, ALL future sequences for the (!b[*0:$] ##1 b) can be ignored, 

and that is why the goto works

my_prop2: assert property( a ##[2:] b |=> ##[1:]c ##1 d);

If the consequent has an infinite range (delay or repeat), you DO NEED A GOTO OR First_match(). This is because in the consequent you also have that ORing, which means any thread is a match thread, any failed matched thread in the consequent is ignored, and the tool will look for other threads. A failure if ALL threads fail, and that will never occur because of the ##[1:$].

my_prop2: assert property( a ##[2:] b |=> c[*1:] ##1 d);

That thread CAN fail (e.g., if the c sequence is 111110XXXX

Note that


$rose(a) ##[1:$]b |=> c);  // DO NOT WRITE THIS 
$rose(a) ##1 b[->1] |=> c);  // WRITE THIS (best practice)
first_match($rose(a) ##[1:$]b) |=> c); // ONE other option,  
$rose(a) |=>  ##[1:5] c); // NO first_match() or goto needed, 
//                           CAN succeed or fail 
$rose(a) |=>  ##[1:5] c ##1 d); // MAY need a first_match() or goto needed,
$rose(a) |=>  first_match(##[1:5] c) ##1 d);  // better, depending on requirements
$rose(a) |=>  ##[1:$] c); // NO NEED a first_match() or goto needed, if c==1, it wil pass
$rose(a) |=>  ##[1:$] c ##1 d); //need a first_match() or goto needed,
$rose(a) |=>  first_match(##[1:$] c) ##1 d);
antecedent1 |-> antecedent2 ||-> consequent  // BAD STYLE, use a single antecedent 
// BTW, antecedent2 ||-> consequent is a property 

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

In reply to ben@SystemVerilog.us:

$rose(a) ##[1:5] b |-> ##3 c;

waveform

@ben, is this how the waveform looks like for this multi threaded assertion ?

In reply to yourcheers:

Not sure What you mean by a waveform looking like.
An assertion specifies cases when the property is true. For
$rose(a) ##[1:5] b |-> ##3 c; // cases for true property are
a b x x c. // $rose(a) ##[1] b |-> ##3
a x b x x c // $rose(a) ##[2] b |-> ##3
a x x b x x c // $rose(a) ##[3] b |-> ##3
a x x x b x x c // $rose(a) ##4] b |-> ##3
a x x x x b x x c // $rose(a) ##[5] b |-> ##3

@ben thanks for the response, apart from the above 5 cases, are there any other cases where this property is true?

Does that mean, from the below code property p0 is same as having 5 different independent properties p1,p2,p3,p4,p5.

property p0;
  $rose(a) ##[1:5] b |-> ##3 c;
endproperty


property p1;
  $rose(a) ##[1] b |-> ##3 c;
endproperty

property p2;
  $rose(a) ##[2] b |-> ##3 c;
endproperty

property p3;
  $rose(a) ##[3] b |-> ##3 c;
endproperty

property p4;
  $rose(a) ##[4] b |-> ##3 c;
endproperty

property p5;
  $rose(a) ##[5] b |-> ##3 c;
endproperty

I am just confused from the explanation below where there is an “and” between the properties, I was thinking it as a property “and” operator between various threads. “($rose(a) ##[1] b |-> ##3 c)” and “($rose(a) ##[2] b |-> ##3 c)”

SVA requires that each of the threads of that antecedent with a range or a repeat statement, must be tested with its appropriate consequent. Thus,
$rose(a) ##[1:5] b |-> ##3 c; // is equivalent to
($rose(a) ##[1] b) or ($rose(a) ##[2] b) or …($rose(a) ##[5] b) |-> ##3 c;
// This ORing in the antecedent creates multiple threads, something like:
($rose(a) ##[1] b |-> ##3 c) and // separate thread
($rose(a) ##[2] b |-> ##3 c) and // separate thread

($rose(a) ##[5] b |-> ##3 c); // last thread

In reply to yourcheers:
Does that mean, from the below code property p0 is same as having 5 different independent properties p1,p2,p3,p4,p5.
NO. However, it means the property ORing of all these properties.


$rose(a) ##[1:5] b |-> ##3 c; // is equivalent to
// Using your properties above
ap_1to5: assert property(@(posedge clk) p0 AND p1 AND p2 AND p3 AND p5); 
// In one property, it really means 
($rose(a) ##1 b) OR 
($rose(a) ##2 b) OR  
($rose(a) ##3 b) OR  
($rose(a) ##4 b) OR  
($rose(a) ##5 b)  |-> ##3 c; 

I stringly encourage you to read my paper
Understanding the SVA Engine,
https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
That paper will clarify many of your misunderstandings with assertions and properties.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: * Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
  1. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

In reply to ben@SystemVerilog.us:

Corrected in above the equivalent assertion to


ap_1to5: assert property(@(posedge clk) p0 AND p1 AND p2 AND p3 AND p5); 

One or more of those properties can be vacuously true, but for nonvacuous assertion success, no property can fail and at least one property must be nonvacously true.
Ben

Hi Ben, a quick follow up. In the accepted solution, you mentioned
"
Quote:
my_prop2: assert property( a ##[2:] b |=> ##[1:]c ##1 d);

If the consequent has an infinite range (delay or repeat), you DO NEED A GOTO OR First_match() . This is because in the consequent you also have that ORing, which means any thread is a match thread, any failed matched thread in the consequent is ignored, and the tool will look for other threads. A failure if ALL threads fail, and that will never occur because of the ##[1:]. Quote: my_prop2: assert property( a ##[2:] b |=> c[*1:$] ##1 d);

That thread CAN fail (e.g., if the c sequence is 111110XXXX
"
On that front can I say the following (Please note: I slightly modified the antecedent):

my_prop2: assert property( a ##2 b |=> ##[1:$]c ##1 d);

This property can Pass but never Fail

my_prop2: assert property( a ##2 b |=> c[*1:$] ##1 d);

This property can Fail but never Pass

Also you mentioned this rule of thumb when the ##[1:$] delay is on the antecedent
“SVA requires that each of the threads of that antecedent with a range or a repeat statement, must be tested with its appropriate consequent” → And for the assertion to pass nonvacously should all these antecedent threads pass or if just any 1 thread passes can we say the assertion to be a nonvacous pass

Similarly is there any rule of thumb (and also the condition for it to be a nonvacous pass) if the ##[1:$]delay is on the consequent, like this:

property p3;
  $rose(a) |=> b ##[1:$] c;
endproperty

Thanks in advance

In reply to curious_learner:
Please read my paper

In that paper I wrote:
Variation with a range in the consequent
Consider a variation to the previous model
**$rose(a) ##2 b |-> ##[1:3]c ##1 d;
**
This property uses the same antecedent as the previous assertion. However, in the consequent instead of (a ##3 c ##1 d) we have a range in the c, specifically (##[1:3] c ##1 d). The ##[1:3]c ##1 d is equivalent to ( (##1 c ##1 d) or (##2 c ##1 d) or (##3 c ##1 d) ), and that sequence (with the sequence ORing) represents three separate threads launched when the antecedent succeeds. For the assertion to succeed, the antecedent must match and any thread in the consequent must match. For an assertion failure, all three threads of the consequent must fail.

[Ben] From straight Boolean logic, expr1 OR expr2 means the property is true if either expression is true.
ALso, a sequence used as a property is either nonvacuously true or is false.
Vacuity is in a property where the antecedent is a non-match.
in your example rose(a) |=> b ##[1:] c;
the consequent is a property specified as a sequence. From 1800, there are several constructs that are identified as a “property”", and a sequence is one of them.

Read my paper!
Ben