Re: [sv-ac] Minutes of SV-AC Meeting

Scott,
Before getting further on this, I thought I could discuss this point on
vacuity and the *implies *operator*. *
I started with an example, and typical uses of the *implies*.
Honestly, I see more of the use of the implies where the antecedent and
consequent are sequences.
I am struggling in understanding the cases where those are properties. The
only exception is the use of the "*not*" operator.
Am looking for some quick feedback, and more on the applications and
meanings for such test cases.

A typical application of the *implies *operator is the specification of the
values of variables at specific timing events, and where those variables
have an antecedent / consequent relationship. This application takes this
form:

sequence {*and *sequence } *implies *sequence {*and *sequence }

For example (simple model):

*module* m;

*logic* clk, req, ack, done, master_mode;

*sequence* t; 1; endsequence

*sequence* t2; ##2 1; endsequence

*sequence* t4; ##4 1; endsequence

 *property* pReqRdyAckDone;

(t ##0 req) *and* (t2 ##0 rdy) *implies*

(t ##0 master_mode) *and* (t4 ##0 ack) *and* (##[5:8] done);

*endproperty* : pReqRdyAckDone

 apReqRdyAckDone: *assert property* (@ (*posedge* clk) pReqRdyAckDone);

endmodule : m

 What is that saying?

   If (req==0 @ attempt) or (rdy==0 @t2), then *master_mode, ack,* and *done
   * can have any value at the defined time steps for an attempt at time t.
   The property is vacuous. Does vacuous true or vacuous false matter here?

In the above example, since the LHS and RHS properties are sequences, thry
cannot be vacuous. Thus, the table gets reduced to:

     p

q

p implies0 q

p implies1 q

p implies2 q

Comments

   F,nv

F,nv

t,nv

t,VA

t,VA

6 implies0 seems wrong

   F,nv

t,nv

t,nv

t,VA

t,VA

8 implies0 seems wrong

   t,nv

F,nv

F,nv

F,nv

F,nv

14

   t,nv

t,nv

t,nv

t,nv

t,nv

16

 Consider this variation:

*property* pComplex;

(req |-> ##2 rdy) *implies*
(master_mode |-> (t4 ##0 ack) *and* (##[5:8] done));
*endproperty* : pComplex

What is that saying?

    1) If *req* is false, then we don't care about the value of rdy @t2.
   What about *master_mode, ack,* and *done? *

On Tue, Oct 12, 2010 at 10:01 AM, Thomas J Thatcher <
thomas.thatcher@oracle.com> wrote:

> Minutes from SV-AC Meeting
> Date: 2010-10-12
> Time: 16:00 UTC (9:00 PDT)
> Duration: 1.5 hours
>
> Dial-in information:
> --------------------
> Meeting ID: 38198
>
> Phone Number(s):
> 1-888-813-5316 Toll Free within North America
>
>
> Live Meeting: https://webjoin.intel.com/?passcode=9261632
>
>
> Agenda:
> -------
> - Reminder of IEEE patent policy.
> See: http://standards.ieee.org/board/pat/pat-slideset.ppt
>
> - Minutes approval
>
> - Issue resolution/discussion
> 2328 - Review and relax restrictions on data types in assertions
> 2904 - Clarify when disable iff condition must occur relative to starting
> and ending of an attempt
> 3135 - Verbal explanation of nexttime and always is misleading for multiple
> clocks
>
> - Enhancement progress update
>
> - Opens
>
>
> Attendance Record:
> ------------------
> Legend:
> x = attended
> - = missed
> r = represented
> . = not yet a member
> v = valid voter (2 out of last 3 or 3/4 overall)
> n = not a valid voter
> t = chair eligible to vote only to make or break a tie
>
> Attendance re-initialized on 2010-07-06:
>
> v[xx-x-xxxxx--xxx] Laurence Bisht (Intel)
> v[-xxxxxxxxxxxxx-] Eduard Cerny (Synopsys)
> v[xx-xxxxx-xxxxxx] Ben Cohen
> v[-xxx-x--xxxxxxx] Surrendra Dudani (Synopsys)
> v[--xxxx---x-xxxx] Dana Fisman (Synopsys)
> v[xxxx-x-xxxxxxxx] John Havlicek (Freescale)
> v[-x-xxxxxxxxxxxx] Tapan Kapoor (Cadence)
> t[xxxxxxxxxxxxxxx] Dmitry Korchemny (Intel ż Chair)
> v[xxxxxx-xxxxxxxx] Scott Little (Freescale)
> v[xxxxxxx-xxxxxxx] Manisha Kulshrestha (Mentor Graphics)
> v[xxxxxxxxxxxxxxx] Anupam Prabhakar (Mentor Graphics)
> v[xx--xxxxxxx-xxx] Erik Seligman (Intel)
> v[xxxxxx-xxxxxxx.] Samik Sengupta (Synopsys)
> v[xxxxxxxxxxx-xxx] Tom Thatcher (Oracle ż Co-Chair)
> |- attendance on 2010-10-12
> |--- voting eligibility on 2010-10-12
>
>
>
> Minutes:
> --------
> - Reminder of IEEE patent policy.
> See: http://standards.ieee.org/board/pat/pat-slideset.ppt
> Participanats were reminded of the policy.
>
> - Minutes approval
> Erik: Move to approve minutes
> Samik: Second
> Voting Results: , 0n, 0a
>
> - Issue resolution/discussion
> 2328 - Review and relax restrictions on data types in assertions
> Scott: Need to get a new proposal together. When it is done, will send it
> out.
>
> - Enhancement progress Update
>
>
> Vacuity discussion:
> Ben: Had created a modification of Scott's table.
>
> Ben: If antecedant is false, why do we care if property vacuous or not
> Scott: Think that you need to separate true/false from vacuous/nonvacuous
>
> Ben: Does a vacuous false mean a less important failure?
> Dmitry: No, you can't ignore failure even if vacuous false.
>
> John: Although standard may distinguish betwee vacuous and non-vacuous
> failure, the end-user doesn't need to. User may want to see all
> failures, and doesn't care about vacuous fail vs non-vacuous fail.
> But
> Ben: In formal verification: does it make any difference?
>
> Ben: a implies b implies c: Which is evaluated first?
> John: Believe it is right associative.
> The order of evaluation is not important to this issue. Can always
> add parenthesis.
>
> Tom: Is this document talking specifically about the property implies
> operator, or is it about implication in general?
> Scott: Document talks about property implies?
> Tom: So the document is proposing two new possible definitions of
> vacuity for a property implies?
> Scott: Current definition in LRM is broken (implies0 in document). The
> implies1 and implies2 are two possible suggestions for a fix.
> A property implies will have cases not seen by sequence implication
> operators.
>
> Manisha: What is difference between implies1 and implies2
> John: The implies2 definition requires non-vacuity of antecedant.
> John: Suggest that we don't try to decide now. Were there any other
> points.
> Ben: Would like to converge. Think that a table in the LRM would make
> things much clearer
> Dmitry: A table would need to go in an annex.
> Ben: Don't care where the table is. Think that a table would make this
> much clearer.
>
> Could vacuity for implies be defined in terms of vacuity of property
> or operator?
> John: Vacuity for implies is not symmetric. Would be suspicious of any
> vacuity definition for property or that was not symmetric.
>
>
> Meeting adjourned.
>
> --
> 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.