[sv-ac] assertion of vacuous_prop_at_t0 or nonvacuous_prop_at_t5 // what results??

Consider the example below that breaks down to:
  ap_or: assert property(a |=> (0 |-> 1)  or (##5 1) ); // assume a==1 at
cycle t
What results should a simulator provide, per LRM?
a) true vacuously, and quit evaluating at cycle t+1?
b) true nonvacuously, and quit evaluating at cycle t+1?  *// Definitely not
becuase of LRM 16.14.8h*
c) Since at cycle t+1 the evaluation is vacuous and there could be a
nonvacuous evaluation in the other term of the or operator,
   then the simulator should evaluate the other term in search of a
potential nonvacuous result.

The LRM is ambiguous on this point. If a tool yield answer
 "a", would that be acceptable?
"b" would be an error,
"c" might be better.

We need to clarify (another mantis) what result should be expected.

16.12.3 Disjunction property
A property is a disjunction if it has the following form:
*property_expr or property_expr*
The property evaluates to true if, and only if, at least one of
property_expr1 and property_expr2 evaluates to true.

16.14.8 Nonvacuous evaluations
e) An evaluation attempt of a property of the form *property_expr1 or
property_expr2
*is nonvacuous
if, and only if, either the underlying evaluation attempt of property_expr1
is nonvacuous or the
underlying evaluation attempt of property_expr2 is nonvacuous.

h) An evaluation attempt of a property of the form sequence_expression |=>
property_expr is
nonvacuous if, and only if, there is a successful match of the antecedent
sequence_expression and
the evaluation attempt of property_expr that starts at the clock event
following the end point of the
match is nonvacuous.

module test_or;
bit clk, a=1'b0, b, c;
initial forever #10 clk=!clk;
 default clocking cb_ck1 @ (posedge(clk));  endclocking
property p_vac;
0 |-> 1;
 endproperty

property p_t_at5;
##5 1'b1;
 endproperty
ap_or: assert property(a |=> p_vac or p_t_at5);
cp_or: cover property(p_vac or p_t_at5);

initial begin
repeat(2) @ (posedge clk);
a <= 1'b1;
 @ (posedge clk) a <= 1'b0;
end
endmodule

Ben Cohen

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.