Coverpoint for consecutive edge sequence

Coverage
, ,
1

I would like to write a coverpoint to capture a sequence of edge events: two toggles of A followed by two toggles of B. There is no predictability in terms of when the second A comes wrt to first A. Similarly, there is no predictability on the two B’s. They can also each stay high for any number of cycles.

1261×115 2.75 KB

I’m thinking to write something like:

cover property (@(posedge clk) !B ##1 $rose(A) ##[1:$] $rose(A) |-> !A ##1 $rose(B) ##[1:$] $rose(B));

But it looks like this won’t work since it does not guarantee that B stays low throughout the first two $rose of A and similarly, A stays low during the two $rose of B. How can I enforce this?

2

In reply to atashinchi:

Didn’t test but how about

cover property (@(posedge clk) $rose(a) ##0 !b throughout a[->2] |=> !a throughout b[->2] );
3

In reply to dave_59:

In reply to atashinchi:
Didn’t test but how about

cover property (@(posedge clk) $rose(a) ##0 !b throughout a[->2] |=> !a throughout b[->2] );

Hi Dave,

Thank you. I tested this as an assertion and I think for the most part it did the trick. I fixed a minor syntax issue:

cover property (@(posedge clk) $rose(a) ##0 (!b throughout a[->2]) |=> !a throughout b[->2] )

However, I think

[->2]

will include the cases where A is high for two consecutive clocks followed by B high for two consecutive clocks. Is there any way to ensure that both A and B each have two $rose?

4

In reply to atashinchi:

a[->2]

is the same as

(!a[*0:$] ##1 a) [*2]

is the same as

!a[*0:$] ##1 a ##1 !a[*0:$] ##1 a
5

In reply to dave_59:

Hi Dave,

Isnt it a[->1], you are already checking $rose(A) in the antecedent? In the waveform there is two highs of A not 3.


cover property (@(posedge clk) $rose(a) ##0 (!b throughout a[->1) |=> !a throughout b[->2] )

]

6

In reply to rag123:

Based on the pic I think it should be ::


cover property (@(posedge clk) ( $rose(a) && !b ) ##1  (  !b  throughout  (  $rose( a )[ ->1 ] ##1 $fell( a ) [ ->1 ]  )  ) |->  !a throughout $rose(b)[->2] )

Another way could be ( May Need some modifications )


cover property (@(posedge clk) (!b throughout ( $rose(a)[->2] ##1 $fell(a)[->1] ) |->  !a throughout $rose(b)[->2] )