Assertion on conditional statements

SystemVerilog
1

Hi,

I have clk, in, out signals. I have 2 conditions.
a) out is asserted immediately if in=1.
b) out is -de-asserted after n cycles if in=0;

I tried writing below code, but its not working as expected

`define TRUE 1'b1
     property abc;
      @(clk)
      if(in) `TRUE |-> out 
      else   `TRUE |=> ##[1:5] out; 
    endproperty

Please suggest me whether it is the write way to do it. If there is any better way please suggest

Thanks,
Anudeep

2

In reply to Anudeep J:
It is best to express this in two assertions instead of one.
In general, multiple smaller assertions are preferred as they are easier to write and understand. Thus, usin “a” instead of your “out”


// a) a is asserted immediately if in=1.
// b) a is -de-asserted after n cycles if in=0;
   let n=20;
   int m=20; 
   ap_aON: assert property(@ (posedge clk)  $rose(in) |-> a);  

   ap_aOFF_staticInfinite: assert property(@ (posedge clk) $fell(in) |=> !a[->1]);  // n== infinity 
   ap_aOFF_staticN: assert property(@ (posedge clk) $fell(in) |=> ##n !a); 
      
   import sva_delay_repeat_range_pkg::*; // see the link to the package below 
   // the import statement should be below the module declaration 
   ap_aOFF: assert property(@ (posedge clk) $fell(in) |=> q_dynamic_delay(m) ##0 !a);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

** 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) Amazon.com
  3. Papers:
3

In reply to Anudeep J:

Just a note about your use of the words asserted and de-asserted. This usually implies a change of state from false to true and then a change from true to false, which is why we use**$rose/$fell**.

What you wrote reads “every cycle that in is true out must be true at the same time, and every cycle that in is false, out must be true at lease once between two and six cycles afterwards”