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

Register transfer level verification system based on hybrid satisfiability engine

作　　者：葛海通[1] 翁延玲[1] 严晓浪[1] 

机构地区：[1]浙江大学超大规模集成电路设计研究所,浙江杭州310027

出　　处：《浙江大学学报（工学版）》2010年第2期289-293,共5页Journal of Zhejiang University：Engineering Science

基　　金：国家自然科学基金资助项目(90207002)

摘　　要：为了提高集成电路验证系统的性能,提出一种面向Verilog描述的寄存器传输级(RTL)电路验证方法.该方法将验证问题转化为RTL可满足性问题,并采用基于混合布尔可满足性问题(SAT)的求解器.与传统方法相比,其综合引擎取消了算术电路逻辑的实现,保留了电路特性及其优化信息.因为所需的待验证模型的抽象层次较高,综合系统所花的综合时间较少,尤其是验证引擎不需要处理较低级别的验证细节,由此大大提升了系统性能.不同规模的加法器实验结果表明,基于混合SAT引擎的RTL验证流程较传统流程有明显优势,对复杂电路的验证时间甚至可减少99%.A new verification method for Verilog described register transfer level （RTL） was proposed to improve verification performance.The method transformed a verification problem to RTL satisfiability （SAT） one based on hybrid SAT engine.The synthesis engine replaced the implementation of arithmetic circuit with abstract description compared with traditional method.Because the abstract level was much higher,the verification engine was not be involved in details of lower-level implementation.Then the system performance was greatly improved.Experimental results show that RTL verification flow based on hybrid SAT engine has obvious advantage and the verification time for complex circuits can even be reduced as much as 99%.

关 键 词：集成电路设计 逻辑综合 等价性验证 混合SAT求解器 

分 类 号：TN47[电子电信—微电子学与固体电子学]