RE: [sv-bc] RE: [sv-ac] RE: [sv-ec] Checkers & Formal

Hi Gord,

Please, see my answers below.

Thanks,
Dmitry

-----Original Message-----
From: Gordon Vreugdenhil [mailto:gordonv@model.com] 
Sent: Monday, March 10, 2008 9:07 AM
To: Korchemny, Dmitry
Cc: sv-bc@server.eda.org; sv-ec@server.eda.org; sv-ac@server.eda.org
Subject: Re: [sv-bc] RE: [sv-ac] RE: [sv-ec] Checkers & Formal



Korchemny, Dmitry wrote:
> Hi all,
> 
> I am attaching a presentation for tomorrow.
> 
> Thanks,
> Dmitry

I've taken a quick look at the slides.  You did deal with
at least one of the questions that I had outstanding -- what
is the meaning of forcing a checker variable?  You suggest
that it should be illegal.  Does that apply to all forms
of procedural continuous assignments to such a variable?

[Korchemny, Dmitry] Yes, I suggest explicitly making all assignments to
a checker variable illegal outside the checker body.
 
What about other assignments?  What would it mean, for
example, to have an NBA to or from a checker freevar?

[Korchemny, Dmitry] I suggest making any assignments. including NBA to
checker variables outside the checker body illegal.

What about use of a freevar on the RHS of a continuous
assignment?  For example:
    assign w = some_checker.some_freevar;
At what point does "some_freevar" change according to
the simulation cycle?  Is it even guaranteed to change?

[Korchemny, Dmitry] If to make such assignments illegal for checker
variables, a fortiori these assignments should be illegal for free
variables. From the scheduling point of view I don't see any difference
here between free and deterministic variables.

Particularly for an unassigned freevar, it seems that
there is no requirement for the freevar to ever change.
How much simulator implementation variability is valid?

[Korchemny, Dmitry] This is correct, but if the variable changes, there
will be an event. If my suggestion is accepted, this problem becomes
irrelevant.

From what I think I've heard, it seems unlikely to me that
inspecting or using a freevar value during simulation would
be terribly useful, particularly given the lack of
constraints on the implementation behavior in assigning to
the unassigned freevars.  Is that the case?

[Korchemny, Dmitry] I agree.

If so, should all non-checker use of a freevar just be made illegal?

[Korchemny, Dmitry] Yes, it makes sense.

It might be more useful in terms of cross-vendor consistency
to define how simulators MUST select the values of unassigned
freevars.  Even something trivial like assigning them all
the value zero or possibly having a separate RNG that is
used.  Vendors could also extend things in other ways,
but having reasonably predictable cross-vendor behavior
would seem to be an important goal.

[Korchemny, Dmitry] My concern here is potential backward
incompatibility. I don't see how to define RNG behavior in the current
time frame, though it is a natural thing to do in the future. Therefore
the only acceptable definition for cross-vendor consistency now is
assigning a default value to all free variables (e.g., o to bit
variables, and X to logic variables). If the RNG behavior is defined
later, the new behavior won't be backward compatible. What do you think?

Gord.
-- 
--------------------------------------------------------------------
Gordon Vreugdenhil                                503-685-0808
Model Technology (Mentor Graphics)                gordonv@model.com

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