Symbolic verification of deterministic machines

Howard Barringer

(University of Manchester)

One approach commonly used for establishing the behavioural equivalence of hardware systems uses state-space exploration to establish a bisimulation relation between the systems, modelled as labelled transition systems. It has the distinct advantage of being automatic, and can produce counter-example information when a verification fails, although this is usually in low level terms of traces leading to divergence. However, it suffers from the problem of combinatorial explosion, even though its domain of applicability can be significantly extended with the introduction of special encodings, such as binary decision diagrams (BDDs).

A second method represents system behaviour using logical expressions, and then establishes equivalence by employing theorem-proving techniques. It operates abstractly at a high level, thus not suffering from combinatorial explosion. Further, when two systems are shown to be different, it is possible to give structured debugging feedback information at the level of the initial system representation. Although varying degrees of automation are possible, the approach currently requires significant user input in order to be able to establish design equivalence.

In this talk, we introduce a novel verification approach which effectively merges the above techniques. We take Park and Milner's standard (strong) bisimulation equivalence as our notion of equivalence between labelled transition systems. However, we present the transition systems abstractly as deterministic machines and then define a state bisimulation relation between the state spaces of the two machines. This is provably equivalent to a strong bisimulation between the derived transition systems for the deterministic machines. The advantage of this is that each system is expressed by a pair of (response and evolution) functions, together with an initial state, and the state bisimulation can then be established semi-automatically through a state evolution rule. The analysis proceeds in a truly symbolic manner, at the level at which the design is expressed.
Tuesday 6th December 1994, 14:30
Seminar Room 322
Department of Computer Science