首页 | 本学科首页   官方微博 | 高级检索  
     

RTL验证中的混合可满足性求解
引用本文:邓澍军,吴为民,边计年.RTL验证中的混合可满足性求解[J].计算机辅助设计与图形学学报,2007,19(3):273-278,285.
作者姓名:邓澍军  吴为民  边计年
作者单位:清华大学计算机科学与技术系,北京,100084
基金项目:国家自然科学基金 , 国家自然科学基金 , 国家重点基础研究发展计划(973计划)
摘    要:RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.

关 键 词:形式验证  寄存器传输级  可满足性  可满足性模理论  验证  混合  可满足性  求解方法  Verification  Satisfiability  研究进展  重要策略  效率  约束信息  电路结构  利用  条件  描述  支持  应用  处理器  逻辑推理  使用  搜索
收稿时间:2006-07-20
修稿时间:2006-07-202006-09-20

Hybrid Satisfiability Solving for RTL Verification
Deng Shujun,Wu Weimin,Bian Jinian.Hybrid Satisfiability Solving for RTL Verification[J].Journal of Computer-Aided Design & Computer Graphics,2007,19(3):273-278,285.
Authors:Deng Shujun  Wu Weimin  Bian Jinian
Affiliation:Department of Computer Science and Technology, Tsinghua University, Beijing 100084
Abstract: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 satisfiability solving for our Formal Verification Research Group is also introduced.
Keywords:formal verification  register transfer level  satisfiability  satisfiability modulo theories (SMT)
本文献已被 CNKI 维普 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号