In reply to E_R_R:
With the following, I see from the waveforms that
- at 10ns, with @(sig) clocking event, the sampled value of sig is 0.
Also at 10ns the sampled value of rst is 1 sampled with @(sig).
Since sig had a default value of 0, @(sig) $changed(sig) is 0.
Thus, the property is vacuous at 10ns. - At 30ns, you have @(sig) and the sampled value of sig is 1, and
the sampled value of rst is 0. Therefore,
$changed(sig) at t30 is 1 (was 0 in the previous @(sig). Also,
$changed(rst) at t30 is 1 (was 1 in the previous @(sig).
The property is true at t30. - Using the same arguments above, you can see why the assertion fails at t35.
Just as a comments, it is a strange requirement for the following:
// if(change in rst) then a change is sig is possible
// if(change in sig) && (no change in rst) then illegal
How do you implement that in RTL? Show code.
Ben