Equivalence Checking of Datapaths Based on Canonical Arithmetic Expressions

Numerous formal verification systems have been proposed and developed for Finite Sate Machine based control units (notably SMV[19] as well as others). However, most research on the equivalence checking of datapaths is still confined to the bit-level. Formal verification of arithmetic expressions and synthesized datapaths, especially considering finite word-length computation, has not been addressed. Thus formal verification techniques have been prohibited from more extensive applications in numerical and Digital Signal Processing. In this paper a formal system, called Conditional Term Rewriting on Attribute Syntax Trees (ConTRAST) is developed and demonstrated for verifying the equivalence between two differently synthesized datapaths. This result arises from a sophisticated integration of attribute grammars, which provide expressive data structures for syntactic and semantic information about designed datapaths, and term rewriting systems, which transform functionally equivalent datapaths into the same canonical form. The equivalence relation is defined as a congruence closure in the rewriting system, which can be generated from arbitrary axioms, such as associativity, commutativity, etc. in a certain algebraic system. Furthermore, the effect of finite word-lengths and their associated arithmetic precision are also considered in the definition of equivalence classes. As a particular application of ConTRAST, a formal verification system is designed to check equivalence under precision constraints. The results of initial DSP synthesis experiments are displayed, where two differently implemented IIR filters in direct II and cascaded architectures are automatically compared under given precision constraints.