RTL到门级设计的等价性验证的研究
|
摘要
超大规模集成电路的验证工作在产品设计周期中所占的比例已达到三分之二。等价性验证作为现代SoC设计流程的一个重要步骤,用于验证不同抽象层设计之间的功能等效性。包含算术电路的设计的验证工作则是等价性验证的热点和难点之一。为了解决这个问题,本文作者结合自主研发等价性验证系统(ZDFV)的工作,在高效综合引擎的研究与实现、单个模块的相似性研究、数据通路的验证方法、结合半加图的算术单元验证以及基于混合SAT引擎的RTL验证流程等五个方面开展了研究:
1.高效综合引擎的研究与实现:等价性验证的效率取决于两个设计的相似性,综合引擎的好坏决定了相似性。本文在充分研究Icarus Verilog可综合子集及相关综合算法的基础上,以ZDFV的综合引擎为代表,分析了高级程序语句的综合方法,提出了一种高效的综合流程,实现了模块的重用,并支持多种宏定义和编译向导。通过对Icarus Verilog和ZDFV的综合引擎的对比分析,并以IWLS_2005_bechmarks_V_1.0为测试基础,实验结果显示:在相同的测试平台下,ZDFV的综合引擎在处理多文件描述的Verilog设计时具有更好的兼容性,而对于不带层次结构描述的Verilog设计时间上的改善度可高达98%。
2.单个模块的相似性研究:模块相似性在等价性验证中具有重要的指引作用,对验证引擎的性能有着关键性的影响。本文提出了一种新的从RTL到门级网表的等价性验证流程:提取电路信息、综合待验证的设计、匹配待验证设计的等价点、比较待验证设计的等价点。不同于传统验证流程,为获得最好的电路相似性,此流程深入研究了综合优化等因素在不同层次上对电路相似性的破坏,提出了在综合阶段对比IP的不同实现方案,并进行启发式决策。以验证不同实现方案的乘法电路为例,本算法的验证准确性更高,而验证时间可减少3%～28%。
3.数据通路的验证:数据通路由一系列的算术表达式在行为域里表示,可按具体的变换规则进行优化组合。依照不同描述级,本文讨论了验证不同数据通路表示的各种算法,通过在寄存器传输级上比较重写数据通路以证明其等价性,提出了在数据通路级指导综合过程,有效简化了网表级等价性验证的复杂度。比如针对加法和乘法连续运算的表达式,算法从实现电路中提取变量顺序和结合顺序并加以利用,实验表明,在验证乘法连续运算的表达式时减少了83%～99%的时间,加法连续运算表达式的验证时间也可减少40%～89%。
4.结合半加图的算术单元验证:论文研究了基于BMD验证乘法电路的方法,该方法使用矩分解(moment decomposition)方式,在BMD的边和节点上赋予权重信息,减少了图的节点数。讨论了一种新的电路表示方法——半加图(Half Adder Graph),提出在综合阶段使用半加图表示算术电路,从中得到算术电路的实现方案,进一步指导算术电路的综合。统计提取电路实现和验证的时间花销,以乘法电路为例,本算法能明显提高验证引擎的性能(4%～63%)。
5.基于混合SAT引擎的RTL验证流程:传统验证流程需要将电路综合为门级网表,但门级验证引擎不能有效利用一些原始的电路的信息。本文提出了一种新的基于混合SAT引擎的验证流程,讨论了混合SAT引擎的约束传递过程。以不同规模的加法单个运算和连续运算表达式为例,比较传统验证流程验证时间最多可减少99%。实验结果表明基于混合SAT引擎的RTL验证流程比传统的验证流程有明显的优势。
VLSI verification takes about two thirds of the whole design time. In modern design flow of SoC, to guarantee the functional consistency of different abstract layers, a formal verification technique called Equivalence Checking (EC) is widely used. One challenging problem in EC is the verification of arithmetic designs. In the past few years, the author took part in the research and development of ZDFV Equivalence Checking System. Based on ZDFV work, the thesis focuses on the following key problems: how to construct an efficient synthesis engine; how to improve the structural similarity of the two designs; how to verify data path designs efficiently; how to use half adder graph to perform arithmetic unit verification; and how to use the hybrid SAT engine in the existing verification flow. The thesis includes the following original ideas and contributions.
1. Research on developing high efficient synthesis engine. Synthesis engine transforms a RTL design into a gate level netlist. The quality of the result gate netlist has a significant effect on the entire verification performance. With studying and analyzing of Icarus Verilog synthesis engine and other synthesis systems/ algorithms, an effective synthesis flow was proposed and implemented in ZDFV. The synthesis engines supports module reuse, macro definition and synthesis directives. Experiments on widely used IWLS_2005_bechmarks_V_l .0 benchmark designs show that, compared with Icarus system, our synthesis method reduces the total synthesis and flattening time by 98%.
2. Study on improving the module level similarity. The state-of-the-art equivalence checking algorithms fully exploit the similarity of the two designs. Better similarity means better performance. A new flow for RTL to gate level netlist equivalence checking was proposed. Our new flow first extracts design information, then synthesize the design, find internal potential equivalent point pairs and verify these potential equivalent point pairs. Unlike traditional flows, the new flow analyzes how different level of synthesis optimizations may affect the design similarity. The synthesis decision making takes different IP implementations into consideration and use heuristics to get better similarity. Experiments conducted on multipliers with different implementations show this leads to 3% to 28% running time reduction of the verification engine.
3. Equivalence checking of datapath: Datapath consists of series arithmetic operations, which can be optimized according to some transformation rules. Verification of different level representations of datapath was discussed. A RTL datapath rewriting technique was developed to achieve better design similarity. For adder and multiplier tree expressions, the proposed technique also considers the variable ordering and variable combinations. Experiments on multiplier tree and adder tree expressions exhibit running time reduction of 83% to 99%, and 40% to 80% respectively.
4. Arithmetic unit check with half adder graph technique: Binary Moment Diagram (BMD) technique has been used in multiplier equivalence checking. Unlike BDD, BMD adds weight (moment) on edges and thus reduces the node quantity of the diagram. A new circuit abstraction method, half adder graph was proposed to represent arithmetic circuits during the synthesis period. The new synthesis engine first analyzes the implementation of the arithmetic unit to gets its architectural information. Then use the information to guide the synthesis of the corresponding RTL design. Applying this approach on multiplier circuits, the performance of verification engine has been improved by 4%～63%.
5. A new equivalence checking flow based on hybrid SAT engine: In traditional equivalence checking flow, since the verification engines are gate-based, the RTL designs have to been synthesized to gate level netlists first. In this RTL to gate translation process, some structural information of the designs is lost. In this research, a hybrid SAT engine based verification flow was proposed. The constraint propagation process in the hybrid SAT engine was discussed. Compared with traditional flow, up to 99% verification time reduction was achieved when verifying single adder unit and adder tree expressions.
1.高效综合引擎的研究与实现:等价性验证的效率取决于两个设计的相似性,综合引擎的好坏决定了相似性。本文在充分研究Icarus Verilog可综合子集及相关综合算法的基础上,以ZDFV的综合引擎为代表,分析了高级程序语句的综合方法,提出了一种高效的综合流程,实现了模块的重用,并支持多种宏定义和编译向导。通过对Icarus Verilog和ZDFV的综合引擎的对比分析,并以IWLS_2005_bechmarks_V_1.0为测试基础,实验结果显示:在相同的测试平台下,ZDFV的综合引擎在处理多文件描述的Verilog设计时具有更好的兼容性,而对于不带层次结构描述的Verilog设计时间上的改善度可高达98%。
2.单个模块的相似性研究:模块相似性在等价性验证中具有重要的指引作用,对验证引擎的性能有着关键性的影响。本文提出了一种新的从RTL到门级网表的等价性验证流程:提取电路信息、综合待验证的设计、匹配待验证设计的等价点、比较待验证设计的等价点。不同于传统验证流程,为获得最好的电路相似性,此流程深入研究了综合优化等因素在不同层次上对电路相似性的破坏,提出了在综合阶段对比IP的不同实现方案,并进行启发式决策。以验证不同实现方案的乘法电路为例,本算法的验证准确性更高,而验证时间可减少3%～28%。
3.数据通路的验证:数据通路由一系列的算术表达式在行为域里表示,可按具体的变换规则进行优化组合。依照不同描述级,本文讨论了验证不同数据通路表示的各种算法,通过在寄存器传输级上比较重写数据通路以证明其等价性,提出了在数据通路级指导综合过程,有效简化了网表级等价性验证的复杂度。比如针对加法和乘法连续运算的表达式,算法从实现电路中提取变量顺序和结合顺序并加以利用,实验表明,在验证乘法连续运算的表达式时减少了83%～99%的时间,加法连续运算表达式的验证时间也可减少40%～89%。
4.结合半加图的算术单元验证:论文研究了基于BMD验证乘法电路的方法,该方法使用矩分解(moment decomposition)方式,在BMD的边和节点上赋予权重信息,减少了图的节点数。讨论了一种新的电路表示方法——半加图(Half Adder Graph),提出在综合阶段使用半加图表示算术电路,从中得到算术电路的实现方案,进一步指导算术电路的综合。统计提取电路实现和验证的时间花销,以乘法电路为例,本算法能明显提高验证引擎的性能(4%～63%)。
5.基于混合SAT引擎的RTL验证流程:传统验证流程需要将电路综合为门级网表,但门级验证引擎不能有效利用一些原始的电路的信息。本文提出了一种新的基于混合SAT引擎的验证流程,讨论了混合SAT引擎的约束传递过程。以不同规模的加法单个运算和连续运算表达式为例,比较传统验证流程验证时间最多可减少99%。实验结果表明基于混合SAT引擎的RTL验证流程比传统的验证流程有明显的优势。
VLSI verification takes about two thirds of the whole design time. In modern design flow of SoC, to guarantee the functional consistency of different abstract layers, a formal verification technique called Equivalence Checking (EC) is widely used. One challenging problem in EC is the verification of arithmetic designs. In the past few years, the author took part in the research and development of ZDFV Equivalence Checking System. Based on ZDFV work, the thesis focuses on the following key problems: how to construct an efficient synthesis engine; how to improve the structural similarity of the two designs; how to verify data path designs efficiently; how to use half adder graph to perform arithmetic unit verification; and how to use the hybrid SAT engine in the existing verification flow. The thesis includes the following original ideas and contributions.
1. Research on developing high efficient synthesis engine. Synthesis engine transforms a RTL design into a gate level netlist. The quality of the result gate netlist has a significant effect on the entire verification performance. With studying and analyzing of Icarus Verilog synthesis engine and other synthesis systems/ algorithms, an effective synthesis flow was proposed and implemented in ZDFV. The synthesis engines supports module reuse, macro definition and synthesis directives. Experiments on widely used IWLS_2005_bechmarks_V_l .0 benchmark designs show that, compared with Icarus system, our synthesis method reduces the total synthesis and flattening time by 98%.
2. Study on improving the module level similarity. The state-of-the-art equivalence checking algorithms fully exploit the similarity of the two designs. Better similarity means better performance. A new flow for RTL to gate level netlist equivalence checking was proposed. Our new flow first extracts design information, then synthesize the design, find internal potential equivalent point pairs and verify these potential equivalent point pairs. Unlike traditional flows, the new flow analyzes how different level of synthesis optimizations may affect the design similarity. The synthesis decision making takes different IP implementations into consideration and use heuristics to get better similarity. Experiments conducted on multipliers with different implementations show this leads to 3% to 28% running time reduction of the verification engine.
3. Equivalence checking of datapath: Datapath consists of series arithmetic operations, which can be optimized according to some transformation rules. Verification of different level representations of datapath was discussed. A RTL datapath rewriting technique was developed to achieve better design similarity. For adder and multiplier tree expressions, the proposed technique also considers the variable ordering and variable combinations. Experiments on multiplier tree and adder tree expressions exhibit running time reduction of 83% to 99%, and 40% to 80% respectively.
4. Arithmetic unit check with half adder graph technique: Binary Moment Diagram (BMD) technique has been used in multiplier equivalence checking. Unlike BDD, BMD adds weight (moment) on edges and thus reduces the node quantity of the diagram. A new circuit abstraction method, half adder graph was proposed to represent arithmetic circuits during the synthesis period. The new synthesis engine first analyzes the implementation of the arithmetic unit to gets its architectural information. Then use the information to guide the synthesis of the corresponding RTL design. Applying this approach on multiplier circuits, the performance of verification engine has been improved by 4%～63%.
5. A new equivalence checking flow based on hybrid SAT engine: In traditional equivalence checking flow, since the verification engines are gate-based, the RTL designs have to been synthesized to gate level netlists first. In this RTL to gate translation process, some structural information of the designs is lost. In this research, a hybrid SAT engine based verification flow was proposed. The constraint propagation process in the hybrid SAT engine was discussed. Compared with traditional flow, up to 99% verification time reduction was achieved when verifying single adder unit and adder tree expressions.
引文
[1]韩俊刚,杜慧敏.数字硬件的形式化验证[M].北京:北京大学出版社,2001.
[2]GWENNAP L.Pentium pro debuts with few bugs.[R]Microprocessor Report December 1995.
[3]KERN C and GREENSTREET M.Formal verification in hardware design:a survey[J].ACM Transactions on Design Automation of E.System,1999,4(8):123-193.
[4]HUANG Shi-Yu and CHENG Kwang-Ting.Formal equivalence checking and design debugging[M].Kluwer Academic Publisher:Boston/Dordrecht/London,1998.
[5]JONES R B,O'LEARY J W,et al.Practical formal verification in microprocessor design[J].IEEE Design and Test of Computer,2001,18(4):16-25.
[6]DANIEL B.Verification of large synthesized design[C].IEEE/ACM International Conference on Computer-Aided Design,Santa Clara,California,USA:IEEE Computer Society,1993:534-537.
[7]翁延玲,葛海通,严晓浪,卢永江.基于等价性形式验证的逻辑综合引擎设计研究[J].电路与系统学报,2007,12(4):1-4.
[8]翁延玲,葛海通,严晓浪.等价性验证中的算符排序[J].浙江大学学报(工学版),2007,41(6):886-889.
[9]WENG Y L,GE H T,YAN X L,REN K.Arithmetic operand ordering for equivalence checking[J].Tsinghua Science and Technology,2007,12(sl):235-239.
[10]严晓浪,郑飞君,葛海通,等.结合二叉判决图和布尔可满足性的等价性验证算法[J].电子学报,2004,31(8):1233-1235.
[11]卢永江,严晓浪,葛海通,等.结合无依赖性割集和量化的等价性验证[J].计算机辅助设计与图形学学报,2005,17(10):2215-2219.
[12]郑伟伟,吴为民,边计年.基于线性规划的RTL可满足性求解和性质检验[J].计算机辅助设计与图形学学报,2006,18(4):538-544.
[13]邓澎军,吴为民,边计年.RTL验证中的混合可满足性求解[J].计算机辅助设计与图形学学报,2007,19(3):273-278.
[14]邵明,李光辉,李晓维.模型检验中的转移关系的分组策略[J].计算机辅助设计与图形学学报,2003,15(9):1101-1104.
[15]李光辉,李晓维.基于增量可满足性的等价性验证方法[J].计算机学报,2004,27(10):1388-1394.
[16]丁敏,唐璞山.改进的时间帧展开的时序电路等价性验证算法[J].计算机辅助设计与图形学学报,2006,18(1):53-61。
[17]丁敏.可满足性问题算法研究以及在时序电路等价性验证中的应用[D].上海:复旦大学,2005.
[18]黄伟,唐璞山.基于切割法的时序电路等价验证[J].复旦学报(自然科学版),2006,45(1):102-106.
[19]WU Qing-hong,RAMIREZ Chavez,SERGIO R.Black/Clad:a layout synthesis tool for combinational blocks from behavioral HDL descriptions [C]// Proceedings of the IEEE 35th Midwest Symposium on Circuits and Systems.Washington D.C.:[s.n.]1992,2:843-846.
[20]FELICE B,GARY Y.Verilog HDL modeling styles for formal verification[C]//Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications.Ottawa,Canada:North-Holland,1993,A-32:453-465.
[21]Stephen W.The icarus verilog compilation system version 0.7[CP/DK].Sep.2000.
[22]CHENG C T,et al.Compiling verilog into timed finite state machines[C]//Proceedings of 1995 IEEE International Verilog HDL Conference.Santa Clara,CA:Press Los Alamitos,1995:32-39.
[23]LAY H T,JIMEN C.Verilog behavioral simulation version 1.4.0[CP/DK].Mar.2007.
[24]AMIT R,ELLIOT M,MARK H.VeriWell Verilog Simulator[CP/DK].AMIT R,ELLIOT M,MARK H,2005.
[25]University of California.ABC:Logic synthesis and verification system [CP/DK].University of California,2005.
[26]SCOTT F.PVSim verilog simulator[CP/DK].SCOTT F,2004.
[27]FISHER L M.Flaw reported in new Intel chip[N].New York Times,p.D,4:3,May 6,1997.
[28]COE T.Inside the pentium fdiv bug[J].Dr.Dobb's Journal,Apr.1996,129-135.
[29]CHANG Ying-Tsai and CHENG Kwang-Ting.Self-referential verification for gate-level implementations of arithmetic circuits [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Jul. 2004,23(7): 1102-1112.
[30]BRYANT R E. Graph-based algorithms for boolean function manipulation [J].IEEE Transactions on Computer, Aug. 1986, C-35: 677-691.
[31] BRYANT R E. On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication [J]. IEEE Transactions on Computer, Feb. 1991,40: 205-213.
[32] CHANG Y-T and CHENG K-T. Induction-based gate-level verification of multipliers[C]//Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, San Jose, California: IEEE Press,Nov. 2001: 190-193.
[33] ZHENG Zhou, WAYNE B. Equivalence checking of datapaths based on canonical arithmetic expressions[C]// Proceeding of the 32nd Design Automation Conference. San Francisco, California: ACM Press, 1995:546-551.
[34] PARHAMI B. Computer arithmetic: algorithms and hardware designs [M].Oxford, U.K.: Oxford Univ. Press, 2000.
[35] GORDON M. HOL: A proof generating system for higher order logic [M].VLSI Specification, Verification, and Synthesis. Boston: Kcademic Press,1988,73-127.
[36]OWRE S, RUSHBY J R, SHANKAR N, et al.A tutorial on using PVS for hardware verification[C]// Proceedings of the 2nd International Conference of Theorem Provers in Circuit Design. London: Springer-Verlag, Sept.1994: 258-279.
[37]CARRENO V A and MINER P S. Specification of the IEEE-854 floating-point standard in HOL and PVS[C]// Proceedings of 1995 International Workshop on High Order Logic Theorem Proving and Its Applications, UT: [s.n],Sept. 1995, 124-134.
[38] MOORE J S, LYNCH T W, KAUFMANN M. A mechanically checked proof of the amd5 86? floating-point division program [J].IEEE transactions on Computer, Sept. 1998,47: 913-926.
[39] KAUFMANN M and MOORE J S. ACL2: An industrial strength version of Nqthm[C]// Proceedings of the 11th Annual Conference on Computer Assurance. Gaithersburg, Maryland, USA: IEEE Computer Society Press, June 1996: 23-34.
[40]Mcsorley O L. High-speed arithmetic in binary computers [J]. Proc. IRE, Jan.1961,49(1), 66-91.
[41]ROBERTSON J E. A new class of digital division methods [J]. IRE Trans.Electron. Computeer, 1958, 7: 218-222.
[42] TOCHER K D. Techniques of multiplication and division for automatic binary computers [J]. Quart. J. Mech. Appl. Math., 1958,11: 363-384.
[43] CLARKE E M, GERMAN S M, and ZHAO X. Verifying the SRT division algorithm using theorem proving techniques[C]// Proceeding of the 8th International Conference on Computer-Aided Verification. New Brunswick, NJ, Berlin: Springer-Verlag, 1996,1102: 111-122.
[44] BROCK B, KAUFMANN M, and MOORE J S. ACL2 theorems about commercial microprocessors [J]. Formal Methods Computer-Aided Design,Nov. 1996:275-293.
[45] BRYANT R E, CHEN Ying-An. Verification of arithmetic circuits with binary moment diagrams[C]//Proceeding of the 32nd ACM/IEEE Design Automation Conference. San Francisco: ACM Press June 1995: 535-541.
[46] CHEN Y A and BRYANT R E. ACV: An arithmetic circuit verifier[C]//Proceeding of 1996 International Conference on Computer-Aided Design.San Francisco: ACM and IEEE Computer Society, Nov. 1996:361-365.
[47] CLARKE E M, FUJITA M, and ZHAO X. Hybrid decision diagrams overcoming the limitations of MTBDDs and BMDs[C]// Proceeding of International Conference on Computer-Aided Design.San Francisco: IEEE Computer Society, Nov. 1995: 159-163.
[48]DRECHSLER R, BECKER B, and RUPPERTZ S. K*BMDs: A new data structure for verification[C]. Proceeding of European Design and Test Conference. Paris: [s.n], Mar. 1996, 2-8.
[49] MITCHELL A T, ADITYA M. Research Results in equivalence checking[R].USA, Southern Methodist University: Department of Computer Science and Engineering, 2004.
[50] JAIN J, BITNER J, ABADIR M S, et al. Indexed BDDs: algorithmic advances in techniques to represent and verify Boolean functions [J]. IEEE Transactions on Computer, 1997, 46(11):1230-1245.
[51]JEONG S W, PLESSIER B, HACHTEL G, et al. Extended BDDs: trading off canonicity for structure in verification algorithms [C]//Proceedings of the 1991 IEEE International Conference on Computer Aided Design. Los Alamitos: IEEE Computer Socitey Press, 1991: 464-467.
[52]ASHAR P, GHOSH A, DEVADAS S. Bollean satisfiability and equivalence checking using general binary decision diagrams[C]//Proceeding of the 1991 IEEE International Conference on Computer Design: VLSI in Computer and Processors. Washington DC: IEEE Computer Society Press, 1991:259-264.
[53] ANDERSEN H R, HULGAARD H. Boolean expression diagrams [C]//Proceedings of the 12~(th) Annual IEEE symposium on Logic in Computer Science. Washington DC: IEEE Computer Society Press, 1997:88.
[54] HULGAARD H, WILLIAMS P F, ANDERSEN H R. Equivalence checking of combinational circuits using Boolean expression diagrams [J]. IEEE Transactions on Computer-Aided Design of Intergrated Circuits and Systems, 1999,18(7):903-917.
[55]BERMAN C L, TREVILLYAN L H. Functional comparison of logic design for VLSI circuits [C]//Proceedings of the International Conference on Computer Aided Design. Washington DC: Computer Society Press, 1989:456-459.
[56]BRAND D. Verification of large synthesiszed designs [C]// Proceedings of 1993 IEEE/ACM International Conference on Computer Aided Design.Los Alamitos: IEEE Computer Society Press, 1993:534-537.
[57]EIJK C A J, JANSSEN G Exploiting structural similarities in a BDD-based verification method [C]// Proceedings of the Second International Conference on Theorem Provers in Circuit Design-Theory, Practice and Experience. London: Springer-Verlag Press, 1994: 110-125.
[58]MATSUNAGA Y. An efficient equivalence checker for combinational circuits[C]//Proceedings of the Design Automation Conference. New York:ACM Press, 1996:629-634.
[59]KUEHLMANN A, KROHM F. Equivalence checking using cuts and heaps [C]// Proceedings of 1997 Design Automation Conference. San Jose, CA,USA: ACM and IEEE Computer Society, 1997: 263-268.
[60]MUKHERJEE R, JAIN J, TAKAYAMA K, et al. Efficient combinational verification using BDDs and a hash table [C]//Proceedings of the 1997 International Symposium on Circuits and Systems. Hong Kong: IEEE Press, 1997: 1025-1028.
[61]NAKAOKA T, WAKABAYASHI S, KOIDE T, et al. A verification algorithm for logic circuits with internal variables [C]//Proceedings of the International Symposium on Circuits and Systems. Seattle: IEEE Press, 1995: 1920-1923.
[62]KUNZ W, PRADHAN D K. Recursive learning: an attractive alternative to the decision tree for test generation in digital circuits [C]//Proceedings of the IEEE International Test Conference. Washington DC: IEEE Computer Society Press, 1992: 816-825.
[63]KUNZ W, HANNBAL A L. An efficient tool for logic verification based on recursive learning [C]//Proceedings of the 1993 IEEE/ACM International Conference on Computer Aided Design. Los Alamitos: IEEE Computer Society Press, 1993: 538-543.
[64] JAIN J, MUKHERJEE R, FUJITA M. Advanced verification techniques based on learning [C]//Proceedings of the 32~(nd) ACM/IEEE Design Automation Conference. New York: ACM Press, 1995: 420-426.
[65]PARADHAN D K, PAUL D, CHATTERJEE M. VERILAT: Verification usigng logic augmentation and transformations [C]//Proceedings of the 1996 IEEE/ACM International Conference on Computer Aided Design.Washington DC: IEEE Computer Society Press, 1996:88-95.
[66] Design Ware Building Block IP Document, Synopsys, May 2000
[67] IEEE P1364.1/D1.4, Draft Standard for Verilog Register Transfer Level Synthesis[S]. New York, IEEE, Inc., April 26, 1999.
[68]FERRANTE J and RACKO C W. The computational complexity of logical theories:lecture notes in mathematics [M]. Berlin: Springer-Verlag, 1979.
[69]KNUTH D E. and BENDIX P B. Simple word problems in universal algebras[M]//Computational Problems in Abstract Algebras.Oxford,England: Pergamon Press, 1970: 263-297.
[70] DOWNEY P J, SETHI R, and TARJAN R E. Variations on the common subexpression problem [J]. Journal of the ACM, 1980, 27(4):758-771.
[71]DERSHOWITZ N, JOUANNAUD J P. Handbook of Theoretical Computer Science (vol. B): formal models and semantics [M]. North-Holland Publishing Company, 1990: 244-319.
[72]BRYANT R E. Graph-based algorithms for boolean functions [J].IEEE Transactions on Computers, 1986, C-35(8):677-691.
[73]BAHAR R I, FROHM E A, GAONA C M, et al. Algebraic decision diagrams and their applications [C]// Proceedings of the International Conference on Computer-Aided Design. California, USA: IEEE Computer Society, 1993:188-191.
[74]KEBSCHULL U, SCHUBERT E, and ROSENSTIEL W. Multilevel logic synthesis based on functional decision diagrams[C]// Proceedings of EuropeanDesign Automation Conference, Los Alamitos, CA : Computer Society Press, 1992: 43-47.
[75] BRYANT R E and CHEN Y A. Verication of arithmetic functions with binary moment diagrams[R]. Technical Report CMU-CS-94-160, Carnegie Mellon University: Department of Computer Sciences, 1994.
[76] LAI Y T and SASTRY S. Edge-valued binary decision diagrams for multi-level hierarchical verication[C]//Proceedings of the 29th ACM/IEEE Design Automation Conference. Washington D.C.: IEEE Computer Society Press,1992:608-613.
[77] STOFFEL D, KUNZ W. Equivalence checking of arithmetic circuits on the arithmetic bit level [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2004,23(5): 586 - 597
[78]GAJSKI D D, DUTT N D, Wu A C, et al. High-level synthesis: introduction to chip and system design [M]. KluwerAcademic Publishers, 1992.
[79]THAPLIYAL H, RAMASAHAYAM A, KOTHA V K, et al. Modified montgomery modular multiplication using 4:2 compressor and CSA adder[C]//Proceedings of the Third IEEE International Workshop on Electronic Design, Test and Applications. Kuala Lumpur, Malaysia: IEEE, 2006:414-417.
[80]RAAHEMIFAR K, AHMADI M. Fast carry-look-ahead adder Electrical and Computer Engineering[C]//Proceedings of IEEE Canadian Conference on Electrical and Computer Engineering. Edmonton, Canada: IEEE, 1999,1:529-532.
[81] WALLACE C S. A suggestion for a fast multiplier[J]. IEEE Transactions on Electronic Computers, 1964, EC-13(1): 14-17.
[82]KUENHLMANN A, PARUTHI V, KROHM F, et al. Robust Boolean reasoning for equivalence checking and functional property verification[J].IEEE Transactions Computer-Aided Design, 2002, C-21:1377-1394.
[83]BOOTH A D. A signed binary multiplication technique [J]. Quart Journal of Mech And Appl, 1951, IV(2):236-240.
[84]ITRS2003,International Technology Roadmap for Semi-conductor[EB/OL].[2004-05-05]http://public.itrs.net.
[85]MARQUES-SILVA J P,SAKALLAH K A.GRASP:A search algorithm for propositional satisfiability[J].IEEE Transaction on Computers,1999,48(5):506-521.
[86]SILVA L G,SILVEIRA L M,MARQUES-SILVA J.Algorithms for solving Boolean satisfiability in combinational circuits[C]// Proceedings of the Design Automation and Test in Europe Conference and Exhibition,Munich,Germany:ACM Press,1999:526-530.
[87]MOSKEWICZ M,MADIGAN C,et al.Chaff:engineering an efficient SAT solver[C]//Proceedings of 2001 Design Automation Conference.Las Vegas:ACM,2001:530-535.
[88]ZHANG Lin-tao,Madigam C F,et al.Efficient conflict driven learning in a Boolean satisfiablity solver[C]// Proceedings of the 20~(th) IEEE/ACM International Conference on Computer-Aided Design,San Jose,CA:ACM Press,2001.279-285.
[89]ZHANG H.SATO:An efficient propositional prover[C]//Proceeding of the 14~(th) International Conference on Automated Deduction,North Queensland,Australia:ACM and IEEE Computer Society,1997:272-275.
[90]LIU Tao,LI Guo-jie.Multi-stage search rearrangement algorithm for solving SAT problem[J].Journal of Software,1996.7(4),201-210.
[91]LIANG Dong-min,WU Ye,MA Shaohan.An efficient local search algorithm for structured SAT problem[J].Chinese Journal of Computers,1998,21(8):394-397.
[92]EEN N,SORENSSON N.An extensible SAT solver[C]//Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing,Santa Margherita Ligure:[s.n.],2003:502-518.
[93]邓雨春,杨士元,王红,等.在形式验证和ATPG中的布尔可满足性问题[J]计算机辅助设计与图形学学报,2003,15(10):1207-1212.
[94]MARQUES-SILVA J P,SAKALLAH K A.Boolean satisfiability in electronic design automation[C]// Proceedings of the 39th Design Automation Conference,Piscataway:IEEE Press,2002:675-680.
[95]SELMAN B,LEVESQUE H,MITCHELL D.A new method for solving hard satisfiability problems[C]// Proceedings Of the 10~(th) National Conference on Artificial Intelligence,Menlo Park,CA:AAAI Press,1992:440-446.
[96] FRANK J. Weighting for godot: learning heuristic for GSAT [C]//Proceedings Of National Conference on Artificial Intelligence, Oregon: AAAI Press 1996:338-343.
[97]SHANG Y, WAH B W. A discriete lagrangian-based global-search method for solving satifiability problems [J]. Journal of Global Optimization, 1998,12:61-99.
[98]SHANG Y, WAH B W. Improving the performance of discrete lagrange-multiplier search for solving hard SAT problems [C]//Proceedings Of IEEE 10~(th) International Conference on Tools with Artificial Intelligence,Taipei, China : IEEE press ,1998: 176-183
[99] DAVIS M, PUTNAM H. A computer procedure for quantification theory [J]. Journal of ACM, 1960, 7:201-214.
[100] DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theorem-proving [J]. Communication of ACM, 1962, 5(7): 394-397.
[101] BURO M, KLEINE-BUNING H. Report on a SAT competition [J]. Bulletin of the European Association for Theoretical Computer Science.1993,49:143-151.
[102]JEROSLOW R G, WANG J. Solving propositional satisfiability problems [J].Annals of Mathematics and Artificial Intelligence. 1990, 1:167-188
[103] FREEMAN J W. Improvements to prepositional satisfiability search algorithms [D]. Pennsylvania: University of Pennsylvania, 1995.
[104]FALLAH F, DEVADAS S, KEUTZER K. Functional vector generation for HDL models using linear programming and 3-satisfiabillty[C]// Proceedings of the 35th Design Automation Conference, San Francisco, CA: ACM Press,1998: 528-533.
[105]FALLAH F. Coverage directed validation of hardware models [D]. CamM dge, Massachusetts: Massachusetts Institute of Technology. 1999.
[106]ZENGz, KALLAz, CIESIELSKIM. "LPSAT: a unified approach to RTL satisfiability[C]// Proceedings of the Conference on Design Automa tion and Test in Europe, New York: ACM Press,2001: 398-402.
[107]KUEHLMANN A, GANAI M K, and PARUTHI V. Circuit-based boolean reasoning[C]// Proceedings of 2001 ACM/IEEE Design Automation Conference, Anaheim, CA: ACM Press, 2001: 232-237.
[108] ZHANG H, STICKEL M. An efficient algorithm for unit propagation[C]//Proceeding of the Fourth International Symposium on Artificial Intelligence and Mathematics. Florida: [s. n.], 1996: 166-179.
[109]STALLMAN R, SUSSMAN G. Forward reasoning and dependency directed backtracking in a system for computer aided circuit analysis [J]. Artificial Intelligence, 1977, 9(2): 135-196.
[110]LU F, WANG L-C, CHENG K-T, et al. A signal correlation guided ATPG solver and its applications for solving difficult industrial cases[C]//Proceedings of 2003 ACM/IEEE Design Automation Conference, Anaheim: [s. n.], Jun. 2003:668-673.
[111]STRICHMAN O. On solving presburger and linear arithmetic with SAT[C]//Proceedings of International Conference on Formal Methods in Computer-Aided Design, OR, Portland: [s. n.], Jan. 2002,2517:160-169.
[112]BARRETT C, DILL D L, and LEVITT J. Validity checking for combinations of theories with equality [C]//Proceedings of the first International Conference on Formal Methods in Computer-Aided Design, California:Springer-Verlag, 1996,1166:187-201.
[113]FILLIATRE J-C, OWRE S, RUE/3 H, et al. ICS: Integrated canonization and solving[C]// Proceedings of the Computer Aided Verification Conference,Paris: Springer-Verlag, July 2001, 2102: 246-249.
[114]SESHIA S, LAHIRI S, and BRYANT R. A hybrid SAT-based decision procedure for separation logic with uninterpreted functions[C]// Proceedings of the ACM/IEEE Design Automation Conference, Anaheim, California:ACM,Jun. 2003: 425-430.
[115]AUDEMARD G, BERTOLI P, CIMATTI A, et al. A SAT based approach for solving formulas over Boolean and linear mathematical propositions[C]//Proceedings of 18th International Conference on Automated Deduction, Copenhagen: Springer Verlag.2003, 2392: 195-210.
[116]LIU C, KUEHLMANN A, and MOSKEWICZ M. CAMA: a Multi-Valued Satisfiablity Solver[C]// Proceedings of the International Conference on Computer-Aided Design, CA, USA: IEEE Computer Society / ACM, Nov.2003:326-333.
[117] HUANG C-Y and CHENG K-T. Using word-level ATPG and modular arithmetic constraint-solving for assertion property checking [J].IEEE Transactions on Computer-Aided Design, June 2001:381-391.
[118] GHOSH I, and FUJITA M. Automatic test pattern generation for functional register-transfer level circuits using assignment decision diagrams [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits &Systems, March 2001:402-415.
[119]PARTHASARATHY G, IYER M, CHENG K-T, et al. An Efficient Finite-domain Constraint Solver for RTL Circuits[C]// Proceedings of the ACM/IEEE Design Automation Conference, New York: ACM Press, 2004:212-217.
[120]GANZINGER H, HAGEN G, and NIEUWENHUIS R, et al. DPLL (T): Fast decision procedures[C]//Proceedings of the Computer Aided Verification Conference, Boston: Springer Verlag, 2004:26-37.
[121] ABRAMOVICI M, BREUER M A., and FRIEDMAN A D. Digital systems testing and testable design [M]. Computer Science Press, 1990.
[122]GIRODIAS P, CERNY E, and OLDER W. Solving linear, min and max constraint systems using CLP based on relational interval arithmetic [J].Theoretical Computer Science, Feb. 1997,173(2):253-281.
[123] KELLY W, MASLOW V, PUGH W, et al. The omega library v1.1.0: interface guide[R]. Department. Of Computer Science, University of Maryland,College Park, November 1996.
[2]GWENNAP L.Pentium pro debuts with few bugs.[R]Microprocessor Report December 1995.
[3]KERN C and GREENSTREET M.Formal verification in hardware design:a survey[J].ACM Transactions on Design Automation of E.System,1999,4(8):123-193.
[4]HUANG Shi-Yu and CHENG Kwang-Ting.Formal equivalence checking and design debugging[M].Kluwer Academic Publisher:Boston/Dordrecht/London,1998.
[5]JONES R B,O'LEARY J W,et al.Practical formal verification in microprocessor design[J].IEEE Design and Test of Computer,2001,18(4):16-25.
[6]DANIEL B.Verification of large synthesized design[C].IEEE/ACM International Conference on Computer-Aided Design,Santa Clara,California,USA:IEEE Computer Society,1993:534-537.
[7]翁延玲,葛海通,严晓浪,卢永江.基于等价性形式验证的逻辑综合引擎设计研究[J].电路与系统学报,2007,12(4):1-4.
[8]翁延玲,葛海通,严晓浪.等价性验证中的算符排序[J].浙江大学学报(工学版),2007,41(6):886-889.
[9]WENG Y L,GE H T,YAN X L,REN K.Arithmetic operand ordering for equivalence checking[J].Tsinghua Science and Technology,2007,12(sl):235-239.
[10]严晓浪,郑飞君,葛海通,等.结合二叉判决图和布尔可满足性的等价性验证算法[J].电子学报,2004,31(8):1233-1235.
[11]卢永江,严晓浪,葛海通,等.结合无依赖性割集和量化的等价性验证[J].计算机辅助设计与图形学学报,2005,17(10):2215-2219.
[12]郑伟伟,吴为民,边计年.基于线性规划的RTL可满足性求解和性质检验[J].计算机辅助设计与图形学学报,2006,18(4):538-544.
[13]邓澎军,吴为民,边计年.RTL验证中的混合可满足性求解[J].计算机辅助设计与图形学学报,2007,19(3):273-278.
[14]邵明,李光辉,李晓维.模型检验中的转移关系的分组策略[J].计算机辅助设计与图形学学报,2003,15(9):1101-1104.
[15]李光辉,李晓维.基于增量可满足性的等价性验证方法[J].计算机学报,2004,27(10):1388-1394.
[16]丁敏,唐璞山.改进的时间帧展开的时序电路等价性验证算法[J].计算机辅助设计与图形学学报,2006,18(1):53-61。
[17]丁敏.可满足性问题算法研究以及在时序电路等价性验证中的应用[D].上海:复旦大学,2005.
[18]黄伟,唐璞山.基于切割法的时序电路等价验证[J].复旦学报(自然科学版),2006,45(1):102-106.
[19]WU Qing-hong,RAMIREZ Chavez,SERGIO R.Black/Clad:a layout synthesis tool for combinational blocks from behavioral HDL descriptions [C]// Proceedings of the IEEE 35th Midwest Symposium on Circuits and Systems.Washington D.C.:[s.n.]1992,2:843-846.
[20]FELICE B,GARY Y.Verilog HDL modeling styles for formal verification[C]//Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications.Ottawa,Canada:North-Holland,1993,A-32:453-465.
[21]Stephen W.The icarus verilog compilation system version 0.7[CP/DK].Sep.2000.
[22]CHENG C T,et al.Compiling verilog into timed finite state machines[C]//Proceedings of 1995 IEEE International Verilog HDL Conference.Santa Clara,CA:Press Los Alamitos,1995:32-39.
[23]LAY H T,JIMEN C.Verilog behavioral simulation version 1.4.0[CP/DK].Mar.2007.
[24]AMIT R,ELLIOT M,MARK H.VeriWell Verilog Simulator[CP/DK].AMIT R,ELLIOT M,MARK H,2005.
[25]University of California.ABC:Logic synthesis and verification system [CP/DK].University of California,2005.
[26]SCOTT F.PVSim verilog simulator[CP/DK].SCOTT F,2004.
[27]FISHER L M.Flaw reported in new Intel chip[N].New York Times,p.D,4:3,May 6,1997.
[28]COE T.Inside the pentium fdiv bug[J].Dr.Dobb's Journal,Apr.1996,129-135.
[29]CHANG Ying-Tsai and CHENG Kwang-Ting.Self-referential verification for gate-level implementations of arithmetic circuits [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Jul. 2004,23(7): 1102-1112.
[30]BRYANT R E. Graph-based algorithms for boolean function manipulation [J].IEEE Transactions on Computer, Aug. 1986, C-35: 677-691.
[31] BRYANT R E. On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication [J]. IEEE Transactions on Computer, Feb. 1991,40: 205-213.
[32] CHANG Y-T and CHENG K-T. Induction-based gate-level verification of multipliers[C]//Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, San Jose, California: IEEE Press,Nov. 2001: 190-193.
[33] ZHENG Zhou, WAYNE B. Equivalence checking of datapaths based on canonical arithmetic expressions[C]// Proceeding of the 32nd Design Automation Conference. San Francisco, California: ACM Press, 1995:546-551.
[34] PARHAMI B. Computer arithmetic: algorithms and hardware designs [M].Oxford, U.K.: Oxford Univ. Press, 2000.
[35] GORDON M. HOL: A proof generating system for higher order logic [M].VLSI Specification, Verification, and Synthesis. Boston: Kcademic Press,1988,73-127.
[36]OWRE S, RUSHBY J R, SHANKAR N, et al.A tutorial on using PVS for hardware verification[C]// Proceedings of the 2nd International Conference of Theorem Provers in Circuit Design. London: Springer-Verlag, Sept.1994: 258-279.
[37]CARRENO V A and MINER P S. Specification of the IEEE-854 floating-point standard in HOL and PVS[C]// Proceedings of 1995 International Workshop on High Order Logic Theorem Proving and Its Applications, UT: [s.n],Sept. 1995, 124-134.
[38] MOORE J S, LYNCH T W, KAUFMANN M. A mechanically checked proof of the amd5 86? floating-point division program [J].IEEE transactions on Computer, Sept. 1998,47: 913-926.
[39] KAUFMANN M and MOORE J S. ACL2: An industrial strength version of Nqthm[C]// Proceedings of the 11th Annual Conference on Computer Assurance. Gaithersburg, Maryland, USA: IEEE Computer Society Press, June 1996: 23-34.
[40]Mcsorley O L. High-speed arithmetic in binary computers [J]. Proc. IRE, Jan.1961,49(1), 66-91.
[41]ROBERTSON J E. A new class of digital division methods [J]. IRE Trans.Electron. Computeer, 1958, 7: 218-222.
[42] TOCHER K D. Techniques of multiplication and division for automatic binary computers [J]. Quart. J. Mech. Appl. Math., 1958,11: 363-384.
[43] CLARKE E M, GERMAN S M, and ZHAO X. Verifying the SRT division algorithm using theorem proving techniques[C]// Proceeding of the 8th International Conference on Computer-Aided Verification. New Brunswick, NJ, Berlin: Springer-Verlag, 1996,1102: 111-122.
[44] BROCK B, KAUFMANN M, and MOORE J S. ACL2 theorems about commercial microprocessors [J]. Formal Methods Computer-Aided Design,Nov. 1996:275-293.
[45] BRYANT R E, CHEN Ying-An. Verification of arithmetic circuits with binary moment diagrams[C]//Proceeding of the 32nd ACM/IEEE Design Automation Conference. San Francisco: ACM Press June 1995: 535-541.
[46] CHEN Y A and BRYANT R E. ACV: An arithmetic circuit verifier[C]//Proceeding of 1996 International Conference on Computer-Aided Design.San Francisco: ACM and IEEE Computer Society, Nov. 1996:361-365.
[47] CLARKE E M, FUJITA M, and ZHAO X. Hybrid decision diagrams overcoming the limitations of MTBDDs and BMDs[C]// Proceeding of International Conference on Computer-Aided Design.San Francisco: IEEE Computer Society, Nov. 1995: 159-163.
[48]DRECHSLER R, BECKER B, and RUPPERTZ S. K*BMDs: A new data structure for verification[C]. Proceeding of European Design and Test Conference. Paris: [s.n], Mar. 1996, 2-8.
[49] MITCHELL A T, ADITYA M. Research Results in equivalence checking[R].USA, Southern Methodist University: Department of Computer Science and Engineering, 2004.
[50] JAIN J, BITNER J, ABADIR M S, et al. Indexed BDDs: algorithmic advances in techniques to represent and verify Boolean functions [J]. IEEE Transactions on Computer, 1997, 46(11):1230-1245.
[51]JEONG S W, PLESSIER B, HACHTEL G, et al. Extended BDDs: trading off canonicity for structure in verification algorithms [C]//Proceedings of the 1991 IEEE International Conference on Computer Aided Design. Los Alamitos: IEEE Computer Socitey Press, 1991: 464-467.
[52]ASHAR P, GHOSH A, DEVADAS S. Bollean satisfiability and equivalence checking using general binary decision diagrams[C]//Proceeding of the 1991 IEEE International Conference on Computer Design: VLSI in Computer and Processors. Washington DC: IEEE Computer Society Press, 1991:259-264.
[53] ANDERSEN H R, HULGAARD H. Boolean expression diagrams [C]//Proceedings of the 12~(th) Annual IEEE symposium on Logic in Computer Science. Washington DC: IEEE Computer Society Press, 1997:88.
[54] HULGAARD H, WILLIAMS P F, ANDERSEN H R. Equivalence checking of combinational circuits using Boolean expression diagrams [J]. IEEE Transactions on Computer-Aided Design of Intergrated Circuits and Systems, 1999,18(7):903-917.
[55]BERMAN C L, TREVILLYAN L H. Functional comparison of logic design for VLSI circuits [C]//Proceedings of the International Conference on Computer Aided Design. Washington DC: Computer Society Press, 1989:456-459.
[56]BRAND D. Verification of large synthesiszed designs [C]// Proceedings of 1993 IEEE/ACM International Conference on Computer Aided Design.Los Alamitos: IEEE Computer Society Press, 1993:534-537.
[57]EIJK C A J, JANSSEN G Exploiting structural similarities in a BDD-based verification method [C]// Proceedings of the Second International Conference on Theorem Provers in Circuit Design-Theory, Practice and Experience. London: Springer-Verlag Press, 1994: 110-125.
[58]MATSUNAGA Y. An efficient equivalence checker for combinational circuits[C]//Proceedings of the Design Automation Conference. New York:ACM Press, 1996:629-634.
[59]KUEHLMANN A, KROHM F. Equivalence checking using cuts and heaps [C]// Proceedings of 1997 Design Automation Conference. San Jose, CA,USA: ACM and IEEE Computer Society, 1997: 263-268.
[60]MUKHERJEE R, JAIN J, TAKAYAMA K, et al. Efficient combinational verification using BDDs and a hash table [C]//Proceedings of the 1997 International Symposium on Circuits and Systems. Hong Kong: IEEE Press, 1997: 1025-1028.
[61]NAKAOKA T, WAKABAYASHI S, KOIDE T, et al. A verification algorithm for logic circuits with internal variables [C]//Proceedings of the International Symposium on Circuits and Systems. Seattle: IEEE Press, 1995: 1920-1923.
[62]KUNZ W, PRADHAN D K. Recursive learning: an attractive alternative to the decision tree for test generation in digital circuits [C]//Proceedings of the IEEE International Test Conference. Washington DC: IEEE Computer Society Press, 1992: 816-825.
[63]KUNZ W, HANNBAL A L. An efficient tool for logic verification based on recursive learning [C]//Proceedings of the 1993 IEEE/ACM International Conference on Computer Aided Design. Los Alamitos: IEEE Computer Society Press, 1993: 538-543.
[64] JAIN J, MUKHERJEE R, FUJITA M. Advanced verification techniques based on learning [C]//Proceedings of the 32~(nd) ACM/IEEE Design Automation Conference. New York: ACM Press, 1995: 420-426.
[65]PARADHAN D K, PAUL D, CHATTERJEE M. VERILAT: Verification usigng logic augmentation and transformations [C]//Proceedings of the 1996 IEEE/ACM International Conference on Computer Aided Design.Washington DC: IEEE Computer Society Press, 1996:88-95.
[66] Design Ware Building Block IP Document, Synopsys, May 2000
[67] IEEE P1364.1/D1.4, Draft Standard for Verilog Register Transfer Level Synthesis[S]. New York, IEEE, Inc., April 26, 1999.
[68]FERRANTE J and RACKO C W. The computational complexity of logical theories:lecture notes in mathematics [M]. Berlin: Springer-Verlag, 1979.
[69]KNUTH D E. and BENDIX P B. Simple word problems in universal algebras[M]//Computational Problems in Abstract Algebras.Oxford,England: Pergamon Press, 1970: 263-297.
[70] DOWNEY P J, SETHI R, and TARJAN R E. Variations on the common subexpression problem [J]. Journal of the ACM, 1980, 27(4):758-771.
[71]DERSHOWITZ N, JOUANNAUD J P. Handbook of Theoretical Computer Science (vol. B): formal models and semantics [M]. North-Holland Publishing Company, 1990: 244-319.
[72]BRYANT R E. Graph-based algorithms for boolean functions [J].IEEE Transactions on Computers, 1986, C-35(8):677-691.
[73]BAHAR R I, FROHM E A, GAONA C M, et al. Algebraic decision diagrams and their applications [C]// Proceedings of the International Conference on Computer-Aided Design. California, USA: IEEE Computer Society, 1993:188-191.
[74]KEBSCHULL U, SCHUBERT E, and ROSENSTIEL W. Multilevel logic synthesis based on functional decision diagrams[C]// Proceedings of EuropeanDesign Automation Conference, Los Alamitos, CA : Computer Society Press, 1992: 43-47.
[75] BRYANT R E and CHEN Y A. Verication of arithmetic functions with binary moment diagrams[R]. Technical Report CMU-CS-94-160, Carnegie Mellon University: Department of Computer Sciences, 1994.
[76] LAI Y T and SASTRY S. Edge-valued binary decision diagrams for multi-level hierarchical verication[C]//Proceedings of the 29th ACM/IEEE Design Automation Conference. Washington D.C.: IEEE Computer Society Press,1992:608-613.
[77] STOFFEL D, KUNZ W. Equivalence checking of arithmetic circuits on the arithmetic bit level [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2004,23(5): 586 - 597
[78]GAJSKI D D, DUTT N D, Wu A C, et al. High-level synthesis: introduction to chip and system design [M]. KluwerAcademic Publishers, 1992.
[79]THAPLIYAL H, RAMASAHAYAM A, KOTHA V K, et al. Modified montgomery modular multiplication using 4:2 compressor and CSA adder[C]//Proceedings of the Third IEEE International Workshop on Electronic Design, Test and Applications. Kuala Lumpur, Malaysia: IEEE, 2006:414-417.
[80]RAAHEMIFAR K, AHMADI M. Fast carry-look-ahead adder Electrical and Computer Engineering[C]//Proceedings of IEEE Canadian Conference on Electrical and Computer Engineering. Edmonton, Canada: IEEE, 1999,1:529-532.
[81] WALLACE C S. A suggestion for a fast multiplier[J]. IEEE Transactions on Electronic Computers, 1964, EC-13(1): 14-17.
[82]KUENHLMANN A, PARUTHI V, KROHM F, et al. Robust Boolean reasoning for equivalence checking and functional property verification[J].IEEE Transactions Computer-Aided Design, 2002, C-21:1377-1394.
[83]BOOTH A D. A signed binary multiplication technique [J]. Quart Journal of Mech And Appl, 1951, IV(2):236-240.
[84]ITRS2003,International Technology Roadmap for Semi-conductor[EB/OL].[2004-05-05]http://public.itrs.net.
[85]MARQUES-SILVA J P,SAKALLAH K A.GRASP:A search algorithm for propositional satisfiability[J].IEEE Transaction on Computers,1999,48(5):506-521.
[86]SILVA L G,SILVEIRA L M,MARQUES-SILVA J.Algorithms for solving Boolean satisfiability in combinational circuits[C]// Proceedings of the Design Automation and Test in Europe Conference and Exhibition,Munich,Germany:ACM Press,1999:526-530.
[87]MOSKEWICZ M,MADIGAN C,et al.Chaff:engineering an efficient SAT solver[C]//Proceedings of 2001 Design Automation Conference.Las Vegas:ACM,2001:530-535.
[88]ZHANG Lin-tao,Madigam C F,et al.Efficient conflict driven learning in a Boolean satisfiablity solver[C]// Proceedings of the 20~(th) IEEE/ACM International Conference on Computer-Aided Design,San Jose,CA:ACM Press,2001.279-285.
[89]ZHANG H.SATO:An efficient propositional prover[C]//Proceeding of the 14~(th) International Conference on Automated Deduction,North Queensland,Australia:ACM and IEEE Computer Society,1997:272-275.
[90]LIU Tao,LI Guo-jie.Multi-stage search rearrangement algorithm for solving SAT problem[J].Journal of Software,1996.7(4),201-210.
[91]LIANG Dong-min,WU Ye,MA Shaohan.An efficient local search algorithm for structured SAT problem[J].Chinese Journal of Computers,1998,21(8):394-397.
[92]EEN N,SORENSSON N.An extensible SAT solver[C]//Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing,Santa Margherita Ligure:[s.n.],2003:502-518.
[93]邓雨春,杨士元,王红,等.在形式验证和ATPG中的布尔可满足性问题[J]计算机辅助设计与图形学学报,2003,15(10):1207-1212.
[94]MARQUES-SILVA J P,SAKALLAH K A.Boolean satisfiability in electronic design automation[C]// Proceedings of the 39th Design Automation Conference,Piscataway:IEEE Press,2002:675-680.
[95]SELMAN B,LEVESQUE H,MITCHELL D.A new method for solving hard satisfiability problems[C]// Proceedings Of the 10~(th) National Conference on Artificial Intelligence,Menlo Park,CA:AAAI Press,1992:440-446.
[96] FRANK J. Weighting for godot: learning heuristic for GSAT [C]//Proceedings Of National Conference on Artificial Intelligence, Oregon: AAAI Press 1996:338-343.
[97]SHANG Y, WAH B W. A discriete lagrangian-based global-search method for solving satifiability problems [J]. Journal of Global Optimization, 1998,12:61-99.
[98]SHANG Y, WAH B W. Improving the performance of discrete lagrange-multiplier search for solving hard SAT problems [C]//Proceedings Of IEEE 10~(th) International Conference on Tools with Artificial Intelligence,Taipei, China : IEEE press ,1998: 176-183
[99] DAVIS M, PUTNAM H. A computer procedure for quantification theory [J]. Journal of ACM, 1960, 7:201-214.
[100] DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theorem-proving [J]. Communication of ACM, 1962, 5(7): 394-397.
[101] BURO M, KLEINE-BUNING H. Report on a SAT competition [J]. Bulletin of the European Association for Theoretical Computer Science.1993,49:143-151.
[102]JEROSLOW R G, WANG J. Solving propositional satisfiability problems [J].Annals of Mathematics and Artificial Intelligence. 1990, 1:167-188
[103] FREEMAN J W. Improvements to prepositional satisfiability search algorithms [D]. Pennsylvania: University of Pennsylvania, 1995.
[104]FALLAH F, DEVADAS S, KEUTZER K. Functional vector generation for HDL models using linear programming and 3-satisfiabillty[C]// Proceedings of the 35th Design Automation Conference, San Francisco, CA: ACM Press,1998: 528-533.
[105]FALLAH F. Coverage directed validation of hardware models [D]. CamM dge, Massachusetts: Massachusetts Institute of Technology. 1999.
[106]ZENGz, KALLAz, CIESIELSKIM. "LPSAT: a unified approach to RTL satisfiability[C]// Proceedings of the Conference on Design Automa tion and Test in Europe, New York: ACM Press,2001: 398-402.
[107]KUEHLMANN A, GANAI M K, and PARUTHI V. Circuit-based boolean reasoning[C]// Proceedings of 2001 ACM/IEEE Design Automation Conference, Anaheim, CA: ACM Press, 2001: 232-237.
[108] ZHANG H, STICKEL M. An efficient algorithm for unit propagation[C]//Proceeding of the Fourth International Symposium on Artificial Intelligence and Mathematics. Florida: [s. n.], 1996: 166-179.
[109]STALLMAN R, SUSSMAN G. Forward reasoning and dependency directed backtracking in a system for computer aided circuit analysis [J]. Artificial Intelligence, 1977, 9(2): 135-196.
[110]LU F, WANG L-C, CHENG K-T, et al. A signal correlation guided ATPG solver and its applications for solving difficult industrial cases[C]//Proceedings of 2003 ACM/IEEE Design Automation Conference, Anaheim: [s. n.], Jun. 2003:668-673.
[111]STRICHMAN O. On solving presburger and linear arithmetic with SAT[C]//Proceedings of International Conference on Formal Methods in Computer-Aided Design, OR, Portland: [s. n.], Jan. 2002,2517:160-169.
[112]BARRETT C, DILL D L, and LEVITT J. Validity checking for combinations of theories with equality [C]//Proceedings of the first International Conference on Formal Methods in Computer-Aided Design, California:Springer-Verlag, 1996,1166:187-201.
[113]FILLIATRE J-C, OWRE S, RUE/3 H, et al. ICS: Integrated canonization and solving[C]// Proceedings of the Computer Aided Verification Conference,Paris: Springer-Verlag, July 2001, 2102: 246-249.
[114]SESHIA S, LAHIRI S, and BRYANT R. A hybrid SAT-based decision procedure for separation logic with uninterpreted functions[C]// Proceedings of the ACM/IEEE Design Automation Conference, Anaheim, California:ACM,Jun. 2003: 425-430.
[115]AUDEMARD G, BERTOLI P, CIMATTI A, et al. A SAT based approach for solving formulas over Boolean and linear mathematical propositions[C]//Proceedings of 18th International Conference on Automated Deduction, Copenhagen: Springer Verlag.2003, 2392: 195-210.
[116]LIU C, KUEHLMANN A, and MOSKEWICZ M. CAMA: a Multi-Valued Satisfiablity Solver[C]// Proceedings of the International Conference on Computer-Aided Design, CA, USA: IEEE Computer Society / ACM, Nov.2003:326-333.
[117] HUANG C-Y and CHENG K-T. Using word-level ATPG and modular arithmetic constraint-solving for assertion property checking [J].IEEE Transactions on Computer-Aided Design, June 2001:381-391.
[118] GHOSH I, and FUJITA M. Automatic test pattern generation for functional register-transfer level circuits using assignment decision diagrams [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits &Systems, March 2001:402-415.
[119]PARTHASARATHY G, IYER M, CHENG K-T, et al. An Efficient Finite-domain Constraint Solver for RTL Circuits[C]// Proceedings of the ACM/IEEE Design Automation Conference, New York: ACM Press, 2004:212-217.
[120]GANZINGER H, HAGEN G, and NIEUWENHUIS R, et al. DPLL (T): Fast decision procedures[C]//Proceedings of the Computer Aided Verification Conference, Boston: Springer Verlag, 2004:26-37.
[121] ABRAMOVICI M, BREUER M A., and FRIEDMAN A D. Digital systems testing and testable design [M]. Computer Science Press, 1990.
[122]GIRODIAS P, CERNY E, and OLDER W. Solving linear, min and max constraint systems using CLP based on relational interval arithmetic [J].Theoretical Computer Science, Feb. 1997,173(2):253-281.
[123] KELLY W, MASLOW V, PUGH W, et al. The omega library v1.1.0: interface guide[R]. Department. Of Computer Science, University of Maryland,College Park, November 1996.