RE: [sv-ac] 1900 Checkers

Hi Tom,

Please, see my comments below. I am not attaching a new version since I
am still working on it to incorporate other comments from F2F.

Thanks,
Dmitry

-----Original Message-----
From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] 
Sent: Thursday, September 27, 2007 1:44 AM
To: Korchemny, Dmitry
Cc: piper@cadence.com; sv-ac@eda-stds.org
Subject: Re: [sv-ac] 1900 Checkers

Hello Everyone,

Here are my comments so fare on the Mantis 1900 proposal "Checkers"
I'm still not done.  I still have to get through the section on free
variables.

Tom


1.  Right before Syntax 9-1:  "four statements"  should be "five",
because the
final block was added.

[Korchemny, Dmitry] I don't think it matters, since "four" is written in
the Draft3a. The new version does not number the statements.

2.  Free Variables:  How are they randomized, How are they repeatable?

[Korchemny, Dmitry] They can be randomized as any random variables. The
proposal does not define how they are repeatable. i.e., there is no
notion of seed. The reason is that non-deterministic free variables are
not intended for simulation, but for debugging FV checkers only. E.g.,
to give one possible trace of a non-deterministic model behavior. I
think that the seeding problem requires more elaboration, and it may be
solved in a backward compatible manner (one can say that the future
versions of LRM may impose repeatability restrictions on the free
variables). As far as I remember it was decided in the F2F not to
require supporting non-deterministic free variables in simulation.

3.  A previous version of the proposal included covergroups as a
possible
checker item. Now they seem to have been taken out. I'd like to see them
in.

[Korchemny, Dmitry] The reason why they have been taken out is the
various problems introduced by supporting RTL in checkers. Some more
work is needed to define their semantics in checkers, and this should be
done in cooperation with SV-EC. I saw that you opened a new Mantis item
for this issue, and I think this is a right way to proceed with it.

4.  p. 6.  "Checker action blocks shall not write into free variables,
and
they may contain any code . . ."
	Re-write as "Action blocks within a checker shall not write into
free
variables, but they may contain any other code . . ."

[Korchemny, Dmitry] "Checker action block" is a term introduced earlier
on this page. I rewrote this statement as: "Checker action blocks shall
not write into free variables, but they may contain any other code which
is normally allowed in action blocks in modules."

5.  p. 8.  "Since my_check1 instantiation is not in a scope of any
conditional
statement, its inferred enable condition is 1'b1."

Re-write as:  "If the enable pin connection had not been specified, the
inferred enable for the assertions in the my_check1 instantiation of the
checker would be 1'b1, since it is not in the scope of any conditional
statement"

As is, the statement almost implied that the inferred enable would
override
the value passed to the checker.

[Korchemny, Dmitry] This comment is not clear to me. We have here a
specific example, therefore the explanation should be specific and not
begin with "if". Also, all inferred enable conditions in the assertions
in any checker are 1'b1 regardless of the checker instantiation context,
since conditional statements inside a checker are not allowed and the
context is not inherited from the checker instantiation point. Therefore
we can speak only about the inferred enable condition for the entire
checker instantiation, and this is the intended meaning of the original
statement.

6.  Default clocking:  Are rules consistent?  For example, does default
clocking apply in module where it appears, any nested checker
definitions, etc.

[Korchemny, Dmitry] I think they are. Subclause 14.12 states: "A default
clocking is valid only within the scope containing the default clocking
specification. This scope includes the module, interface, or program
that contains the declaration as well as any nested modules or
interfaces. It does not include instantiated modules or interfaces." The
same rule was extrapolated to checkers: "Clock and disable context are
inherited from the scope of the checker declaration"
 
7.  What is the purpose for initial_check?  It's only to limit what may
appear in an initial block? What kind of event controls are allowed.

[Korchemny, Dmitry] In initial blocks the same event controls are
allowed as in always blocks. And clock events are likely to be used in
initial blocks containing concurrent assertions.

Right off the bat, it doesn't seem like a very useful construct, since
you
can't initialize anything in it.

[Korchemny, Dmitry] If you want an assertion to be monitored only once
you have to put it into an initial block, e.g. (in a module),

initial @(posedge clk) a1: assert property (a);
always @(posedge clk) a2: assert property (a);

a1 checks the value of a only at the first rising clock edge, while a2
checks the value of a at each rising clock edge.

Therefore there are no alternatives to initial blocks in checkers. The
reason of introducing a new construct initial_check is the same as for
always_check:

initial @clk a1: assert property (a);

will not infer the clocking event for a1, while initial_check will.



8.  p. 12, example a:  Shouldn't the variable idx be 6 bits, not 64
bits?
	const freevar bit [5:0] idx;

That is enough bits to index a 64-bit variable.

[Korchemny, Dmitry] Fixed.

9.  Note that example a would not work in simulation.  In simulation,
idx
would be initialized to one value, which it would keep throughout the
simulation.  The corresponding bit of data1 and data2 would match, but
the
other bits would not.

[Korchemny, Dmitry] It depends how we define the simulation of
non-deterministic free variables. The final decision was not to require
from simulators to support non-deterministic free variables. 

10.  Free variables can change at every time step?

[Korchemny, Dmitry] Continuous free variables are assigned when their
RHS changes (the proposal states that they are assigned every step to
avoid the definition of what changing of sampled value means and when it
happens), therefore this actually does not mean that their value does
change at each time step. Sequential free variables are synchronized by
a clock in case they are assigned. The non-deterministic free variables
are not required to be supported in simulation, therefore the issue is
not relevant for them.

11. Page 14:  Fragment sentence "This assignment shall at every time
step."

[Korchemny, Dmitry] Rewrote it as "This assignment shall execute at
every tine step."

Korchemny, Dmitry wrote On 09/19/07 02:27 AM,:
> Hi Lisa, Tom,
> 
>  
> 
> I uploaded the updated version of the proposal ready for review. This
> proposal does not contain a description of formal semantics yet.
> 
>  
> 
> Thanks,
> 
> Dmitry
> 
> ---------------------------------------------------------------------
> 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* <http://www.mailscanner.info/>, and
is
> believed to be clean.

-- 
------------------
Thomas J. Thatcher
Sun Microsystems
408-616-5589
------------------
---------------------------------------------------------------------
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.