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

Scott,
Thanks, I missed it.
16.14.8 d) An evaluation attempt of a property of the form not
property_expr is nonvacuous if, and only if, the
underlying evaluation attempt of property_expr is nonvacuous.

In that case, that vendor needs to bet compliant.
Ben

On Thu, Jan 26, 2012 at 12:11 PM, Little, Scott <scott.little@intel.com>wrote:

> 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.