Using go-to v/s non-consecutive repetition within intersect operator

SystemVerilog
, , , ,
1

Hi Ben ,
I am trying a concurrent assertion for following requirement

Once A is de-asserted, B should toggle 5 times prior to A being re-asserted.
i.e between $fell(a) & $rose(a), b should have toggled 5 times.
The 1st toggle for ‘b’ could overlap with $fell(a)
The last i.e 5th toggle for ‘b’ could overlap with $rose(a)

Here is my attempt
The results can be summarized as ::

  1. On using go-to repetition as lhs of intersect i.e using +define+P2

  • Only if the 5th toggle for ‘b’ overlaps with $rose(a) the assertion passes (as observed in +define+ST2)

  • If the 5th toggle occurs before $rose(a) the assertion fails (as observed in +define+ST1)

    Hence using go-to repetition gives unexpected results for +define+ST1

  1. On using non-consecutive repetition as lhs of intersect i.e using +define+P3

  • Even if the 5th toggle for ‘b’ occurs before $rose(a) the assertion passes
    (as observed in +define+ST1).
    This resolves the limitation with go-to repetition i.e using +define+P2 +define+ST1

  • If the 5th toggle for b overlaps with $rose(a) the assertion passes (as observed in +define+ST2)

    Hence using non-consecutive repetition gives us the intended results

I have a question on observed results with $display as sequence_match_item using
non-consecutive repetition i.e with +define+P3 +define+ST1

( $changed(b)[=1] )[*1:$] is equivalent to
( $changed(b)[->1] )[*1:$] ##1 !$changed(b)[*0:$]

$changed(b)[->1] is equivalent to !$changed(b)[*0:$] ##1 $changed(b)

Hence ( $changed(b)[=1] )[*1:$] is equivalent to
( !$changed(b)[*0:$] ##1 $changed(b) )[*1:$] ##1 !$changed(b)[*0:$]

($changed(b)[=1])[*1:$] begins evaluation at overlapping edge (b/w @(posedge clk) in antecedent & @(clk) in consequent) at T:15

On 2 tools I observe “Cntr incremented to 1” twice due to match of sequences
sub_seq1 :: !$changed(b)[*2] ##1 $changed(b) at T:25 and
sub_seq2 :: !$changed(b)[*2] ##1 $changed(b) ##1 !$changed(b) at T:30

On same 2 tools I observe “Cntr incremented to 2” twice due to match of sequences
!$changed(b)[*2] ##1 $changed(b) ##1 !changed(b) ##1 $changed(b) at T:35 and
!$changed(b)[*2] ##1 $changed(b) ##1 !$changed(b) ##1 $changed(b) at T:35
Which is same as ::
sub_seq1 ##1 !changed(b) ##1 $changed(b) matching at T:35 and
sub_seq2 ##1 $changed(b) matching at T:35

For further re-use assume that
sub_seq11 is sub_seq1 ##1 !changed(b) ##1 $changed(b)
sub_seq22 is sub_seq2 ##1 $changed(b)

At T:35 both sub_seq11 and sub_seq22 match due to which “Cntr incremented to 2” is observed twice

However, these 2 tools give different results for “Cntr incremented to 3”

Tool1 shows it 10 times whereas Tool2 shows it 5 times !!

[Q1] What should be the ideal output ?

As per my understanding the following sequences would match
At T:40 :: sub_seq11 ##1 $changed(b) as well as sub_seq22 ##1 $changed(b) match
Hence I believe we should observe “Cntr incremented to 3” twice at T:40

At T:45 :: sub_seq11 ##1 $changed(b) ##1 !$changed(b) as well as
sub_seq22 ##1 $changed(b) ##1 !$changed(b) match
Hence I believe we should observe “Cntr incremented to 3” twice at T:45

At T:50 :: sub_seq11 ##1 $changed(b) ##1 !$changed(b)[*2] as well as
sub_seq22 ##1 $changed(b) ##1 !$changed(b)[*2] match
Hence I believe we should observe “Cntr incremented to 3” twice at T:50

At T:55 :: sub_seq11 ##1 $changed(b) ##1 !$changed(b)[*3] as well as
sub_seq22 ##1 $changed(b) ##1 !$changed(b)[*3] match
Hence I believe we should observe “Cntr incremented to 3” twice at T:55

At T:60 :: sub_seq11 ##1 $changed(b) ##1 !$changed(b)[*4] as well as
sub_seq22 ##1 $changed(b) ##1 !$changed(b)[*4] match
Hence I believe we should observe “Cntr incremented to 3” twice at T:60

2

The p3 solution works on my licensed tools.
(changed(b)[=1], cntr++ ) )[*1:]
causes multiple threads, each with a different repeat. e.g.,
($changed(b)[=1], cntr++ ) )[*1] or
($changed(b)[=1], cntr++ ) )[*2] or …
The thread with [*2] is equivalent to
($changed(b)[=1], cntr++ ) ##1 ($changed(b)[=1], cntr++ )
SInce the cntr variable is increment on one side of the intersect (which is a form of “and”), that varible flows out of the intersect sequence and is evaluated after ##0 ( cntr == 5).

// When b changes, cntr increments
the

  property p3;
    int unsigned cntr;        
    ($fell(a),cntr = 0) |->  @(clk)(  ( ( $changed(b)[=1], cntr++ , $display("T:%3t Cntr incremented to %0d",$time,cntr) )[*1:$] ) 
           intersect $rose(a)[->1] ) ##0 ( cntr == 5 );
//                                                   ==== 
  endproperty  
  
  ap3:assert property( @(posedge clk) p3 ) $display("T:%0t ap3 Pass",$time); else $display("T:%0t ap3 Fails",$time);    
``
1 Like
3

Hi Ben,
I added $display as sequence_match_item for debugging purposes
i.e when is seq_expr $changed(b)[=1] considered a match
Would like to hear your thoughts the no. of times one should observe ::
" Cntr incremented to 2" & Cntr incremented to 3