Subject: Re: An objection to the assume_guarantee keyword
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Mon Feb 11 2002 - 02:46:41 PST
Danny and all,
I chime in with all those saying that proof strategy should not be part of the
language; it should be handled by the tools and their controllers. If my
answer to
Cindy's request for clarification about what "can be used from outside the
language" means was not clear enough, the discussion of the last few days
is a good illustration.
Concerning Danny's points below: I don't think Erich was suggesting that the
tools should always be expected automatically to determine which properties
are
assertions and which are assumptions. This could be indicated in a control
script, not part of the standard language, but easily adaptable for use with
different tools.
However ....
The distinction between assertions and assumptions is part of the
specification of
the design, not of a proof strategy. I am in favour of allowing the
distinction to be
made in the language, for two reasons:
1. It encourages clear thinking about which properties a design has a
responsibility
for guaranteeing, and which properties it can rely on in discharging its
responsibilities.
Too often, everyone knows what shouldn't happen, but the designers on
different
sides of an interface don't know exactly what they are supposed to do to stop
it
happening.
2. A property specification may contain a hundred or more assumptions about
the environment or internal parts of the design. We don't want to have to
refer to
them all in a separate control script.
Anthony
GEIST@il.ibm.com wrote:
> Hi All,
> Two comments on this weekends discussion:
> 1. I agree with Eric. The usage of properties should not be part of the
> property language per say. It will be also useful to make it easy for the
> tools to identify the proof scripts in order to manipulate them in a
> nontrivial manner. This means that I would prefer that keywords like assume
> and assert would appear only in constructs that are dedicated for proofs.
> On the other hand there may be times when the users would like to use them
> on-the-fly in their verilog code. I don't have a have a good understanding
> yet of what would be the best compromise between flexibility to the users
> on the one hand and the need to provide useful tools for a wide class of
> users. Real experts would want total flexibility while less sophisticated
> users would want powerful tools that would chew a lot of the work for them.
>
> 2. Its not clear that a tool will always be able to deduce what part of the
> verification problem is the environment and what is the design (thus deduce
> if to use a property as an assume or assert). For example SMV accepts a
> monolithic smv file.
>
> Regards,
> Danny
>
> Daniel Geist
> IBM Haifa Research Lab. Phone:
> 972-4-8296286
> Haifa University, Mount Carmel Fax:
> 972-4-8296112
> Haifa, ISRAEL
> e-mail: geist@il.ibm.com
-- Anthony McIsaacSTMicroelectronics Limited 1000 Aztec West Almondsbury Bristol BS32 4SQ
Tel: ++44 (0)1454 462466 Fax: ++44 (0)1454 617910
Email: Anthony.McIsaac@st.com
This archive was generated by hypermail 2b28 : Mon Feb 11 2002 - 02:49:55 PST