DocumentCode :
1017052
Title :
Self-referential verification for gate-level implementations of arithmetic circuits
Author :
Chang, Ying-Tsai ; Cheng, Kwang-Ting
Author_Institution :
Novas Software, San Jose, CA, USA
Volume :
23
Issue :
7
fYear :
2004
fDate :
7/1/2004 12:00:00 AM
Firstpage :
1102
Lastpage :
1112
Abstract :
Verification of gate-level implementations of arithmetic circuits is challenging for a number of reasons: the existence of some hard-to-verify arithmetic operators, the use of different operand ordering, the incorporation of merged arithmetic with cross-operator implementations, and the employment of circuit transformations based on arithmetic relations. It is hence a peculiar problem that does not fit well within the existing register-transfer-level-to-gate equivalence-checking methodology. We propose a self-referential functional verification approach which uses the gate-level implementation of the arithmetic circuit under verification to verify itself. The verification task is decomposed into a sequence of equivalence-checking subproblems, each of which compares structurally similar circuit pairs derived from the implementation under verification. These equivalence-checking subproblems represent the functional equations that uniquely define the intended arithmetic function. Based on these self-referential functional equations, a decomposition heuristic using structural information is employed to guide the verification process for better efficiency. Experimental results on a number of implementations of the multipliers, the multiply-add units, and the inner product units with different architectures demonstrate the versatility of this approach.
Keywords :
circuit simulation; digital arithmetic; formal verification; logic CAD; logic gates; arithmetic circuits; arithmetic operators; circuit transformations; decomposition heuristic; equivalence-checking subproblems; formal verification; gate-level implementations; operand ordering; register-transfer-level-to-gate equivalence-checking; self-referential functional verification approach; self-referential verification; Arithmetic; Circuits; Employment; Equations; Formal verification; Hardware design languages; Job shop scheduling; Robustness; Timing; Very large scale integration; Arithmetic circuit; equivalence checking; formal verification;
fLanguage :
English
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
Publisher :
ieee
ISSN :
0278-0070
Type :
jour
DOI :
10.1109/TCAD.2004.829799
Filename :
1308403
Link To Document :
بازگشت