[sv-ac] ballot result for 1757

Hi Folks:

Our ballot on 1757 failed due to negative votes.

See the results below.

J.H.

----------------------------------------------------------------------------------
Ballot on Mantis 1757

- Called on 2007-10-29, final ballots due by 2007-11-05 T 23:59-08:00.

yv[xxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel)
yv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)     
 n[------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys)
 v[xxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
 t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair)
yv[xxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair)
yv[xxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics)
 n[--------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics)
 n[------------x--xxx.....................] Joseph Lu (Altera)
yv[xxxxxxxxx..............................] Johan Martensson (Jasper)
 n[-----------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
nv[-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
yv[-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel)
 n[----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics)
yv[xxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
nv[xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems)
   |--------------------------------------- attendance on 2007-10-23
 |----------------------------------------- voting eligibility for this ballot
|------------------------------------------ email ballots received

        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

----------------------------------------------------------------------------------
Rationale for Negative Vote:

[LP]

I vote no for the following reason (sorry!):  I think it is VERY
CONFUSING to be calling this a "reset property" and then calling the
condition a "disable condition".  Especially when the disable iff
condition is called the "reset condition".  Perhaps a way around this is
to call this an "override" or "interupt" or "early termination clause".
And in fact, the accept_on and reject_on conditions don't disable the
assertion, they cause it to pass or fail.

[TT]

I vote no on 1757, for the same reasons that Lisa mentioned.

----------------------------------------------------------------------------------
Friendly Amendments:

[DK]

The assertion (page 3):

assert property (go ##1 get[*2] |-> reject_on(stop) put[->2]);

requires a clock:

assert property (@clk go ##1 get[*2] |-> reject_on(stop) put[->2]);


[JM]

Beginning of 16.12.3:
=================================================

REPLACE (Two not three differences)
The semantics of accept_on is similar to disable iff, except for the
following three differences:   
 accept_on operates at the property level rather than the verification statement level   
 accept_on uses sampled values
WITH
The semantics of accept_on is similar to disable iff, except for the
following two differences:   
 accept_on operates at the property level rather than the verification statement level   
 accept_on uses sampled values

Explanation of examples:
============================

property p; (accept_on(a) p1) and (reject_on(b) p2); endproperty
----------------------------------------------------------------

REPLACE (Irrelevant whether second operand completes)
If a becomes true during the evaluation of p1 and the second term of the
and operation completed evaluation, the truth of p1 is ignored in
deciding the truth of p.  
WITH
If a becomes true during the evaluation of p1, the truth of p1 is ignored in
deciding the truth of p. 


REPLACE ('p2' missing)
deciding the truth of p.  On the other hand, if b becomes true during the
evaluation of then p evaluates to false.
WITH
deciding the truth of p.  On the other hand, if b becomes true during the
evaluation of p2 then p evaluates to false.

property p; (accept_on(a) p1) or (reject_on(b) p2); endproperty 
----------------------------------------------------------------

REPLACE (Irrelevant whether first operand completes)
If a becomes true during the evaluation of p1 then p evaluates to true.
On the other hand, if b becomes true during the evaluation of p2 and the
first term completed evaluation then the second term is ignored in
deciding the truth of p  
WITH
If a becomes true during the evaluation of p1 then p evaluates to true.
On the other hand, if b becomes true during the evaluation of p2 then
the second term is ignored in deciding the truth of p  


[LP]

1. Table 16-25 the reference is not exact  (if...else)  -> if-else in d4
and more significantly your text has a line for -> and <-> that is blank
in the replacement. (seems to be dependent on that other proposal)

2. There are a couple of issues with the following:

h) A property is a reset if it is of the following forms :

 accept_on(expression_or_dist) property_expr

 reject_on(expression_or_dist) property_expr

where the expression_or_dist is called the disable condition.

Issue a)  if you follow the format of existing text for other
letters(see e or f for example), it should read (ignore unintended font
changes):

h) A property is a reset if it has either the form is of the following
forms:

 accept_on(expression_or_dist) property_expr


or the form

 reject_on(expression_or_dist) property_expr

where the expression_or_dist is called the disable condition.

   Issue b) note in draft 4 that in the statement "where the
expression_or_dist is called the disable condition" that
expression_or_dist is now in times new roman italic instead of courier.
This means you can't italicize "disable condition" to differentiate it.


3. This is wrong if the last sentence is also comparing to disable iff:
Like disable iff, reject_on_and_accept_on_expressions may contain
sampled value functions (see

16.8.3). The clock argument shall be explicitly specified. The
expressions shall not contain any reference to

local variables and the sequence methods_ended, triggered_and_matched__
_ _


I think we should avoid the analogy to disable iff.  How about:

reject_on_and_accept_on_expressions may contain sampled value functions
(see

16.8.3). . If a sampled value function is

used in the reset expression, the sampling clock must be explicitly
specified in its actual argument list as

described in 16.8.3.  The expressions shall not contain any reference to

local variables and the sequence methods_ended, triggered_and_matched


This has the advantage of not confusing it with disable iff.  They are
not the same since disable iff can reference triggered. The new wording
that references 16.8.3 for sampling of a sampled value function was a
cut and paste from the description of this for disable iff.


4. There are several references to "property_expr" in the text that
should be italicized (new rule I think)


5. Should the references to "property" be "property_expr" in the
following:

 "The semantics of_reject_on(expression) property are the same as
not(accept_on(expression) not(property))."


[MK]

1.       In the statement "If during the evaluation the disable
condition becomes true, then the overall evaluation of the property
results in true." There should be a comma after "If during the
evaluation".

2.       In 1648 it is changing this part. I think there should be mention of
reset conditions in this part of the LRM. The first statement "In the
sequences used to build properties" does not seem to cover these.

There are two places where Boolean boolean expressions occur in
concurrent properties assertions:

- In the sequences used to build properties

- In the disable condition inferred for an assertion, specified either
in a top-level disable iff

clause (see 16.12) or in a default disable declaration (see 16.15)

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