In reply to Dhaval_Pandya:Requirements:
- If signal A goes low, signal B should go LOW after the COUNT variable.
- If after signal A goes low, it goes HIGH during the COUNT then the assertion should be disabled.
I would use the sync_reject_on property operator; see below for more info. Thus,
ap_ab: assert property(@ (posedge clk) $fell(a) |->
sync_reject_on($rose(a)) dynamic_delay(delay) ##0 $fell(b) );
Your assertion becomes vacuous when during the count a==1 because the antecedent is false.
(
(!A && count==0), count=count-1)[*1:$]
// Your assertion
@(posedge clk) ($fell(A), count=X) ##1 ((!A && count==0), count=count-1)[*1:$] |-> $fell(B);
From my SVA book: 3.10.9 accept_on, reject_on, sync_accept_on, reject_onsync_reject_on
This family of property operators provide an abort of the property being evaluated when the abort condition is true anytime during the evaluation of the property, and with an exit of vacuously true (for the accepts) or false (for the rejects) as the result of the property expression. This family of operators is not like the disable iff, which cannot be nested and asynchronously cancels the evaluation of the assertion with no contribution to the statistics. The accept_on/reject_on family of operators just terminates the property as an accept (true vacuously, with no contribution to the pass statistics) or reject (false, with contributions to the failed statistics). The abort operators can be nested (i.e., a lower property embedded into a higher level property can be aborted), and multiple aborts can exist in one property definition, whereas the disable iff must be at the top level of the assertion. If the abort condition is false, then the property expression continues to be evaluated until completion (i.e., to its end point, it is not aborted). These properties have the following forms:
accept_on ( expression_or_dist ) property_expr
reject_on ( expression_or_dist ) property_expr
sync_accept_on ( expression_or_dist ) property_expr
sync_reject_on ( expression_or_dist ) property_expr
