my_prop1: assert property( a ##[2:] b |=> c ##[1:] d);
my_prop2: assert property( a ##[2:] b |=> c[*1:] ##1 d);
- 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
- 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).
- 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.
- 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
- 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
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue - SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
- 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