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

Gord,

I agree with Fred Brooks that "Conceptual integrity is the most
important consideration in system design."  And I believe KISS is an
important design principle -- it's wise to be skeptical when confronted
by a proliferation of special cases and rococo embellishments.

However, I feel that for these checkers proposals, your extremely
productive focus on detecting and correcting defects in the proposals
may be setting off engineering warning bells in you that are not fully
warranted.  

Or you could be right.  KISS is partly a matter of taste, and one
person's elegance can be another person's Rube Goldberg machine.

So what alternative design would you propose?  I personally find
compelling the practical case for some checkers-like mechanism.  I don't
think we can keep the users waiting until a Copernicus comes along to
show a new, simpler way of looking at the issue.

If you could be our Copernicus right now, then all the more power to
you!  But, if the only alternative on offer is making users who need a
solution now wait years instead for another rev of the standard, then
I'm inclined to say, "Good enough is good enough." 

-- Brad


-----Original Message-----
From: owner-sv-ec@eda.org [mailto:owner-sv-ec@eda.org] On Behalf Of
Gordon Vreugdenhil
Sent: Thursday, March 06, 2008 2:41 AM
To: Korchemny, Dmitry
Cc: sv-bc@eda.org; sv-ec@eda.org; sv-ac@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?


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?

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.


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