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

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. This is equivalent to adding the inferred condition in the iff clause of the clocking event.

For example,

always @(posedge clk) begin

if (rst) ...

else begin

...

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

c: cover property (a && b);

...

end

end

this is equivalent to writing

always @(posedge clk) begin

if (rst) ...

else begin

...

...

end

end

a: assert property (@(posedge clk iff $sampled(!rst)) a |-> b);

c: cover property (@(posedge clk iff $sampled(!rst)) a && b);