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

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.