ap_check_encoder: assert property(
@(posedge byte_complete) disable iff (!stream_synchronised)
not(dec_error || $rose(dec_error)));
Now, the issue is that I spotted that this is only checked once upon the enabling of the assertion (i.e. when stream_synchronised == 1) and it then goes to a “finnished” state and never transitions to “inactive”. Is this because the signal never changes? Can I rely on this?
when the assertion (assert property or cover property or assume property) is enabled, at every clocking event (posedge byte_complete)) the assertion is tested. If the assertion lasts one cycle (like this one), then if can only succeed or fail for that attempt. At the next clocking event, the assertion is retested.
If the assertion is temporal (lasting over multiple cycles, e.g., a ##1 |-> c) then if it has an implication operator and the first element (the “a”) is false, then the resulting assertion for that individual attempt is vacuous. Else, a new thread is started for that attempt. EVERY attempt, and its resulting thread and computation is INDEPENDENT from previous or future attempts. Thus, I don’t understand your statement: never transitions to “inactive”.
property triggers_sent;
@(posedge CLK) (physics_event.triggered) |-> (send_trigger.triggered);
endproperty
cover property(triggers_sent);
Only gets triggered once and then disables itself (i.e. state goes to “off” rather than inactive) and does not count any of the other occurrences of the above sequence.
Same story here for the attempts. Since you’re using .triggered, physics_event and send_trigger are sequences defined in sequence declarations. Srini answered the cover issue.
Ben SystemVerilog.us