QQ客服 官方微博 反馈留言

	RTL验证中的混合可满足性求解
	邓澍军 ; 吴为民 ; 边计年 ; Deng Shujun ; Wu Weimin ; Bian Jinian
	2010-07-15 ; 2010-07-15
会议名称	第四届中国测试学术会议论文集 ; 第四届中国测试学术会议 ; 中国河北秦皇岛北戴河 ; CNKI ; 中国计算机学会容错计算专业委员会
关键词	形式验证 寄存器传输级 可满足性 可满足性模理论 formal verification, register transfer level, satisfiability, SMT TN402
其他题名	Hybrid Satisfiability Solving for RTL Verification
中文摘要	验证是当前越来越复杂的集成电路设计中的瓶颈,在寄存器传输级(RTL)直接做验证是目前比较有效的一种途径。RTL混合可满足性求解是RTL验证中的关键技术。本文将RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类。基于SMT的求解方法主要使用逻辑推理的方法,目前在处理器验证中获得了广泛的应用,这主要得益于SMT支持用于描述验证条件的基础理论。基于电路结构搜索的方法能够充分利用电路中的约束信息,因而求解效率较高。文中分别介绍了每一大类中的典型研究及它们所采用的重要策略,并对不同方法的优缺点和运行效率进行了对比。本文还介绍了我们在RTL可满足性求解方面的研究进展。; 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.; 国家自然科学基金项目(NSFC-60273011和NSFC-60236020); 国家重点基础研究项目(973-2005CB321605)的资助
语种	中文 ; 中文
内容类型	会议论文
源URL	[http://hdl.handle.net/123456789/69993]
专题	清华大学
推荐引用方式 GB/T 7714	邓澍军,吴为民,边计年,等. RTL验证中的混合可满足性求解[C]. 见:第四届中国测试学术会议论文集, 第四届中国测试学术会议, 中国河北秦皇岛北戴河, CNKI, 中国计算机学会容错计算专业委员会.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。