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

From: Korchemny, Dmitry <dmitry.korchemny_at_.....>
Date: Thu Mar 20 2008 - 08:31:57 PDT
I agree, if you believe it is feasible to insert this change at the
current time frame.

Thanks,
Dmitry

-----Original Message-----
From: Gordon Vreugdenhil [mailto:gordonv@model.com] 
Sent: Thursday, March 20, 2008 4:27 PM
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:
[...]
> 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?

Hmm.  X doesn't seem to be a good idea to me; that will essentially
make it impossible to satisfy most semi-interesting dependent
freevar assignment assumptions since computations involving X generally
result in X.  In other words, won't X results in most cases just end up
causing most assertions to fail?  That would seem to be an unfortunate
result
of standardizing on that approach.

I don't think that the RNG approach is really that hard, is it?
Why not just say that there is one system-wide RNG that is used for
all freevar assignments and that such an RNG is assigned as though
it were in a separate top-level module.  That should, I think,
preserve random stability even when the number of checkers
changes within the design.  In addition, since RNG results don't
produce X or Z values, I think that the likelihood of having
reasonable results is much higher.

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.
Received on Thu Mar 20 09:01:14 2008

This archive was generated by hypermail 2.1.8 : Thu Mar 20 2008 - 09:01:48 PDT