Key words: Taylor Expension Diagrams, Equivalence verification, canonic representations
Abstract:
Recently a theory of a compact, canonical representation for arithmetic
expressions, called (TED)has been proposed.
This representation, based on a novel, non-binary decomposition principle,
raises a level of design abstraction from bits to bit vectors and words,
thus facilitating the verification of behavioral and RTL specifications
of arithmetic designs.
This paper presents the first practical results of using TED in the
context of high-level design representation and verification.
It discusses the use of TED for equivalence checking of behavioral and RTL
designs and comments on its limitations. It also demonstrates the application
of TEDs to verification of designs on algorithmic level
and comments on their potential use in high level synthesis.
Full Paper: Click Here
Authors: Priyank Kalla, Maciej Ciesielski, Emmanuel Boutillon, Eric Martin
Reference: "High-level Design Verification using Taylor Expansion Diagrams: First Results", Accepted to the Seventh Annual IEEE International Workshop on High Level Design Validation and Test, HLDVT'02, Cannes, Oct. 2002.