RE: [sv-ac] 16.14.8 Nonvacuous evaluations // the not(property)

Hi Ben,

Doesn't 16.14.8 d) address the not operator? I way I read the definition not doesn't change the vacuity result.

Thanks,
Scott

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben cohen
Sent: Thursday, January 26, 2012 11:14 AM
To: sv-ac@eda-stds.org; Korchemny, Dmitry
Subject: [sv-ac] 16.14.8 Nonvacuous evaluations // the not(property)

Section "16.14.8 Nonvacuous evaluations" does not address the vacuity of a not operator.
Specifically, what should the result of a "not(vacuous_property)" be?
I tried the following model on a simulator, and ap_t was evaluated as vacuous, and the pass and fail counts were not incremented.
That is expected.
However, ap_t_not was evaluated as fail, and the pass count was 0, and fail counts was 4 for a run of 100ns. The fail count is incremented.
I can understand the argument that since a vacuous property is evaluated as "true", the not of "true" is "false"
To me the "not(vacuous_property)" should be evaluated as vacuously false, and the failure count should not be incremented.
The pass count for "(vacuous_property)" is not incremented. So, why should the fail count be incremented for "not(vacuous_property)"?
Do we want to address that for the next 1800, past 2012? Should I write a mantis?
Ben Cohen
module vac;
    timeunit 1ns;
    timeprecision 1ns;
    logic clk =1'b1, a=1, b=0, c=0;
    default clocking @(negedge clk);
    endclocking

    ap_t: assert property(@ (posedge clk) a |=> b |-> c);
    ap_t_not: assert property(@ (posedge clk) not(a |=> b |-> c));
    initial forever #10 clk=!clk;
endmodule : vac

--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.