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

So we have 4 possibiblities in fact:
- pass
- vacuous pass
- fail
- vacuous fail

While action block allows only 2 possibilities:
     ap_t_not: assert property(@ (posedge clk) not(a |=> b |-> c))
       $display("pass");
     else
       $display("fail");

Maybe it should be addresed somehow in LRM ie by adding funciton
is_vacuous()
     ap_t_not: assert property(@ (posedge clk) not(a |=> b |-> c))
       if (is_vacuous())
          $display("vacuous pass");
       else
          $display("pass");
     else
       if (is_vacuous())
          $display("vacuous fail");
       else
          $display("fail");

DANiel

On 1/26/2012 9:24 PM, ben cohen wrote:
> 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 <mailto: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>
> [mailto: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 <mailto: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* <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.