Coverpoint for consecutive edge sequence

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.

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?

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] );

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?

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

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] ) 

]

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] )