SVA to check whether a signal is stable between 2 events

SystemVerilog
, , , , ,
1

I want to check whether a signal name xyz is stable between the fall of signal ‘reset’ and the rise of signal ‘enable’.
I have tried something like this

property stable_check(xyz); 
  @(posedge clk) disable iff (enable)
   $stable(xyz) within ($fell(ares) ##[1,*] $rose(enable)) ;
endproperty

Please let me know whether this is correct or not.
If not let me know the correct answer.

2

In reply to nsiddams:
xyz is stable between the fall of signal ‘reset’ and the rise of signal ‘enable’.


// from fall of reset, XYZ is stable continuously  until and with rose of enable
property stable_check(xyz);
   @(posedge clk) // NO on "disable iff (enable):
   $fell(reset) |-> $stable(xyz) s_until_with $rose(enable);
endproperty



// from fall of reset, XYZ is stable at any time  until, but not 
// necessarily with rose of enable
property stable_check(xyz);
   @(posedge clk) // NO on "disable iff (enable):
   $fell(reset) |-> $stable(xyz) within $rose(enable)[->1];
endproperty

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
http://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
3

In reply to nsiddams:

I want to check whether a signal name xyz is stable between the fall of signal ‘reset’ and the rise of signal ‘enable’.
I have tried something like this
property stable_check(xyz);
@(posedge clk) disable iff (enable)
$stable(xyz) within ($fell(ares) ##[1,*] $rose(enable)) ;
endproperty
Please let me know whether this is correct or not.
If not let me know the correct answer.

can you explain this line $stable(xyz) within ($fell(ares) ##[1,*] $rose(enable)); what mean * ?

4

In reply to pavan_krishna:

I updated code above to
$fell(reset) |-> $stable(xyz) within $rose(enable)[->1];

Syntax error in your code.
You meant:

$stable(xyz) within (fell(ares) ##[1:] $rose(enable))
Xyz is stable anytime within the fell of ares and rose of enable.

5

In reply to ben@SystemVerilog.us:
Ben, the code you have give:
$fell(reset) |-> $stable(xyz) within $rose(enable)[->1];
It is not working, I can see the waveform of the signal xyz changing, but the assertion is not catching it. Is there anyother way?

6

In reply to nsiddams:

Please try making a small testbench that tests your property in the failing case. It makes it much easier for people to understand your problem.

7

In reply to dave_59:
Edit code - EDA Playground code
EPWave Waveform Viewer wave
Works for me

module top;
  bit clk , a , b , c , d, start, stable;
  int pass, fail; 
  always #5 clk = !clk;
  // $fell(reset) |-> $stable(xyz) within $rose(enable)[->1];

  function automatic void f1(); start =1; endfunction 
  function automatic void f2(); stable =1; endfunction 

  property abc; 
    @(posedge clk)  ($rose(a), f1())  |-> ($stable(b), f2()) within $rose(c)[->1];
  endproperty

  assert property( abc )  begin  pass=pass+1; $display("T:%0t Pass",$time);  end
           else begin fail=fail+1; $display("T:%0t Fails",$time);  end

 initial
           begin
            $dumpfile("dump.vcd"); $dumpvars;
            @(posedge clk); a <=1; b <= !b;
            repeat(2) @(posedge clk) b <= !b;
             repeat(3) @(posedge clk); 
            c <=1; 
            repeat(3) @(posedge clk); 
             #20; $finish();
           end 
endmodule
start at t15, 
b is unstable at t15, 25, 35
b is stable at t45
c[->1' occurs at t65
Thus, b is stable within rose(a) and 1st occurrence of c

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

8

you can use sequence and property constructs to create assertions. To check whether a signal is stable between two events, you can define a sequence that captures the behavior you want and then create a property that checks for the stability. Here’s an example:

// Define a sequence to capture the events
sequence stable_sequence(logic signal, bit value);
  @(posedge signal) $rose(value);
  ##1;
  @(posedge signal) $fell(value);
endsequence

// Define a property to check for stability
property stable_property(logic signal, bit value);
  @(posedge signal) disable iff (!value)
    stable_sequence(signal, value);
endproperty

// Use the property in an assertion
assert property (stable_property(my_signal, 1))
  else $fatal("Signal is not stable between events");