[sv-ac] Request Tuesday meeting: ref: mantis 4037, false vacuity and simulation

Ed,
Can we schedule a meeting for Tuesday?
Ref; http://www.eda-stds.org/svdb/view.php?id=4037
Define false vacuity and contributions to pass/fail counters in simulation
Dmitry,
I am bringing this up because the LRM is ambiguous as to how a vacuous
property that is false should simulate and report the "failure";
specifically should a vacuous property that is false behave as a vacuous
property and not contribute to the fail stattistics. A vacuous property
that is false occurs in a negated property that is vacuous, or a in
property with a reject_on(expr) when expr is true.

Note that if a vacuous false property is considered as nonvacuous false by
reporting it as an error, then that gives the way to convert a
a vacuously true property to nonvacuous true property : Simply do a
(not(not(vac_true))).

In the model show below, what should the result of simulation be? Should I
see the pass/fail counters incremented?
I am in favor of considering a property that is vacuous regardless of the
reason as vacuous and should not contribute to the statistics counters for
assertions or coverage.
Thanks,
Ben
module test_vacuity;
    bit clk, a, b, c, rst=0;
    initial forever #10 clk=!clk;
    default clocking cb_clk @ (posedge clk);
    endclocking
    property vac_true;
        1'b0 |-> 1'b1;
    endproperty : vac_true
    ap_vac_true: assert property(vac_true);
    ap_vac_false: assert property(not(vac_true));
    ap_vac_not_false: assert property(not(not(vac_true)));
    ap_reject_on: assert property(reject_on(1'b1) 1'b1);

endmodule : test_vacuity

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