RTL验证中的混合可满足性求解

摘要：

RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.

关键词：形式验证、寄存器传输级、可满足性、可满足性模理论

所属期刊栏目：19

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金60273011;60673034;国家自然科学基金60236020;90607001;国家重点基础研究发展计划973计划2005CB321605

在线出版日期：2007-04-19（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：273-278,285