RE: [sv-ac] call to vote on 2005

-----Original Message-----
From: Seligman, Erik [mailto:erik.seligman@intel.com] 
Sent: Monday, January 21, 2008 5:51 PM
To: Lisa Piper; john.havlicek@freescale.com; sv-ac@eda.org
Subject: RE: [sv-ac] call to vote on 2005

Hi Lisa-- thanks for your comments.  See my responses below. 

-----Original Message-----

> "The counter for number of times evaluated, however, shall include all
>executions of the cover statement."   Like Dmitry, I don't understand
>why this includes all, versus only those matured. I think we need to
define "executions of" if this remains, because I 
> thought it was only executed when mature. 

[ES] Actually, this is a littly tricky.  Since deferred covers are only
queued & mature when actually triggered, we can't count only matured
executions-- this would mean that failed attempts to check the cover
point would not be counted, which defeats the purpose of this
measurement.  I consider an "execution" for this purpose to mean any
time the boolean condition is evaluated, which I think is the intention
of the evaluation count.  If that is correct, then I believe the current
wording works.  (Another possibility is to define a concept of maturing
of a failed cover evaluation which results in no action, but I think
this would needlessly complicate the proposal.)
[Lisa Piper >>>] I admit it is ambiguous - you could argue both ways.
For clarity, I would say when the boolean condition is evaluated.  It
may be appropriate to spell out that for deferred assertions, there can
be many evaluations per attempt, if that is what is desired. I think the
relationship between evaluation and attempt is the confusion around
$assertoff as well.


> "- Syntax: Deferred assertions use #0 after the assert."   I would
> suggest changing the "assert" to the "verification directive" to make
it applicable to assume and cover as well, and 
> independent of 1729.
> Applies in two places.

[ES] Will fix.


>"In the case of a deferred assertion (see 16.4 editor correct
reference), currently queued reports are not flushed, though 
>further checking is prevented until the $asserton."  I would think it
would continue checking for that time step, report the >result in the
Reactive region, and then stop. This sounds like it could report interim
results after $asserton resumes
>checking. The wording in the VPI section was more clear.

[ES] Well, this is another slightly ambiguous area.  I thought that to
be consistent with expected $assertoff behavior, checking should be
stopped immediately, rather than at the end of the time step.  As I read
it in the current LRM, an $assertoff instantly stops further
evaluations, while not interfering with current evaluations.  I think
the danger of interim results is minimal, because $assertoff doesn't
prevent flushing for other reasons:  if a procedure that failed an
immediate assert is re-executed in the same time step, a current queued
failure might be flushed, even though the assertion is not re-evaluated
due to $assertoff.
Does this make sense?
[Lisa Piper >>>] I read it as it stops further "attempts" since prior to
deferred assertions, an evaluation is an attempt.  Why would it be ok
for the VPI to work differently?  I think if you want to flush
everything, you simply use $assertkill.  Maybe we need to change the
definition of $assertoff to specify "an assertion attempt" rather than
"an assertion".






-----Original Message-----
From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of John
Havlicek
Sent: Wednesday, January 16, 2008 8:25 PM
To: sv-ac@eda.org
Subject: [sv-ac] call to vote on 2005

Hi Folks:

This is the call to vote on the proposal for Mantis 2005, revised to
address comments from Tej Singh.

The document on Mantis is 

   assertdefer080116es.pdf

Please vote if you are eligible.  See details below.

J.H.

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

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

 v[xxxxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan
(Intel)
 v[xxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny
(Synopsys)     
 n[----------------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani
(Synopsys)
 v[xxxxxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais
(Freescale)
 t[xxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek
(Freescale - Chair)
v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny
(Intel - Co-Chair)  v[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)
 v[xxxxx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper
(Cadence)
 v[xxxxxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman
(Intel)
 n[-------x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor
Graphics)
 v[xxxxxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara
(Synopsys)
 v[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

--
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.



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