[sv-ac] FW: [SystemVerilog P1800 0002938]: Surprising (to some users) interaction between deferred assertions & short-circuiting

I have uploaded a new version of this proposal to fix the issues mentioned by the champions.

>-----Original Message-----
>From: Accellera Mantis Bug Tracker [mailto:mantis@eda.org]
>Sent: Tuesday, October 12, 2010 4:16 PM
>To: Seligman, Erik
>Subject: [SystemVerilog P1800 0002938]: Surprising (to some users)
>interaction between deferred assertions & short-circuiting
>
>
>The following issue has been REOPENED.
>======================================================================
>http://www.eda-twiki.org/svdb/view.php?id=2938
>======================================================================
>Reported By: Erik_Seligman
>Assigned To: Erik_Seligman
>======================================================================
>Project: SystemVerilog P1800
>Issue ID: 2938
>Category: SV-AC
>Reproducibility: always
>Severity: feature
>Priority: normal
>Status: feedback
>Type: Clarification
>======================================================================
>Date Submitted: 2009-12-30 13:03 PST
>Last Modified: 2010-10-12 16:15 PDT
>======================================================================
>Summary: Surprising (to some users) interaction
>between
>deferred assertions & short-circuiting
>Description:
>Consider this piece of code:
> function f1(v)
> p1: assert #0 (v)
> ...
> always_comb begin: myblk
> a = b || f1(c)
>
>Now suppose, during some time step, the following happens:
>- Initially b is set to 0 while c==1, and myblk is entered. When f1 is
>called, assertion p1 has a passing value.
>- Later in the time step b settles at a value of 1, while c becomes 0.
>This time, due to short-circuiting, f1 is never evaluated-- so the new
>failing value of assertion p1 is never seen.
>- At the end of the time step, the simulator has reported that p1 was
>evaluated and passed, even though the final values for the time step
>would
>violate it.
>
>Strictly speaking, this is not a problem-- it's the behavior caused by
>the
>spec. But some of our designers have been caught off-guard, as it
>violates
>the intuition that a deferred assertion's result reflects the final
>settled
>values for each time step. It could actually be quite dangerous, in
>that
>the missed assertion failure could be seen as a false positive in
>testing.
>
>We had a proposal to hack our tools to turn off short-circuiting if any
>later term contains assertions, but realized that that would be
>dangerous,
>as it wouldn't be backwards-compatible, and some clever users may be
>intentionally causing this type of behavior.
>
>So... Should we do something about this? Due to the way it violates
>intuitive notions of deferred assertions, I think we should consider
>adding an example of this specific case to the deferred assertions
>section, or at least including such an example in supplemental
>clarifications documents.
>
>======================================================================
>
>----------------------------------------------------------------------
> (0009207) shalom (manager) - 2009-12-30 21:34
> http://www.eda-twiki.org/svdb/view.php?id=2938#c9207
>----------------------------------------------------------------------
>Another reason not to use logical operators where a bit-wise operator
>will
>do the job just as well.
>
>----------------------------------------------------------------------
> (0009555) Ben Cohen (developer) - 2010-07-18 12:44
> http://www.eda-twiki.org/svdb/view.php?id=2938#c9555
>----------------------------------------------------------------------
>I simulated the following code with both conditions: ( a = b || f2(c);)
>and
> (a = b | f2(c); )
>With regards to "Another reason not to use logical operators where a
>bit-wise operator will do the job just as well." the bitwise OR
>operator
>is not intuitive, as the intent is really the logical OR.
>But this is not the final solution to this issue, as shown in the
>example
>
> always_comb begin: myblk1 if (!b)
> a = f1(c);
>We need better guidelines.
>module m_or;
> logic clk=1, a=0, b=0, c=0, d=0, e=0;
> function f2(v);
> p2: assert #0 (v);
> endfunction : f2
> always_comb begin : myblk2
> // a = b || f2(c);
> a = b | f2(c);
> end : myblk2
> initial forever #10 clk = ! clk;
> initial begin
> c=1;
> b=0;
> e=1;
> c=0;
> b=1;
>
> end
>
>----------------------------------------------------------------------
> (0009641) Dmitry Korchemny (manager) - 2010-08-17 03:54
> http://www.eda-twiki.org/svdb/view.php?id=2938#c9641
>----------------------------------------------------------------------
>Passed by email ballot 2010-08-16: 11y/n/0a.
>
>----------------------------------------------------------------------
> (0009843) Neil Korpusik (administrator) - 2010-10-12 16:15
> http://www.eda-twiki.org/svdb/view.php?id=2938#c9843
>----------------------------------------------------------------------
>The proposal was opppsed by the Champions in the email vote which ended
>on September 29, 2010.
>
>Brad - opposed
> '#0' shouldn't be bold. The 'always_comb' procedure is missing an
>'end' or
> an ellipsis.
> More importantly, I think the final workaround sentence is
> counter-productive, unless we intend to deprecate '||'.
>
>Dave Rich - opposed (same reasons as Shalom)
>Shalom - opposed
> There are some syntax problems with the example.
> Some statements are missing semicolons at the ends of the line.
> The function declaration is missing a declaration of the argument v.
> The function should have an endfunction, and the always_comb "begin"
>should have an "end".
>
>Issue History
>Date Modified Username Field Change
>======================================================================
>2009-12-30 13:03 Erik_Seligman New Issue
>2009-12-30 13:03 Erik_Seligman Type =>
>Clarification
>2009-12-30 13:04 Erik_Seligman Issue Monitored: Erik_Seligman
>
>2009-12-30 21:33 shalom Issue Monitored: shalom
>2009-12-30 21:34 shalom Note Added: 0009207
>2010-06-28 04:46 Dmitry KorchemnyStatus new =>
>assigned
>2010-06-28 04:46 Dmitry KorchemnyAssigned To =>
>Erik_Seligman
>2010-07-09 10:12 Erik_Seligman File Added: proposal_2938.pdf
>
>2010-07-09 10:13 Erik_Seligman File Added: proposal_2938.docx
>
>2010-07-16 10:21 Erik_Seligman File Deleted: proposal_2938.pdf
>
>2010-07-16 10:21 Erik_Seligman File Deleted: proposal_2938.docx
>
>2010-07-16 10:21 Erik_Seligman File Added: proposal_2938.docx
>
>2010-07-16 10:22 Erik_Seligman File Added: proposal_2938.pdf
>
>2010-07-18 12:44 Ben Cohen Note Added: 0009555
>2010-08-09 12:17 Erik_Seligman File Deleted: proposal_2938.pdf
>
>2010-08-09 12:17 Erik_Seligman File Deleted: proposal_2938.docx
>
>2010-08-09 12:18 Erik_Seligman File Added: proposal_2938.pdf
>
>2010-08-09 12:18 Erik_Seligman File Added: proposal_2938.docx
>
>2010-08-10 10:14 Erik_Seligman File Deleted: proposal_2938.pdf
>
>2010-08-10 10:14 Erik_Seligman File Deleted: proposal_2938.docx
>
>2010-08-10 10:14 Erik_Seligman File Added: proposal_2938.pdf
>
>2010-08-10 10:14 Erik_Seligman File Added: proposal_2938.docx
>
>2010-08-17 03:54 Dmitry KorchemnyNote Added: 0009641
>2010-08-17 03:54 Dmitry KorchemnyStatus assigned =>
>resolved
>2010-08-17 03:54 Dmitry KorchemnyResolution open => fixed
>2010-08-17 03:54 Dmitry KorchemnyFixed in Version => 1800-2012
>2010-08-17 19:28 Steven Sharp Issue Monitored: Steven Sharp
>
>2010-08-17 19:51 Steven Sharp Issue End Monitor: Steven Sharp
>
>2010-10-12 16:15 Neil Korpusik Note Added: 0009843
>2010-10-12 16:15 Neil Korpusik Status resolved =>
>feedback
>2010-10-12 16:15 Neil Korpusik Resolution fixed =>
>reopened
>======================================================================
>
>
>--
>This message has been scanned for viruses and
>dangerous content by MailScanner, and is
>believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.