SVA - Ignoring glitches (some toggles) in the signal

SystemVerilog
,
2

In reply to Bhaskar44:
Sorry, but your requirements are not clear.
In your assertion the signals are sampled wth @(posedge clk2). Why are you considering those as “glitches”? If you want just check for (sout == 0) ##[0:$] (sout == 1) you can do one of the followings:


ap_cmd2sout1: assert property(@(posedge clk2)$rose(cmd) |-> sout[->1] );  // use of the goto 
// which is same as 
ap_cmd2sout1b: assert property(@(posedge clk2)$rose(cmd) |-> !sout[*0:$] ##1 sout);  

// What you described with 
$rose(cmd) |-> (sout == 0) ##[0:$](sout == 1) ##1 
               (sout == 0) ##[0:$](sout == 1);  
// Is 2 toggles of sout, starting at the next cyle after cmd. 
 That can also be done with the goto as shown below (starting from same cycle as cmd)
ap_cmd2sout1_2times: assert property(@(posedge clk2)$rose(cmd) |-> sout[->2] ); 
// which is same as 
ap_cmd2sout1b: assert property(@(posedge clk2)$rose(cmd) |-> 
              !sout[*0:$] ##1 sout ##1 !sout[*0:$] ##1 sout);  
------------------------
A COMMENT: 
a==0 ##[0:$] a==1 is same as 
a==0 ##0 a==1 || // This is always false, "a" cannot be 0 and 1 in the same cycle. 
// this is confusing and unnecessary 
a==0 ##1 a==1 || .. 
a==0 ##n a==1

Any glitches between the signal samples is ignored.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr