Problem in how to write an assertion for indefinite delay

SystemVerilog
, ,
1

Hi,
I am working with a task that requires defining an assertion that should flag an error if a signal does not changes value (in particular rise from 0 to 1) after a first signal has risen.
The problem is that this could happen anytime, i.e. no fix delay.
At first I thought to use this:


property p_4toggle_r(i,o);
    @(dtg) disable iff (rst_n === 1'b0)
      ($rose(i))  |=> strong(##[1:$] ($rose(o)));      
  endproperty

a_ctrl_delay_r: 
  assert    
    property(p_4toggle_r(i,o))
  else 
    `uvm_error($psprintf("%m"),"rising o did not come out")

But this seems not to work. Or better it does not flag the error when I force signal “o” not to change (I force to be always ‘0’)
I also tried “s_eventually” instead of “[1:$]”.

I know that this is a typical case of “vacuous pass” and I also used “cover”, but this not solve my problem (I want to flag an error) since it jsut gives me a message that the property pass (I would prefer to have the other way around).

I tried to find alternative ways to do this (like checking $rose(o) and using $past to check if it was triggered by a rise in ‘i’), but due to my lack of experience with SVA I failed. Either I do not have error, or I have to many (even when they should not be there).

A possible work around would be using an interval like [1:delay], where “delay” is a variable, but SVA does not allow it in a direct way.
Looking at an old answer in the forum to a similar problem I tried to create this property:


int dly1 = 200;  // just for test... to be changed to the value from an input port
property p_4toggle_r3(i,o); 
     int v;
    @(dtg) disable iff (rst_n === 1'b0)   
      ($rose(i), v=dly1+1'b1) |-> (v>0, v=v-1'b1)[*0:$] ##1 v==0 ##0 ($rose(o)); //          
  endproperty

But also this way does not work properly (again due the lack of experience in SVA)

Does anybody have any idea/suggestion/solution to this issue?

Thanks in advance
Federico

2

your original code should work

property p_4toggle_r(i,o);
    @(dtg) disable iff (rst_n === 1'b0)
      ($rose(i))  |=> strong(##[1:$] ($rose(o)));      
  endproperty
 
a_ctrl_delay_r: 
  assert    
    property(p_4toggle_r(i,o))
  else 
    `uvm_error($psprintf("%m"),"rising o did not come out")

In Questa, Vsim has a switch named “-onfinish” (please see below).
Specifying “-onfinish stop” on the vsim command line should get you the desired results.
-onfinish Customize the kernel shutdown behavior at the end of simulation
Valid modes - ask, stop, exit, final (Default: ask)

 
//You also need in your verification code something like 
  initial #4000 $finish();  // change that number to what you need
// the $finish is needed somewhere, used initial delay as an example

Ben Cohen http://www.systemverilog.us/

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books