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 verification statement. Such derivation takes place when a verification statement is placed in an if..else block or a case block. The enabling condition assumed from the context is used to modify the property_expr of the verification statement as follows:

- If the verification statement is assume property or assert property then the enabling condition is used as the antecedent of an overlapping implication of which the consequent is the property_expr stated in the verification statement.

- If the verification statement is cover property then the enabling condition is used as the antecedent of a negated overlapping implication of which the consequent is the negated property_expr stated in the verification statement. The double negation used in the property expression represents the dual property to the overlapping implication and it is often called "followed by".

The resulting new property_expr then replaces the original property_expr in the verification statement. 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.

For example,

always @(posedge clk) begin

if (rst) ...

else begin

...

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

cc: cover property (a && b);

...

end

end

The equivalent concurrent verification statements after clock and enabling condition inference are as follows:

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

cc: cover property (@(posedge clk) not (!rst |-> not (a && b));