Within ' disable iff ( ! reset ) , is the reset synchronous OR asynchronous?

SystemVerilog
, ,
1

Typically we can disable a property expression via :: ’ disable iff ’


 property  ab ;
  @( posedge clk ) disable iff ( ! reset )  $rose( a ) |=> b ;  
 endproperty

Variables ’ a ’ N ’ b ’ are Sampled ( in preponed region ) and the expression is evaluated ( in Observed region ) ONLY during posedge of clk .

**Is the active low variable ’ reset ’ evaluated ONLY during posedge of clk ( i.e evaluated synchronously ) OR

if the reset were to go low during negedge of clk ( i.e when the property isn’t evaluated ) the assertion would still be disabled / discarded ?**

2

In reply to hisingh:
The disable iff ( ! reset ) is asynchronous.
From my SVA book:
To provide a synchronous abort, three not identical options with specific implications can be used: 1) With the sync_accept_on (see 3.9.14); for example:


ap_sync: assert property(@ (posedge clk)
   sync_accept_on (!rst_n) // If rst_n==0 then assertion is vacuously true
     a |-> ##3 b);
  1. With a sampled valued function (see 4.2.1.2); for example :

ap_dis_sync: assert property(@ (posedge clk) // If synchronous fell(rst_n)
   disable iff ($fell(!rst_n, @(posedge clk))) // then assertion is cancelled
     a |-> ##3 b);
/* Note that this approach is not always ideal, particularly for designs where the reset signal is active low and is generated from a power supply circuit and is maintained in the zero state until the supply voltage is stable (e.g., at 5V). In this case, there is no $fell(!rst_n); $rose(!rst_n) would work, but any future resets would be problematic since they would not emulate RTL logic.*/
  1. With the triggered of a sequence; for example:

sequence qSoftReset2; @ (posedge clk) $rose(soft_hardware_reset_command) ##1 ack;
endsequence : qSoftReset2
apTest: assert property (
    @ (posedge clk) disable iff (qSoftReset2.triggered)
     a |=> b);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to ben@SystemVerilog.us:

Ben is there a way to check the aysnchronous part via reports ( $display() ) .

For example ::


 //  Within  procedural  blocks

   always @( negedge rst_n  ,  posedge clk ) 
    begin
 
       if ( ! rst_n )  begin
   
        $display($time,,,"...") ; //  Can  report  N  check  that  reset  was  asynchronous 
         
         //  Drive  initial  values  to  signals
       end
      else
        begin
          //  Non - Reset Logic  here
          .............................
        end
    end

Similarly can we have a report specifically when the reset is asserted in the concurrent assertion ?

4

In reply to hisingh:

Instead of the $display, use the immediate cover with an action block.

5

In reply to ben@SystemVerilog.us:

Ben I am not sure if I get your comment .

Do you mean this way ::


always @( negedge rst_n  ,  posedge clk ) 
    begin
 
       if ( ! rst_n )  begin
 
        assert ( ! rsn ) $display($time,,,"...") ;  //  Immediate  assertion . 
 
         //  Drive  initial  values  to  signals
       end
      else
        begin
          //  Non - Reset Logic  here
          .............................
        end
    end

I was looking for a way in concurrent assertion written outside procedural block. Like in the example at the top .

6

In reply to hisingh:


always @( negedge rst_n  ,  posedge clk ) 
    begin 
       if ( ! rst_n )  begin 
        c_reset: cover(1) $display($time,,,"...") ;  //  Immediate  assertion . 
        // Since you know that rst_n==0, you can use "1" 
        // but cover or assert of rst_n is OK too
          //  Drive  initial  values  to  signals
       end
      else
        begin
          //  Non - Reset Logic  here
          .............................
        end
    end
   // concurrent assertion statement; it needs a clocking event  
   cp: cover property(@(negedge rst_n) 1); //  negedge rst_n occurred

Ben

7

In reply to ben@SystemVerilog.us:

What seems to work for me as well is this:


ap_dis_sync: assert property(@(posedge clk) 
   disable iff ($sampled(rsti_i)) // sample `rst_i` at the beginning of the simulation tick

@Ben: Do you see anything wrong with that?

8

In reply to No:

That’s OK too.
I used that form before.