RTL验证中的混合可满足性求解
验证是当前越来越复杂的集成电路设计中的瓶颈,在寄存器传输级(RTL)直接做验证是目前比较有效的一种途径.RTL混合可满足性求解是RTL验证中的关键技术.本文将RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.基于SMT的求解方法主要使用逻辑推理的方法,目前在处理器验证中获得了广泛的应用,这主要得益于SMT支持用于描述验证条件的基础理论.基于电路结构搜索的方法能够充分利用电路中的约束信息,因而求解效率较高.文中分别介绍了每一大类中的典型研究及它们所采用的重要策略,并对不同方法的优缺点和运行效率进行了对比.本文还介绍了我们在RTL可满足性求解方面的研究进展.
形式验证 寄存器传输级 模理论 集成电路设计
邓澍军 吴为民 边计年
清华大学计算机科学与技术系,北京,100084
国内会议
北戴河
中文
417-423
2006-08-07（万方平台首次上网日期，不代表论文的发表时间）