【作者】 邓澍军； 吴为民； 边计年；

【Author】 Deng Shujun, Wu Weimin, Bian Jinian Department of Computer Science and Technology, Tsinghua University, Beijing 100084

【机构】 清华大学计算机科学与技术系；

【摘要】 验证是当前越来越复杂的集成电路设计中的瓶颈,在寄存器传输级(RTL)直接做验证是目前比较有效的一种途径。RTL混合可满足性求解是RTL验证中的关键技术。本文将RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类。基于SMT的求解方法主要使用逻辑推理的方法,目前在处理器验证中获得了广泛的应用,这主要得益于SMT支持用于描述验证条件的基础理论。基于电路结构搜索的方法能够充分利用电路中的约束信息,因而求解效率较高。文中分别介绍了每一大类中的典型研究及它们所采用的重要策略,并对不同方法的优缺点和运行效率进行了对比。本文还介绍了我们在RTL可满足性求解方面的研究进展。更多还原

【Abstract】 Verification is the bottleneck of more and more complex integrated circuit designs, and doing verification directly on register transfer level (RTL) is a promising solution. RTL hybrid satisfiability solving is the key technique of RTL verification. This paper classifies the RTL hybrid satisfiability solving methods into two classes: One is based on Satisfiability Modulo Theories (SMT), and the other is based on circuit structure search. The methods based on SMT mainly use logic reasoning, and are widely applied in processor verification because SMT supports the foundation theories used to express the verification conditions. The methods based on circuit structure search are efficient because they can take full advantage of constraint information in circuits. Representative works and their key strategies are introduced for each class respectively. Advantages and disadvantages of different methods and their efficiencies are compared. Research progress of RTL hybrid satisfiability solving for our Formal Verification Research Group is also introduced.更多还原