SV. Assertion for this scenario

SystemVerilog
1

I have two signals X and Y.
X is a 10 bit signal
How to write an assertion to check X changes (toggles) atleast once before every positive edge of Y. There is no requirement on how many cycles before positive edge of Y , X should toggle.

I was thinking of a forward looking assertion of this type

  property toggle_check;
    @(posedge clk) disable iff (0)
    $changed(x) [*1:$] ##1 $rose(y);
  endproperty : toggle_check

However if this gets satisfied once and then post that we never have a toggle of X before $rose(y) then i think the assertion wont catch it. Am I right ?

Any better way/suggestions on how to write this assertion ?

Thanks in advance

2

Use always_ff to set a tag when X changes value.
Reset the tag when rose of Y.

$rose(Y) |-> tag
3

Got it

The reseting of tag will happen in NBA
tag <= 0

but the assertion will use the preponed value of tag (which would be !=0)

4

Req: X changes (toggles) atleast once before every positive edge of Y
$rose(Y) |-> tag
Y, tag values are the sampled values at the Preponed region.
// support logic
@(posedge clk) if($rose(Y)) tag <=0;
tag is 0 in NBA

What issues do you see?
Need to think about how to handle tag when rose of Y and change of X occur in the same cycle.
Do that in the support logic.

5

I dont see any issues. I just mentioned the rationale behind why your mentioned solution works.
Thanks