I have written following assertion:
assert property(@(posedge ClkRs_ix.clk)
disable iff (ClkRs_ix.reset) $stable(Signal_ia)[*20] |->
(Signal_oq==Signal_ia));
I wanted to express that 20 clock cycles for which the input signal is stable, at the 21st cycle the output has to have the same value as input.
This one works, but only if I assure no changes in the state of Signal_ia during the reset. If I assert reset, change the state of Signal_ia, then release the reset, this condition always fails. This usually happens when I start the simulation with Signal_ia = 'X' and during reset it becomes '0'.
Is there any way how to write this better? Resp. is there a way how to ignore first event after reset, as it might be tripping due to conditions happening at reset? If I understood well, iff assures, that this assertion is ignored during reset. Effects I'm trying to describe have some latency, ideally I would need to ignore this condition not only in reset, but as well 20 cycles following the deassertion of the reset state.
thanks .d.
The first thing to note is that the disable iff (rst) clause is asynchronous. Thus, it does not obey the regular assertion sampling rules.
From the LRM:
The expression of the disable iff is called the disable condition. The disable iff clause allows preemptive resets to be specified. For an evaluation of the property_spec, there is an evaluation of the underlying property_expr. If the disable condition is true at anytime between the start of the attempt in the Observed region, inclusive, and the end of the evaluation attempt, inclusive, then the overall evaluation of the property results in disabled. A property has disabled evaluation if it was preempted due to a disable iff condition. The values of variables used in the disable condition are those in the current simulation cycle, i.e., not sampled.
In your case, for every cycle prior to the reset, a new thread for your assertion is spawned. Once, the reset comes along, all these instances are disabled and their property evaluation suspended. Any new evaluations will only be started once the reset is de-asserted. Thus, I can't see how this can be the cause of your issue.
However, I can suggest two possible problems that may be causing your problem: 1. At the beginning of your sim Signal_ia is 'X. After 20 cycles if the reset hasn't been asserted, the antecedent sequence $stable(Signal_ia) will evaluate to true and the assertion will immediate move to evaluating the consequent sequence Signal_oq==Signal_ia (in the same cycle since non-overlapping implication was used). If both these signals are 'X, 1'X == 1'X evaluates to 1'X, thus the assertion will fail. 2. You mentioned that you want to have the check occur on the 21st cycle. However, this assertion will actually check on the 20th cycle. If there are 20 flops, the output will still be 'X at this point, even if the input has been 0 for 20 cycles.
I suspect option 1. is more likely since 2. would've probably been obvious.
To address both of these, I would recommend that you alter the assertion to trigger on a change of the input to address this.
CHECK_OUTPUT: assert property(@(posedge ClkRs_ix.clk)
disable iff (ClkRs_ix.reset) $changed(Signal_ia) |=>
$stable(Signal_ia)[*20] ##0 (Signal_oq==Signal_ia));
As pointed out you can also selectively enable the assertion. $asserton and $assetkill (assertoff) can help you do that:
$asserton[(levels[, list])] is equivalent to $assertcontrol(3, 15, 7, levels [,list]) — $assertoff[(levels[, list])] is equivalent to $assertcontrol(4, 15, 7, levels [,list]) — $assertkill[(levels[, list])] is equivalent to $assertcontrol(5, 15, 7, levels [,list])
assertkill will kill any threads that are already running (as opposed to asseroff, which will only prevent future threads). It sounds to me that you would be after assertkill. You can then re-enable your assertion through asserton.
As pointed out, in a formal scenario, naturally this would need to be achieved through a control signal in the assertion and an FSM to generate it.