[sv-ac] Revised version of proposal 2005 (deferred assertions)

From: Seligman, Erik <erik.seligman_at_.....>
Date: Mon Dec 17 2007 - 11:28:08 PST
 
Hi guys-- I have posted a revised version which attempts to fix most of
your concerns.  I have attached a doc with change tracking on, so you
can take a quick look at the changes. Also, a few responses to specific
points from Doron & Lisa; tell me if these answers seem satisfactory:

[DB]  "16.4.2 shouldn't an always block like
		always @(a) b = a; 
	be considered as a flush point."
[ES] Actually, this is a standalone procedure with no deferred
assertions in it, so the concept of a flush point is not relevant.  The
change to 'b' might trigger another procedure, of course... And if that
has its own deferred assertions, the re-triggering due to b would cause
a flush.  Or am I misunderstanding your concern?

[LP] "in 9.6.2, why is a deferred assertion singled out?"  
[ES] This is just for emphasis, since deferred assertions have the
additional time in the queue between initial failure and reporting,
which gives more of an opportunity for external processes to disable &
flush them.

[LP] " 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."
[ES] Actually, I took a look at Annex Q, and it seems very minimal
currently-- it doesn't even define the difference between immediate &
concurrent asserts, as you point out, and is only 3 pages total!  Thus I
don't think the additional sub-terminology for this section would be
appropriate here, other than the definition of 'assertion' & reference
to Clause 16 that is currently there, unless we want to do a general
expansion of this annex to make it much more comprehensive.  Perhaps
that is an item for another proposal?

[LP] '" "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?'  
[ES] I have clarified this language to make it clearer that this
restriction applies only to deferred assertions.  This restriction was
added because of the complication of the time between the procedural
execution and the action block execution:  many things can change, and
we wanted to very crisply define what info can be passed from the
assertion context.

[LP] "why are only deferred assertions allowed outside of procedural
code.  This seems to be another divergence from immediate assertions."
[ES] Well, this feature wouldn't make much sense for non-deferred
immediate assertions, since they would be checking conditions at some
uncontrollable arbitrary point amidst procedural execution.  Thus we
define it only for deferred assertions, rather than trying to generally
extend immediate assertions.  It's an important feature in Intel's usage
model, where we support general assertion macros that design engineers
can instantiate in a procedure, function, or module context.



-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Bustan, Doron
Sent: Monday, December 17, 2007 7:17 AM
To: john.havlicek@freescale.com; sv-ac@server.eda.org
Subject: RE: [sv-ac] call to vote on 2005

These are my comments 

1. end of page 3, 

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

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

   Should be

   "An immediate differed assume will often be useful in cases where a 
    combinational condition is checked in a function, but needs to be
used 
    as an assumption rather than a proof target by formal tools. An 
    immediate cover is useful to avoid crediting tests for covering a  
    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 
   "pending assertion reports may mature"?

3. 16.4.2 shouldn't an always block like

   always @(a) b = a; 

   be considered as a flush point.

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

Doron


>>-----Original Message-----
>>From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org]
On
>>Behalf Of John Havlicek
>>Sent: Thursday, December 13, 2007 2:52 AM
>>To: sv-ac@server.eda.org
>>Subject: [sv-ac] call to vote on 2005
>>
>>Hi Folks:
>>
>>This is the call to vote on the proposal for Mantis 2005.
>>
>>This ballot will close on 2007-12-17 as discussed in our meeting on 
>>2007-12-11.
>>
>>The document on Mantis is
>>
>>  assertdefer071211es.pdf
>>
>>Please vote if you are eligible.  See the details below.
>>
>>J.H.
>>
>>----------------------------------------------------------------------
----
>>--------
>>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)
>> v[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)
>> v[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)
>> v[xx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper
(Cadence)
>> v[xxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman
(Intel)
>> n[----x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor
>>Graphics)
>> v[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
>>
>>
>>--
>>This message has been scanned for viruses and dangerous content by 
>>MailScanner, and is believed to be clean.
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution by
others is strictly prohibited. If you are not the intended recipient,
please contact the sender and delete all copies.


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


Received on Mon Dec 17 13:01:03 2007

This archive was generated by hypermail 2.1.8 : Mon Dec 17 2007 - 13:02:12 PST