Assertion to check for toggling of a bus based on another event

UVM
1

I am new to writing SVA and am trying to figure out the correct way to write an assertion for the below case.

I have two signals - one is a single bit signal (let’s say ‘bit A’) and the other is n-bit data-bus (let’s say ‘bit [7:0] B’)

Whenever ‘A’ toggles (going from 0->1 or 1->0), in the next 1 to 10 cycles, there must be a change in the value of signal B. So basically, everytime A changes it’s value, it is expected to see a change on the data-bus, B in the next 1-10 cycles.

2

In reply to tpan:

The recommended way to implement SV concurrent assertions is


In your case A has been checked for the prc-condition.
The implication operator would be the non-overlapping implication operator.
In your condition you are using the concatenation [1:10].

3

In reply to tpan:

I would just use $stable to detect the change. My untested code
assert property(@(posedge clk) disable iff(reset)
!$stable(A) → ##[1:10] !stable(B));

4

In reply to sanjeevs:

In latest SV LRM we have $changed and is more intuitive to use in this case:

 

  a_change_chk : assert property( // Assuming def clk, rst

    $changed(A) |-> ##[1:10] $changed(B));

You need to think about multiple changes in A within 10 clocks and other corner cases.

Srini

5

In reply to Srini @ CVCblr.com:

Thanks Srini. I did not know about $changed. It helped me in solving this case.

Thanks all for your suggestions.