一种基于混合SAT求解器的RTL验证方法

• 作者: 严晓浪 翁延玲 葛海通
• 来源期刊: 浙江大学学报(工学版)
• 学科: 工学
• 关键词: 集成电路设计 逻辑综合 等价性验证 混合SAT求解器
• 年，卷（期）: 2010,（2）
• 所属期刊栏目: 计算机技术、电信技术
• 页码范围: 289-293
• 页数: 5页
• 分类号: TN47
• 语种: 中文
• DOI: 10.3785/j.issn.1008-973X.2010.02.014

摘要

为了提高集成电路验证系统的性能,提出一种面向Verilog描述的寄存器传输级(RTL)电路验证方法.该方法将验证问题转化为RTL可满足性问题,并采用基于混合布尔可满足性问题(SAT)的求解器.与传统方法相比,其综合引擎取消了算术电路逻辑的实现,保留了电路特性及其优化信息.因为所需的待验证模型的抽象层次较高,综合系统所花的综合时间较少,尤其是验证引擎不需要处理较低级别的验证细节,由此大大提升了系统性能.不同规模的加法器实验结果表明,基于混合SAT引擎的RTL验证流程较传统流程有明显优势,对复杂电路的验证时间甚至可减少99%.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	严晓浪		246	1634	19.0	29.0
2	葛海通		52	293	8.0	14.0
3	翁延玲		5	16	3.0	4.0