This proposal corrects an incomplete fix for item 1381 regarding when an evaluation attempt takes place under inferred enabling condition from an always block.

P1800-2008-draft1, 17.13.5, p. 289 (IEEE Std 1800™-2005)

Replace

Another inference made from the context is the enabling condition for a property. Such derivation takes place when a property is placed in an if..else block or a case block. The enabling condition assumed from the context is used as the antecedent of the property. A concurrent assertion embedded in procedural code specifies that a new evaluation attempt of the underlying property_spec begins at every occurrence of the inferred clocking event.

With

Another inference made from the context is the enabling condition for a property. Such derivation takes place when a property is placed in an if..else block or a case block. A concurrent assertion embedded in procedural code in an if...else block or a case block specifies that a new evaluation attempt of the underlying property_spec begins at every occurrence of the (inferred) clocking event provided that the condition leading to the location of the assertion in the block is true. If the condition is false then no evaluation attempt is started.

For example,

always @(posedge clk) begin

if (rst) ...

else begin

...

aa: assert property (a |-> b);

cc: cover property (a && b);

...

end

end

If the sampled value of rst is false at a given tick of the inferred clocking event posedge clk then the evaluation attempts of the assert property statement aa and the cover property statement cc are not started at that clock tick.