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

Hi Tom,

Please, see my comments below. I will send the updated version once I
address all the comments I received.

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, November 13, 2007 3:44 AM
To: john.havlicek@freescale.com
Cc: sv-ac@server.eda.org
Subject: 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?

[Korchemny, Dmitry] Substitution semantics is required to be able to
pass sequences and properties as checker arguments. There are other
reasons as well, see your second comment as an example.

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.

[Korchemny, Dmitry] I think that checkers are more flexible than
modules. Essentially checkers do support parameters because of the
substitution semantics. Parameters as syntactical units would improve
error message quality, but I don't think they will improve the
flexibility. Could you provide an example when there is a need to use
modules because of the lack of the special syntax for parameters in
checkers?
 
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)

[Korchemny, Dmitry] At present there is a need to provide detailed
explanation about .* connections in checkers, since modules currently do
not allow default ports while checkers do. This was a point that Gord
rose in the F2F. There is an open SV-BC enhancement 1619 concerning the
same problem, and when it is approved, we will be able to remove the
whole section about argument passing syntax leaving only a reference to
it. Unfortunately this enhancement hasn't been accepted yet, and it is
not clear whether it is accepted in the near future.

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"?

[Korchemny, Dmitry] According to the BNF 

sequence_actual_arg ::=
event_expression
| sequence_expr

event_expression37 ::=
[ edge_identifier ] expression [ iff expression ]
| sequence_instance [ iff expression ]
| event_expression or event_expression
| event_expression , event_expression
| ( event_expression )

edge_identifier ::= posedge | negedge

Therefore for sequence "posedge clk" is a legal way to pass the actual
argument. The same is true for properties. I think that the same rules
should be applied for checker actual arguments.

5.  Page 8:
    Will the "default disable"  need to change to "default disable iff"?

[Korchemny, Dmitry] Changed.

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.

[Korchemny, Dmitry] As far as understand this issue was addressed by
your new mail. See my comments about the changes I made there.

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

[Korchemny, Dmitry] "bit" is legal here, but "event" makes more sense. I
changed it to "event" in this and other examples.

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"

[Korchemny, Dmitry] Fixed.

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.

[Korchemny, Dmitry] This was suggested by Doron, but we decided to keep
continuous free variables. The main reason of doing this was to allow
the output arguments of the checker. let statement cannot be used as an
output argument.

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.

[Korchemny, Dmitry] Fixed.

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)"

[Korchemny, Dmitry] Fixed it as:
The expression $past(v,1, en, clk) is equivalent to a free variable w.

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

[Korchemny, Dmitry] I added a comma, it looks OK.

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);

[Korchemny, Dmitry] I think that the correct form should be

assign a = $changed_gclk(clk) ? $past_gclk(b) && c : $past_gclk(a);

b affects the value of a only when the clk ticks.

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.