Formal Verification Based on Boolean Expression Diagrams

Poul F. Williams

August 2000

Abstract

Equivalence checking of combinational circuits is a formal verification problem which translates into tautology checking of Boolean formulae. Using BEDs we are able to preserve much of the structure of the circuits within the Boolean formulae. We show how to exploit the structural information in the verification process.

Sometimes combinational circuits are specified in a hierarchical or modular way. We present a method for verifying equivalence between two such circuits. The method builds on cut propagation. Assuming that the two circuits are given identical inputs, we propagate this knowledge through the circuits from the inputs to the outputs. The result is the knowledge of how the outputs of the two circuits correspond, e.g., are the outputs of the two circuits pairwise equivalent? The circuits and the movements of cuts can be described using Boolean formulae.

Symbolic model checking is a technique for verifying temporal specifications of finite state machines. It is well known how finite state machines and the evaluation of the temporal specifications can be expressed using Boolean formulae. We show how to do these manipulations using BEDs. We concentrate on examples which are hard for standard symbolic model checking methods.

Determining whether a formula is satisfiability is a problem which occurs in verification of combinational circuits and in symbolic model checking. Often satisfiability checking is associated with detecting errors. We examine how satisfiability checking can be done using the BED data structure.

Finally, we take a look at how it is possible to extend the BED data structure. Among other operations, we introduce an operator for computing minimal p-cuts in fault trees. A fault tree is a Boolean formula expressing whether a system fails based on the condition (``failure'' or ``working'') of each of the components. A minimal p-cut is a representation of the most likely reasons for system failure. This method can be used to calculate approximately the probability of system failure given the failure probabilities of each of the components.

As part of this research, we have developed a BED package. The appendices describe the package both from a user's and a programmer's point of view.

Ph.D. dissertation at Department of Information Technology, Technical University of Denmark, Lyngby, Denmark, August 2000. 2000 Poul Frederick Williams.

Available as PostScript(gzip'ed), BibTeX.