[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, and is
believed to be clean.