[SVA] signal rises and stays stable check -> how to write an assertion?

In reply to rohithgm:
Oops! My mistake in the use of the always with a sequence Per 1800


property_expr ::= 
  ...
    sequence_expr #-# property_expr   // followed-by operator 
  | sequence_expr #=# property_expr
  ...
  | always property_expr
  | always [ cycle_delay_const_range_expression ] property_expr
  | s_always [ constant_range] property_expr
// Thus, one cannot do the following 
$rose(a)[->1] |-> ##3 always(b)); // because
// "##3" is a sequence that is followed by the "always(b)" property 
// If you want a sequence followed by a property, then you have to the followed-by operator 
  sequence_expr #-# property_expr // concatenation with zero cycle delay
  sequence_expr #=# property_expr // concatenation with one cycle delay

below is code that compiles OK 
module m; 
    bit clk, a, b; 
    initial 
    ap_a_init: assert property(@(posedge clk) $rose(a)[->1] |->
    ##3 1'b1 #-# always(b));

    initial // with the cycle_delay_const_range_expression
    ap_a_init1: assert property(@(posedge clk) $rose(a)[->1] |->
      always[3:$] (b));
    
    initial 
    ap_a_init2: assert property(@(posedge clk) $rose(a)[->1] |-> 
    strong (##3 !(b)[*0:$])) ;
    // Had an opened "("
endmodule
// EDA Playground simulator
https://www.edaplayground.com/x/xij
 

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


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy