A Specification Language for GSTE

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.


Project Background

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.

Research Problem and Approach

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:

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.

References

  1. 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.
  2. 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.

Tom Melham, last updated in September 2005.