Some research projects on PSL/Sugar and HOL

Over the last year or so, a detailed machine readable semantics of PSL/Sugar has been developed in the version of higher order logic supported by the HOL system. Several sanity checking properties have been proved, including the equivalence of the clocked semantics with the composition of clock elimination rewrites followed by the unclocked semantics.

The semantics in higher order logic is believed to be an accurate formalisation of the semi-formal semantics in Appendix B of the Language Reference Manual. The semantics of PSL/Sugar is expected to change (e.g. modifications to the treatment of clocking and the semantics of aborts), but we expect to keep our machine readable semantics synchronised with the latest Accellera semantics.

We list below some research projects that could build on the existing HOL semantics.

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.

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.

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].

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.

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.

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.

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.