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

this would be another feature which will force all to finally define and
implement vacouoses well ;)

DANiel

On 1/31/2012 2:42 PM, Dana Fisman Ofek wrote:
>
> Hi Daniel,
>
> Since vacuity is not well defined (as we have discussed in the past) I
> don't think adding is_vacuous()is a good idea.
>
> Best,
>
> Dana
>
> *From:*owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of
> *Daniel Mlynek
> *Sent:* Tuesday, January 31, 2012 8:39 AM
> *To:* ben@systemverilog.us
> *Cc:* ben cohen; Little, Scott; sv-ac@eda-stds.org; Korchemny, Dmitry
> *Subject:* 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* <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.