摘要
RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.
RTL hybrid satisfiability solving methods are classified into two categories： One is based on SMT （Satisfiability Modulo Theories）, and the other is based on circuit structure searching. The methods of the former category mainly use logic reasoning, and are widely applied in processor verification because SMT supports the fundamental theories used to express the verification conditions. The methods of the latter category are efficient because they can take full advantage of constraint information in circuits. Representative works and their key strategies are introduced for each category. Research progress of RTL hybrid sa＇tisfiability solving for our Formal Verification Research Group is also introduced.
出处
《计算机辅助设计与图形学学报》
EI
CSCD
北大核心
2007年第3期273-278,285,共7页
Journal of Computer-Aided Design & Computer Graphics
基金
国家自然科学基金(60273011
60673034)
国家自然科学基金重点项目(60236020
90607001)
国家"九七三"重点基金研究发展规划项目(2005CB321605)
关键词
形式验证
寄存器传输级
可满足性
可满足性模理论
formal verification
register transfer level
satisfiability
satisfiability modulo theories （SMT）
