A Unified Framework for Equivalence Verification of Datapath Oriented Applications

Bijan ALIZADEH  Masahiro FUJITA 

Publication
IEICE TRANSACTIONS on Information and Systems  Vol.E92-D  No.5  pp.985-994
Publication Date: 2009/05/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Hardware Verification
Keyword: 
equivalence verification,  canonical form,  RTL model,  gate-level implementation,  decision diagram, 

Full Text: PDF(1MB)

Summary: 
In this paper, we introduce a unified framework based on a canonical decision diagram called Horner Expansion Diagram (HED) [1] for the purpose of equivalence checking of datapath oriented hardware designs in various design stages from an algorithmic description to the gate-level implementation. The HED is not only able to represent and manipulate algorithmic specifications in terms of polynomial expressions with modulo equivalence but also express bit level adder (BLA) description of gate-level implementations. Our HED can support modular arithmetic operations over integer rings of the form Z2n. The proposed techniques have successfully been applied to equivalence checking on industrial benchmarks. The experimental results on different applications have shown the significant advantages over existing bit-level and also word-level equivalence checking techniques.