The
We list below some research projects that could build on the existing HOL semantics.
The HOL semantics is a manual transcription of the official semantics
into the HOL logic. Great care was taken to get all the details right, but
various transcription errors were revealed by the sanity checking proofs.
One cannot be sure that further errors are not lurking.
Ideally there should be a single "golden" semantics from which the
English text in the LRM and the HOL definitions are derived. The
standard way to do this would be to use XML technology (e.g. MathML), and we have had
some discussions with Sam
Owre of SRI International's PVS
group about this (Sam is developing XML schemas for SRI's logical
languages like SAL
and PVS and we discussed sharing infrastructure).
An alternative ad hoc approach would be to develop a set of latex
macros corresponding to the logical operations used in the semantics,
and then to derive the HOL from these using a script. This would have
little scientific interest, but might get the job done quickly, and could
subsequently be a foundation for an XML approach.
A way to do this using HOL would be to write metalanguage scripts
(i.e. ML programs) that deduce checking automata from properties. This
could be done by tuned rewriting, and would guarantee the validity of
the checkers. It would be an application of the
convergence of
deduction and computation. See
our paper in CHARME 2003 for an
ongoing preliminary attempt.
Besides implementing a monolithic property-to-checker tool one could
also try to produce a scripting workbench that verification engineers
could use to generate and tune checkers, and to split and combine
properties. The LCF methodology of HOL would ensure the scripting was
guaranteed sound.
It is unclear to what extent PSL/Sugar will displace these. One could
semantically embedded other property languages in HOL and
then develop and verify translators to PSL/Sugar. A specific project
would be investigating and validating translations between resets in
ForSpec and aborts in Sugar.
Furthur sanity checking
So far we have mainly applied mechanised reasoning to the core logic
to try to ensure the HOL representation is correct. Much of the power
of PSL/Sugar comes from the rich set of defined operators that it
supports. A relatively straightforward project would be to check that all the defined
operators actually have the semantics intended, and to verify that
expected dualities and other properties hold.
Machine readable golden semantics
The official semantics in the Language Reference
Manual (LRM) is given as typeset text (derived from latex). It is
quite clear and rigorous, but is essentially a natural language
specification, and so is not easily machine processable.
Synthesising checkers from PSL/Sugar
Manually writing testbench monitors to check that properties hold is
said to be tedious and error-prone, so there has been work on
automatically generating checkers from properties
[FoCs,
Feng & Hu].
Validating translations between PSL/Sugar and other languages
OpenVera
seems to be a rival organisation to Accellera supported by Synopsys and Intel
with its own property specification language derived from
ForSpec.
Another specification language is contained in the proprietary e language of
the Specman Elite testbench automation tool from
Verisity.
Compiling very high level properties into PSL/Sugar
PSL/Sugar provides a layer of derived constructs to help make the writing
of properties simple and natural. However, there is still a large gap
between the natural language descriptions of behaviour, e.g. in
protocol manuals, and PSL/Sugar syntax. There have been attempts to
translate natural language into temporal logic [Holt, R. Nelken and
N. Francez], but these have had to face daunting natural language
processing (NLP) issues. An approach that lies between temporal logic
and full NLP would be to create high level properties, maybe using
ideas from the
classification of patterns and expressed in a precisely defined controlled
subset of English with a compositional
semantics represented in HOL. One could then define and verify a
translation from high-level properties into PSL/Sugar.
Verification using theorem proving
Verification of PSL/Sugar properties is primarily intended to be by model
checking (for infinite paths) and simulation (for finite paths).
However, theorem proving can be applied to the HOL semantics and could
be used as another verification method. One way of doing this is to
use theorem proving to deductively decompose problems into smaller
chunks that could then be handed to automatic oracles (e.g. model
checkers). This is already done in systems like PVS or Cadence
SMV. More radical, however, would be to apply program
verification techniques to HDL by developing a programming logic based
on PSL/Sugar and, say, Verilog. One might, for example, investigate
deriving assume-guarantee rules and implementing proof tactics based
on them for modular reaoning.
The embedding of PSL/Sugar in HOL is over arbitrary non-empty sets of
atomic propositions and states. Thus atomic propositions can be
configured to include statements about numbers and other high level
datatypes, without any finiteness requirements. This would in general
not be suitable for model checking, but could be supported by theorem
proving.
Investigating relations between PSL/Sugar and ITL
PSL/Sugar has a separate class of regular expressions called SEREs (Sequential Extended Regular Expressions). Instead of
putting regular expressions into a separate class one can embed them in formulas. This involves
extending sugar with constructs similar to those found in
Interval Temporal Logic (ITL).
The resulting version of PSL/Sugar has some confusing properties. For example, Dana Fisman writes
(email 13 Feb, 2003):
a user might write (a & X (b & X c)) as the left argument of {f1}(f2)
(once {r}(f)) and think that it is equivalent to writing {a;b;c}
(while it is not)
However, in spite of user-unfriendly properties like this, further
explorations of ITL-like extensions might nevertheless be an interesting
route to new specificatios styles and logics.