// 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,
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 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
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 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
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: