Asynchronous reset assertion

SystemVerilog
, ,
1

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
2

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

  1. Verification Horizons - March 2018 Issue | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. 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
3

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?

4

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

5

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?

6

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

7

Another option


 always_comb if(!rst_n)
   assert(ptr==0);
Ben systemverilog.us
8

Thanks for the various suggestions. I get it now.

9

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

  1. https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. 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
10

In reply to ben@SystemVerilog.us:

Agreed about using deferred immediate assert here.