in the following code:
property req_ack;
@(posedge clk) disable iff(!en)
$rose(req) |=> ack;
endproperty
assert property(req_ack);
if en goes high after $rose(req) but before ack, will (should) the assertion be activated ?
@(posedge clk) disable iff(!en)
$rose(req) |=> ack;
if en goes high after $rose(req) but before ack, will (should) the assertion be activated ?
When en==0, the assertion is cancelled, and any new attempt (at every leading cloking event, the posedge clk) is rejected. Thus, if en goes high after $rose(req) but before ack, the previous $rose(req) is not considered, as that previous attempt was never activated. Haever, when en==1’b1, all future attempts are considered and the assertion will be evaluated.
Ben Cohen http://www.systemverilog.us/
- SystemVerilog Assertions Handbook, 3rd Edition, 2013
- A Pragmatic Approach to VMM Adoption
- Using PSL/SUGAR … 2nd Edition
- Real Chip Design and Verification
- Cmpt Design by Example
- VHDL books