Formal Verification of Arithmetic Circuits by Function Extraction

被引：29

作者：

Yu C. ^{[1
]}

Brown W. ^{[1
]}

Liu D. ^{[2
]}

Rossi A. ^{[3
]}

Ciesielski M. ^{[1
]}

机构：

[1] Department of Electrical and Computer Engineering, University of Massachusetts, Amherst, 01003, MA

[2] Intel Corporation, Hudson, 01749, MA

[3] LERIA Lab, Computer Sciences Department, University of Angers, Angers

来源：

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems | 2016年 / 35卷 / 12期

基金：

美国国家科学基金会;

关键词：

Arithmetic circuits; computer algebraic; formal verification; functional verification;

D O I：

10.1109/TCAD.2016.2547898

中图分类号：

学科分类号：

摘要：

This paper presents an algebraic approach to functional verification of gate-level, integer arithmetic circuits. It is based on extracting a unique bit-level polynomial function computed by the circuit directly from its gate-level implementation. The method can be used to verify the arithmetic function computed by the circuit against its known specification, or to extract an arithmetic function implemented by the circuit. Experiments were performed on arithmetic circuits synthesized and mapped onto standard cells using ABC system. The results demonstrate scalability of the method to large arithmetic circuits, such as multipliers, multiply-accumulate, and other elements of arithmetic datapaths with up to 512-bit operands and over 2 million gates. The results show that our approach wins over the state-of-the-art SAT/satisfiability modulo theory solvers by several orders of magnitude of CPU time. The procedure has linear runtime and memory complexity, measured by the number of logic gates. © 2016 IEEE.

引用

页码：2131 / 2142

页数：11

共 50 条

[1]

Bryant R.E., Graph-based algorithms for Boolean function manipulation, IEEE Trans. Comput., C-35, 8, pp. 677-691, (1986)

[2]

Bryant R.E., Chen Y.-A., Verification of arithmetic functions with binary moment diagrams, Proc. Design Autom. Conf., pp. 535-541, (1995)

[3]

Chen Y.-A., Bryant R.E., PHDD: An efficient graph representation for floating point circuit verification, School Comput. Sci., (1997)

[4]

Ciesielski M., Kalla P., Askar S., Taylor expansion diagrams: A canonical representation for verification of data flow designs, IEEE Trans. Comput., 55, 9, pp. 1188-1201, (2006)

[5]

Farahmandi F., Alizadeh B., Navabi Z., Effective combination of algebraic techniques and decision diagrams to formally verify large arithmetic circuits, Proc. IEEE Comput. Soc. Annu. Symp. VLSI (ISVLSI), pp. 338-343, (2014)

[6]

Kaivola R., Et al., Replacing testing with formal verification in Intel CoreTM i7 processor execution engine validation, Computer Aided Verification (CAV), pp. 414-429, (2009)

[7]

Mishchenko A., Et al., ABC: A System for Sequential Synthesis and Verification, (2007)

[8]

Sorensson N., Een N., Minisat v1. 13-A SAT solver with conflictclause minimization, SAT, 2005, (2005)

[9]

Soos M., Enhanced Gaussian elimination in DPLL-based SAT solvers, Proc. Pragmatics SAT, pp. 2-14, (2010)

[10]

Fallah F., Devadas S., Keutzer K., Functional vector generation for HDL models using linear programming and 3-satisfiability, Proc. Design Autom. Conf. (DAC), pp. 528-533, (1998)

← 1 2 3 4 5 →