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