Hi,
it’s getting difficult for me to understand the always property in SVA. Please can you post few examples?
In reply to Rahul Patel:
These are mainly used for liveness and safety properties in formal verification. See https://www.win.tue.nl/~jschmalt/teaching/2IMF20/SvaFvTutorialHVC2013.pdf
In reply to dave_59:
There is an implicit always associated with concurrent assertions, thus allowing the assertion to be retested at each occurrence of its clocking event. For example:
initial
ap_resetf_hi_ater_hi: assert property(@ (posedge clk)
##20 |=> always reset_f==1'b1 );
Note that assertion ap_resetf_hi_ater_hi is attempted ONCE because of the initial.
However, after 20 cycles, reset_f must always stay in the high state.
You could write this as
initial begin
repeat(20) @(posedge clk);
forever
always @(posedge clk)
ap_reset_f_hi: assert property(reset_f==1'b1 );
end
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
Verification Horizons - March 2018 Issue | Verification Academy - SVA: Package for dynamic and range delays and repeats | Verification Academy
- SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
In reply to ben@SystemVerilog.us:
Hi Ben,
Thanks for the reply.
assert property ( always [4:5] a ##[1:4] b |=> c );
//Assertion isn't failing for this case. I don't understand why it isn't failing?
initial begin
a=0; b=0; c=0;
@(negedge clk); a = 0; b=0; c=0;
@(negedge clk); a = 1; b=0; c=0;
@(negedge clk); a = 1; b=0; c=0;
@(negedge clk); a = 0; b=0; c=0;
@(negedge clk); a = 0; b=1; c=0;
@(negedge clk); a = 0; b=0; c=0;
@(negedge clk); a = 0; b=0; c=0;
end
//Assertion is failing for this case where same sequence is happening but it is 1 clock delayed.
initial begin
a=0; b=0; c=0;
@(negedge clk); a = 0; b=0; c=0;
@(negedge clk); a = 0; b=0; c=0;
@(negedge clk); a = 1; b=0; c=0;
@(negedge clk); a = 1; b=0; c=0;
@(negedge clk); a = 0; b=0; c=0;
@(negedge clk); a = 0; b=1; c=0;
@(negedge clk); a = 0; b=0; c=0;
@(negedge clk); a = 0; b=0; c=0;
end
In reply to Rahul Patel:
From my SVA Handbook
always [3:4] a ##[1:4] b |-> c
* For every attempt, property must be true at 3rd and 4th cycle of that attempt
* Must be nonvacuously true at either 3rd or 4th cycle of that attempt
Now, with your example:
module m;
... variable declarations..
initial forever #10 clk=!clk;
assert property ( always [4:5] a ##[1:4] b |=> c );
In your testbench the antecedent is a no-match in cycles 4 and 5, thus the assertion is vacuously true.
On a separate note, I believe that you are misusing the "always"
// You are stating that at every clocking event (i.e., every 20ns) you have an attempt, and for that attempt, you want that in the 4th and 5th cycle thereafter the property is true.
Thus, at every attempt (every cycle) you have a new thread that behaves separately from the other threads.
Attempt 1 ^ . . . . P
Attempt 2 ^ . . . . P
Attempt 2 ^ . . . . . P
....
Attempt n ^ . . . . P
You can see the confusion!!! Actually, after the 4th cycle, you are checking the property at every cycle. If this is what you want, then write
assert property ( ##4 a ##[1:4] b |=> c );
Personally, if you must or want to use the always in an assertion, use it in an initial statement. Thus,
initial assert property ( always [4:5] a ##[1:4] b |=> c );
Thus, you want the property "a ##[1:4] b |=> c " to be true only in cycles 4 and 5.
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
Verification Horizons - March 2018 Issue | Verification Academy - SVA: Package for dynamic and range delays and repeats | Verification Academy
- SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
In reply to ben@SystemVerilog.us:
Thanks Ben for the very good explanation.