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

Hi Doron,

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 Bustan, Doron
Sent: Tuesday, December 18, 2007 5:50 PM
To: john.havlicek@freescale.com; sv-ac@server.eda.org
Subject: RE: [sv-ac] call to vote on 1900

More comments:

1. At 16.18.5.1 : the sentence below

  "Continuous assignments (see 10.3) shall drive values onto checker 
   variables, both vector (packed) and scalar. This assignment shall
   execute at every time step."

   Is not consistent with ordinary continuous assignment when an
assignment   
   occurs every time the right hand expression changes.
   Why the differences?

[Korchemny, Dmitry] The regular definition of continuous assignment -
"the continuous assignment occurs every time the right hand side
expression changes" - will work for checker variables only if all the
assignment statements and the sequences are topologically sorted.

E.g.,

sequence s;
	a[*2];
endsequence

assign a = exp1;
assign b = exp2 && s.ended;

If b evaluates before a then the sequence s has to be reevaluated. The
LRM defines that the sequences are evaluated in the Observed region only
once. To adopt the definition you suggest the assertion simulation
semantics will have to be modified.

Also, the regular definition of continuous assignments will require
changing the description of the general simulation semantics, e.g., when
exp1 changes, the event has to be scheduled in the Observed region.

I think that the statement that the continuous assignment of checker
variables shall execute at every time step is clearer than the
explanation about topological sorting (this is explained in the
subclause describing the simulation semantics). Essentially, this
definition is a matter of phrasing only, and the implementation may be
event-driven, it should just take the topological sort into account.

2. second example at page 17, I think that

    "checkvar bit fv1[1:0] = '{1:1'b0};"

   Should be 
    
   "checkvar bit fv1[1:0] = '{1,1'b0};"

[Korchemny, Dmitry] I think that this definition is correct since only
fv1[1] is initialized. fv[0] is a continuous bit, and it is illegal to
initialize it.

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:49 AM
>>To: sv-ac@server.eda.org
>>Subject: [sv-ac] call to vote on 1900
>>
>>Hi Folks:
>>
>>This is the call to vote on the proposal for Mantis 1900.
>>
>>This ballot will close on 2007-12-17 as we discussed in our
>>meeting on 2007-12-11.
>>
>>The document on Mantis is
>>
>>   checkers_071209dk.pdf
>>
>>Please vote if you are eligible.  See the details below.
>>
>>J.H.
>>
>>----------------------------------------------------------------------
----
>>--------
>>Ballot on Mantis 1900
>>
>>- 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.


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