Hello,
I am trying to write an assertion using SVA for the following scenario:
When the signal called 'valid' goes HIGH, it results in another signal called 'alert' going HIGH 2 or more clock cycles later. The alert signal is eventually cleared by another part of the HW. For each rising edge of valid, I expect to see a rising edge for alert. The assertion I initially wrote was this:
property valid_alert_p(valid, alert);
@(posedge clk) valid |-> ##[2:$] $rose(alert);
endproperty
This works in most scenarios. However, when a situation arises where alert has not yet been cleared and I see two consecutive rising edges for valid, and then alert is eventually cleared, the very next rising edge on alert causes the assertions for both of those consecutive valid triggers to pass. What I instead want to see is a separate assertion for each pair of valid and alert. I have attached a waveform to demonstrate the problem:
Any help would be appreciated.
Thank you!