[sv-ac] ballot result for 2005

----------------------------------------------------------------------------------
Ballot on Mantis 2005

- Called on 2007-12-12, final ballots due by 2007-12-17 T 23:59-08:00.

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

1. In the following text:

=20

The following example illustrates how user code can explicitly flush a
pending assertion report. In this case, failures of a1 are only reported
in time steps where bad_val_ok does not settle at a value of 1.

=20

always @(bad_val or bad_val_ok) begin : b1

   aa: assert #0 (bad_val) else $fatal("Sorry");

   if (bad_val_ok)

   disable a4;

end

=20

the reference to a1 does not exist in the example. Also, the target of
the disable "a4" does not exist.  I suspect aa -> a1 and a4 -> b1.

=20

2. as with disable of a block, there where probably be references to
assertion disables via VPI or $assertkill/$assertoff

=20

3. in 9.6.2, why is a deferred assertion singled out?  Doesn't this
apply to any assertion - simple immediate or concurrent?

=20

4. shouldn't we be adding "deferred assertion" and "simple immediate
assertion" to the glossary (annex Q). I am surprised that immediate
assertion is not already there.

=20

5. "The pass and fail statements in an action_block, if present, shall
each consist of a single subroutine call."  This paragraph sounds like
you are redefining action blocks. Why are they different from a simple
immediate assertion? =20

=20

6. why are only deferred assertions allowed outside of procedural code.
This seems to be another divergence from immediate assertions.

=20

7. Do we need to state somewhere that the attempt counter is only ever
incremented when the evaluation matures? =20

=20

8. I think it goes in Annex N, not Annex L.  Also, where should the
vpiIsDeferred to be added? I would think it belongs after:  #define
vpiImmediateAssert 665

On page 1124


[MK]

I vote 'no' as I did not get time to review this proposal. Please extend
the voting period.

----------------------------------------------------------------------------------
Other Comments

[DB]

1. end of page 3,=20

   "An immediate assume will often be useful in cases where a
combinational  =20
    condition is checked in a function, but needs to be used as an=20
    assumption rather than a proof target by formal tools. An immediate

    cover is useful to avoid crediting tests for covering a condition
that   =20
    is only met in passing by glitched values."

   Should be

   "An immediate differed assume will often be useful in cases where a=20
    combinational condition is checked in a function, but needs to be
used=20
    as an assumption rather than a proof target by formal tools. An=20
    immediate cover is useful to avoid crediting tests for covering a =20
    condition that is only met in passing by glitched values."

2. At 16.4.1 I don't understand this paragraph. What does it mean that=20
   "pending assertion reports may mature"?

3. 16.4.2 shouldn't an always block like

   always @(a) b =3D a;=20

   be considered as a flush point.

4. First example at 16.4.4 - label of assertion should be a4.


[LP]

1. "A deferred assertion is similar to a simple immediate assertion, but
with one key difference."

=20

is changed to list the key distinctions, because there are several:

=20

A deferred assertion is similar to a simple immediate assertion, but
with the following distinctions:

-       syntax

-       action block limitations

-       when it is evaluated

-       it can exist in a module outside of a process (is this the same
as a concurrent assertion but using current values instead of sampled
values?  I think I might have asked this but can't remember the answer.)

=20

2. I don't think you can disable an assertion with a disable statement,
only tasks or blocks. =20

disable_statement ::=3D

disable hierarchical_task_identifier ;

| disable hierarchical_block_identifier ;

| disable fork ;

=20

So in the example you need to disable the block "b1", not the assertion
"a1"

=20

always @(bad_val or bad_val_ok) begin : b1

  a1: assert #0 (bad_val) else $fatal("Sorry");=20

  if (bad_val_ok)=20

  disable a1;
end

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