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

Hi Manisha,

I updated the proposal according to our yesterday's discussion and
uploaded the new version. Here are the main changes.

* Added a description of free variable handling by simulator (page 12):

"Simulators shall assign arbitrary values to the free variables
consistent with the assumptions and the assignments. If a simulator
cannot assign consistent values to the free variables, it shall report a
violation of the corresponding assumptions. The simulator shall report a
violation of an assertion containing free variables if the assertion is
violated for the values of the free variables assigned by the simulator.
Optionally the simulator may choose to check the assertions for all
possible values of the free variables imposed by the assumptions and
assignments if it supports relevant formal verification techniques,
e.g., if it supports model checking on the fly."

* Added the following explanation of constant free variable simulation
(page 14):

Formal analysis tools shall take into account any possible values of a
constant free variable consistent with the imposed assumptions.
Simulators shall assign an arbitrary constant value to a constant free
variable consistent with its assumptions. If a simulator cannot assign a
right value to the constant free variable, it shall report a violation
of the corresponding assumptions. The simulator shall report a violation
of an assertion containing a constant free variable if the assertion is
violated for the value of the constant free variable assigned by the
simulator. Optionally the simulator may choose to check the assertions
for all possible values of the constant free variables imposed by the
assumptions if it supports relevant formal verification techniques,
e.g., if it supports model checking on the fly.

* Added notes that the checker implementations in examples a) and b),
pages 14-15 are equivalent for formal tools but not necessarily
equivalent in simulation.

* Added an example of the matched method in a checker variable
assignment (page 17). Also added an explicit clock for sequences used
with ended and matched.

* Added a  note in 16.13.6 that the method ended may be used not only in
sequences but also in checker variable assignments.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Kulshrestha, Manisha
Sent: Tuesday, December 18, 2007 9:00 AM
To: john.havlicek@freescale.com; sv-ac@server.eda.org
Subject: RE: [sv-ac] call to vote on 1900

Hi,

I vote 'no' as I am not comfortable with the explanation of const
freevars.

1. On page 14, example (a), I am not sure how the two things can be
considered equivalent in simulation. In the first case (where it is
comparing bit selects), the simulation tool will only compare one of the
indices of the array where as in the second case it will compare
complete array. Is simulation tool supposed to do something special here
? Since the index is a const how will simulation tool use all possible
indices ?

2. I do not understand example (b) also. I think more explanation is
required how simulation tool is going to simulate const free vars.

3. On page 16, it says that sequence method 'matched' can be used in
assignments. The method 'matched' has been there for synchronizing in
multi-clock case. What is the reason for allowing matched here ? What
will it be synchronizing with ?

4. On page 17, example (c), why is there a difference in sampling of
free bits based on assignments ? It will be good to have an example of
why this is being done.

Thanks.
Manisha

-----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 6:19 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.


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