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

Hi Brad,

My goodness! In 5 paragraphs you manage to quote "The Mythical 
Man-Month", support reductionist KISS philosophy, draw analogies to 
baroque architecture, mention an amusing series of cartoons, and 
celebrate an early Renaissance polymath. Impressive.

I guess all that eloquence was intended to downplay Gord's concerns 
about resolving conceptual and systemic issues with narrow 
clarifications. You must either disagree with Gord as to the presence of 
conceptual and systemic issues or you mustn't really agree with Fred 
Brooks (since the sentence immediately following the one you quote is 
wonderfully appropriate here: /"It is better to have a system omit 
certain anomalous features and improvements, but to reflect one set of 
design ideas, than to have one that contains many good but independent 
and uncoordinated ideas."/)

My perception is that Gord has been working with the SV-AC team to 
integrate their work and ideas with the rest of the language and your 
mention of Fred Brooks' essay brings the need for better integrity into 
sharp focus. Thank you for that.

I find your final sentiments a bit on the offensive side, though. It 
seems to be a "put up or shut up" kind of message delivered to someone 
who has given so much to this community already.

And whether we achieve "good enough" status on the checkers proposal is 
a matter of opinion, deliberation, and vote. Most of us would be 
delighted to have something as modular and powerful as the checkers 
proposal be part of the language's verification capabilities. If the 
final proposal winds up being conceptually integrated with the rest of 
the language, it should be a no-brainer. If it isn't perceived to be so, 
I reckon it will come down to folks grappling with the trade-off between 
this feature's obvious benefits and the very real need for some sense of 
conceptual integrity (ie, when is good enough /not /good enough?).

-randy.

Brad Pierce wrote:
> 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.