In reply to verificator:
OOPS! We don’t discuss specific tools (delete the specific tool name and replace it with something like “a simulation tool”.
I modified your code a bit (put everything in one module, added some data and timing info)
assign q = cent; // line 27
always @(negedge rstn)
rst_val : assert final (q == 'h0) // line 56
** Error: 0 CNT reset value check failed in updncounter.rst_cnt q=xxxxxxxx
# Time: 0 ns Scope: updncounter.rst_cnt File: testbench.sv Line: 65
# 1 CNT reset value check passed in updncounter.rst_cnt q=00000000
# ** Error: 1 q reset value check failed in updncounter.rst_val q=xxxxxxxx
// So the q is not seen as updated in the assertion (though final).
// Am not sure why because the final is in the Postponed region ????
Consider Edit code - EDA Playground where I comment always @(negedge rstn)
Immediate assertions can be inside or outside procedural statements.
That fixes the problem
// always @(negedge rstn)
rst_val : assert final (q == 'h0)
$display("%t q reset value check passed in %m q=%b", $realtime, q);
else
$error("%t q reset value check failed in %m q=%b", $realtime, q);
// -----------------
rst_cnt : assert final (cnt == 'h0)
$display("%t CNT reset value check passed in %m q=%b", $realtime, cnt);
else
$error("%t CNT reset value check failed in %m q=%b", $realtime, cnt);
# ** Error: 0 q reset value check failed in updncounter.rst_val q=xxxxxxxx
# Time: 0 ns Scope: updncounter.rst_val File: testbench.sv Line: 60
# ** Error: 0 CNT reset value check failed in updncounter.rst_cnt q=xxxxxxxx
# Time: 0 ns Scope: updncounter.rst_cnt File: testbench.sv Line: 65
# 1 CNT reset value check passed in updncounter.rst_cnt q=00000000
# 1 q reset value check passed in updncounter.rst_val q=00000000
On non-overlapping implication |=> operator
upcnt : assert property (
disable iff (!rstn)
@(posedge clk)
(!ld && en && updn) // |-> q == $past(q) + 8'h1 // ERROR
|=> q == $past(q) + 8'h1);
If antecedent is true thenat the next cycle q should be equal to the previous value of q + 1’b1.
With the overlapping implication, you are saying:
If antecedent is true then in the SAME cycle q should be equal to the previous value of q + 1’b1. That is not what you want.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home
- 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