RE: [sv-ac] New 1900 proposal: Feedback

Hi Tom,

Please, see my answers below.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Thomas Thatcher
Sent: Friday, August 24, 2007 12:51 AM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] New 1900 proposal: Feedback

Hello Everyone,

I saw that there was a new proposal for Mantis 1900 uploaded on Aug 20.
I
have a couple of feedback items:

First, in the list of constructs that may appear in the checker, an
initial
block is included, but not a final block.  I believe this is an
oversight, and
shouldn't be too much trouble to include.  This allows checks to occur
at the
end of simulation.

[Korchemny, Dmitry] As far as I understood the discussion results in one
of the last SV-AC meetings, it was decided to limit the initial proposal
for checkers with concurrent assertions and free variable assignments
only. The reason for doing that was that introducing the checkers is a
major feature, and allowing the common SV code to appear in the checker
is unrealistic to be accepted in the window of the current PAR.
Therefore the proposal describes a limited version only, but this
proposal has been written with further enhancements in mind, so that it
can be enhanced to include other usable things: regular variables,
immediate assertions, etc.

Neither concurrent assertions nor free variable assignments are
permitted inside a final procedure (=block), that is why the final
blocks have not been included into this proposal.

It's not specifically mentioned, by immediate assertions may be included
too,
correct?  They will be very good for checks in the final block.

[Korchemny, Dmitry] See my previous comment.

On page 5:
> * If a free variable is declared with an initial value, this value is
only valid until its first clocked
> assignment is triggered. If it has both an initial value and a
continuous assignment, that is an SAR
> violation, and thus illegal. If it has an initial value and no clocked
or continuous assignment, then it
> has that initial value at the start of simulation, but is assigned a
nondeterminstic value at the first
> global clock edge.
  ^^^^^^
Should this be "inferred clock edge"?

[Korchemny, Dmitry] I think this should be a global clock: in this case
the transition relation includes the initialization only, all subsequent
values are undefined.

What happens if I don't have a global clock definition?

[Korchemny, Dmitry] This shall be illegal. One of the reasons of
introducing the global clock was support of free variables. Note
however, that such corner cases are typical for formal verification when
building an abstract model. If checkers are wanted for simulation, all
the free variables will typically be fully assigned; in the latter case
they do not rely on the global clock.

Next, I have a question.  Would there be a way to use the result of a
checker
to control another checker?

If I am writing a series of complicated checkers,
I might want to encapsulate common functionality in a checker, then
instantiate that checker in the top-level checker that I am writing.
The
results of the common checker would be used to enable or otherwise
control
assertions or other checkers instantiated within the top-level checker.

Currently, checkers as defined in this proposal have no outputs, so the
only
way I see to do this would be through cross-module references.

[Korchemny, Dmitry] I agree. The only way to use a value produced by a
checker described in the current proposal is through XMR. To allow
output checker arguments requires some more thought and discussion, and
we will try to find an appropriate way to do this. Then we'll update our
proposal accordingly.

Thanks,

Tom
-- 
------------------
Thomas J. Thatcher
Sun Microsystems
408-616-5589
------------------


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.