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

To implement vacuous success indication in all generality could be pretty costly in performance, I am afraid.
ed

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Daniel Mlynek
Sent: Tuesday, January 31, 2012 8:48 AM
To: Dana Fisman Ofek
Cc: ben@systemverilog.us; ben cohen; Little, Scott; sv-ac@eda-stds.org; Korchemny, Dmitry
Subject: 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> [mailto:owner-sv-ac@eda.org] On Behalf Of Daniel Mlynek
Sent: Tuesday, January 31, 2012 8:39 AM
To: ben@systemverilog.us<mailto:ben@systemverilog.us>
Cc: ben cohen; Little, Scott; sv-ac@eda-stds.org<mailto: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<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.