Subject: Re: VFV Committee Final Requirements
From: Anthony Mcisaac (Anthony.Mcisaac@st.com)
Date: Tue Nov 20 2001 - 11:53:06 PST
First, may I introduce myself to this mailing list. Anthony
McIsaac: I lead a team that has been applying model checking
in STMicroelectronics for seven years. We have used both an
in-house tool and IBM's RuleBase. Other groups in the company
use RuleBase and FormalCheck. We attach great importance to model
checking, and are keen to improve links between specialist
model checking and traditional simulation.
I have read the requirements with much interest, and would like to
offer a few comments from a user's point of view.
1. R55b and R56b: the language semantics .... must be intuitive.
In my view, the acceptance of this requirement means that
the logic should be linear rather than branching time (which
appears to be the general view of the committee). Very few
users in our company have an intuitive understanding of AF(AG(P)).
2. R71c and R71d: support for formulae that can specify any
omega-regular language.
The requirement does say "formulae", but can the committee
confirm that it really does want any omega-regular language
to be specified by a formula alone? Our view in ST is that we do
want this degree of expressiveness, but will be perfectly
satisfied if it is available through the use of formulae plus
the supporting modelling language. I wonder if concern about
the expressiveness of the set of formulae on its own is a
distraction from a practical viewpoint.
I see that support for strong fairness is not a requirement,
whereas omega-regular expressiveness is - which reinforces
my doubt whether the latter is really intended to be a requirement
on just the formulae.
3. R58a and R58b. Tool support for model checking.
The votes are clear: there must be a path to model checking, but
the language does not have to be supported by a commercial
model checker. This suggests that there's ground between these
two proposed requirements, that the committee might want to
explore.
Efficient model checkers are beasts to develop, and
painful experience is needed, as well as theoretical knowledge.
I hope that the requirement of a demonstrable path to a model
checker will be given a strong interpretation: I do not think
a demonstration of algorithms is sufficient, or even an
implementation of the algorithms, unless the language
and algorithms are very similar to those supported by tried
and tested model checkers (commercial or otherwise).
Efficiency in practical use is an important issue for us in ST.
General points that struck me - forgive me if they've
already been covered in your discussions.
A. The discussion in the mailing list archive has focussed on the
language for property formulae (this is indeed the brief of the
committee). However, property specification is often the most
straightforward part of our model checking work. We may have
a two-line property, and 20 pages of abstract modelling of
the environment, or of internal portions of the design. I am
a little surprised that more attention has not been given to
this aspect of the language.
B. Languages may have features that support management,
maintenance and reuse of properties and constraints. It isn't
clear to me whether the committee will be considering such
features as part of the language definition, or whether this will
be something provided in different ways by suppliers of tools
using the language.
C. It is apparent from the requirements that the committee
will produce a language for which it is admirably clear how
the properties are to be interpreted on an abstraction of the
HDL design (either a trace, or some finite state machine).
It wasn't clear to me whether the abstraction of the design
will be either
- defined once and for all for certain subsets of VHDL and Verilog;
- controlled to some extent by features of the language;
- left to some extent to the discretion of the tool supplier (with
possible choices for the user).
Two examples I'm thinking of are:
- abstractions of latch-based designs;
- interpretations of traces as starting from any state, reachable
or not (rather than from any initial state in the standard
interpretation). This will support tools that offer cheaper property
checks that don't do a reachability analysis, leaving it to the
user to determine whether any counterexamples indicate real
bugs.
I believe some of these points may be worth discussing as the
language definition reaches its later stages.
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 Nov 20 2001 - 11:54:11 PST