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

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: Wednesday, November 14, 2007 12:44 AM
To: john.havlicek@freescale.com
Cc: sv-ac@server.eda.org
Subject: Re: [sv-ac] call to vote on 1900

Hello Everyone,

In today's meeting we discussed what alternative language to use to
describe
the relationship between non-deterministic free variables and assume
property
statements that involve these signals.

First,  I'll quote from the LRM clause 16.14.2:

	"The purpose of the assume statement is to allow properties to
be
	considered as assumptions for formal analysis as well as for
dynamic
	simulation tools. When a property is assumed, the tools
constrain the
	environment so that the property holds.

	For formal analysis, there is no obligation to verify that the
assumed
	properties hold. An assumed property can be considered as a
hypothesis
	to prove the asserted properties.

	For simulation, the environment must be constrained so that the
	properties that are assumed shall hold. Like an asserted
property, an
	assumed property must be checked and reported if it fails to
hold."

I believe that assumptions on free variables should be consistent with
the
above section.  I would propose language similar to the following to
replace
the first paragraph on page 12.

	"One or more assume property statement may be written which
involve
	a non-deterministic free variable.  Formal analysis tools may
use
	these assumptions to constrain the values generated for these
	variables.

	For simulation, an assumed property on a non-deterministic free
	variable must be checked and reported if it fails to hold."

This paragraph should be moved before the example.
[Korchemny, Dmitry] I added the following language before the examples:

"Formal analysis tools shall take into account all possible values of
the free variables imposed the assumptions and assignments (see
16.18.5.1). For simulation an assumption containing free variable shall
be checked and reported if it is failed to be satisfied."

  The explanation of the
example should show that for *formal* analysis the free variable flag
has been
restricted by the assumptions m1, m2, & m3.

[Korchemny, Dmitry] I added the following sentence: "Formal analysis
tools shall take all possible legal behaviors of flag into account."

One more thing about free variables.  At a minimum, I think we're going
to
need a sentence somewhere that reads something like this:

	"Non-deterministic free variables must have the same random
stability
	properties that *rand* variables have (see 17.14)"


We also need to make a change to 17.14.1:

Replace:
"Initialization RNG.  Each module instance, interface instance, program
instance, and package has an initialization RNG."

With
"Initialization RNG.  Each module instance, interface instance, program
instance, checker instance, and package has an initialization RNG."

We'll probably need a way to manually randomize the checker as well.  We
may
need to define an srandom() method for the checker to allow this.

[Korchemny, Dmitry] I think that the random simulation is too important
to consider it in 1900. We need a separate proposal for it.

Tom

Thomas Thatcher wrote On 11/12/07 05:43 PM,:
> Hello Everyone,
> 
> I will vote no on 1900.  It doesn't seem ready just yet.
> 
> Here are the issues I found.
> 
> 
> 1.  Page 7:  "When a checker is instantiated . . ."
> 
>     Are we sure that we want to continue using substitution semantics
for the
>     checker construct?   Maybe an instantiation semantics would be
easier to
>     define?
> 
> 2.  Page 2:  "Parameters for checkers and properties"
> 
>     OK, I at least see one reason for using substitution semantics.
It at
>     least allows the checker to handle variations in signal width or
type.
>     However, beyond that, it will be impossible to write a flexible
checker
>     without some support for parameters.  We'll be forced to use
modules for
>     any checker that requires parameters to set options for the
checker.
> 
> 3.  Page 7:  "An implicit .* port connection . . ."
> 
>     This paragraph spends too much time explaining the difference
betweeen
>     .name and .* port connections.  That is explained elsewhere.  This
>     paragraph needs to concentrate on the interaction between the port
>     connection method and default values on the formal argument.  For
example,
>     a default value will never be used if the argument is connected
with
>     .name.
> 
>     Also, on the bullet points directly above, we could clarify as
follows:
> 
> 	-- Named port connection using implicit connections (.name
syntax)
> 	-- Named port connection using a wildcard port name (.* syntax)
> 
> 
> 4.  Page 8:
> 
>     When connecting a clock of a checker, what is the proper syntax?
> 
> 	my_check check_inside (a, posedge clk);
>     or
> 	my_check check_inside (a, @posedge clk);
>     and why?
>     Is it currently allowed to connect a port to "posedge clk"?
> 
> 
> 5.  Page 8:
>     Will the "default disable"  need to change to "default disable
iff"?
> 
> 6.  Page 12:  "Note that although the behavior . . ."
> 
>     I thought we had decided not to specify the effect of assume
property
>     statements on free variable values.
> 
> 
> 7.  Page 16:  Example 1:
> 
>     What is the proper type for a checker clock?  Here it's defined as
"bit",
>     just like any other signal.  However, it's being passed an event
>     (@posedge clk).
> 
> 8.  Page 16:  Example 2:  "In this example fv1[0] is assigned . . ."
> 	"In the assignment of fv2 the sampled value of fv1[0] is sampled
> 	since fv1[0] is a continuous free bit and the value of fv1[1] is
> 	not sampled since fv1[1] is a sequential free bit"
> 
>     This seems backward from the paragraph above:
> 
> 	"All variables participating in the right-hand side of a free
variable
> 	assignment are sampled, except the continuous free bits"
> 
> 9.  Page 16:
>     Didn't we decide to drop continuous assignments to free variables
at one
>     point?  It seems they add a lot of complexity to the proposal.
> 
> 10.  Page 17: 16.18.5.2
> 	"the value of b in the assertion is sampled while the value of c
is
> 	not"
> 
>     Again, this is backwards with respect to the paragraph cited
above.
> 
> 11.  Page 20:  "Then $sampled(v) returns v.$past(v,1,en, clk)
> 
>     This needs to change for clarity:
> 	"Then $sampled(v) returns v.  The expression $past(v,1,en, clk)"
> 
> 12.  Page 20:   "The future value of v $future_gclk(v)"
> 
>     This also needs to change for clarity  add a comma to separate v
from the
>     expression that follows.  If that doesn't visually separate them
enough
>     we may have to rewrite further:
> 	"The future value of v, given by $future_gclk(v) . . ."
> 
> 13.  Page 20:  "The equivalent form after rewriting is . . ."
> 
>     In the re-written form, a does not change if b changes:  only if c
>     changes.  To account for that, an extra term has to be added
> 
> 	"assign a = $changed_gclk($past_gclk(b)) || $changed_gclk(c) ?
> 		$past_gclk(b) && c : $past_gclk_(a);
> 
> Tom
> 
> John Havlicek wrote On 11/06/07 12:05 PM,:
> 
>>Hi Folks:
>>
>>This is the call to vote on the proposal for Mantis 1900.
>>
>>The document is
>>
>>   checkers_071104dk.pdf
>>
>>Please vote if you are eligible.  See the details below.
>>
>>J.H.
>>
>>----------------------------------------------------------------------
------------
>>Ballot on Mantis 1900
>>
>>- Called on 2007-11-06, final ballots due by 2007-11-13 T 23:59-08:00.
>>
>> v[xxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel)
>> v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)

>> n[--------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani
(Synopsys)
>> v[-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
>> t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale
- Chair)
>> v[xxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel
- Co-Chair)
>> v[xxxxxxx-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[xxxxxxxxxxx..............................] Johan Martensson
(Jasper)
>> n[-------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller
(Freescale)
>> v[xx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
>> n[-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel)
>> n[-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor
Graphics)
>> v[-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara
(Synopsys)
>> v[x-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun
Microsystems)
>>   |----------------------------------------- attendance on 2007-11-06
>> |------------------------------------------- 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
>>
>>
> 
> 

-- 
------------------
Thomas J. Thatcher
Sun Microsystems
------------------

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