This research is looking at developing a high-level specification notation for formal hardware verification and a compiler from this notation to Assertion Graphs for model checking by Generalized Symbolic Trajectory Evaluation. The work is funded by a donation from Intel Corporation and is the topic of a DPhil project conducted by Ed Smith at the Oxford University Computing Laboratory.

*Tom
Melham, October 2004*.

Symbolic trajectory evaluation (STE) is a highly efficient model checking algorithm for verifying properties of large datapath designs. Although basic STE is a well-established and successful industrial formal verification tool, its scope of application is rather limited. STE can verify only properties written in a very simple form of temporal logic, and many complex circuit behaviours that one would like to check cannot be stated directly.

Research at Intel's Strategic CAD Labs has produced a highly significant new form of symbolic trajectory evaluation, called Generalized STE [1, 2]. The language of Generalized STE (GSTE) is vastly more expressive than STE's and can cover much more complex circuit behaviours. Effective model checking algorithms for GSTE have also been devised that inherit the efficiency of the abstraction ideas pioneered in STE. But perhaps the most significant property of GSTE is that it provides a flexible and principled framework in which a skilled engineer can seek the most effective balance between abstraction and precision in model-checking [1].

GSTE supports this flexibility through a two-dimensional
specification language, called *assertion graphs*. An assertion
graph is a directed graph whose edges are labelled with boolean
formulas that express desired circuit behaviour. The structure of the
graph gives a kind of trace or abstract map of the sequences of states
through which the circuit under analysis is expected to pass. The
boolean formulas on the edges describe a pattern of cause-and-effect
properties that are expected to hold across these sequences. By
elaborating a graph or adjusting its labels, the verification engineer
is able to seek a balance of tradeoffs between precision of results
and verification efficiency. In this way, the assertion graph notation
provides for very fine control over model-checking execution.

GSTE supports this flexibility through a two-dimensional
specification language, called *assertion graphs*. An assertion
graph is a directed graph whose edges are labelled with boolean
formulas that express desired circuit behaviour. The structure of the
graph gives a kind of trace or abstract map of the sequences of states
through which the circuit under analysis is expected to pass. The
boolean formulas on the edges describe a pattern of cause-and-effect
properties that are expected to hold across these sequences. By
elaborating a graph or adjusting its labels, the verification engineer
is able to seek a balance of tradeoffs between precision of results
and verification efficiency. In this way, the assertion graph notation
provides for very fine control over model-checking execution.

Although experience shows that verifiers are able to work directly with at least modestly-sized assertion graphs, in the longer term there are two problems with this. First, the assertion graph notation can easily get unwieldy for complex behaviours. One might try to solve this by employing suitable abbreviations (e.g. macros) to generate larger graphs. But this is awkward because the assertion graphs are essentially a 2-dimensional notation; writing scripts to generate them introduces a rather substantial and unnatural layer of indirection.

The second, more serious, problem is that it is difficult to devise a smooth system of reasoning rules for combining assertion graphs at higher levels of verification. Experience from STE shows that it is highly desirable to have such rules, so that large systems can be analysed by decomposition. But GSTE reasoning directly at the graph level is likely to be very messy, given the very minimal constraints that GSTE places on the structure of assertion graphs. For reasoning, we need an (abstract) syntax that is more structured and controlled.

This research will seek to address these issues by treating assertion graphs as an intermediate language for a higher-level specification notation, rather than as a user-level notation. With this approach, user specifications would be written in an imperative-style language that expresses control flow, augmented with logical annotations for expected state/signal behaviour. The user would write an imperative structure (program) that describes the execution sequences along which the specified computation must pass. This program would also be annotated with boolean formulas (invariants) that express expected cause-effect relationships among state and signal variables. The program would then be compiled into an assertion graph for checking with GSTE.

The expected advantages of this approach are that it should give a more scalable user notation and that reasoning rules could be expressed as a variety of Hoare logic for the higher level language. The research challenges include these key issues:

- How can we design our language so that we don't lose one of the most significant benefits of GSTE, namely fine-grained and intuitive control over abstraction/efficiency/precision tradeoffs?
- The target for our language is almost certainly going to be a subset of the whole space of assertion graphs. Can we identify a sufficiently useful class of graphs into which we can compile?

Another idea, of course, would be to investigate ways in which existing formal verification languages (for example PSL or ForSpec) might be compiled into assertion graphs. This is also interesting, but has the different aim of providing better model-checking support for an existing language. The proposed research, on the other hand, seeks to shape the user-level language to fit the expressive power of GSTE.

- J. Yang and C.-J. H. Seger,
‘Generalized Symbolic Trajectory Evaluation: Abstraction in
Action’, in
*Formal Methods in Computer-Aided Design: 4th International Conference: Proceedings*, edited by M. D. Aagaard and J. W. O'Leary, Lecture Notes in Computer Science, vol. 2517 (Springer-Verlag, 2002), pp. 70-87. - J. Yang and C.-J. H. Seger,
‘Introduction to Generalized Symbolic Trajectory
Evaluation’, in
*Proceedings of 2001 IEEE International Conference on Computer Design*(IEEE, 2001), pp. 360-365.