Subject: expressiveness and reuse
From: Anthony Mcisaac (Anthony.Mcisaac@st.com)
Date: Tue Jan 15 2002 - 07:44:36 PST
I don't know whether the points below are the only ones,
or even the most important; but I thought I'd make some comments
before the deadline.
First, on thinking about requests to make to Motorola and IBM,
it seemed that most things would be pretty easy for the languages
to accommodate, without changes to their essential nature and
features. It would seem to be a waste of time for both candidates
to propose detailed minor changes at this stage. The selection
can be made on the basis of new proposals incorporating any
major changes required; then the chosen language can be
subjected to very detailed scrutiny.
The major question for me is how CBV will be modified to meet the
requirements of more expressiveness. I understand that it's felt
that this would compromise some of the advantages of CBV. I
don't know if it would be possible to add some, if not full, expressiveness
to CBV without losing these advantages, and if so, whether the
committee would accept a final choice between Sugar and a
CBV which did not fully meet the requirements, but claimed to
have other advantages.
I would certainly like more expressiveness for constraints in formal
verification with CBV.
As far as I can see, users can't introduce free variables in CBV (am
I right here? I imagine that when a variable is declared, it takes a
default rather than an arbitrary value.) I'd like to be able to specify,
or partially specify, quite complex packet structures as inputs to
a design. For example, I might want to introduce a free variable,
say message_length, and to specify the individual inputs in a complicated
way in terms of that. Can this be done at present? If not, it's a request.
Ideally, I'd also like to be able to express any relationship between the
inputs as a constraint, i.e. to assume any property.
I also have some comments concerning reuse. It is important to be able
to switch between simulation and model checking; and CBV is very
interesting in this respect. But this is not the whole story: one may want
to reuse specifications with very different tools, using different methods
of compilation and internal representation, and of linking with the design.
Different groups may reuse the same specification for very different
purposes, and the key elements must be clearly identifiable and
accessible.
An example: a formal spec has been written for a design D, with some
properties and some constraints. The simulation of D is now controlled
by a testbench automation tool, which controls the inputs at the interface
I, and is linked with a cycle-accurate C model of part of the environment,
which has an interface J with D. The testbench automation tool supports
the property language. We want it to check that the constraints at J are
satisfied; and if these constraints use free variables, it must find whether
there are values of the free variables such that the constraints are
satisfied. We also want the tool to generate inputs at the interface I that
are consistent with the constraints; if there are free variables, it
generates random values for them.
This is just to illustrate that we may want to use different properties
and variables in different ways; and we perhaps won't know in the
first place how other people may want to use them. We therefore want clear
access to properties and some of the variables in the specification. This
isn't access through directives in the language, but access through names
that can be used by other tools.
So my request is for IBM and Motorola to indicate how they will (or do) fulfil
requirement R45(a): the language must support the definition of
named assertions.
I suggest that there should be names of instances of properties, and that
the names should be useful from outside the language, not (or not
just) accessed within it - which means that it should be clear to a reader
just what the property attached to the name is saying.
Anthony
-- 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 : Tue Jan 15 2002 - 08:39:53 PST