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

Does the LRM state any rules for deciding to terminate an assertion evaluation early, due to concluding that it's true, false, or vacuous?  At a quick glance, I didn't see such a rule.   If there are no explicit rules for early termination, your answer (c) would look right to me.

Is this something that should be prescribed by the language, or is it intentionally left up to EDA tool implementers to decide when to optimize in this area?


From: Ben Cohen [mailto:hdlcohen@gmail.com]
Sent: Tuesday, December 11, 2012 8:31 AM
To: sv-ac@eda-stds.org; Korchemny, Dmitry; Bresticker, Shalom; Seligman, Erik
Subject: [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.