基于PSA的集成电路形式验证方法研究
|
摘要
现今社会已是海量信息的世界，而支持处理这些信息的最主要物质基础是数字芯片。为了满足日益复杂的系统功能需求，数字电路的设计工作遇到了前所未有的挑战。在数字电路设计流程中，为确保数字电路功能的正确性与完整性，验证工作的重要作用越来越突显，特别是在设计过程中的早期阶段，对系统进行正确的功能验证对该系统的成功开发有着至关重要的意义。数字电路形式验证方法由于具有抽象级别高、建模能力强的特点，特别适合数字电路设计流程中的顶层设计的功能验证问题。目前业界常用的验证方法已经不能完全满足现代设计工作的需要，因此系统研究形式验证方法有其特有的现实意义。本文以多项式符号代数（Polynomial SymbolicAlgebra, PSA）理论为基础，针对于数字电路，研究适合算术密集型产品的形式验证方法。
（1）为解决数字芯片设计中模型检验问题，提出基于多项式理论的定界模型检验方法。首先，给出基于多项式形式的电路功能的统一描述。为了能够采用多项式形式描述电路功能，本文在传统的电路控制逻辑描述方法的基础上，将其进一步扩展，将传统方法中的原子命题转化为多项式形式，将布尔特征函数转化为多项式集合的形式。这样，可以与电路数据通路部分建立统一的多项式描述形式。其次，通过建立高级语言的关系模型，给出了电路在高层次描述中目标性质的抽取方法，通过该方法形成待验证性质的多项式形式描述，从而形成了待验证性质与电路功能统一的多项式形式。基于以上两点，本文将定界模型检验问题转化为基于多项式理论的定理证明问题。并采用计算多项式集合良好三角列的方法解决定理证明问题。与传统方法相比，本文方法可在电路高级别抽象上直接进行定界模型检验。
（2）为解决数字芯片的数据通路RTL级模型与优化后的RTL级描述之间的等价性检验问题，提出基于多项式理论的等价性验证方法。首先，证明了多项式集合零点集与数据通路等价的关系。将数据通路看作黑盒结构，只考虑输入/输出关系，因此，两个数据通路功能等价，可看作对同一组输入，两个数据通路有相同输出。为此，将多项式集合的解集合看作是多维空间中的点，通过多项式代数簇理论，将空间的点向平面投影，从代数的角度证明了数据通路等价与多项式集合零点集的关系。其次，给出判定多项式集合零点集相等的代数方法。采用多项式理想理论处理零点集等价判定问题，并利用理想良性基的可计算性给出了具体的判定过程。基于以上两点，本文提出验证高级别数据通路功能等价性的求解算法。
（3）为提高数字芯片的验证速度，提出基于多项式理论的模块化验证方法。首先，采用模块化的形式描述电路的结构。其次，给出模块化的电路功能计算方法。从基本门电路或电路基本部件出发，从电路模块化的结构描述中获得各个部件的相互约束关系，并以多项式代数中的消元与扩张原理为基础，逐级递归地计算出每一个电路节点的多项式集合的消元理想的Gr bner基，最终获得电路的整体功能描述。基于以上两点，提出基于模块化思想的电路验证问题的代数求解算法。
基于Maple等工具建立实验系统，针对上述算法进行了实验研究。实验结果表明，针对算术密集型电路，本文基于PSA的方法在验证效率上要优于传统方法。
Today’s society is a world which people have to face a lot of information, What helpspeople to deal with those information is the industry of the integrated circuit(IC), It is a greatchallenge of the design in the IC that the systerm must to meet to the use’s demands. In theflowing of the design of IC, How to ensure the IC’s complentment and correntment of thechip’s functiong is more and more a key point. The verification methods which currently usedin the industry of IC are not meeting the demand of the design work. It has more importantsignificance that we can ensure correntment of the IC in the errly phase of the flowing ofdesign. Because the formal verification mathods have the fearures, One it can abstract the IC’sfunction at high level. Anther it has a good description of the model of the IC. It is especiallysutable for the work of verification in design of early phase. Research on formal verificationmethods have the actual significance. In this paper, We based on the polynomial symbolicalgebra to study on those problems, Especially major to the arithmetic intensive digital IC wedo some work:
(1) In order to achieve model checking of the digital chip, We propose a method of thebound model checking(BMC) based on the polynomial theory. In that method, First, We givean unified description for the circuit function based on the polynomial theory. In order todescription the circuit function with the the polynomial theory, We develop the traditiondescription method of the control logic of the circuit. We use the polynomial to representationthe atomic proposition and transform the boolean characteristic function into a set ofpolynomial. So, We can describe the circuit function with the polynomial. Secend, We give arelation model about the high level language. With the model we transfer the designspecification to the description with the relation model, and extract the target property, and awe get the description of the property with polymomial. At the same time, We get an unifieddescription with the polymomial about the he circuit function and target property. Based onthose two points, we can tramsfer the tradition BMC problem into a problem of the theoremproving, and with calculating the set of polynomial’ well triangular column to solve thetheorem proving. The method in the thesis can do BMC direct at the high level abstractcontrast the tradition method.
(2) In order to verification the datapaths of the digital chip function’s equivalance which is between the RTL level description and optimized RTL description, We propose a newmethod about the datapath based on polynomial theory. First, We prove the equivalencerelationship between the zero set of polynomial sets and the equivalence of datapath. Theequivalence of the two datapaths mean that the circuit has a same output with the same input.When we see the circuit as a black box. So, We can see the solution set of polynomial as thepoint of a multidimensional space. Based on the theory of algebra cluster, We prove theequivalence relationship between the equivalence of datapath and the zero set of polynomialsets from the view of the algebra. Secend, We give the algebra method to judge the equal of thetwo zero sets of polynomial sets, And we use the theory of polynomial idea and the wellbehaved basid of the idea to judge that problem. Based on those two points, We propose theequivalence algorithm about the high level datapath.
(3) In order to enhance the speed of the verification, We propose a module method aboutthe digital chip verification based on polynomial theory. First, We describe the structure of thecircuit based on a module form. Secend, We propose a method to calculate the function ofcircuit from the view of the module point. starting from the gate circuit or the circuitcomponent and get the structure information from the module description, We can recursivecalculate every circuit node’ function which have the form of the Grobner of the eliminatinideal about the polynomial ste based on the theory of the theory of eliminatin and expandment.At last, We get the the function of whole circuit. Based on those two points, We propose analgebra algorithm of the circuit verification based on module form.
We build a experiment systerm with Maple and study those algorithms. The he result ofthe experiment shows that the verification efficiency of the method based an the PSA is betterthan the the tradition method towards the arithmetic intensive IC.
（1）为解决数字芯片设计中模型检验问题，提出基于多项式理论的定界模型检验方法。首先，给出基于多项式形式的电路功能的统一描述。为了能够采用多项式形式描述电路功能，本文在传统的电路控制逻辑描述方法的基础上，将其进一步扩展，将传统方法中的原子命题转化为多项式形式，将布尔特征函数转化为多项式集合的形式。这样，可以与电路数据通路部分建立统一的多项式描述形式。其次，通过建立高级语言的关系模型，给出了电路在高层次描述中目标性质的抽取方法，通过该方法形成待验证性质的多项式形式描述，从而形成了待验证性质与电路功能统一的多项式形式。基于以上两点，本文将定界模型检验问题转化为基于多项式理论的定理证明问题。并采用计算多项式集合良好三角列的方法解决定理证明问题。与传统方法相比，本文方法可在电路高级别抽象上直接进行定界模型检验。
（2）为解决数字芯片的数据通路RTL级模型与优化后的RTL级描述之间的等价性检验问题，提出基于多项式理论的等价性验证方法。首先，证明了多项式集合零点集与数据通路等价的关系。将数据通路看作黑盒结构，只考虑输入/输出关系，因此，两个数据通路功能等价，可看作对同一组输入，两个数据通路有相同输出。为此，将多项式集合的解集合看作是多维空间中的点，通过多项式代数簇理论，将空间的点向平面投影，从代数的角度证明了数据通路等价与多项式集合零点集的关系。其次，给出判定多项式集合零点集相等的代数方法。采用多项式理想理论处理零点集等价判定问题，并利用理想良性基的可计算性给出了具体的判定过程。基于以上两点，本文提出验证高级别数据通路功能等价性的求解算法。
（3）为提高数字芯片的验证速度，提出基于多项式理论的模块化验证方法。首先，采用模块化的形式描述电路的结构。其次，给出模块化的电路功能计算方法。从基本门电路或电路基本部件出发，从电路模块化的结构描述中获得各个部件的相互约束关系，并以多项式代数中的消元与扩张原理为基础，逐级递归地计算出每一个电路节点的多项式集合的消元理想的Gr bner基，最终获得电路的整体功能描述。基于以上两点，提出基于模块化思想的电路验证问题的代数求解算法。
基于Maple等工具建立实验系统，针对上述算法进行了实验研究。实验结果表明，针对算术密集型电路，本文基于PSA的方法在验证效率上要优于传统方法。
Today’s society is a world which people have to face a lot of information, What helpspeople to deal with those information is the industry of the integrated circuit(IC), It is a greatchallenge of the design in the IC that the systerm must to meet to the use’s demands. In theflowing of the design of IC, How to ensure the IC’s complentment and correntment of thechip’s functiong is more and more a key point. The verification methods which currently usedin the industry of IC are not meeting the demand of the design work. It has more importantsignificance that we can ensure correntment of the IC in the errly phase of the flowing ofdesign. Because the formal verification mathods have the fearures, One it can abstract the IC’sfunction at high level. Anther it has a good description of the model of the IC. It is especiallysutable for the work of verification in design of early phase. Research on formal verificationmethods have the actual significance. In this paper, We based on the polynomial symbolicalgebra to study on those problems, Especially major to the arithmetic intensive digital IC wedo some work:
(1) In order to achieve model checking of the digital chip, We propose a method of thebound model checking(BMC) based on the polynomial theory. In that method, First, We givean unified description for the circuit function based on the polynomial theory. In order todescription the circuit function with the the polynomial theory, We develop the traditiondescription method of the control logic of the circuit. We use the polynomial to representationthe atomic proposition and transform the boolean characteristic function into a set ofpolynomial. So, We can describe the circuit function with the polynomial. Secend, We give arelation model about the high level language. With the model we transfer the designspecification to the description with the relation model, and extract the target property, and awe get the description of the property with polymomial. At the same time, We get an unifieddescription with the polymomial about the he circuit function and target property. Based onthose two points, we can tramsfer the tradition BMC problem into a problem of the theoremproving, and with calculating the set of polynomial’ well triangular column to solve thetheorem proving. The method in the thesis can do BMC direct at the high level abstractcontrast the tradition method.
(2) In order to verification the datapaths of the digital chip function’s equivalance which is between the RTL level description and optimized RTL description, We propose a newmethod about the datapath based on polynomial theory. First, We prove the equivalencerelationship between the zero set of polynomial sets and the equivalence of datapath. Theequivalence of the two datapaths mean that the circuit has a same output with the same input.When we see the circuit as a black box. So, We can see the solution set of polynomial as thepoint of a multidimensional space. Based on the theory of algebra cluster, We prove theequivalence relationship between the equivalence of datapath and the zero set of polynomialsets from the view of the algebra. Secend, We give the algebra method to judge the equal of thetwo zero sets of polynomial sets, And we use the theory of polynomial idea and the wellbehaved basid of the idea to judge that problem. Based on those two points, We propose theequivalence algorithm about the high level datapath.
(3) In order to enhance the speed of the verification, We propose a module method aboutthe digital chip verification based on polynomial theory. First, We describe the structure of thecircuit based on a module form. Secend, We propose a method to calculate the function ofcircuit from the view of the module point. starting from the gate circuit or the circuitcomponent and get the structure information from the module description, We can recursivecalculate every circuit node’ function which have the form of the Grobner of the eliminatinideal about the polynomial ste based on the theory of the theory of eliminatin and expandment.At last, We get the the function of whole circuit. Based on those two points, We propose analgebra algorithm of the circuit verification based on module form.
We build a experiment systerm with Maple and study those algorithms. The he result ofthe experiment shows that the verification efficiency of the method based an the PSA is betterthan the the tradition method towards the arithmetic intensive IC.
引文
[1] Semiconductor Industry Association. International Technology Roadmap forSemiconductors, Design Chapter,2011Edition [EB/OL]. http://www.itrs.net.
[2] Bryant R E. Graph Based Algorithms for Boolean Function Manipulation. IEEETransactions on Computers.1986, C-35:677–691P
[3] Clarke E, Fujita and Zhao X. Hybrid Decision Diagrams. In Proceeding of InternationalConference on Computer Aided Design (ICCAD), San Jose, California, USA.1995:159-163P
[4] Lai Y T, Pedram M, Vrudhula S B K. Formal Verification Using Edge-Valued BinaryDecision Diagrams. IEEE Transcations on Computers.1996,45(2):247-255P
[5] Chen Z. On polynomial functions fromZ n1×Z n2××Znrto Zm. Discrete Math.1996,162(1-3):67-76P
[6] Narayan A, Jain J and Fujita M. Partitioned ROBDDs-A Compact, Canonical andEfficiently Manipulable Representation for Boolean Functions. In Proceeding ofInternational Conference on Computer Aided Design (ICCAD), San Jose, California,USA.1996:547-554P
[7] Tafertshofer P and Pedram M. Factored Edge-Valued Binary Decision Diagrams. FormalMethods in System Design.1997,10(2-3):243-270P.
[8] Clarke E, Fujita M and Mcgeer P. Muti Terminal Binary Decision Diagrams: An EfficientData Structure for Matrix Representation. Formal Methods in System Design.1997,10(4):149-169P
[9] Dreschler R, Becher B and Ruppertz S. The K*BMD: A Verification Data structure. IEEEDesign&Test.1997,14(2):51-59P
[10] Becker B, Drechsler R and Enders R. On the Representational Power of Bit-Level andWord-Level Decision Diagrams. In Proceedings of Asia and South Pacific DesignAutomation Conference (ASP-DAC), Chiba, Japan.1997:461-467P
[11] Drechsler R, Sauerhoff M and Sieling D. The Complexity of the Inclusion Operation onOFDD's. IEEE Transactions on Computer-Aided Design of Integrated Circuits andSystems.1998,17(5):457-459P
[12] Drechsler R and Horeth S. Manipulation of*BMD. In Proceeding of Asia and SouthPacific Design Automation Conference (ASP-DAC), Yokohama, Japan.1998:433-438P
[13] Smith J and Micheli D G. Polynomial Methods for Component Matching and Verification.In Proceeding of International Conference on Computer Aided Design (ICCAD). San Jose,California, USA.1998:678-685P
[14] Drechsler R and Becker B. Ordered Kronecker Functional Decision Diagrams-a DataStructure for Representation and Manipulation of Boolean Functions. IEEE Transactionson Computer-Aided Design of Integrated Circuits and Systems.1998,17(10):965-973P
[15] Smith J and Micheli D G. Polynomial Methods for Allocating Complex Components. InProceedings of Design, Automation and Test in Europe (DATE), Munich, Germany.1999:217-222P
[16] Horeth S and Drechsler. Formal Verification of Word-Level Specifications. In InProceedings of Design, Automation and Test in Europe (DATE), Munich, Germany.1999:52–58P
[17] Biere A, Cimatti A, Clarke E and Zhu Y. Symbolic Model Checking without BDDs. InProceedings of International Conference on Tools and Algorithms for the Constructionand Analysis of Systems (TACAS), Amsterdam, the Netherlands.1999:193-207P
[18] Smith J and Micheli D G. A Methodology for Synthesis with Reusable Components froman Arithmetic Specification, In Proceedings of European Conference on Circuit Theoryand Design (ECCTD), Stresa, Italy.1999:1195-1198P
[19]张健.逻辑公式的可满足性判定—方法、工具及应用.北京：科学出版社，2000年
[20] Smith J. Allocation and Interface Synthesis Algorithms for Component-Based Design.Technical Report. No.: CSL-TR-00-793,2000:32-58P
[21] Smith J and Micheli D G. Polynomial Circuit Models for Component Matching inHigh-level Synthesis. IEEE Transactions on Very Large Scale Integration (VLSI) Systems.2001,9(6):783-799P
[22] Clarke E, Biere A, Raimi R and Zhu Y. Bounded Model Checking Using SatisfiabilitySolving. Formal Methods in System Design,2001,19(1):7-34P
[23] Bentley B. Validating the Intel Pentium4Microprocessor. In Proceedings of DesignAutomation Conference (DAC), Las Vegas, USA,2001:244-248P
[24] Moskewicz M, Madigan C, Zhao Y, Zhang L and Malik S. Chaff: Engineering an EfficientSAT Solver. In Proceedings of Design Automation Conference (DAC). Las Vegas, USA2001:530-535P
[25] C Kern C. Formal Verification in Hardware Design: A Survey. ACM Transactions onDesign Automation of Electronic Systems.2001,4(2):123-193P
[26]王东明.消去法及其应用.北京：科学出版社，2002年:223-235P
[27] Bryant R E and Chen Y A. Verification of Arithmetic Circuits Using Binary MomentDiagrams. International Journal on Software Tools for Technology Transfer (STTT).2001,3(2):137-155P
[28] Minato, S. Streaming BDD Manipulation. IEEE Transactions on Computers.2002,51(5):474-485P
[29] Joao P M and Karem A S. Boolean Satisfiablity in Electornic Design Automation. InProceedings of Design Automation Conference (DAC), Los Angeles, California, USA.2003:675-680P
[30]严晓浪，郑飞君，葛海通，杨军.结合二叉判决图和布尔可满足性的等价性验证算法.电子学报.2004,32(8):1233-1235页
[31]李光辉,李晓维.基于增量可满足性的等价性检验方法.计算机学报.2004,27(10):1388-1394页
[32] Goldberg E and BerkMin N Y. A Fast and Robust SAT Solver. In Proceedings of DesignAutomation and Test in Europe Conference and Exhibition (DATE). Paris, France.2004:142-149P
[33]李光辉，邵明，李晓维.电路宽度制导的布尔推理.计算机辅助设计与图形学学报.2004,16(11):1568-1574页
[34] Radecka K and Zilic Z. Arithmetic Transforms for Verifying Compositions of SequentialDatapaths. In Proceedings of IEEE International Conference on Computer Design (ICCD),Austin, Texas, USA.2005:348-353P
[35]丁敏，唐璞山，周电.结合高级正向推理过程的可满足性问题解决器.中国科学E辑.2005,35(4):426—438页
[36] Park J, Pixley C. Burns M and Cho H. An Efficient Logic Equivalence Checker forIndustrial Circuits. Journal of Electronic Testing: Theory and Applications.2005,16(1):91-106P
[37]郑飞君，严晓浪，葛海通等.使用布尔可满足性的组合电路等价性验证算法.电子信息学报.2005,27(4):651-654页
[38] Kapur D and Cai Y Y. An Algorithm for Computer a Gr bner Basis of a Polynomial Idealover a Ring with Zero Divisors. Technical Report. No.: TR-CS-2003-43,2005:1-44P
[39]卢永江，竺红卫，严晓浪，葛海通.利用改善的静态隐含策略加速等价性验证.电路与系统学报.2005,10(3):47-51页
[40] Ozguner F, Marhefka D, DeGroat J and Wile B. Teaching Future Verification Engineers:The Forgotten Side of Logic Design. In Proceedings of Design Automation Conference(DAC), Las Vegas, USA,2005:253-255P
[41]鲁巍，吕涛，杨修涛，李晓维.针对可观测性语句覆盖准则的RTL激励生成.计算机研究与发展.2005,42(12):2169-2175页
[42]邵明，李光辉,李晓维.求解可满足问题的调查传播算法以及步长的影响规律.计算机学报.2005,28(5):849-855页
[43] Chen Y A and Bryant R E. An Efficient Graph Representation for Arithmetic CircuitVerification. IEEE Transactions on Computer-Aided Design of Integrated Circuits andSystems.2005,20(12):1443-1454P
[44]王海霞，韩承德.整数乘法电路的形式化验证方法研究.计算机研究与发展.2005,42(3):404-410页
[45] Kinder S, Fey G and Drechsler R. Controlling the Memory during Manipulation ofWorld-Level Decision Diagrams. In Proceedings of IEEE International Symposium onMultiple-Valued Logic (ISMVL), Calgary, Canada.2005:250-255
[46]李光辉，邵明，李晓维.通用CPU设计验证中的等价性检验方法.计算机辅助设计与图形学学报.2005,17(2):230-235页
[47] Chen J C and Chen Y A. Equivalence Checking of Integer Multiplier. In Proceedings ofAsia and South Pacific Design Automation Conference (ASP-DAC), Yokohama, Japan.2006:169-174P
[48] Alizadeh B, Kakoee M R. Using integer equations for high level formal verificationproperty checking. In Proceedings of International Symposium on Quality ElectronicDesign (ISQED), San Jose, USA.2006:69-74P
[49]陈云霁，马麟，沈海华，胡伟武.龙芯2号微处理器浮点除法功能部件的形式验证.计算机研究与发展.2006,43(10):1835-1841页
[50] Keim M, Dreschler R, Becker B, Martin M and Molitor P. Polynomial Formal Verificationof Multipliers. Formal Methods in System Design.2006,22(1):39-58P
[51] Dasgupta P, Chakrabarti P P, Nandi A and Krishna S. Abstraction of Word-level LinearArithmetic Functions from Bit-level Component Description, In Proceedings of Design,Automation and Test in Europe (DATE), Munich, Germany.2006:4-8P
[52] Zeng Z, Talupuru K R and Ciesielski M. LPSAT: A Unified Approach to RTL Satisfiability.In Proceedings of Design, Automation and Test in Europe (DATE), Munich, Germany.2006:398-402P
[53]丁敏,唐璞山.改进的时间帧展开的时序电路等价验证算法.计算机辅助设计与图形学学报.2006,18(1):53-61页
[54] Guillot J, Boutillon E, Ren Q and Ciesielski M. Efficient Factorization of DSP TransformsUsing Taylor Expansion Diagrams. In Proceedings of Design, Automation and Test inEurope (DATE), Munich, Germany.2006:754-755P
[55] Jone R B and Leary J W. Practical Formal Verification in Microprocessor Design. IEEEDesign&Test of Computers.2006,18(4):16-25P
[56]郑伟伟，吴为民，边计年．基于线性规划的RTL可满足性求解和性质检验.计算机辅助设计与图形学学报.2006,18(4):538-544页
[57] Kalla P, Ciesielski M, Boutillon E and Martin E. High-level Design Verification UsingTaylor Expansion Diagrams: First Results. In Proceedings of IEEE International HighLevel Design Validation and Test Workshop (HLDVT), Monterey, California, USA.2006:13-17P
[58] Radecka K and Zilic Z. Specifying and Verifying Imprecise Sequential Datapaths byArithmetic Transforms. In Proceedings of International Conference on Computer AidedDesign (ICCAD), San Jose, California, USA.2006:128-131P
[59] C Zorian Y. Error-Free Products. IEEE Design&Test of Computers.2006,18(4):2-2P
[60]陈云霁，张健，沈海华，胡伟武.一种基于SAT的运算电路查错方法.计算机学报.2007,30(12):2082-2089页
[61] Ciesielski M, Kalla P, Zeng Z, and Rouzeyre B. Taylor Expansion Diagrams: A CompactCanonical Representation with Application to Symbolic Verification, In Proceedings ofDesign, Automation and Test in Europe (DATE), Paris, France.2007:285-289P
[62]荆明娥，周电，唐璞山，周晓方.利用近似解加速求解SAT问题的启发式完全算法.计算机辅助设计与图形学学报.2007,19(9):1184-1189页
[63]邓澍军，吴为民，边计年. RTL验证中的混合可满足性求解.计算机辅助设计与图形学学报.2007,19(3):273-278页
[64] Fey G, Drechsler R, Ciesielski M. Algorthms for Taylor expansion diagrams, InProceeding of IEEE International Symposium on Multiple-Valued Logic (ISMVL),Toronto, Canada.2007:235-240P
[65]荆明娥，周电，唐璞山，周晓方，张华.启发式极性决策算法解SAT问题.中国科学E辑.2007,37(12):1597-1606页
[66] Yang Xiaoqing, Bian jinian, Deng Shujun and Zhao Yanni. EHSAT Modeling fromAlgorithm Description for RTL Model Checking. In Proceedings of Asian TestSymposium (ATS), Beijing, China.2007:178-183P
[67]刘领一，赵阳，吕涛，李华伟，李晓维.结合ATPG和SAT的无界模型检验前像计算方法.计算机辅助设计与图形学学报.2007,19(3):376-380页
[68]杨军，卢永江，葛海通，郑飞君，严晓浪.一种避免存爆炸的组合电路等价性验证方法.电路与系统学报.2007,12(3):21-25页
[69] Raik B and Drechsler R. RTL-Datapath Verification Using Integer Linear Programming.In Proceedings of Asia and South Pacific Design Automation Conference (ASP-DAC),Bangalore, India.2008:741-746P
[70] Navarro H, Montiel-Nelson J A, Sosa J, Garcia J C and Fay D Q M. Multiplexer Modelfor RTL Satisfiability Using MILP. Electronics Letters.2008,40(7):417-418P
[71]杨志，马光胜，冯刚，邵晶波.应用吴方法进行高层次定界模型检验.计算机辅助设计与图形学学报.2008,20(2):137-143页
[72] Peymandoust A and Micheli D G. Using Symbolic Algebra in Algorithmic Level DSPSynthesis. In Proceedings of Design Automation Conference (DAC), Las Vegas, NV,USA.2008:277-282P
[73] Mao Weibo and Wu Jinzhao. Application of Wu’s Method to Symbolic Model Checking.In Proceedings of International Symposium on Symbolic and Algebraic Computation(ISSAC), Beijing, China.2008:237-244P
[74]杨军，翁延龄，葛海通，严晓浪.利用状态缓存的时序等价性验证算法.计算机辅助设计与图形学学报.2008,20(2):149-154页
[75] Radecka K and Zilic Z. Design Verification by Test Vectors and Arithmetic TransformUniversal Test Set. IEEE Transctions on Computers.2008,53(5):628-640P
[76] Stoffel D, Kunz W. Equivalence Checking of Arithmetic Circuits on the Arithmetic BitLevel. IEEE Transactions on Computer-Aided Design of Integerated Circuits and Systems.2008,23(5):586-597P
[77] Pradhan D K, Askar S and Ciesielski M. Mathematical Framework for RepresentingDiscrete Functions as Word-level Polynomials. In Proceeding of IEEE International HighLevel Design Validation and Test Workshop (HLDVT), San Francisco, California, USA.2008:135-139P
[78] Ciesielski M, kalla P, Askar S. Taylor Expansion Diagrams: A Canonical Representationfor Verification of Data Flow Designs, IEEE Transactions on Computers.2009,55(9):1188-1201P
[79] Lu Wei, Yang Xiutao, Lv Tao and Li Xiaowei. An Efficient Evaluation and VectorGeneration Method for Observablity-Enhanced Satament Coverage. Journal of ComputerScience and Technology.2009,20(6):875-884P
[80] Rgomez-Prado D, Ren Q, Askar S, Ciesielski M, Boutillon E. Variable Ordering forTaylor Expansion Diagrams. In Proceedings of IEEE International High Level DesignValidation and Test Workshop (HLDVT), Sonoma Valley, California, USA.2009:55-59P
[81] Iyer M K, Parthasarathy G and Cheng K T. Efficient Conflict-Based Learning in an RTLCircuit Constraint Solver. In Proceedings of Design, Automation and Test in Europe(DATE), Munich, Germany.2009:666-671P
[82] Prasad M, Biere A and Gupta A, A Survey of Recent Advances in SAT-based FormalVerification. Software Tools for Technology Transfer.2009,7(2):156-173P
[83] Babic D and Musuvathi M. Modular Arithmetic Decision Procedure. Technical Report.No.: MSR-TR-2005-114,2009:1-10P
[84] Hungerbuehler N and Specker E. A Generalization of the Smarandache Function toSeveral Variables. Integers: Electronic Journal of Combinatorial Number Theory.2009,6(1):#A23
[85] Deng Shujun, Bian jinian, Wu weimin, Yang Xiaoqing and Zhao Yanni. EHSAT: AnEfficient RTL Satisfiability Solver Using an Extended DPLL Procedure. In Proceedings ofDesign Automation Conference (DAC), San Diego, California, USA.2009:588-593P
[86] Velev N M. Integrating Formal Verification into an Advanced Computer ArchitectureCourse. IEEE Transactions on Education.2009,48(2):216-222P
[87] Radecka K and Zilic Z. Arithmetic Transforms for Compositions of Sequential andImprecise Datapaths. IEEE Transactions on Computer-Aided Design of IntegratedCircuits and Systems,2009.25(7):1382-1391P
[88] Peymandoust A and Micheli D G. Application of Symbolic Computer Algebra inHigh-level Data-Flow Synthesis, IEEE Transctions on Computer-Aided Design ofIntegrated Circuits and Systems.2009,22(9):1154-1165P
[89] Hosangadi A, Fallah F and Kastner R. Factoring and Eliminating CommonSubexpressions in Polynomial Expressions. In Proceeding of International Conference onComputer Aided Design (ICCAD), San Jose, California, USA.2009:169-174P
[90] Hosangadi A, Fallah F and Kastner R. Reducing Hardware Complexity of Linear DSPSystems by Iteratively Eliminating Two-Term Common Subexpressions. In Proceedingsof Asia and South Pacific Design Automation Conference (ASP-DAC), Shanghai, China.2009:532-528P
[91] Lee D U, Gaffar A A, Cheung R C C, Mencer O, Luk W and Constantinides G A.Accuracy-Guaranteed Bit-Width Optimization. IEEE Transactions on Computer-AidedDesign of Integrated Circuits and Systems.2009,25(10):1990-2000P
[92] Ugarte I and Sanchez P. Assertion Checking of Behavioral Descriptions with Non-linearSolver. In Proceedings of International Conference on Computer Design (ICCD), San Jose,California, USA,2009.229-231P
[93] Hosangadi A, Fallah F and Kastner R. Common Subexpression Elimination InvolvingMultiple Variables for Linear DSP Synthesis. In Proceedings of15th IEEE InternationalConference on Application-Specific Systems, Architectures and Processors, Galveston,Texas, USA.2009:202-212P
[94] Shekhar N, Kalla P, Enescu F and Gopalakrishnan S. Equivalence Verification ofPolynomial Datapaths with Fixed-Size Bit-Vectors Using Finite Ring Algebra. InProceeding of International Conference on Computer Aided Design (ICCAD), San Jose,California, USA.2009:291-296P
[95] Wedler M, Stoffel D, Brinkmann R and Kunz W. A Normalization Method for ArithmeticData-Path Verification. IEEE Transactions on Computer-Aided Design.2009,26(11):1909-1922P
[96] Kroening D and Seshia S A. Formal Verification at Higher Levels of Abstraction. InProceedings of International Conference on Computer-Aided Design (ICCAD), San Jose,California, USA.2010:572-578P
[97] Peymandoust A and Micheli D G. Symbolic Algebra and Timing Driven Data-flowSynthesis. In Proceedings of International Conference on Computer Aided Design(ICCAD), San Jose, California, USA.2010:300-305P
[98] Drechsler R, Fey G and Kinder S. An Integrated Approach for Combining BDD and SATProvers. In Proceedings of International Conference on VLSI Design (VLSID),Hyderabad, India.2010:237-242P
[99] Disch S and Schollm C. Combinational Equivalence Checking Using Incremental SATSolving, Output Ordering, and Resets. In Proceedings of Asia and South Pacific DesignAutomation Conference (ASP-DAC), Yokohama, Japan.2010:938-943P
[100] Zeng Z, Talupuru K R and Ciesielski M. Function Test Generation Based on Word-levelSAT. Journal of Systems Architecture.2010,51(8):488-511P
[101] Peymandoust A, Simunic T and Micheli D G. Complex Library Mapping for EmbeddedSoftware Using Symbolic Algebra, In Proceedings of Design Automation Conference(DAC), New Orleans, Los Angeles, USA.2010:325-330P
[102] Gopalakrishnan S and Kalla P. Optimization of Polynomial Datapaths Using Finite RingAlgebra. ACM Transactions on Design Automation of Electronic System.2010,12(4):Article No49
[103] Raudvere R, Singh K A, Sander I and Jantsch A. System Level Verification of DigitalSignal Processing Application Based on the Polynomial Abstraction Technique. InProceedings of International Conference on Computer Aided Design (ICCAD), San Jose,CA, USA.2010:285-290P
[104] Shekhar N, Kalla P, Enescu F and Gopalakrishnan S. Exploiting Vanishing Polynomialfor Equivalence Verification of Fixed-Size Arithmetic Datapaths. In Proceedings ofIEEE International Conference on Computer Design (ICCD), San Jose, CA, USA.2010:215-220P
[105] Shekhar N, Kalla P and Enesu F. Equivalence Verification of Polynomial DatapathsUsing Ideal Membership Testing. IEEE Transactions on Computer-Aided Design ofIntegrated Circuits and Systems.2010,26(7):1320-1330P
[106] Du Zhenjun, Ma Guangsheng and Feng Gang. A New Model for Verification. Journal ofHarbin Institute of Technology.2010,14(3):305-310P
[107] Hosangadi A, Fallah F and Kastner R. Optimizing Polynomial Expressions by AlgebraicFactorization and Common Subexpression Elimination, IEEE Transctions onComputer-Aided Design of Integrated Circuits and Systems.2010,25(10):2012-2022P
[108] Shekhar N, Kalla P, Meredith B and Enescu F. Simulation Bounds for EquivalenceVerification of Arithmetic Datapaths with Finite Word-Length Operands. In Proceedingsof International Conference Formal Methods in Computer-Aided Design (FMCAD), SanJose, California, USA.2010:179-186P
[109] Sasao T and Nagayama S. Representations of Elementary Functions Using BinaryMoment Diagrams. In Proceedings of IEEE International Symposium on Multiple-ValuedLogic (ISMVL), Singapore.2010:28-33P
[110] Brickenstein M, Dreyer A, Greuel G M, Wedler M and Wienand O. New Developmentsin the Theory of Grobner Bases and Application to Formal Verification. http://arxiv.org/PS_cache/arxiv/pdf/0801/0801.1177v2.pdf
[111] Watanabe Y, Homma N, Aoki T and Higuchi T. Application of Symbolic ComputerAlgebra to Arithmetic Circuit Verification. In Proceedings of International Conferenceon Computer Design (ICCD), Lake Tahoe, California, USA.2010:25-32P
[112] Wienand O. The Gr bner Basis of the Ideal of Vanishing Polynomials. http://arxiv.org/PS_cache/arxiv/pdf/0709/0709.2978v1.pdf
[113] Wienand O, Wedler M, Stoffel D, Kunz W and Greuel G. An Algebra Approach forProving Data Correctness in Arithmetic Data Paths. In Proceedings of InternationalConference on Computer Aided Verification (CAV), Princeton USA.2010:473-486P
[114] Peymandoust A, Simunic T and Micheli D G. Complex Instruction and Software LibraryMapping for Embedded Software Using Symbolic Algebra, IEEE Transactions onComputer-Aided Design of Integrated Circuits and Systems.2011,22(8):964-975P
[115] Semiconductor Industry Association. International Technology Roadmap forSemiconductors, Design Chapter,2011Edition [EB/OL]. http://www.itrs.net.
[116] Peymandoust A, Simunic T and Micheli D G. Low Power Embedded SoftwareOptimization Using Symbolic Algebra, In Proceedings of Design, Automation and Testin Europe (DATE), Paris, France.2011:1052-1058P
[117] Bhadra J, Abadir M S and Ray S. A Survey of Hybrid Techniques for FunctionalVerification. IEEE Design&Test of Computers.2011,24(2):112-122P
[118] Raudvere R, Singh K A, Sander I and Jantsch A. Polynomial Abstraction for Verificationof Sequentially Implemented Combinational Circuits. In Proceedings of Design,Automation and Test in Europe (DATE), Paris, France.2011:690-691P
[119] Shekhar N, Kalla P, Mereduth M B and Enesu F. Simulation Bounds for EquivalenceVerification of Polynomial Datapaths Using Finite Ring Algebra. IEEE Transactions onVery Large Scale Integration (VLSI) Systems.2011,16(5):517-527P
[120] Gopalakrishnan S and Kalla P. Integrating Common Sub-Expression Elimination withAlgebraic Methods for Polynomial System Synthesis. In Proceedings of InternationalWorkshop on Logic and Synthesis (IWLS), Lake Tahoe, California, USA,2011:31-37P
[121] Li Xiaowei, Li Guanghui and Shao Ming. Formal Verification Technique Based onBoolean Satisfiability Problem. Journal of Computer Science and Technology.2011,20(1):38-47P
[122] Gopalakrishnan S, Kalla P and Mereduth M B. Finding Linear Building-Blocks for RTLSynthesis of Polynomial Datapaths with Fixed-Size Bit-Vectors. In Proceedings ofInternational Conference on Computer-Aided Design (ICCAD), San Jose, California,USA.2011:413-418P
[123] Peymandoust A, Pozzi L, Ienne P and Micheli D G. Automatic Instruction Set Extensionand Utilization for Embedded Processors. In Proceedings of IEEE InternationalConference on Application-Specific Systems, Architectures and Processors.2011:108-118P
[124] Shekhar N, Kalla P and Enescu F. Equivalence Verification of Arithmetic Datapaths withMultiple Word-Length Operands, In Proceedings of Design, Automation and Test inEurope (DATE), Munich, Germany.2011:824-829P
[125] Hosangadi A, Fallah F and Kastner R. Energy Efficient Hardware Synthesis ofPolynomial Expressions. In Proceedings of International Conference on VLSI Design(VLSID), Kolkata, India.2011:653-658P
[126]边计年，薛宏熙，苏明，吴为民.数字系统设计自动化.北京：清华大学出版社，2005年:231-247P
[127] Hosangadi A, Fallah F and Kastner R. Optimizing High Speed Arithmetic Circuit UsingThree-Term Extraction, In Proceedings of Design, Automation and Test in Europe
(DATE), Munich, Germany.2011:1294-1299P
[2] Bryant R E. Graph Based Algorithms for Boolean Function Manipulation. IEEETransactions on Computers.1986, C-35:677–691P
[3] Clarke E, Fujita and Zhao X. Hybrid Decision Diagrams. In Proceeding of InternationalConference on Computer Aided Design (ICCAD), San Jose, California, USA.1995:159-163P
[4] Lai Y T, Pedram M, Vrudhula S B K. Formal Verification Using Edge-Valued BinaryDecision Diagrams. IEEE Transcations on Computers.1996,45(2):247-255P
[5] Chen Z. On polynomial functions fromZ n1×Z n2××Znrto Zm. Discrete Math.1996,162(1-3):67-76P
[6] Narayan A, Jain J and Fujita M. Partitioned ROBDDs-A Compact, Canonical andEfficiently Manipulable Representation for Boolean Functions. In Proceeding ofInternational Conference on Computer Aided Design (ICCAD), San Jose, California,USA.1996:547-554P
[7] Tafertshofer P and Pedram M. Factored Edge-Valued Binary Decision Diagrams. FormalMethods in System Design.1997,10(2-3):243-270P.
[8] Clarke E, Fujita M and Mcgeer P. Muti Terminal Binary Decision Diagrams: An EfficientData Structure for Matrix Representation. Formal Methods in System Design.1997,10(4):149-169P
[9] Dreschler R, Becher B and Ruppertz S. The K*BMD: A Verification Data structure. IEEEDesign&Test.1997,14(2):51-59P
[10] Becker B, Drechsler R and Enders R. On the Representational Power of Bit-Level andWord-Level Decision Diagrams. In Proceedings of Asia and South Pacific DesignAutomation Conference (ASP-DAC), Chiba, Japan.1997:461-467P
[11] Drechsler R, Sauerhoff M and Sieling D. The Complexity of the Inclusion Operation onOFDD's. IEEE Transactions on Computer-Aided Design of Integrated Circuits andSystems.1998,17(5):457-459P
[12] Drechsler R and Horeth S. Manipulation of*BMD. In Proceeding of Asia and SouthPacific Design Automation Conference (ASP-DAC), Yokohama, Japan.1998:433-438P
[13] Smith J and Micheli D G. Polynomial Methods for Component Matching and Verification.In Proceeding of International Conference on Computer Aided Design (ICCAD). San Jose,California, USA.1998:678-685P
[14] Drechsler R and Becker B. Ordered Kronecker Functional Decision Diagrams-a DataStructure for Representation and Manipulation of Boolean Functions. IEEE Transactionson Computer-Aided Design of Integrated Circuits and Systems.1998,17(10):965-973P
[15] Smith J and Micheli D G. Polynomial Methods for Allocating Complex Components. InProceedings of Design, Automation and Test in Europe (DATE), Munich, Germany.1999:217-222P
[16] Horeth S and Drechsler. Formal Verification of Word-Level Specifications. In InProceedings of Design, Automation and Test in Europe (DATE), Munich, Germany.1999:52–58P
[17] Biere A, Cimatti A, Clarke E and Zhu Y. Symbolic Model Checking without BDDs. InProceedings of International Conference on Tools and Algorithms for the Constructionand Analysis of Systems (TACAS), Amsterdam, the Netherlands.1999:193-207P
[18] Smith J and Micheli D G. A Methodology for Synthesis with Reusable Components froman Arithmetic Specification, In Proceedings of European Conference on Circuit Theoryand Design (ECCTD), Stresa, Italy.1999:1195-1198P
[19]张健.逻辑公式的可满足性判定—方法、工具及应用.北京：科学出版社，2000年
[20] Smith J. Allocation and Interface Synthesis Algorithms for Component-Based Design.Technical Report. No.: CSL-TR-00-793,2000:32-58P
[21] Smith J and Micheli D G. Polynomial Circuit Models for Component Matching inHigh-level Synthesis. IEEE Transactions on Very Large Scale Integration (VLSI) Systems.2001,9(6):783-799P
[22] Clarke E, Biere A, Raimi R and Zhu Y. Bounded Model Checking Using SatisfiabilitySolving. Formal Methods in System Design,2001,19(1):7-34P
[23] Bentley B. Validating the Intel Pentium4Microprocessor. In Proceedings of DesignAutomation Conference (DAC), Las Vegas, USA,2001:244-248P
[24] Moskewicz M, Madigan C, Zhao Y, Zhang L and Malik S. Chaff: Engineering an EfficientSAT Solver. In Proceedings of Design Automation Conference (DAC). Las Vegas, USA2001:530-535P
[25] C Kern C. Formal Verification in Hardware Design: A Survey. ACM Transactions onDesign Automation of Electronic Systems.2001,4(2):123-193P
[26]王东明.消去法及其应用.北京：科学出版社，2002年:223-235P
[27] Bryant R E and Chen Y A. Verification of Arithmetic Circuits Using Binary MomentDiagrams. International Journal on Software Tools for Technology Transfer (STTT).2001,3(2):137-155P
[28] Minato, S. Streaming BDD Manipulation. IEEE Transactions on Computers.2002,51(5):474-485P
[29] Joao P M and Karem A S. Boolean Satisfiablity in Electornic Design Automation. InProceedings of Design Automation Conference (DAC), Los Angeles, California, USA.2003:675-680P
[30]严晓浪，郑飞君，葛海通，杨军.结合二叉判决图和布尔可满足性的等价性验证算法.电子学报.2004,32(8):1233-1235页
[31]李光辉,李晓维.基于增量可满足性的等价性检验方法.计算机学报.2004,27(10):1388-1394页
[32] Goldberg E and BerkMin N Y. A Fast and Robust SAT Solver. In Proceedings of DesignAutomation and Test in Europe Conference and Exhibition (DATE). Paris, France.2004:142-149P
[33]李光辉，邵明，李晓维.电路宽度制导的布尔推理.计算机辅助设计与图形学学报.2004,16(11):1568-1574页
[34] Radecka K and Zilic Z. Arithmetic Transforms for Verifying Compositions of SequentialDatapaths. In Proceedings of IEEE International Conference on Computer Design (ICCD),Austin, Texas, USA.2005:348-353P
[35]丁敏，唐璞山，周电.结合高级正向推理过程的可满足性问题解决器.中国科学E辑.2005,35(4):426—438页
[36] Park J, Pixley C. Burns M and Cho H. An Efficient Logic Equivalence Checker forIndustrial Circuits. Journal of Electronic Testing: Theory and Applications.2005,16(1):91-106P
[37]郑飞君，严晓浪，葛海通等.使用布尔可满足性的组合电路等价性验证算法.电子信息学报.2005,27(4):651-654页
[38] Kapur D and Cai Y Y. An Algorithm for Computer a Gr bner Basis of a Polynomial Idealover a Ring with Zero Divisors. Technical Report. No.: TR-CS-2003-43,2005:1-44P
[39]卢永江，竺红卫，严晓浪，葛海通.利用改善的静态隐含策略加速等价性验证.电路与系统学报.2005,10(3):47-51页
[40] Ozguner F, Marhefka D, DeGroat J and Wile B. Teaching Future Verification Engineers:The Forgotten Side of Logic Design. In Proceedings of Design Automation Conference(DAC), Las Vegas, USA,2005:253-255P
[41]鲁巍，吕涛，杨修涛，李晓维.针对可观测性语句覆盖准则的RTL激励生成.计算机研究与发展.2005,42(12):2169-2175页
[42]邵明，李光辉,李晓维.求解可满足问题的调查传播算法以及步长的影响规律.计算机学报.2005,28(5):849-855页
[43] Chen Y A and Bryant R E. An Efficient Graph Representation for Arithmetic CircuitVerification. IEEE Transactions on Computer-Aided Design of Integrated Circuits andSystems.2005,20(12):1443-1454P
[44]王海霞，韩承德.整数乘法电路的形式化验证方法研究.计算机研究与发展.2005,42(3):404-410页
[45] Kinder S, Fey G and Drechsler R. Controlling the Memory during Manipulation ofWorld-Level Decision Diagrams. In Proceedings of IEEE International Symposium onMultiple-Valued Logic (ISMVL), Calgary, Canada.2005:250-255
[46]李光辉，邵明，李晓维.通用CPU设计验证中的等价性检验方法.计算机辅助设计与图形学学报.2005,17(2):230-235页
[47] Chen J C and Chen Y A. Equivalence Checking of Integer Multiplier. In Proceedings ofAsia and South Pacific Design Automation Conference (ASP-DAC), Yokohama, Japan.2006:169-174P
[48] Alizadeh B, Kakoee M R. Using integer equations for high level formal verificationproperty checking. In Proceedings of International Symposium on Quality ElectronicDesign (ISQED), San Jose, USA.2006:69-74P
[49]陈云霁，马麟，沈海华，胡伟武.龙芯2号微处理器浮点除法功能部件的形式验证.计算机研究与发展.2006,43(10):1835-1841页
[50] Keim M, Dreschler R, Becker B, Martin M and Molitor P. Polynomial Formal Verificationof Multipliers. Formal Methods in System Design.2006,22(1):39-58P
[51] Dasgupta P, Chakrabarti P P, Nandi A and Krishna S. Abstraction of Word-level LinearArithmetic Functions from Bit-level Component Description, In Proceedings of Design,Automation and Test in Europe (DATE), Munich, Germany.2006:4-8P
[52] Zeng Z, Talupuru K R and Ciesielski M. LPSAT: A Unified Approach to RTL Satisfiability.In Proceedings of Design, Automation and Test in Europe (DATE), Munich, Germany.2006:398-402P
[53]丁敏,唐璞山.改进的时间帧展开的时序电路等价验证算法.计算机辅助设计与图形学学报.2006,18(1):53-61页
[54] Guillot J, Boutillon E, Ren Q and Ciesielski M. Efficient Factorization of DSP TransformsUsing Taylor Expansion Diagrams. In Proceedings of Design, Automation and Test inEurope (DATE), Munich, Germany.2006:754-755P
[55] Jone R B and Leary J W. Practical Formal Verification in Microprocessor Design. IEEEDesign&Test of Computers.2006,18(4):16-25P
[56]郑伟伟，吴为民，边计年．基于线性规划的RTL可满足性求解和性质检验.计算机辅助设计与图形学学报.2006,18(4):538-544页
[57] Kalla P, Ciesielski M, Boutillon E and Martin E. High-level Design Verification UsingTaylor Expansion Diagrams: First Results. In Proceedings of IEEE International HighLevel Design Validation and Test Workshop (HLDVT), Monterey, California, USA.2006:13-17P
[58] Radecka K and Zilic Z. Specifying and Verifying Imprecise Sequential Datapaths byArithmetic Transforms. In Proceedings of International Conference on Computer AidedDesign (ICCAD), San Jose, California, USA.2006:128-131P
[59] C Zorian Y. Error-Free Products. IEEE Design&Test of Computers.2006,18(4):2-2P
[60]陈云霁，张健，沈海华，胡伟武.一种基于SAT的运算电路查错方法.计算机学报.2007,30(12):2082-2089页
[61] Ciesielski M, Kalla P, Zeng Z, and Rouzeyre B. Taylor Expansion Diagrams: A CompactCanonical Representation with Application to Symbolic Verification, In Proceedings ofDesign, Automation and Test in Europe (DATE), Paris, France.2007:285-289P
[62]荆明娥，周电，唐璞山，周晓方.利用近似解加速求解SAT问题的启发式完全算法.计算机辅助设计与图形学学报.2007,19(9):1184-1189页
[63]邓澍军，吴为民，边计年. RTL验证中的混合可满足性求解.计算机辅助设计与图形学学报.2007,19(3):273-278页
[64] Fey G, Drechsler R, Ciesielski M. Algorthms for Taylor expansion diagrams, InProceeding of IEEE International Symposium on Multiple-Valued Logic (ISMVL),Toronto, Canada.2007:235-240P
[65]荆明娥，周电，唐璞山，周晓方，张华.启发式极性决策算法解SAT问题.中国科学E辑.2007,37(12):1597-1606页
[66] Yang Xiaoqing, Bian jinian, Deng Shujun and Zhao Yanni. EHSAT Modeling fromAlgorithm Description for RTL Model Checking. In Proceedings of Asian TestSymposium (ATS), Beijing, China.2007:178-183P
[67]刘领一，赵阳，吕涛，李华伟，李晓维.结合ATPG和SAT的无界模型检验前像计算方法.计算机辅助设计与图形学学报.2007,19(3):376-380页
[68]杨军，卢永江，葛海通，郑飞君，严晓浪.一种避免存爆炸的组合电路等价性验证方法.电路与系统学报.2007,12(3):21-25页
[69] Raik B and Drechsler R. RTL-Datapath Verification Using Integer Linear Programming.In Proceedings of Asia and South Pacific Design Automation Conference (ASP-DAC),Bangalore, India.2008:741-746P
[70] Navarro H, Montiel-Nelson J A, Sosa J, Garcia J C and Fay D Q M. Multiplexer Modelfor RTL Satisfiability Using MILP. Electronics Letters.2008,40(7):417-418P
[71]杨志，马光胜，冯刚，邵晶波.应用吴方法进行高层次定界模型检验.计算机辅助设计与图形学学报.2008,20(2):137-143页
[72] Peymandoust A and Micheli D G. Using Symbolic Algebra in Algorithmic Level DSPSynthesis. In Proceedings of Design Automation Conference (DAC), Las Vegas, NV,USA.2008:277-282P
[73] Mao Weibo and Wu Jinzhao. Application of Wu’s Method to Symbolic Model Checking.In Proceedings of International Symposium on Symbolic and Algebraic Computation(ISSAC), Beijing, China.2008:237-244P
[74]杨军，翁延龄，葛海通，严晓浪.利用状态缓存的时序等价性验证算法.计算机辅助设计与图形学学报.2008,20(2):149-154页
[75] Radecka K and Zilic Z. Design Verification by Test Vectors and Arithmetic TransformUniversal Test Set. IEEE Transctions on Computers.2008,53(5):628-640P
[76] Stoffel D, Kunz W. Equivalence Checking of Arithmetic Circuits on the Arithmetic BitLevel. IEEE Transactions on Computer-Aided Design of Integerated Circuits and Systems.2008,23(5):586-597P
[77] Pradhan D K, Askar S and Ciesielski M. Mathematical Framework for RepresentingDiscrete Functions as Word-level Polynomials. In Proceeding of IEEE International HighLevel Design Validation and Test Workshop (HLDVT), San Francisco, California, USA.2008:135-139P
[78] Ciesielski M, kalla P, Askar S. Taylor Expansion Diagrams: A Canonical Representationfor Verification of Data Flow Designs, IEEE Transactions on Computers.2009,55(9):1188-1201P
[79] Lu Wei, Yang Xiutao, Lv Tao and Li Xiaowei. An Efficient Evaluation and VectorGeneration Method for Observablity-Enhanced Satament Coverage. Journal of ComputerScience and Technology.2009,20(6):875-884P
[80] Rgomez-Prado D, Ren Q, Askar S, Ciesielski M, Boutillon E. Variable Ordering forTaylor Expansion Diagrams. In Proceedings of IEEE International High Level DesignValidation and Test Workshop (HLDVT), Sonoma Valley, California, USA.2009:55-59P
[81] Iyer M K, Parthasarathy G and Cheng K T. Efficient Conflict-Based Learning in an RTLCircuit Constraint Solver. In Proceedings of Design, Automation and Test in Europe(DATE), Munich, Germany.2009:666-671P
[82] Prasad M, Biere A and Gupta A, A Survey of Recent Advances in SAT-based FormalVerification. Software Tools for Technology Transfer.2009,7(2):156-173P
[83] Babic D and Musuvathi M. Modular Arithmetic Decision Procedure. Technical Report.No.: MSR-TR-2005-114,2009:1-10P
[84] Hungerbuehler N and Specker E. A Generalization of the Smarandache Function toSeveral Variables. Integers: Electronic Journal of Combinatorial Number Theory.2009,6(1):#A23
[85] Deng Shujun, Bian jinian, Wu weimin, Yang Xiaoqing and Zhao Yanni. EHSAT: AnEfficient RTL Satisfiability Solver Using an Extended DPLL Procedure. In Proceedings ofDesign Automation Conference (DAC), San Diego, California, USA.2009:588-593P
[86] Velev N M. Integrating Formal Verification into an Advanced Computer ArchitectureCourse. IEEE Transactions on Education.2009,48(2):216-222P
[87] Radecka K and Zilic Z. Arithmetic Transforms for Compositions of Sequential andImprecise Datapaths. IEEE Transactions on Computer-Aided Design of IntegratedCircuits and Systems,2009.25(7):1382-1391P
[88] Peymandoust A and Micheli D G. Application of Symbolic Computer Algebra inHigh-level Data-Flow Synthesis, IEEE Transctions on Computer-Aided Design ofIntegrated Circuits and Systems.2009,22(9):1154-1165P
[89] Hosangadi A, Fallah F and Kastner R. Factoring and Eliminating CommonSubexpressions in Polynomial Expressions. In Proceeding of International Conference onComputer Aided Design (ICCAD), San Jose, California, USA.2009:169-174P
[90] Hosangadi A, Fallah F and Kastner R. Reducing Hardware Complexity of Linear DSPSystems by Iteratively Eliminating Two-Term Common Subexpressions. In Proceedingsof Asia and South Pacific Design Automation Conference (ASP-DAC), Shanghai, China.2009:532-528P
[91] Lee D U, Gaffar A A, Cheung R C C, Mencer O, Luk W and Constantinides G A.Accuracy-Guaranteed Bit-Width Optimization. IEEE Transactions on Computer-AidedDesign of Integrated Circuits and Systems.2009,25(10):1990-2000P
[92] Ugarte I and Sanchez P. Assertion Checking of Behavioral Descriptions with Non-linearSolver. In Proceedings of International Conference on Computer Design (ICCD), San Jose,California, USA,2009.229-231P
[93] Hosangadi A, Fallah F and Kastner R. Common Subexpression Elimination InvolvingMultiple Variables for Linear DSP Synthesis. In Proceedings of15th IEEE InternationalConference on Application-Specific Systems, Architectures and Processors, Galveston,Texas, USA.2009:202-212P
[94] Shekhar N, Kalla P, Enescu F and Gopalakrishnan S. Equivalence Verification ofPolynomial Datapaths with Fixed-Size Bit-Vectors Using Finite Ring Algebra. InProceeding of International Conference on Computer Aided Design (ICCAD), San Jose,California, USA.2009:291-296P
[95] Wedler M, Stoffel D, Brinkmann R and Kunz W. A Normalization Method for ArithmeticData-Path Verification. IEEE Transactions on Computer-Aided Design.2009,26(11):1909-1922P
[96] Kroening D and Seshia S A. Formal Verification at Higher Levels of Abstraction. InProceedings of International Conference on Computer-Aided Design (ICCAD), San Jose,California, USA.2010:572-578P
[97] Peymandoust A and Micheli D G. Symbolic Algebra and Timing Driven Data-flowSynthesis. In Proceedings of International Conference on Computer Aided Design(ICCAD), San Jose, California, USA.2010:300-305P
[98] Drechsler R, Fey G and Kinder S. An Integrated Approach for Combining BDD and SATProvers. In Proceedings of International Conference on VLSI Design (VLSID),Hyderabad, India.2010:237-242P
[99] Disch S and Schollm C. Combinational Equivalence Checking Using Incremental SATSolving, Output Ordering, and Resets. In Proceedings of Asia and South Pacific DesignAutomation Conference (ASP-DAC), Yokohama, Japan.2010:938-943P
[100] Zeng Z, Talupuru K R and Ciesielski M. Function Test Generation Based on Word-levelSAT. Journal of Systems Architecture.2010,51(8):488-511P
[101] Peymandoust A, Simunic T and Micheli D G. Complex Library Mapping for EmbeddedSoftware Using Symbolic Algebra, In Proceedings of Design Automation Conference(DAC), New Orleans, Los Angeles, USA.2010:325-330P
[102] Gopalakrishnan S and Kalla P. Optimization of Polynomial Datapaths Using Finite RingAlgebra. ACM Transactions on Design Automation of Electronic System.2010,12(4):Article No49
[103] Raudvere R, Singh K A, Sander I and Jantsch A. System Level Verification of DigitalSignal Processing Application Based on the Polynomial Abstraction Technique. InProceedings of International Conference on Computer Aided Design (ICCAD), San Jose,CA, USA.2010:285-290P
[104] Shekhar N, Kalla P, Enescu F and Gopalakrishnan S. Exploiting Vanishing Polynomialfor Equivalence Verification of Fixed-Size Arithmetic Datapaths. In Proceedings ofIEEE International Conference on Computer Design (ICCD), San Jose, CA, USA.2010:215-220P
[105] Shekhar N, Kalla P and Enesu F. Equivalence Verification of Polynomial DatapathsUsing Ideal Membership Testing. IEEE Transactions on Computer-Aided Design ofIntegrated Circuits and Systems.2010,26(7):1320-1330P
[106] Du Zhenjun, Ma Guangsheng and Feng Gang. A New Model for Verification. Journal ofHarbin Institute of Technology.2010,14(3):305-310P
[107] Hosangadi A, Fallah F and Kastner R. Optimizing Polynomial Expressions by AlgebraicFactorization and Common Subexpression Elimination, IEEE Transctions onComputer-Aided Design of Integrated Circuits and Systems.2010,25(10):2012-2022P
[108] Shekhar N, Kalla P, Meredith B and Enescu F. Simulation Bounds for EquivalenceVerification of Arithmetic Datapaths with Finite Word-Length Operands. In Proceedingsof International Conference Formal Methods in Computer-Aided Design (FMCAD), SanJose, California, USA.2010:179-186P
[109] Sasao T and Nagayama S. Representations of Elementary Functions Using BinaryMoment Diagrams. In Proceedings of IEEE International Symposium on Multiple-ValuedLogic (ISMVL), Singapore.2010:28-33P
[110] Brickenstein M, Dreyer A, Greuel G M, Wedler M and Wienand O. New Developmentsin the Theory of Grobner Bases and Application to Formal Verification. http://arxiv.org/PS_cache/arxiv/pdf/0801/0801.1177v2.pdf
[111] Watanabe Y, Homma N, Aoki T and Higuchi T. Application of Symbolic ComputerAlgebra to Arithmetic Circuit Verification. In Proceedings of International Conferenceon Computer Design (ICCD), Lake Tahoe, California, USA.2010:25-32P
[112] Wienand O. The Gr bner Basis of the Ideal of Vanishing Polynomials. http://arxiv.org/PS_cache/arxiv/pdf/0709/0709.2978v1.pdf
[113] Wienand O, Wedler M, Stoffel D, Kunz W and Greuel G. An Algebra Approach forProving Data Correctness in Arithmetic Data Paths. In Proceedings of InternationalConference on Computer Aided Verification (CAV), Princeton USA.2010:473-486P
[114] Peymandoust A, Simunic T and Micheli D G. Complex Instruction and Software LibraryMapping for Embedded Software Using Symbolic Algebra, IEEE Transactions onComputer-Aided Design of Integrated Circuits and Systems.2011,22(8):964-975P
[115] Semiconductor Industry Association. International Technology Roadmap forSemiconductors, Design Chapter,2011Edition [EB/OL]. http://www.itrs.net.
[116] Peymandoust A, Simunic T and Micheli D G. Low Power Embedded SoftwareOptimization Using Symbolic Algebra, In Proceedings of Design, Automation and Testin Europe (DATE), Paris, France.2011:1052-1058P
[117] Bhadra J, Abadir M S and Ray S. A Survey of Hybrid Techniques for FunctionalVerification. IEEE Design&Test of Computers.2011,24(2):112-122P
[118] Raudvere R, Singh K A, Sander I and Jantsch A. Polynomial Abstraction for Verificationof Sequentially Implemented Combinational Circuits. In Proceedings of Design,Automation and Test in Europe (DATE), Paris, France.2011:690-691P
[119] Shekhar N, Kalla P, Mereduth M B and Enesu F. Simulation Bounds for EquivalenceVerification of Polynomial Datapaths Using Finite Ring Algebra. IEEE Transactions onVery Large Scale Integration (VLSI) Systems.2011,16(5):517-527P
[120] Gopalakrishnan S and Kalla P. Integrating Common Sub-Expression Elimination withAlgebraic Methods for Polynomial System Synthesis. In Proceedings of InternationalWorkshop on Logic and Synthesis (IWLS), Lake Tahoe, California, USA,2011:31-37P
[121] Li Xiaowei, Li Guanghui and Shao Ming. Formal Verification Technique Based onBoolean Satisfiability Problem. Journal of Computer Science and Technology.2011,20(1):38-47P
[122] Gopalakrishnan S, Kalla P and Mereduth M B. Finding Linear Building-Blocks for RTLSynthesis of Polynomial Datapaths with Fixed-Size Bit-Vectors. In Proceedings ofInternational Conference on Computer-Aided Design (ICCAD), San Jose, California,USA.2011:413-418P
[123] Peymandoust A, Pozzi L, Ienne P and Micheli D G. Automatic Instruction Set Extensionand Utilization for Embedded Processors. In Proceedings of IEEE InternationalConference on Application-Specific Systems, Architectures and Processors.2011:108-118P
[124] Shekhar N, Kalla P and Enescu F. Equivalence Verification of Arithmetic Datapaths withMultiple Word-Length Operands, In Proceedings of Design, Automation and Test inEurope (DATE), Munich, Germany.2011:824-829P
[125] Hosangadi A, Fallah F and Kastner R. Energy Efficient Hardware Synthesis ofPolynomial Expressions. In Proceedings of International Conference on VLSI Design(VLSID), Kolkata, India.2011:653-658P
[126]边计年，薛宏熙，苏明，吴为民.数字系统设计自动化.北京：清华大学出版社，2005年:231-247P
[127] Hosangadi A, Fallah F and Kastner R. Optimizing High Speed Arithmetic Circuit UsingThree-Term Extraction, In Proceedings of Design, Automation and Test in Europe
(DATE), Munich, Germany.2011:1294-1299P