基于多项式符号代数的数字电路形式验证方法研究
|
摘要
随着数字集成电路设计规模的增大和功能复杂性的提高,功能验证已经成为设计流程中的瓶颈。传统的模拟验证方法无法满足现时复杂集成电路设计带来的巨大的验证需求。形式验证技术,例如模型检验和等价验证,因此发展成为模拟验证方法的一种重要补充,正日益受到学术界的关注。现有的形式验证技术大多基于传统的位级方法,例如BDD或布尔SAT,它们主要针对低层次门级电路和以控制流为主的电路的验证,难以胜任以数据流为主的高层次复杂电路设计的验证。作为一种新近提出的电路表示和计算方法,多项式符号代数能够克服BDD和布尔SAT方法的某些不足。本文深入研究了多项式符号代数方法在数字电路形式验证中的应用,取得了如下创新性成果：
(1)提出了基于多项式符号代数的模型检验方法。首先,扩展了传统的Kripke结构的概念,得到了所谓状态转换系统的新概念。用该状态转换系统代替传统的Kripke结构来抽象高层次设计中的控制逻辑,并统一用多项式方法描述高层次设计中的数据通路和控制逻辑,从而有效地避免了数据域和控制域之间频繁的约束传播和回溯操作。进而,给出了一个高层次设计模型检验的方法框架。在该方法框架之下,原有的模型检验问题被转化为一个假设和结论均具有多项式形式的一阶逻辑定理证明问题,一个基于多项式符号计算的判定过程被用来有效地解决该定理证明问题。针对典型高层次设计的实验结果表明,与现有的基于非线性求解器的高层次模型检验方法相比,该方法在保证验证准确性的情况下,平均要快1到5倍。
(2)提出了基于多项式符号代数的等价验证方法。该方法直接在高层次建模数据通路设计,给出了高层次数据通路的多项式集合表示的一般形式及构造方法。由于避免了将高层次数据通路设计展开为门级网表,对于同样的验证问题,该方法涉及的信号变量的数目和约束表达式的数目要比基于BDD和布尔SAT的等价验证方法少得多。进而,从多项式集合公共零点的角度定义了高层次数据通路的功能等价性,并给出了一个基于多项式符号计算的有效的代数求解算法。针对高层次基准数据通路的实验结果表明,与现有的基于*BMD和整数线性规划的高层次等价验证方法相比,该方法在保证错误诊断能力的情况下,平均要快1倍到1个数量级。
(3)提出了基于多项式符号代数的层次化验证方法。首先,引入了一种基于广义表数据结构的层次化电路表示模型。基于此种层次化表示,并应用多项式代数中的消元定理和扩张定理,得到了一种层次化的电路功能计算方法。该方法将原本规模较大的计算问题划分为一些小的计算问题,并以一种逐层递归的方式完成原有计算,从而有效地提高了计算效率。进而,将这种新的电路功能计算方法用于设计验证,实现了层次化的模型检验和等价验证算法。实验结果表明,采用层次化策略能够有效地提高原有模型检验和等价验证算法的验证效率。就本文的实验电路而言,模型检验算法的效率平均提高了23%,等价验证算法的效率平均提高了17%。
As the size and functional complexity of integrated circuits increase, functional verification has been the main bottleneck of the design flow. Traditional simulation based verification methods cannot meet with the tremendous verification demand of today's complex integrated circuit designs. Because of this, formal verification techniques, such as model checking and equivalence verification, receive more and more attention from academic circle as an important assistant. Existing formal verification techniques are mostly based on bit-level methods, such as BDD and Boolean SAT, which are generally geared towards verification of low-level control-dominated circuits, and are hard to satisfy the verification requirements of high-level data-dominated designs. As a newly devolopted technique for circuit representation and computation, polynomial symbolic algebra can overcome some drawbacks of BDD and Boolean SAT. This thesis investigates the application of polynomial symbolic algebra in digital cricuit verification deeply. The contributions of this thesis are as follows.
(1) A model checking approach based on polynomial symbolic algebra has been proposed. First, a new concept called state transition system is obtained by extending the concept of classical Kripke structure, which is used to represent the control logic of high-level designs as a substitution of the latter. Datapath and control logic of high-level designs can thus be modeled in a unified framework using polynomial method, and frequent constraint propagation and backtracking between data domain and control domain are therefore avoided. Then, a framework for high-level model checking is presented. In the framework, the original model checking problem is translated into a first-order theorem proving problem, in which both hypothesis and conclusion of the theorem are of polynomial form. A symbolic computation based decision procedure is ultilized to prove the theorem efficiently. The experimental results on some typical high-level designs show that, the proposed approach is on average one to five times faster than the nonlinear solver based high-level model checking approache, while keeping the verification accuracy.
(2) An equivalence verification method based on polynomial symbolic algebra has been proposed. Datapaths are modeled at higher levels of abstraction directly. The general form of the polynomial set representations of high-level datapaths and the method to construct it are presented. Since high-level datapaths no longer need to be transformed into gate-level netlists, our approach usually involves much less signal variables and constraints for a given verification problem compared with the BDD and Boolean SAT based equivalence verification methods. Furthermore, the functional equivalence of high-level datapaths is defined from the prospective of common zeros of polynomial sets, and an efficient algebraic solution based on symbolic computation is presented. The experimental results on some benchmark datapaths show that, the proposed method is on everage one factor to one order of magnitude faster than the *BMD and integer linear programming based equivalence verification methods, while keeping the error detecting capability.
(3) The hierarchical verification methods based on polynomial symbolic algebra have been proposed. First, a generalized list based hierarichical representation for circuit designs is introduced. Based on this hierarchical representation and ultilizing the elimination and extension theorems from polynomial algebra, a new method is proposed to calculate the functionality of circuit designs, which breaks the original calculation into small sub-tasks to finish recursively. The computational efficiency can thus be improved efficienctly. Applying this new calculation method to design verification, hierarchical model checking and equivalence verification methods are realized. The experimental results show that, the hierarchical verification methods are much more efficient than the original verification methods. For our experimental circuits, efficiencies of the model checking and equivalence verification algorithms increase 23% and 17% respectively.
(1)提出了基于多项式符号代数的模型检验方法。首先,扩展了传统的Kripke结构的概念,得到了所谓状态转换系统的新概念。用该状态转换系统代替传统的Kripke结构来抽象高层次设计中的控制逻辑,并统一用多项式方法描述高层次设计中的数据通路和控制逻辑,从而有效地避免了数据域和控制域之间频繁的约束传播和回溯操作。进而,给出了一个高层次设计模型检验的方法框架。在该方法框架之下,原有的模型检验问题被转化为一个假设和结论均具有多项式形式的一阶逻辑定理证明问题,一个基于多项式符号计算的判定过程被用来有效地解决该定理证明问题。针对典型高层次设计的实验结果表明,与现有的基于非线性求解器的高层次模型检验方法相比,该方法在保证验证准确性的情况下,平均要快1到5倍。
(2)提出了基于多项式符号代数的等价验证方法。该方法直接在高层次建模数据通路设计,给出了高层次数据通路的多项式集合表示的一般形式及构造方法。由于避免了将高层次数据通路设计展开为门级网表,对于同样的验证问题,该方法涉及的信号变量的数目和约束表达式的数目要比基于BDD和布尔SAT的等价验证方法少得多。进而,从多项式集合公共零点的角度定义了高层次数据通路的功能等价性,并给出了一个基于多项式符号计算的有效的代数求解算法。针对高层次基准数据通路的实验结果表明,与现有的基于*BMD和整数线性规划的高层次等价验证方法相比,该方法在保证错误诊断能力的情况下,平均要快1倍到1个数量级。
(3)提出了基于多项式符号代数的层次化验证方法。首先,引入了一种基于广义表数据结构的层次化电路表示模型。基于此种层次化表示,并应用多项式代数中的消元定理和扩张定理,得到了一种层次化的电路功能计算方法。该方法将原本规模较大的计算问题划分为一些小的计算问题,并以一种逐层递归的方式完成原有计算,从而有效地提高了计算效率。进而,将这种新的电路功能计算方法用于设计验证,实现了层次化的模型检验和等价验证算法。实验结果表明,采用层次化策略能够有效地提高原有模型检验和等价验证算法的验证效率。就本文的实验电路而言,模型检验算法的效率平均提高了23%,等价验证算法的效率平均提高了17%。
As the size and functional complexity of integrated circuits increase, functional verification has been the main bottleneck of the design flow. Traditional simulation based verification methods cannot meet with the tremendous verification demand of today's complex integrated circuit designs. Because of this, formal verification techniques, such as model checking and equivalence verification, receive more and more attention from academic circle as an important assistant. Existing formal verification techniques are mostly based on bit-level methods, such as BDD and Boolean SAT, which are generally geared towards verification of low-level control-dominated circuits, and are hard to satisfy the verification requirements of high-level data-dominated designs. As a newly devolopted technique for circuit representation and computation, polynomial symbolic algebra can overcome some drawbacks of BDD and Boolean SAT. This thesis investigates the application of polynomial symbolic algebra in digital cricuit verification deeply. The contributions of this thesis are as follows.
(1) A model checking approach based on polynomial symbolic algebra has been proposed. First, a new concept called state transition system is obtained by extending the concept of classical Kripke structure, which is used to represent the control logic of high-level designs as a substitution of the latter. Datapath and control logic of high-level designs can thus be modeled in a unified framework using polynomial method, and frequent constraint propagation and backtracking between data domain and control domain are therefore avoided. Then, a framework for high-level model checking is presented. In the framework, the original model checking problem is translated into a first-order theorem proving problem, in which both hypothesis and conclusion of the theorem are of polynomial form. A symbolic computation based decision procedure is ultilized to prove the theorem efficiently. The experimental results on some typical high-level designs show that, the proposed approach is on average one to five times faster than the nonlinear solver based high-level model checking approache, while keeping the verification accuracy.
(2) An equivalence verification method based on polynomial symbolic algebra has been proposed. Datapaths are modeled at higher levels of abstraction directly. The general form of the polynomial set representations of high-level datapaths and the method to construct it are presented. Since high-level datapaths no longer need to be transformed into gate-level netlists, our approach usually involves much less signal variables and constraints for a given verification problem compared with the BDD and Boolean SAT based equivalence verification methods. Furthermore, the functional equivalence of high-level datapaths is defined from the prospective of common zeros of polynomial sets, and an efficient algebraic solution based on symbolic computation is presented. The experimental results on some benchmark datapaths show that, the proposed method is on everage one factor to one order of magnitude faster than the *BMD and integer linear programming based equivalence verification methods, while keeping the error detecting capability.
(3) The hierarchical verification methods based on polynomial symbolic algebra have been proposed. First, a generalized list based hierarichical representation for circuit designs is introduced. Based on this hierarchical representation and ultilizing the elimination and extension theorems from polynomial algebra, a new method is proposed to calculate the functionality of circuit designs, which breaks the original calculation into small sub-tasks to finish recursively. The computational efficiency can thus be improved efficienctly. Applying this new calculation method to design verification, hierarchical model checking and equivalence verification methods are realized. The experimental results show that, the hierarchical verification methods are much more efficient than the original verification methods. For our experimental circuits, efficiencies of the model checking and equivalence verification algorithms increase 23% and 17% respectively.
引文
[1]SIA. The International Technology Roadmap for Semiconductors.http.// public.itrs.net./
[2]韩俊刚,杜慧敏.数字硬件的形式化验证.北京：北京大学出版社,2001
[3]Drechsler R. Advanced Formal Verification. New York:Kluwer Academic Publishers,2004
[4]Bryant R E. Graph based algorithms for Boolean function manipulation. IEEE Transactions on Computers,1986, C-35(8):677-691P
[5]张健.逻辑公式的可满足性判定——方法、工具及应用.北京：科学出版社,2000
[6]Drechsler R. Towards formal verification on the system level. Proceedings of the 15th IEEE International Workshop on Rapid System Prototyping, Geneva, Switzerland,2004,2-5P
[7]Kroening D, Seshia S A. Formal verification at higher levels of abstraction. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2007,572-578P
[8]Cox D, Little J, O'Shea D. Ideals, Varieties and Algorithms:an Introduction to Computational Algebraic Geometry and Commutative Algebra. New York: Springer-Verlag,1997
[9]吴文俊.数学机械化.北京：科学出版社,2003
[10]王东明,夏壁灿.计算机代数.北京：清华大学出版社,2004
[11]Smith J, Micheli D G. Polynomial methods for component matching and verification. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,1998,678-685P
[12]Smith J, Micheli D G Polynomial methods for allocating complex components. Proceedings of the Conference on Design Automation and Test in Europe, Munich,Germany,1999,217-222P
[13]Smith J, Micheli D G. Polynomial circuit models for component matching in
high-level synthesis. IEEE Transactions on VLSI Systems,2001,9(6): 783-799P
[14]Peymandoust A, Micheli D G Using symbolic algebra in algorithmic level DSP synthesis. Proceedings of the ACM/IEEE Design Automation Conference, Las Vegas, NV, USA,2001,277-282P
[15]Peymandoust A, Micheli D G. Symbolic algebra and timing driven data-flow synthesis. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2001,300-305P
[16]Peymandoust A, Micheli D G Application of symbolic computer algebra in high-level data-flow synthesis. IEEE Transactions on CAD of IC & Systems, 2003,22(9):1154-1165P
[17]Xing X, Jong C C. Using symbolic computer algebra for subexpression factorization and subexpression decomposition in high level synthesis. Proceedings of the International Symposium on Circuits and Systems, Kobe, Japan,2005,5645-5648P
[18]Hosangadi A. Fallah F, Kastner R. Factoring and eliminating common subexpressions in polynomial expressions. Proceedings of the IEEE/ACM International Conference on Computer Aided Design,2004,169-174P
[19]Hosangadi A, Fallah F, Kastner R. Energy efficient hardware synthesis of polynomial expressions. Proceedings of the International Conference on VLSI Design, Kolkata, India,2005,653-658P
[20]Hosangadi A, Fallah F, Kastner R. Reducing hardware complexity of linear DSP systems by iteratively eliminating two-term common subexpressions. Proceedngs of the Asia and South Pacific Design Automation Conference, Yokohama, Japan,2005,532-528P
[21]Hosangadi A, Fallah F, Kastner R. Optimizing polynomial expressions by algebraic factorization and common subexpression elimination. IEEE Transactions on CAD of IC & Systems,2006,25(10):2012-2022P
[22]Gopalakrishnan S, Kalla P, Enescu F. Optimizing fixed-size bit-vector arithmetic using finite ring algebra. Proceedings of the International
Workshop on Logic and Synthesis, Vail, Colorado, USA,2006,110-117P
[23]Gopalakrishnan S, Kalla P, Meredith M B, et al. Finding linear building-blocks for RTL synthesis of polynomial datapaths with fixed-size bit-vectors. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2007,413-418P
[24]Gopalakrishnan S, Kalla P. Optimization of polynomial datapaths using finite ring algebra. ACM Transactions on Design Automation of Electronic Systems,2007,12(4):1-30P
[25]Ciesielski M, Kalla P, Askar S. Taylor expansion diagrams:a canonical representation for verification of data flow designs. IEEE Transactions on Computers,2006,55(9):1188-1201P
[26]季晓慧,张健.约束问题求解.自动化学报,2007,33(2)：125-131页
[27]DeMoura L, Dutertre B, Shankar N. A tutorial on satisfiability modulo theories. Proceedings of the International Conference on Computer Aided Verification, Berlin, Germany,2007,20-36P
[28]Sebastiani R. Lazy satisability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation,2007,3(1):141-224P
[29]邓澍军,吴为民,边计年.RTL验证中的混合可满足性求解.计算机辅助设计与图形学学报,2007,19(3)：273-278页
[30]K. L. McMillan. Symbolic Model Checking. Boston:Kluwer Academic Publisher,1993.
[31]Fujita M, McGeer P C, Yang J C-Y. Multi terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods in System Design,1997,10(2-3):149-169P
[32]Bryant R E, Chen Y A. Verification of arithmetic circuits with binary moment diagram. Proceedings of the ACM/IEEE Design Automation Conference, San Francisco, CA, USA,1995,535-541P
[33]Lai Y T, Pedram M, Vrudhula S B K. Formal verification using edge-valued binary decision diagrams. IEEE Transactions on Computers,1996,45(2): 247-255P
[34]Drechsler R, Horeth S. Manipulation of *BMD. Proceedings of the Asia South Pacific Design Automation Conference, Tokyo, Japan,1998,433-438P
[35]Keim M, Dreschler R, Becker B, et al. Polynomial formal verification of multipliers. Formal Methods in System Design,2003,22(1):39-58P
[36]Ciesielski M, Kalla P, Zeng Z, et al. Taylor expansion diagrams:a compact canonical representation with application to symbolic verification, Procee-dngs of the Conference on Design Automation and Test in Europe, Paris, France,2002,285-289P
[37]Fey G, Drechsler R, Ciesielski M. Algorthms for Taylor expansion diagrams. Proceedings of the IEEE International Symposium on Multiple-Valued Logic, Toronto, Canada,2004,235-240P
[38]Gomez-Prado D, Ren Q, Askar S, et al. Variable ordering for Taylor expansion diagrams. Proceedings of the International Workshop on High Level Design Validation and Test, Sonoma Valley, CA, USA,2004,55-59P
[39]Kalla P, Ciesielski M, Boutillon E, et al. High-level design verification using Taylor expansion diagrams:first results. Proceedings of the International Workshop on High Level Design Validation and Test, Cannes, France,2002, 13-17P
[40]Guillot J, Boutillon E, Ren Q, et al. Efficient factorization of DSP transforms using Taylor expansion diagrams. Proceedings of the Conference on Design Automation and Test in Europe, Munich, Germany,2006,754-755P
[41]Ciesielski M, Askar S, Gomez-Prado D, et al. Data-flow transformations using Taylor expansion diagrams. Proceedings of the Conference on Design Automation and Test in Europe, Nice, France,2007,455-460P
[42]Gu J, Purdom P W, Franco J, et al. Algorithms for the satisfiability (SAT) problem:a survey. DIMACS Series on Discrete Mathematics and Theoretical Computer Science,1997,35:19-151P
[43]Bordeaux L, Hamadi Y, Zhang L. Propositional satisfiability and constraint programming:a comparative survey. ACM Computing Surveys,2006,38(4): 1-54P
[44]Gu J. Local search for satisfiability (SAT) problem. IEEE Transactions on Systems, Man and Cybernetics,1993,23(4):1108-1129P
[45]Gu J. Global Optimization for satisfiability (SAT) problem. IEEE Transac-tions on Data and Knowledge Engineering,1994,6(3):361-381P
[46]Selman B, Levesque H, Mitchell D. A new method for solving hard satisfiability problems. Proceedings of the National Conference on Artificial and Intelligence, San Jose, CA, USA,1992,440-446P
[47]Frank J. Weighting for godot:learning heuristic for GSAT. Proceedings of the National Conference on Artificial and Intelligence, Portland, OR, USA, 1996,338-343P
[48]Selman B, Kautz H A, Cohen B. Noise strategies for improving local search. Proceedings of the National Conference on Artificial and Intelligence, Seattle, WA, USA,1994,337-343P
[49]Davis M, Logemann G, Loveland D. A machine program for theorem proving. Communications of the ACM,1962,5(7):394-397P
[50]Li X W, Li G H, Shao M. Formal verification techniques based on Boolean satisfiability Problem. Journal of Computer Science and Technology,2005, 20(1):38-47P
[51]Prasad M, Biere A, Gupta A. A survey of recent advances in SAT-based formal verification. Software Tools for Technology Transfer,2005,7(2): 156-173P
[52]Goldberg E I, Prasad M R, Brayton R K. Using SAT for combinational equivalence checking. Proceedings of the Conference on Design Automa-tion and Test in Europe, Munich, Germany,2001,114-121P
[53]郑飞君,严晓浪,葛海通等.使用布尔可满足性的组合电路等价性验证算法.电子与信息学报,2005,27(4)：651-654页
[54]李光辉,李晓维.基于增量可满足性的等价性检验方法.计算机学报,2004,27(10)：1388-1394页
[55]Disch S, Schollm C. Combinational equivalence checking using incremental SAT solving, Output Ordering, and Resets. Proceedings of the Asia South
Pacific Design Automation Conference, Yokohama, Japan,2007,938-943P
[56]Khasidashvili Z, Hanna Z. SAT-based methods for sequential hardware equivalence verification without synchronization. Electronic Notes in Theoretical Computer Science,2003,89(4):593-607P
[57]Syal M, Hsiao M. VERISEC:Verifying equivalence of sequential circuits using SAT. Proceedings of the International Workshop on High Level Design Validation and Test, Napa, CA, USA,2005,52-59P
[58]丁敏,唐璞山.改进的时间帧展开的时序电路等价验证算法.计算机辅助设计与图形学学报,2006,18(1)：53-61页
[59]Biere A, Cimatti A, Clarke E, et al. Symbolic model checking without BDDs. Proceedings of the International Conference on Tools and Algorithm for Construction and Analysis of Systems, Amsterdam, Netherlands,1999,193-207P
[60]Clarke E, Biere A, Raimi A, et al. Bounded model checking using satisfiability solving. Formal Methods in System Design,2001,19(1):7-34P
[61]Biere A, Cimatti A, Clarke E, et al. Bounded model checking. Advances in Computers,2003,58(1):118-149P
[62]McMillan K L. Applying SAT methods in unbounded symbolic model checking. Proceedings of the International Conference on Computer Aided Verification, Copenhagen, Denmark,2002,250-264P
[63]Kang H J, Park I C. SAT-based unbounded symbolic model checking. Proceedings of the ACM/IEEE Design Automation Conference, Anaheim, CA, USA,2003,840-843P
[64]Ganai M K, Gupta A, Ashar P. Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA, 2004,510-517P
[65]Bryant R E, Lahiri S K, Seshia S A. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. Proceedings of the International Conference on Computer Aided
Verification, Copenhagen, Denmark,2002,78-92P
[66]Strichman O. On solving presburger and linear arithmetic with SAT. Proceedings of the International Conference on Formal Methods in Computer Aided Design, Portland, Oregon, USA,2002,160-170P
[67]Strichman O, Seshia S A, Bryant R E. Deciding separation formulas with SAT. Proceedings of the International Conference on Computer Aided Verification,2002,209-222P
[68]Seshia S A, Lahiri S K, Bryant R E. A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. Proceedings of the ACM/IEEE Design Automation Conference, Anaheim, CA, USA,2003, 425-430P
[69]Bozzano M, Bruttomesso R, Cimatti A, et al. An incremental and layered procedure for the satisfiability of linear arithmetic logic. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Edinburgh, Scotland,2005,317-333P
[70]Dutertre B, DeMoura L. A fast linear-arithmetic solver for DPLL(T). Proceedings of the International Conference on Computer Aided Verification, Seattle, WA, USA,2006,81-94P
[71]DeMoura L, Bjorner N. Z3:An efficient SMT solver. Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems, Budapest, Hungary,2008,337-340P
[72]Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories:from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM,2006,53(6):937-977P
[73]Ganzinger H, Hagen G, Nieuwenhuis R, et al. DPLL(T):fast decision procedures. Proceedings of the International Conference on Computer Aided Verification, Boston, MA, USA,2004,175-188P
[74]Fallah F, Devadas S, Keutzer K. Functional vector generation for HDL models using linear programming and 3-satisfiability. Proceedings of the ACM/IEEE Design Automation Conference, San Francico, CA, USA,1998,
528-533P
[75]Fallah F, Devadas S, Keutzer K. Functional vector generation for HDL models using linear programming and Boolean satisfiability. IEEE Transactions on CAD,2001,20(8):994-1002P
[76]Huang C Y, Cheng K T. Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques. Proceedings of the ACM/IEEE Design Automation Conference, Los Angeles, CA, USA,2000, 118-123P
[77]Huang C Y, Cheng K T. Using word-level ATPG and modular arithmetic constraint-solving techniques for assertion property checking. IEEE Transactions on CAD,2001,20(3):381-391P
[78]Wu S H, Chen M C, Wu W M, et al. RTL property checking technology based on ATPG and ILP. Proceedings of the International Conference on ASIC, Shanghai, China,2005,890-893P
[79]Zeng Z, Kalla P, Ciesielski M. LPSAT:a unified approach to RTL satisfiability. Proceedngs of the Conference on Design Automation and Test in Europe, Munich, Germany,2001,398-402P
[80]Zeng Z, Talupuru K R, Ciesielski M. Functional test generation based on word-level SAT. Journal of Systems Architecture,2005,51(8):488-511P
[81]Navarro H, Montiel-Nelson J A, Sosa J, et al. Multiplexer model for RTL satisfiability using MILP. Electronics Letters,2004,40(7):417-418P
[82]Brinkmann R, Rolf D. RTL-datapath verification using integer linear programming. Proceedngs of the Asia and South Pacific Design Automation Conference, Bangalore, India,2002,741-746P
[83]Ugarte I, Sanchez P. Assertion checking of behavioral descriptions with non-linear solver. Proceedngs of the International Conference of Computer Design, San Jose, CA, USA,2005,229-231P
[84]Ugarte I, Sanchez P. Assertion-based verification of behavioral descriptions with non-linear solver. Proceedings of the International Workshop on High Level Design Validation and Test, Monterey, CA,USA,2006.61-68P
[85]Liu C, Kuehlmann A, Moskewicz M W. CAMA:a multi-valued satisfiability solver. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2003,326-333P
[86]Parthasarathy G, Iyer M K, Cheng K T, et al. An efficient finite-domain constraint solver for circuits. Proceedings of the ACM/IEEE Design Automation Conference, San Diego, CA, USA,2004,212-217P
[87]Deng S J, Bian J N, Wu W M, et al. EHSAT:an efficient RTL satisfiability solver using an extended DPLL procedure. Proceedings of the ACM/IEEE Design Automation Conference, San Diego, CA, USA,2007,588-593P
[88]Parthasarathy G, Iyer M K, Cheng K T, et al. Structural search for RTL with predicate learning. Proceedings of the ACM/IEEE Design Automation Conference, San Diego, CA, USA,2005,451-456P
[89]Pradhan D K, Askar S, Ciesielski M. Mathematical framework for representing discrete functions as word-level polynomials. Proceedings of International Workshop on High Level Design Validation and Test, San Francisco, CA, USA,2003,135-139P
[90]Raudvere K, Singh K A, Sander I, et al. Polynomial abstraction for verification of sequentially implemented combinational circuits. Proceedings of the Conference on Design Automation and Test in Europe, Paris, France, 2004,690-691P
[91]Raudvere K, Singh K A, Sander I, et al. System level verification of digital signal processing application based on the polynomial abstraction technique. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2005,285-290P
[92]Mao W B, Wu J Z. Application of Wu's method to symbolic model checking. Proceedings of the International Symposium on Symbolic and Algebraic Computation, Beijing, China,2005,237-244P
[93]Tran Q, Vardi M Y. Groebner bases computation in Boolean rings for symbolic model checking. Proceedings of the 18th conference on Proceedings of the 18th IASTED International Conference:Modelling and
Simulation, Montreal, Quebec, Canada,2007,440-445P
[94]Wu J Z, Lin Z. Multi-valued model checking via Groebner basis approach. Proceedings of the IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, Shanghai, China,2007,35-44P
[95]Alizadeh B, Kakoee M R. Using integer equations for high level formal verification property checking. Proceedings of the International Symposium on Quality Electronic Design, San Jose, CA, USA,2003,69-74P
[96]Shekhar N, Kalla P, Enescu F, et al. Exploiting vanishing polynomial for equivalence verification of fixed-size arithmetic datapaths. Proceedngs of the International Conference of Computer Design,2005, San Jose, CA, USA, 215-220P
[97]Shekhar N, Kalla P, Enescu F, et al. Equivalence verification of polynomial datapaths with fixed-size bit-vectors using finite ring algebra. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2005,291-296P
[98]Shekhar N, Kalla P, Enescu F. Equivalence verification of arithmetic datapaths with multiple word-length operands. Proceedings of the Conference on Design Automation and Test in Europe, Munich, Germany,2006,824-829P
[99]Shekhar N, Kalla P, Enesu F. Equivalence verification of polynomial datapaths using ideal membership testing. IEEE Transactions on CAD of IC & Systems,2007,26(7):1320-1330P
[100]Shekhar N, Kalla P, Meredith B, et al. Simulation bounds for equivalence verification of arithmetic datapaths with finite word-length operands. Proceedings of the International Conference on Formal Methods in Computer Aided Design, San Jose, CA, USA,2006,179-186P
[101]Shekhar N, Kalla P, Meredith B, et al. Simulation bounds for equivalence verification of polynomial datapaths using finite ring algebra. IEEE Transactions on VLSI Systems,2008,16(4):376-387P
[102]Ghodrat M A, Givargis T, Nicolau A. Equivalence checking of arithmetic
expressions using fast evaluation. Proceedings of the International Conference on Compilers, Architectures and Synthesis for Embedded Systems, San Francisco, CA, USA,2005,147-156P
[103]Ghodrat M A, Givargis T, Nicolau A. Expression equivalence checking using interval analysis. IEEE Transactions on VLSI Systems,2006,14(8): 830-842P
[104]Van Eijk C A J. A BDD-based verification engine for combinational equivalence checking. Proceedings of the ProRISC/TEEE-Benelux Workshop on Circuits, Systems and Signal Processing, Mierlo, Netherlands,1997,155-162P
[105]Matsunaga Y. An efficient equivalence checker for combinational circuits. Proceedings of the ACM/IEEE Design Automation Conference, Las Vegas, Nevada, USA,1996,629-634P
[106]Kuehlmann A, Krohm F. Equivalence checking using cuts and heaps. Proceedings of the ACM/IEEE Design Automation Conference, Anaheim, CA, USA,1997,263-268P
[107]卢永江,严晓浪,葛海通,杨军.结合无依赖性割集和量化的等价性验证.计算机辅助设计与图形学学报,2005,17(10)：2215-2219页
[108]Pixley C. A theory and implementation of sequential hardware equivalence. IEEE Transactions on CAD of IC & Systems,1992,11(12):1469-1478P
[109]Jiang J H, Brayton R K. On the verification of sequential equivalence. IEEE Transactions on CAD of IC & Systems,2003,22(6):686-697P
[110]Rahim S, Rouzeyre B, Torres L, et al. Matching in the presence of don't cares and redundant sequential elements for sequential equivalence checking. Proceedings of the International Workshop on High Level Design Validation and Test, San Francisco, CA, USA,2003,129-134P
[111]Bjesse P, Claessen K. SAT-based verification without state space traversal. Proceedings of the International Conference on Formal Methods in Computer Aided Design, Austin, Texas, USA.2000,372-389P
[112]Eijk C A J. Sequential equivalence checking based on structural similarities. IEEE Transactions on CAD of IC & Systems,2000,19(7):814-819P
[113]郑伟伟,吴为民,边计年.基于线性规划的RTL可满足性求解和性质检验.计算机辅助设计与图形学学报,2006,18(4)：538-544页
[114]聂江波,边计年,薛宏熙等.基于模块的层次化模型判别.微电子学与计算机,2003,20(12)：64-67页
[115]Zheng W W,Wu W M, Bian J N. Hierarchical property checking for RTL circuits by LP-based satisfiability solving. Proceedings of the 6th Workshop on RTL and High level Test Symposium, Harbin, China,2005,213-218P
[116]Chen Y A, Bryant R E. ACV:an arithmetic circuit verifier. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,1996,361-365P
[117]Radecka K, Zilic Z. Design verification by test vectors and arithmetic transform universal test set. IEEE Transactions on Computers,2004,53(5): 628-640P
[2]韩俊刚,杜慧敏.数字硬件的形式化验证.北京：北京大学出版社,2001
[3]Drechsler R. Advanced Formal Verification. New York:Kluwer Academic Publishers,2004
[4]Bryant R E. Graph based algorithms for Boolean function manipulation. IEEE Transactions on Computers,1986, C-35(8):677-691P
[5]张健.逻辑公式的可满足性判定——方法、工具及应用.北京：科学出版社,2000
[6]Drechsler R. Towards formal verification on the system level. Proceedings of the 15th IEEE International Workshop on Rapid System Prototyping, Geneva, Switzerland,2004,2-5P
[7]Kroening D, Seshia S A. Formal verification at higher levels of abstraction. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2007,572-578P
[8]Cox D, Little J, O'Shea D. Ideals, Varieties and Algorithms:an Introduction to Computational Algebraic Geometry and Commutative Algebra. New York: Springer-Verlag,1997
[9]吴文俊.数学机械化.北京：科学出版社,2003
[10]王东明,夏壁灿.计算机代数.北京：清华大学出版社,2004
[11]Smith J, Micheli D G. Polynomial methods for component matching and verification. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,1998,678-685P
[12]Smith J, Micheli D G Polynomial methods for allocating complex components. Proceedings of the Conference on Design Automation and Test in Europe, Munich,Germany,1999,217-222P
[13]Smith J, Micheli D G. Polynomial circuit models for component matching in
high-level synthesis. IEEE Transactions on VLSI Systems,2001,9(6): 783-799P
[14]Peymandoust A, Micheli D G Using symbolic algebra in algorithmic level DSP synthesis. Proceedings of the ACM/IEEE Design Automation Conference, Las Vegas, NV, USA,2001,277-282P
[15]Peymandoust A, Micheli D G. Symbolic algebra and timing driven data-flow synthesis. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2001,300-305P
[16]Peymandoust A, Micheli D G Application of symbolic computer algebra in high-level data-flow synthesis. IEEE Transactions on CAD of IC & Systems, 2003,22(9):1154-1165P
[17]Xing X, Jong C C. Using symbolic computer algebra for subexpression factorization and subexpression decomposition in high level synthesis. Proceedings of the International Symposium on Circuits and Systems, Kobe, Japan,2005,5645-5648P
[18]Hosangadi A. Fallah F, Kastner R. Factoring and eliminating common subexpressions in polynomial expressions. Proceedings of the IEEE/ACM International Conference on Computer Aided Design,2004,169-174P
[19]Hosangadi A, Fallah F, Kastner R. Energy efficient hardware synthesis of polynomial expressions. Proceedings of the International Conference on VLSI Design, Kolkata, India,2005,653-658P
[20]Hosangadi A, Fallah F, Kastner R. Reducing hardware complexity of linear DSP systems by iteratively eliminating two-term common subexpressions. Proceedngs of the Asia and South Pacific Design Automation Conference, Yokohama, Japan,2005,532-528P
[21]Hosangadi A, Fallah F, Kastner R. Optimizing polynomial expressions by algebraic factorization and common subexpression elimination. IEEE Transactions on CAD of IC & Systems,2006,25(10):2012-2022P
[22]Gopalakrishnan S, Kalla P, Enescu F. Optimizing fixed-size bit-vector arithmetic using finite ring algebra. Proceedings of the International
Workshop on Logic and Synthesis, Vail, Colorado, USA,2006,110-117P
[23]Gopalakrishnan S, Kalla P, Meredith M B, et al. Finding linear building-blocks for RTL synthesis of polynomial datapaths with fixed-size bit-vectors. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2007,413-418P
[24]Gopalakrishnan S, Kalla P. Optimization of polynomial datapaths using finite ring algebra. ACM Transactions on Design Automation of Electronic Systems,2007,12(4):1-30P
[25]Ciesielski M, Kalla P, Askar S. Taylor expansion diagrams:a canonical representation for verification of data flow designs. IEEE Transactions on Computers,2006,55(9):1188-1201P
[26]季晓慧,张健.约束问题求解.自动化学报,2007,33(2)：125-131页
[27]DeMoura L, Dutertre B, Shankar N. A tutorial on satisfiability modulo theories. Proceedings of the International Conference on Computer Aided Verification, Berlin, Germany,2007,20-36P
[28]Sebastiani R. Lazy satisability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation,2007,3(1):141-224P
[29]邓澍军,吴为民,边计年.RTL验证中的混合可满足性求解.计算机辅助设计与图形学学报,2007,19(3)：273-278页
[30]K. L. McMillan. Symbolic Model Checking. Boston:Kluwer Academic Publisher,1993.
[31]Fujita M, McGeer P C, Yang J C-Y. Multi terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods in System Design,1997,10(2-3):149-169P
[32]Bryant R E, Chen Y A. Verification of arithmetic circuits with binary moment diagram. Proceedings of the ACM/IEEE Design Automation Conference, San Francisco, CA, USA,1995,535-541P
[33]Lai Y T, Pedram M, Vrudhula S B K. Formal verification using edge-valued binary decision diagrams. IEEE Transactions on Computers,1996,45(2): 247-255P
[34]Drechsler R, Horeth S. Manipulation of *BMD. Proceedings of the Asia South Pacific Design Automation Conference, Tokyo, Japan,1998,433-438P
[35]Keim M, Dreschler R, Becker B, et al. Polynomial formal verification of multipliers. Formal Methods in System Design,2003,22(1):39-58P
[36]Ciesielski M, Kalla P, Zeng Z, et al. Taylor expansion diagrams:a compact canonical representation with application to symbolic verification, Procee-dngs of the Conference on Design Automation and Test in Europe, Paris, France,2002,285-289P
[37]Fey G, Drechsler R, Ciesielski M. Algorthms for Taylor expansion diagrams. Proceedings of the IEEE International Symposium on Multiple-Valued Logic, Toronto, Canada,2004,235-240P
[38]Gomez-Prado D, Ren Q, Askar S, et al. Variable ordering for Taylor expansion diagrams. Proceedings of the International Workshop on High Level Design Validation and Test, Sonoma Valley, CA, USA,2004,55-59P
[39]Kalla P, Ciesielski M, Boutillon E, et al. High-level design verification using Taylor expansion diagrams:first results. Proceedings of the International Workshop on High Level Design Validation and Test, Cannes, France,2002, 13-17P
[40]Guillot J, Boutillon E, Ren Q, et al. Efficient factorization of DSP transforms using Taylor expansion diagrams. Proceedings of the Conference on Design Automation and Test in Europe, Munich, Germany,2006,754-755P
[41]Ciesielski M, Askar S, Gomez-Prado D, et al. Data-flow transformations using Taylor expansion diagrams. Proceedings of the Conference on Design Automation and Test in Europe, Nice, France,2007,455-460P
[42]Gu J, Purdom P W, Franco J, et al. Algorithms for the satisfiability (SAT) problem:a survey. DIMACS Series on Discrete Mathematics and Theoretical Computer Science,1997,35:19-151P
[43]Bordeaux L, Hamadi Y, Zhang L. Propositional satisfiability and constraint programming:a comparative survey. ACM Computing Surveys,2006,38(4): 1-54P
[44]Gu J. Local search for satisfiability (SAT) problem. IEEE Transactions on Systems, Man and Cybernetics,1993,23(4):1108-1129P
[45]Gu J. Global Optimization for satisfiability (SAT) problem. IEEE Transac-tions on Data and Knowledge Engineering,1994,6(3):361-381P
[46]Selman B, Levesque H, Mitchell D. A new method for solving hard satisfiability problems. Proceedings of the National Conference on Artificial and Intelligence, San Jose, CA, USA,1992,440-446P
[47]Frank J. Weighting for godot:learning heuristic for GSAT. Proceedings of the National Conference on Artificial and Intelligence, Portland, OR, USA, 1996,338-343P
[48]Selman B, Kautz H A, Cohen B. Noise strategies for improving local search. Proceedings of the National Conference on Artificial and Intelligence, Seattle, WA, USA,1994,337-343P
[49]Davis M, Logemann G, Loveland D. A machine program for theorem proving. Communications of the ACM,1962,5(7):394-397P
[50]Li X W, Li G H, Shao M. Formal verification techniques based on Boolean satisfiability Problem. Journal of Computer Science and Technology,2005, 20(1):38-47P
[51]Prasad M, Biere A, Gupta A. A survey of recent advances in SAT-based formal verification. Software Tools for Technology Transfer,2005,7(2): 156-173P
[52]Goldberg E I, Prasad M R, Brayton R K. Using SAT for combinational equivalence checking. Proceedings of the Conference on Design Automa-tion and Test in Europe, Munich, Germany,2001,114-121P
[53]郑飞君,严晓浪,葛海通等.使用布尔可满足性的组合电路等价性验证算法.电子与信息学报,2005,27(4)：651-654页
[54]李光辉,李晓维.基于增量可满足性的等价性检验方法.计算机学报,2004,27(10)：1388-1394页
[55]Disch S, Schollm C. Combinational equivalence checking using incremental SAT solving, Output Ordering, and Resets. Proceedings of the Asia South
Pacific Design Automation Conference, Yokohama, Japan,2007,938-943P
[56]Khasidashvili Z, Hanna Z. SAT-based methods for sequential hardware equivalence verification without synchronization. Electronic Notes in Theoretical Computer Science,2003,89(4):593-607P
[57]Syal M, Hsiao M. VERISEC:Verifying equivalence of sequential circuits using SAT. Proceedings of the International Workshop on High Level Design Validation and Test, Napa, CA, USA,2005,52-59P
[58]丁敏,唐璞山.改进的时间帧展开的时序电路等价验证算法.计算机辅助设计与图形学学报,2006,18(1)：53-61页
[59]Biere A, Cimatti A, Clarke E, et al. Symbolic model checking without BDDs. Proceedings of the International Conference on Tools and Algorithm for Construction and Analysis of Systems, Amsterdam, Netherlands,1999,193-207P
[60]Clarke E, Biere A, Raimi A, et al. Bounded model checking using satisfiability solving. Formal Methods in System Design,2001,19(1):7-34P
[61]Biere A, Cimatti A, Clarke E, et al. Bounded model checking. Advances in Computers,2003,58(1):118-149P
[62]McMillan K L. Applying SAT methods in unbounded symbolic model checking. Proceedings of the International Conference on Computer Aided Verification, Copenhagen, Denmark,2002,250-264P
[63]Kang H J, Park I C. SAT-based unbounded symbolic model checking. Proceedings of the ACM/IEEE Design Automation Conference, Anaheim, CA, USA,2003,840-843P
[64]Ganai M K, Gupta A, Ashar P. Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA, 2004,510-517P
[65]Bryant R E, Lahiri S K, Seshia S A. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. Proceedings of the International Conference on Computer Aided
Verification, Copenhagen, Denmark,2002,78-92P
[66]Strichman O. On solving presburger and linear arithmetic with SAT. Proceedings of the International Conference on Formal Methods in Computer Aided Design, Portland, Oregon, USA,2002,160-170P
[67]Strichman O, Seshia S A, Bryant R E. Deciding separation formulas with SAT. Proceedings of the International Conference on Computer Aided Verification,2002,209-222P
[68]Seshia S A, Lahiri S K, Bryant R E. A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. Proceedings of the ACM/IEEE Design Automation Conference, Anaheim, CA, USA,2003, 425-430P
[69]Bozzano M, Bruttomesso R, Cimatti A, et al. An incremental and layered procedure for the satisfiability of linear arithmetic logic. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Edinburgh, Scotland,2005,317-333P
[70]Dutertre B, DeMoura L. A fast linear-arithmetic solver for DPLL(T). Proceedings of the International Conference on Computer Aided Verification, Seattle, WA, USA,2006,81-94P
[71]DeMoura L, Bjorner N. Z3:An efficient SMT solver. Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems, Budapest, Hungary,2008,337-340P
[72]Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories:from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM,2006,53(6):937-977P
[73]Ganzinger H, Hagen G, Nieuwenhuis R, et al. DPLL(T):fast decision procedures. Proceedings of the International Conference on Computer Aided Verification, Boston, MA, USA,2004,175-188P
[74]Fallah F, Devadas S, Keutzer K. Functional vector generation for HDL models using linear programming and 3-satisfiability. Proceedings of the ACM/IEEE Design Automation Conference, San Francico, CA, USA,1998,
528-533P
[75]Fallah F, Devadas S, Keutzer K. Functional vector generation for HDL models using linear programming and Boolean satisfiability. IEEE Transactions on CAD,2001,20(8):994-1002P
[76]Huang C Y, Cheng K T. Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques. Proceedings of the ACM/IEEE Design Automation Conference, Los Angeles, CA, USA,2000, 118-123P
[77]Huang C Y, Cheng K T. Using word-level ATPG and modular arithmetic constraint-solving techniques for assertion property checking. IEEE Transactions on CAD,2001,20(3):381-391P
[78]Wu S H, Chen M C, Wu W M, et al. RTL property checking technology based on ATPG and ILP. Proceedings of the International Conference on ASIC, Shanghai, China,2005,890-893P
[79]Zeng Z, Kalla P, Ciesielski M. LPSAT:a unified approach to RTL satisfiability. Proceedngs of the Conference on Design Automation and Test in Europe, Munich, Germany,2001,398-402P
[80]Zeng Z, Talupuru K R, Ciesielski M. Functional test generation based on word-level SAT. Journal of Systems Architecture,2005,51(8):488-511P
[81]Navarro H, Montiel-Nelson J A, Sosa J, et al. Multiplexer model for RTL satisfiability using MILP. Electronics Letters,2004,40(7):417-418P
[82]Brinkmann R, Rolf D. RTL-datapath verification using integer linear programming. Proceedngs of the Asia and South Pacific Design Automation Conference, Bangalore, India,2002,741-746P
[83]Ugarte I, Sanchez P. Assertion checking of behavioral descriptions with non-linear solver. Proceedngs of the International Conference of Computer Design, San Jose, CA, USA,2005,229-231P
[84]Ugarte I, Sanchez P. Assertion-based verification of behavioral descriptions with non-linear solver. Proceedings of the International Workshop on High Level Design Validation and Test, Monterey, CA,USA,2006.61-68P
[85]Liu C, Kuehlmann A, Moskewicz M W. CAMA:a multi-valued satisfiability solver. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2003,326-333P
[86]Parthasarathy G, Iyer M K, Cheng K T, et al. An efficient finite-domain constraint solver for circuits. Proceedings of the ACM/IEEE Design Automation Conference, San Diego, CA, USA,2004,212-217P
[87]Deng S J, Bian J N, Wu W M, et al. EHSAT:an efficient RTL satisfiability solver using an extended DPLL procedure. Proceedings of the ACM/IEEE Design Automation Conference, San Diego, CA, USA,2007,588-593P
[88]Parthasarathy G, Iyer M K, Cheng K T, et al. Structural search for RTL with predicate learning. Proceedings of the ACM/IEEE Design Automation Conference, San Diego, CA, USA,2005,451-456P
[89]Pradhan D K, Askar S, Ciesielski M. Mathematical framework for representing discrete functions as word-level polynomials. Proceedings of International Workshop on High Level Design Validation and Test, San Francisco, CA, USA,2003,135-139P
[90]Raudvere K, Singh K A, Sander I, et al. Polynomial abstraction for verification of sequentially implemented combinational circuits. Proceedings of the Conference on Design Automation and Test in Europe, Paris, France, 2004,690-691P
[91]Raudvere K, Singh K A, Sander I, et al. System level verification of digital signal processing application based on the polynomial abstraction technique. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2005,285-290P
[92]Mao W B, Wu J Z. Application of Wu's method to symbolic model checking. Proceedings of the International Symposium on Symbolic and Algebraic Computation, Beijing, China,2005,237-244P
[93]Tran Q, Vardi M Y. Groebner bases computation in Boolean rings for symbolic model checking. Proceedings of the 18th conference on Proceedings of the 18th IASTED International Conference:Modelling and
Simulation, Montreal, Quebec, Canada,2007,440-445P
[94]Wu J Z, Lin Z. Multi-valued model checking via Groebner basis approach. Proceedings of the IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, Shanghai, China,2007,35-44P
[95]Alizadeh B, Kakoee M R. Using integer equations for high level formal verification property checking. Proceedings of the International Symposium on Quality Electronic Design, San Jose, CA, USA,2003,69-74P
[96]Shekhar N, Kalla P, Enescu F, et al. Exploiting vanishing polynomial for equivalence verification of fixed-size arithmetic datapaths. Proceedngs of the International Conference of Computer Design,2005, San Jose, CA, USA, 215-220P
[97]Shekhar N, Kalla P, Enescu F, et al. Equivalence verification of polynomial datapaths with fixed-size bit-vectors using finite ring algebra. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,2005,291-296P
[98]Shekhar N, Kalla P, Enescu F. Equivalence verification of arithmetic datapaths with multiple word-length operands. Proceedings of the Conference on Design Automation and Test in Europe, Munich, Germany,2006,824-829P
[99]Shekhar N, Kalla P, Enesu F. Equivalence verification of polynomial datapaths using ideal membership testing. IEEE Transactions on CAD of IC & Systems,2007,26(7):1320-1330P
[100]Shekhar N, Kalla P, Meredith B, et al. Simulation bounds for equivalence verification of arithmetic datapaths with finite word-length operands. Proceedings of the International Conference on Formal Methods in Computer Aided Design, San Jose, CA, USA,2006,179-186P
[101]Shekhar N, Kalla P, Meredith B, et al. Simulation bounds for equivalence verification of polynomial datapaths using finite ring algebra. IEEE Transactions on VLSI Systems,2008,16(4):376-387P
[102]Ghodrat M A, Givargis T, Nicolau A. Equivalence checking of arithmetic
expressions using fast evaluation. Proceedings of the International Conference on Compilers, Architectures and Synthesis for Embedded Systems, San Francisco, CA, USA,2005,147-156P
[103]Ghodrat M A, Givargis T, Nicolau A. Expression equivalence checking using interval analysis. IEEE Transactions on VLSI Systems,2006,14(8): 830-842P
[104]Van Eijk C A J. A BDD-based verification engine for combinational equivalence checking. Proceedings of the ProRISC/TEEE-Benelux Workshop on Circuits, Systems and Signal Processing, Mierlo, Netherlands,1997,155-162P
[105]Matsunaga Y. An efficient equivalence checker for combinational circuits. Proceedings of the ACM/IEEE Design Automation Conference, Las Vegas, Nevada, USA,1996,629-634P
[106]Kuehlmann A, Krohm F. Equivalence checking using cuts and heaps. Proceedings of the ACM/IEEE Design Automation Conference, Anaheim, CA, USA,1997,263-268P
[107]卢永江,严晓浪,葛海通,杨军.结合无依赖性割集和量化的等价性验证.计算机辅助设计与图形学学报,2005,17(10)：2215-2219页
[108]Pixley C. A theory and implementation of sequential hardware equivalence. IEEE Transactions on CAD of IC & Systems,1992,11(12):1469-1478P
[109]Jiang J H, Brayton R K. On the verification of sequential equivalence. IEEE Transactions on CAD of IC & Systems,2003,22(6):686-697P
[110]Rahim S, Rouzeyre B, Torres L, et al. Matching in the presence of don't cares and redundant sequential elements for sequential equivalence checking. Proceedings of the International Workshop on High Level Design Validation and Test, San Francisco, CA, USA,2003,129-134P
[111]Bjesse P, Claessen K. SAT-based verification without state space traversal. Proceedings of the International Conference on Formal Methods in Computer Aided Design, Austin, Texas, USA.2000,372-389P
[112]Eijk C A J. Sequential equivalence checking based on structural similarities. IEEE Transactions on CAD of IC & Systems,2000,19(7):814-819P
[113]郑伟伟,吴为民,边计年.基于线性规划的RTL可满足性求解和性质检验.计算机辅助设计与图形学学报,2006,18(4)：538-544页
[114]聂江波,边计年,薛宏熙等.基于模块的层次化模型判别.微电子学与计算机,2003,20(12)：64-67页
[115]Zheng W W,Wu W M, Bian J N. Hierarchical property checking for RTL circuits by LP-based satisfiability solving. Proceedings of the 6th Workshop on RTL and High level Test Symposium, Harbin, China,2005,213-218P
[116]Chen Y A, Bryant R E. ACV:an arithmetic circuit verifier. Proceedings of the IEEE/ACM International Conference on Computer Aided Design, San Jose, CA, USA,1996,361-365P
[117]Radecka K, Zilic Z. Design verification by test vectors and arithmetic transform universal test set. IEEE Transactions on Computers,2004,53(5): 628-640P
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |