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

Hi Tom,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Thomas Thatcher
Sent: Tuesday, February 05, 2008 3:56 AM
To: john.havlicek@freescale.com
Cc: sv-ac@server.eda.org; Bustan, Doron; eduard.cerny@synopsys.com;
yaniv.fais@freescale.com; Korchemny, Dmitry;
Manisha_Kulshrestha@mentor.com; johan.martensson@jasper-da.com;
piper@cadence.com; Seligman, Erik; bassam.tabbara@synopsys.com
Subject: Re: [sv-ac] call to vote on 2110

I will vote no on 2110

1.  The proposal needs more detail on what happens to procedures within 
the checker when that checker is instantiated in a loop.
For example, I assume that the intet is that an always_check will be 
executed just once every triggering event.  It won't be executed 
multiple times for each pass of the loop the checker is instantiated in.
But this is not stated.  The text says only:

     "A checker in a procedural loop executes its contents for each 
possible valid set of loop control variables."

[Korchemny, Dmitry] I agree, the description should be refined.

2.  Note that there will be a very interesting gotcha:  A cover property

appearing in a checker which is instantiated in a loop will be executed 
once for every valid combination of loop control variables.  However, a 
covergroup (assuming 2088 passes) will be executed only once (If I 
understand the intent correctly), because it is triggered by its 
triggering event.  (Sounds like material for another "Gotchas" paper at 
SNUG 2009 for Stu :-)

[Korchemny, Dmitry] This should not be a problem, just a limitation:
cover property may depend on loop control variables, while covergroup
cannot. Therefore a covergroup should be counted only once, and this
agrees with the intuition. There is indeed a minor issue with assertion
statements that do not depend on loop control variables, since they will
be reported several times:

cover property(a); // Does not depend on loop control variable

will be executed according to the number of loop iterations (as any
assertion in loops).

A few more questions:

In the example at the top of page 3.  The checker formal argument is of 
type bit.  the actual args of the instances are "foo[i] |-> bar[i]",
"foo |-> bar"  Aren't these actual args of type property?

[Korchemny, Dmitry] Yes, either it should be of type property, or should
be "foo[i] -> bar[i] (using boolean implication introduced in 1758. I
would use in this example some existing operator such as && in order to
avoid dependency on 1758).

[Korchemny, Dmitry] BTW, I noticed that in the following line:

if (foo[i] != baz[i]) break;

it is written "baz" instead of "bar".


Once these points are explained clearly, the proposal should be
acceptable.

Tom

John Havlicek wrote:
> Hi Folks:
> 
> This is the call to vote on 2110.
> 
> The document on Mantis is
> 
>    checkerinloop080121es.pdf
> 
> Please vote if you are eligible.  See details below.
> 
> J.H.
> 
>
------------------------------------------------------------------------
----------
> Ballot on Mantis 2110
> 
> - Called on 2008-01-29, final ballots due by 2008-02-04 T 23:59-08:00.
> 
>  v[xxxxxxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan
(Intel)
>  v[xxxxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny
(Synopsys)     
>  n[------------------------x-xxx---------x-x-xxx-x---x] Surrendra
Dudani (Synopsys)
>  v[-xxxxxxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais
(Freescale)
>  t[xxxxxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek
(Freescale - Chair)
>  v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry
Korchemny (Intel - Co-Chair)
>  v[xxxxxxx-xxxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha
Kulshrestha (Mentor Graphics)
>  n[-x-------------------------------------------------] Ah-Lam Lee
(Qualcomm)
>  n[--------------------------------xxxxx-------x-xx-x-] Jiang Long
(Mentor Graphics)
>  n[-----------x------------x--xxx.....................] Joseph Lu
(Altera)
>  n[--xxxxxxxxxxxxxxxxxxx..............................] Johan
Martensson (Jasper)
>  n[-----------------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller
(Freescale)
>  v[xxxxxxx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper
(Cadence)
>  v[xxxxxxxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman
(Intel)
>  n[---------x-x----x--------xxxx-----xxxx-xx----------] Tej Singh
(Mentor Graphics)
>  v[x-xxxxxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara
(Synopsys)
>  v[xxxxxxxxxxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher
(Sun Microsystems)
>    |--------------------------------------------------- attendance on
2008-01-29
>  |----------------------------------------------------- voting
eligibility for this ballot
> |------------------------------------------------------ e-mail votes
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.