Equivalence checking of datapaths based on canonical arithmetic expressions
Zheng Zhou, Wayne P. Burleson · 1995
Abstract| Numerous formal veri cation 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 con ned to the bit-level.F ormal veri cation of arithmetic expressions and synthesized datapaths, especially considering nite word-length computation, has not been addressed.Thus formal veri cation 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 dierently 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 de ned 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 eect of nite word-lengths and their associated arithmetic precision are also considered in the de nition of equivalence classes.As a particular application of ConTRAST, a formal veri cation system is designed to check equivalence under precision constraints.The results of initial DSP synthesis experiments are displayed, where two dierently implemented IIR lters in direct II and cascaded architectures are automatically compared under given precision constraints.