To verify certain signals upon an async reset, which of these is deemed correct?
property async_rst_signal;
@(posedge clk) (!rst_n |-> (ptr==0 && cnt==0));
endproperty
OR
property async_rst_signal;
(!rst_n |-> (ptr==0 && cnt==0));
endproperty
In reply to kernalmode1:
// Handles case of rst_n going to zero
ap_async_rst: assert property(@(negedge rst_n) 1'b1 |=> @(posedge clk) ptr==0 && cnt==0);
// Handles case of powerup, when clk goes live
// changed the |-> to |=>
ap_sync_rst: assert property(@(posedge clk) !rst_n |=> ptr==0 && cnt==0);
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
- Verification Horizons - March 2018 Issue | Verification Academy
- http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
- “Using SVA for scoreboarding and TB designs”
http://systemverilog.us/papers/sva4scoreboarding.pdf - “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
October 2013 | Volume 9, Issue 3 | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
FREE BOOK: Component Design by Example
… A Step-by-Step Process Using VHDL with UART as Vehicle
http://systemverilog.us/cmpts_free.pdf
In reply to ben@SystemVerilog.us:
Ben,
With async resets, it is not tied to the clock in anyway. The signal can assert at any instant of a clock period. The registers are expected to go to their reset values instantly.
So, why tie them with posedge or negedge inside the property? Doesn’t it make the check for a synchronous reset instead?
In reply to kernalmode1:
In reply to ben@SystemVerilog.us:
Ben,
With async resets, it is not tied to the clock in anyway. The signal can assert at any instant of a clock period. The registers are expected to go to their reset values instantly.
So, why tie them with posedge or negedge inside the property? Doesn’t it make the check for a synchronous reset instead?
(@(negedge rst_n) 1’b1 |=> @(posedge clk) ptr==0 && cnt==0);
@(negedge rst_n) the values of ptr and cnt are those sampled taken just before @(negedge rst_n). If you want to check the values of those 2 signals after @(negedge rst_n) you need a delay. That delay can be the next clk edge. Another option is to create though an always block a #1 delay after the @(negedge rst_n) and use that signal.
BTW, if you use the clk edge, you’ll need the |=> instead of |-> to account for the case rst_n and the clk edge occur on the same cycle, otherwise you’ll get the sampled values of the 2 signals you are checking.
Ben systemverilog.us
In reply to ben@SystemVerilog.us:
Hi Ben,
Not to come off as argumentative, but why use a reference to clock within the assertion in the first place? This is for asynchronous reset isn’t it?
Can we get away with just the non-overlapping implication?
In reply to kernalmode1:
In reply to ben@SystemVerilog.us:
Hi Ben,
Not to come off as argumentative, but why use a reference to clock within the assertion in the first place? This is for asynchronous reset isn’t it?
Can we get away with just the non-overlapping implication?
SVA is based on sampling based on events.
(@(negedge rst_n) 1’b1 |-> ptr==0 );
Says that (@(negedge rst_n) the SAMPLED value of ptr==0.
The sampled value is just before the (negedge rst_n).
(@(negedge rst_n) 1’b1 |=> ptr==0 );
Says that (@(negedge rst_n), then at the next negedge of rst_n, the SAMPLED value of ptr==0.
The sampled value is just before that 2nd (negedge rst_n
You could writeb
always @(negedge rst_n)
#1 assert(ptr==0 );
Ben systemverilog.us
Another option
always_comb if(!rst_n)
assert(ptr==0);
Ben systemverilog.usThanks for the various suggestions. I get it now.
In reply to kernalmode1:
One more point on immediate assertions from my SVA book:
In addition, there are two categories of immediate assertions: simple immediate and deferred immediate (specified with #0 or final after the directive, such as assert #0, assert final).
- An assertion that depends only on variables that are updated in a nonblocking manner need not be deferred. This is because all the values are evaluated in the active region but updated in the NBA region.
- An assertion that depends on combinational logic or that uses external signals the use of a deferred assertion is preferable. Is the simulation supports assert final, then use that structure because the action block subroutine is called in the Postponed region.
Thus, you may want to consider:
always_comb if(!rst_n)
assert final(ptr==0);
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
- https://verificationacademy.com/news/verification-horizons-march-2018-issue
- http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
- “Using SVA for scoreboarding and TB designs”
http://systemverilog.us/papers/sva4scoreboarding.pdf - “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-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
FREE BOOK: Component Design by Example
… A Step-by-Step Process Using VHDL with UART as Vehicle
http://systemverilog.us/cmpts_free.pdf
In reply to ben@SystemVerilog.us:
Agreed about using deferred immediate assert here.
Do not you think the assertion for asynchronous behaviours is wrong here because what if reset persisted for more than 3 cycles and after 1sst cycle of clock in 2nd clock cyle signals got asserted though reset is asserted but since there is no negedge of reset assertion is not able to catch that .
So i am confused in that part only that how can we make concurrent assertion for reset such that it checks forever when the reset is deasserted it checks the signal values.
@Kshitij I believe you want to enhance the check to ensure that the signals remain at default value ( 0 ) throughout assertion of reset.
If yes, we could simply add a throughout operator in the consequent
ap_aync_rst: assert property( @(negedge rst_n) 1 |=> @(posedge clk) ( (ptr == 0) && (cnt==0) ) ##1 ( $stable( {ptr,cnt} ) throughout $rose(rst_n)[→1] ) );
just one question that @(negedge rst )1|=> so does it makes this to go after 1 cycle of negedge of rst ?
if yes than this would be wrong right?
The 1 after the @(negedge rst) |=> says that the edge is unconditional, not that it takes one cycle. You can read this as “the first posedge clk after the negedge rst”.
ya so can we say this is the proper assertion to check for the asynchronous reset?