| Summary: | Numerous formal verification systems have been proposed and developed for FSM based control units (notably SMV (71) as well as others). However, most research on the equivalence checking of datapaths is still confined to the bit- or word-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 dissertation 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 three key techniques: attribute grammars, which contribute expressive data structures for syntactic and semantic information about designed datapaths, term rewrite systems, which transform functionally equivalent datapaths into the same canonical form, and LR parsing, which provides an efficient tool for integrating the attribute grammar and the term rewriting system. Unlike other canonical representations, such as BDD (15), and BMD$\sp*$ (17), ConTRAST makes canonicity by manipulating symbolic expressions instead of enumerating values of expressions at the bit- or word-level. 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 DSP design verification tool called Fixed-Point Verifier (FPV) has been developed. Similar to present DSP hardware design tools, FPV allows users to describe filters in the form of arithmetic expressions and to specify arbitrary fixed-point wordlengths on various signals. However, unlike simulation-based verification methods like Cadence/Alta's Fixed Point Optimizer and Mentor's DSPstation, FPV can automatically perform correctness-checking and equivalence-checking for a given filter design under the effect of finite word length.
|
|---|
