The high level of complexity of current hardware systems has led to an interest in formal methods for proving their correctness. This thesis presents a methodology for formal verification of inductively-defined hardware, based on automatic symbolic manipulation of classes of inductive Boolean functions (IBFs). It combines reasoning by induction and symbolic tautology-checking in a way that incorporates the advantages of both, where the key idea is that by building an inductive argument into the IBF representations, explicit proofs by induction can be avoided. The methodology consists of identifying classes of inductive Boolean functions that are useful for representation of hardware and specifications, associating a schema with each class (consisting of a canonical representation and symbolic manipulation algorithms), and appropriately manipulating these representations for performing formal verification.
The thesis research focusses on two classes of IBFs -- linearly inductive functions (LIFs) and exponentially inductive functions (EIFs), intended to capture a serial style of induction and a divide-and-conquer style of induction, respectively. Their canonical representations and symbolic manipulation algorithms are based on extensions of Bryant's Binary Decision Diagrams (BDDs), where the complexity is independent of the induction parameters. The thesis also explores additional representation machinery required to capture structurally-inductive hardware in terms of LIFs and EIFs, including support for handling compositions of inductive descriptions.
The LIF schema is particularly useful since it naturally captures the temporal induction inherent in sequential system descriptions. It provides canonical representations and symbolic manipulations for sequential functions in much the same way as BDDs provide for combinational functions. An interesting aspect of the LIF representation is that it corresponds to a minimal reverse deterministic finite state automaton (DFA), i.e. a minimal DFA that accepts input strings in reverse order. Its practical usefulness is demonstrated by showing that in comparison to classic (forward) DFAs, several datapath circuits have exponentially more compact reverse DFAs.
Symbolic IBF manipulations can be used to perform both functional
verification of size-parametric hardware (regular in structure), and
behavioral verification of sequential circuits (regular in time).
As an example of the former, a proof by induction for a specification
property corresponds to performing a tautology-check on the
specification IBF formula. For the latter, the LIF equivalence method
can be directly used to check input/output equivalence of two
differently-encoded finite state machines. Furthermore, the unified
framework for handling induction in the structural and the temporal
domains is useful for handling a combination of both, through techniques
such as symbolic simulation of space-parametric circuits, and language
containment for obtaining network invariants.
The thesis includes a practical implementation of the outlined
verification methodology, including a core package for symbolic LIF
manipulation.