[sv-ac] ballot result for 2089

Hi Folks:

Our ballot on 2089 failed due to negative votes.

See the results below.

J.H.

----------------------------------------------------------------------------------
Ballot on Mantis 2089

- Called on 2008-01-15, final ballots due by 2008-01-21 T 23:59-08:00.

yv[xxxxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel)
 v[xxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)     
 n[----------------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys)
nv[xxxxxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
 t[xxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair)
yv[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair)
nv[xxxxx-xxxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics)
 n[------------------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics)
 n[---------x------------x--xxx.....................] Joseph Lu (Altera)
 v[xxxxxxxxxxxxxxxxxxx..............................] Johan Martensson (Jasper)
 n[---------------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
nv[xxxxx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
yv[xxxxxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel)
 n[-------x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics)
yv[xxxxxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
yv[xxxxxxxxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems)
   |------------------------------------------------- attendance on 2008-01-15
 |--------------------------------------------------- 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

[MK]

1. I think the following statement (page 2) should be re-phrased.I
assume the intention is to say that that checker action blocks may
contain any code which is normally allowed in action blocks and final
blocks may contain any code which is normally allowed in final blocks.
By combining the two together, it gives the impression that final blocks
may contain the code which is normally allowed in action blocks or final
procedures. Which is incorrect.=20

"Checker action blocks or final procedures shall not write into free
variables, but they may contain any other code which is normally allowed
in action blocks or final procedures in modules."

2. I do not understand allowing assignments to formal arguments in final
blocks in a checker. Since these final blocks run at the end and their
order is non-deterministic, what will be the use of this ? Since the
formal may be a checker variable of an upper level checker, the
following contradicts with a statement in 16.18.4 where it says that
writing to a checker variable is not allowed in final procedure:
"However declarations of other variable types, which are not allowed
within a checker body are allowed, and code within a final procedure is
allowed to read from (but not write to) checker variables declared in
the checker body which contains the procedure."

"Checkers may assign values to their formal arguments, treating them as
output arguments, though no explicit
notation of this is required in the checker declaration statement. Each
formal argument used in this way may
be assigned a value either in a checker body, or in checker action
blocks, or in a final procedure. If a formal
argument is written in the checker body, its corresponding actual
argument shall be a checker variable or a
formal argument in another checker. If a formal argument is assigned a
value in a checker, it shall be
untyped. The output actual argument shall have a static lifetime."

[MK]

Please ignore my comment about contradiction in (2) as I did not
understand that part properly.

[YF]

in page 2 it is said:



Action blocks of assertions within a checker will be referred to as checker action blocks, and the rest of the

checker, with the exception of any final procedure code, will be referred to as checker body

 

but the following page has this section:

A checker body may contain the following elements:

... 

 initial_check, and always_check, and final procedures

Also page 3 (16.18.4 Checker procedures) says:

The following procedures are allowed inside a checker body:

 initial_check procedure, and

 always_check procedure

 final procedure

 
I think this is contradictory (or at least I don't understand it) , what is the reason for the exception mentioned in page 2 ? if there isn't any I think it should simply be removed.

[LP]

1. I find it confusing that a "final procedure" is in a checker body but
is not part of the checker body. I'm not sure why this distinction is
needed. It adds unnecessary confusion.

=20

2.   "Checker action blocks or final procedures shall not write into
free variables, but they may contain any other

code which is normally allowed in action blocks or final procedures in
modules."

=20

I am wondering if it would be better to say the following so that there
is no question whether things like action block controls apply:

=20

Checker action blocks are almost the same as non-checker action blocks.
They may contain any code that is allowed in an action block outside of
a checker, have the same default characteristics, and are impacted by
the same action block controls.  An additional restriction is that a
checker action block shall not write into free variables.  Similarly, a
final procedure in a checker follows all the same rules and regulations
as a final procedure in a module, with the additional restriction that
it shall not write info free variables.=20

----------------------------------------------------------------------------------
Friendly Amendments

[ES]

Minor friendly amendment near end of 16.18.4:  "However declarations of
other variable types, which are not allowed within a
checker body are allowed, ..." =3D=3D>
"However declarations of other variable types, which are not allowed
within a
checker body, are allowed, ..." =3D=3D>

[DK]

Top of page 5: "end" should be in bold.

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