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

Hi Gord,

Please, see my comments below.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Gordon Vreugdenhil
Sent: Thursday, March 06, 2008 12:41 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:
> Hi Gord,
[...]
> Could you clarify the following sentence: "Some of the special
routines
> (for example those related to enables) for checkers really need to be
> explained in terms of how they relate to the outer language
> constructs."?

Consider the use of $inferred_enable.  What does it produce in a
type sense?  Can I use it with an untyped formal?  With such a
formal, can I do coverage on it?  What if the inferred enable is
a condition that relates to a loop variable?  Are all combinations
checked in that context as well?  What if the enable is automatic?
Is that legal?  Clearly (from 16.18.4) you expect $inferred_enable
to be able to produce a sequence and be able to use a non-sequence
expression in that inferred role.  Is there anything else that
the $inferred_enable can produce?  After looking at LRM 16.14.5,
Mantis 1674 and 1648, it still isn't clear to me what the
combination of rules implies.  16.14.5 says that for a concurrent
assertion, an inferred enable can't occur in a loop.  Does
that apply to a checker as well?  What if the inferred_enable
isn't actually used in an assertion in the checker?  Would that
be legal?

DK: $inferred_enable is not actually part of the checker proposal, but
is a subject of Mantis 1674 as you mentioned above. $inferred_enable
returns the enabling condition which would have been inferred by the
compiler if a concurrent assertion had been placed at the instantiation
point as explained in 16.14.5.

Consider the following example:

always @(posedge clk) begin
	if (cond1) begin
		if (cond2) begin
			// Checker is instantiated here
			...
		end
	end
end

In this case $inferred_enable is (cond1 && cond2), and its type is the
type of this expression. $inferred_enable is always integral and not a
sequence, and its exact type is unambiguously inferred. $inferred_enable
is legal only as a default value of a formal argument of a sequence,
property or checker. This should answer your other questions:

* You can use it with an untyped argument since its exact type is known
at the compile time.
* If you can do coverage on a sampled value, you can do it in this case
also. I don't see a reason why coverage on a sampled value should be
forbidden.
* As defined in 2110, a loop index should be treated as a constant and
it is allowed in assertions only, so you cannot collect coverage on it
in checkers.
* It should be illegal to place a checker in a conditional context
dependent on an automatic variable, as it is illegal to place an
assertion there. If it is not stated explicitly enough in 16.14.5, it
should be clarified there, and it is not related directly to the checker
proposal.

---

16.14.5 says that for a concurrent assertion, an inferred enable can't
occur in a loop.  Does that apply to a checker as well?  What if the
inferred_enable isn't actually used in an assertion in the checker?
Would that be legal?

DK: This is fixed in 1995.

---

I would like to move beyond a narrow discussion of specific rules
at some point -- no one has addressed my larger concerns about
consistency and regularity of the various constructs.  One
can make the overall LRM as convoluted as necessary to deal
with all the cases that one can imagine, but then one has to
re-examine all of those special cases and rules with any future
change.  I don't think that is a good direction and have said
as much for quite a while now with no response from anyone in
AC -- the only focus has been on adding new rules and covering
specific cases that I am raising.  My basic concern is that
it just shouldn't be this much work -- is it not possible to
devise a simpler set of more consistent abstractions for interaction
between the assertions constructs and the rest of the language?

DK: My assumption is that SV is a language of (besides of its other well
known functions) assertion specification and validation. If this
assumption is incorrect, then the LRM Clause 16 and the SV-AC existence
is redundant. If my assumption is true then the language should provide
adequate support for assertions. I agree, assertions are different from
other language features, e.g., the assertions are declarative, while
most of SV has an imperative nature. RTL assertions require sampling and
static data, there is nothing to do here. If you ask whether one can
envisage assertions that capture any legal SV behavior, including
asynchronous transitions, then the answer is that such assertions are
possible in principle, but they will verify SV simulation program, and
will have nothing to do with the RTL validation (let alone the questions
of complexity and decidability).

The direction of the language development seems quite natural and
logical to me, and I don't consider it as making patches in order to
satisfy immediate user needs. I don't think that the checkers are less
consistent with the rest of the language than its other parts:
functional coverage, random constraints, clocking blocks and classes.
 
Gord.
-- 
--------------------------------------------------------------------
Gordon Vreugdenhil                                503-685-0808
Model Technology (Mentor Graphics)                gordonv@model.com


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