Asynchronous Stable Signal SVA

SystemVerilog
, , , ,
1

I am attempting to write a SystemVerilog assertion to evaluate a circumstance where a given signal (sig) maintains static value any time the design is either in or out of asynchronous reset. Meaning that I would only like the value of sig to potentially change when the value for reset (rst) has asynchronously changed. Can this be done in a truly asynchronous manner?

I attempted to use $stable to accomplish this however it is still not capturing the desired functionality.

property prop_sig_stable(rst, sig);
    @(rst)
        $changed(rst) |-> $stable(sig);
endproperty : prop_sig_stable

Example Testbench:

module tb();

    logic rst;
    logic o_sig;

    initial begin
        rst = '1;
        #10;
        rst = '0;
        #20;
        rst = '1;
        #10;
        rst = '0;

    end

    dut u_dut(   
        .rst(rst),
        .o_sig(o_sig)
    );
    

endmodule : tb

Example DUT:

module dut(
    input   logic rst,
    output  logic o_sig
);

    logic int_sig = '0;

    always_ff @(rst) begin
        int_sig <= !int_sig;
    end

    assign o_sig = int_sig;

    property prop_sig_stable(rst, sig);
    @(rst)
        $changed(rst) |-> $stable(sig);
    endproperty : prop_sig_stable

    assert property (prop_sig_stable(rst, int_sig));


endmodule : dut

Failing at all rst transitions:

2

In reply to E_R_R:

I am not clear about your requirements:
@(rst)
$changed(rst) |-> $stable(sig);
would only like the value of sig to potentially change when the value for reset (rst) has asynchronously changed
Isn’t @(rst) a change in rst?
Do you mean that @(rst) then sometime later sig can change?
What length of time?
Can you write the behavior you are checking in a task?
Ben

3

In reply to ben@SystemVerilog.us:

Hello,

To clarify the change of sig would be caused only by the change in the rst signal. Thus, in a perfect world they would happen simultaneously. sig should only be able to change when rst does, but should be stable at all other times. It also important to note that it is not mandatory for sig to change when rst does. Only that if sig does change it must do so with rst.

4

In reply to E_R_R:
You could try something like the following:


/* The change of sig would be caused only by the change in the rst signal.
  Thus, in a perfect world they would happen simultaneously. 
  sig should only be able to change when rst does, but should be stable at all other times. */
// if(change in rst) then a change is sig is possible
// if(change in sig) && (no change in rst) then illegal

module m;
  bit sig, rst;
  bit sig_stretch, rst_stretch; // support

  always @(rst)  begin
    #1 rst_stretch =1;
    #1 rst_stretch =0; // need to tune this number. maybe #2 or #3
  end
  always @(sig)  begin
    #1 sig_stretch =1;
    #1 sig_stretch =0; 
  end
   
   am_sig: assert #0 (!(sig_stretch && !rst_stretch));  // no sig change when no rst
  
endmodule

Let me know if this is working for you or how you modified this.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

5

In reply to E_R_R:

Try:


// Code your testbench here
// or browse Examples
module tb();
 
    logic rst;
    logic o_sig;
 
    bit tmp_sig;
  
    initial begin
        rst = '1;
        #10;
        rst = '0;
      tmp_sig = 1;
        #20;
        rst = '1;
        #10;
        rst = '0;
      
      #100;
      tmp_sig = 0;
      #10;
 
      #100;
      $info ("Changing tmp_sig without RST");
      tmp_sig = 1;
      #10;
     #100;
      tmp_sig = 0;
      #10;

    end
 
    dut u_dut(   
        .rst(rst),
        .o_sig(o_sig)
    );
 
    a1 : assert property (
      @(tmp_sig) 1'b1 |-> $changed (rst));
 
 
endmodule : tb

It is not perfect - as the $changed(rst) is using tmp_sig as “clock” (to detect a change), so it sort of misses to flag the first change in tmp_sig without an accompanying change in rst, but guess you get the idea.

6

In reply to Srini @ CVCblr.com:
@(tmp_sig) 1’b1 |-> $changed (rst));
requires that when tmp_sig changes then $sampled(rst) is different than its previous sampled value when tem_sig occurred the last time.
There is no flexibility in the time zone when sig can change just after rst,
Good attempt Srini. Your and my solution need to be evaluated for requirements.
Ben

7

In reply to ben@SystemVerilog.us:

Hello,

Thank you for this insight. After testing in simulation, it appears to work as desired.

1021×174 8.92 KB

    initial begin
        sig = '0;
        rst = '1;
        #10;
        sig = '1;
        rst = '0;
        #20;
        sig = '0;
        #5;
        rst = '1;
        sig = '1;
        #10;
        rst = '0;

    end

    always @(rst)  begin
        #1 rst_stretch = 1;
        #1 rst_stretch = 0;
    end
    always @(sig)  begin
        #1 sig_stretch = 1;
        #1 sig_stretch = 0; 
    end
      
    am_sig: assert #0 (!(sig_stretch && !rst_stretch));

Are you aware of a way to get the same functionality to work in a formal application rather than in simulation? In the solution you shared it is still dependent on the timescale of the testbench.

8

In reply to E_R_R:

I doubt if popular FV tools would support asynchronous SVA such as these. However, this seems to be a RDC-related check (more or less a structural check) and there are special tools that may fit the bill here.

Regards
Srini

9

In reply to Srini @ CVCblr.com:

Ok, thank you. I will investigate RDC further and see what my options are.

10

In reply to Srini @ CVCblr.com:

I think I may have gotten close. I have come up with the property…

    property prop_sig_stable(rst, sig);
    @(sig)
        $changed(sig) |-> $changed(rst);
    endproperty : prop_sig_stable

this property appears to work in detecting the situation that I desire; however, it seems to flag the assertion on the edge of sig following the actual error.

1166×119 8.46 KB

11

In reply to ben@SystemVerilog.us:

    property prop_sig_stable(rst, sig);
@(sig)
$changed(sig) |-> $changed(rst);
endproperty : prop_sig_stable

1166×119 8.46 KB

I think that I may have gotten close with the solution above. However, it seems to flag the assertion on the edge of sig following the actual error. Are you aware of a way to insist that an error using the $changed operator will assess on edge of failure?

12

In reply to E_R_R:
With the following, I see from the waveforms that

  • at 10ns, with @(sig) clocking event, the sampled value of sig is 0.
    Also at 10ns the sampled value of rst is 1 sampled with @(sig).
    Since sig had a default value of 0, @(sig) $changed(sig) is 0.
    Thus, the property is vacuous at 10ns.
  • At 30ns, you have @(sig) and the sampled value of sig is 1, and
    the sampled value of rst is 0. Therefore,
    $changed(sig) at t30 is 1 (was 0 in the previous @(sig). Also,
    $changed(rst) at t30 is 1 (was 1 in the previous @(sig).
    The property is true at t30.
  • Using the same arguments above, you can see why the assertion fails at t35.

Just as a comments, it is a strange requirement for the following:
// if(change in rst) then a change is sig is possible
// if(change in sig) && (no change in rst) then illegal
How do you implement that in RTL? Show code.
Ben

13

In reply to ben@SystemVerilog.us:

Thank you for getting back to me about this. I appreciate your feedback. Unfortunately, I am unable to access the RTL code at this time. However, I am writing the sva properties to meet the requirements outlined in an IP document for a port.

Port signal specification:

signal should be treated as a STATIC input. If the value changes during operation, data corruption will occur.

It is also mentioned that signal is independent of the clocks and thus asynchronous.

From this specification I gathered that the signal is only able to legally change state on an edge of the system reset.

14

In reply to E_R_R:
I read the requirements differently. “signal should be treated as a STATIC input.” says that this is an input that is hardwired, possibly after the board is built with a jumper to provide options. If you want to include rst you can use the following code that can be used in formal:


/*  signal should be treated as a STATIC input. If the value changes during operation, data corruption will occur.
    It is also mentioned that signal is independent of the clocks and thus asynchronous.
    From this specification I gathered that the signal is only able to legally change state 
    on an edge of the system reset. */
bit sig_support; 
always_comb begin 
    if(rst) sig_support=sig; 
    am_sig: assert #0 (!rst && sig==sig_support || rst);
end

Ben

15

In reply to ben@SystemVerilog.us:

Thank you very much I think that is a good option. I appreciate all of your help on this!