SVA - Ignoring glitches (some toggles) in the signal

SystemVerilog
,
1

Hello!
I was writing an assertion sequence for a signal checking its values over the period of lot of changes. Currently, I have the below code which just works fine for one case, but is not true always:


property check_s1;
@(posedge clk2)
$rose(cmd) |-> (sout == 0) ##[0:$](sout == 1) ##1 (sout == 0) ##[0:$] (sout == 1); // (sout == 1) ##1 (sout == 0) - I want to ignore this toggling, and just check for (sout == 0) ##[0:$]  (sout == 1)

It would be really helpful, if there is a way to do this! In this case, this is a digital signal.

But I have other signals which come from DAC and have more of these glitches. Help would be much appreciated.

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

3

In reply to ben@SystemVerilog.us:

Dear Ben

Thanks for the response and I did get the point. There are a few points which I didn’t follow:

  1. Is there any difference between [*0:] ##1 and ##[0:]

  2. Any glitches between the signal samples is ignored - What do you mean by this ?
    Say for ex: I have a [3:0] sout following the pattern 1,1,2,3,5,8 and each value stays true for 5 clock cycles. However, a value of 4 comes in between for just one clock cycle and this value of 4 need to be ignored by the SVA sequence. Here the main requirement of SVA is to check for the sequence 1-1-2-3-5-8 (Each number can appear after any number of clock cycles) and ignore if some intermediate value appeared. Would the below sequence work ?


property check_s1;
@(posedge clk2)
$rose(cmd) |-> (sout == 1) ##[0:$](sout == 1) ##[0:$] (sout == 2) ##[0:$] (sout == 3) ##[0:$](sout == 5) ##[0:$] (sout == 8);

Your help is much appreciated!

4

In reply to Bhaskar44:

In reply to ben@SystemVerilog.us:

  1. Is there any difference between [*0:] ##1 and ##[0:]

Question is really “any diff between a[*:] ##1 b" vs "a ##[0:] b”?

 
******  a[*0:$] ##1 b[/b] is same as 
 (b) or  //  (a[*0] ##1 b)  // null ##1 b IS SAME as "b" 
(a[*1] ##1 b) or // sequence OR operator 
(a[*2] ##1 b or //... and so ON 
   
****** a ##[0:$] b is same as 
(a ##0 b) or 
(a ##1 b) or //... and so ON 
(a ##n b)

****** goto [->n]
From my SVA Handbook 4th Edition
The goto repetition operator (Boolean[->n]) allows a Boolean expression (and not a sequence) to be repeated in either consecutive or non-consecutive cycles, but the Boolean expression must hold on the last cycle of the expression being repeated. The number of repetitions can be a fixed constant or a fixed range.

 
Note: b [->m] is equivalent to ( !b [*0:$] ##1 b)[*m]
b[->1] is equivalent to:
!b[*0:$] ##1 b
b[->2] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b
  1. Any glitches between the signal samples is ignored - What do you mean by this ?

Assume that I have a clock with a period of 10ns, and I sample the signals with @(posedge clk). Thus, if a==1 @t=100ns (the @(posedge clk) edge), a==0 @t=104ns, a=2 @t==107ns, and a=1 @t=109ns, the sampling at t=110ns is “1”. all values of a between clock edges are not considered nor evaluated. SVA samples signals at events.

Say for ex: I have a [3:0] sout following the pattern 1,1,2,3,5,8 and each value stays true for 5 clock cycles. However, a value of 4 comes in between for just one clock cycle and this value of 4 need to be ignored by the SVA sequence. Here the main requirement of SVA is to check for the sequence 1-1-2-3-5-8 (Each number can appear after any number of clock cycles) and ignore if some intermediate value appeared. Would the below sequence work ?


property check_s1;
@(posedge clk2)
$rose(cmd) |-> (sout == 1) ##[0:$](sout == 1) ##[0:$] (sout == 2) ##[0:$] (sout == 3) ##[0:$](sout == 5) ##[0:$] (sout == 8);

Not quite! what you have is **not correct
**


let a=sout; // your sequence becomes 
(a== 1) ##[0:$](a== 1) ##[0:$] (a== 2) ##[0:$] (a== 3) ##[0:$](a== 5) ##[0:$] (a== 8); 
That equation has a lot of non-sense terms with the ##0 
Above has the terms as one possibility: 
a==1 ##0 a==1 // same as a==1 in the same cycle, no repeat of 2 
a==1 ##0 a==2 // so you are asserting that a==1 and a==2 in the SAME CYCLE!!! 
a==1 ##0 a==3 // also a==0,2, and 3 in the same cycle!!  
That sequence can be satisfied with the sequence 
a==1 ##1a==2 ##1 a==3 ##1 a==5 ##1 a==8 // Not what you want.

I would use the goto operator 
//1,1,2,3,5,8
a==1[->2] ##1 a==3[->1] ##1 a==5[->1] ##1 a==8[->1]

I strongly recommend that you understand the meaning of the sequence operators.

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