Please wait a minute...
浙江大学学报(工学版)
J4  2010, Vol. 44 Issue (2): 289-293    DOI: 10.3785/j.issn.1008-973X.2010.02.014
计算机技术﹑电信技术     
一种基于混合SAT求解器的RTL验证方法
葛海通, 翁延玲, 严晓浪
（浙江大学 超大规模集成电路设计研究所,浙江 杭州 310027）
Register transfer level verification system based on hybrid satisfiability engine
GE Hai-tong, WENG Yan-ling, YAN Xiao-lang
(Institute of VLSI Design, Zhejiang University, Hangzhou 310027, China)
 全文: PDF  HTML
摘要：

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

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%.
出版日期: 2010-03-09
:  TN 47  
基金资助:

国家自然科学基金资助项目（90207002）.
通讯作者: 葛海通(1972—)，男，浙江宁海人, 高工.     E-mail: haitong_ge@c-sky.com
服务　　
把本文推荐给朋友
加入引用管理器
E-mail Alert
RSS
作者相关文章　　

引用本文:

葛海通, 翁延玲, 严晓浪. 一种基于混合SAT求解器的RTL验证方法[J]. J4, 2010, 44(2): 289-293.

GE Hai-Tong, WENG Yan-Ling, YAN Xiao-Lang. Register transfer level verification system based on hybrid satisfiability engine. J4, 2010, 44(2): 289-293.

链接本文:

http://www.zjujournals.com/eng/CN/10.3785/j.issn.1008-973X.2010.02.014    或    http://www.zjujournals.com/eng/CN/Y2010/V44/I2/289

［1］  MARQUES-SILVA J P, SAKALLAH K A. GRASP: a search algorithm for propositional satisfiability［J］. IEEE Transaction on Computers, 1999, 48(5): 506521.
［2］ KUEHLMANN A, GANAI M K, PARUTHI V. Circuit-based boolean reasoning［C］// Proceedings of 2001 ACM/IEEE Design Automation Conference. Anaheim, CA: ACM, 2001: 232237.
［3］ ZHANG H, STICKEL M. An efficient algorithm for unit propagation［C］// Proceeding of the 4th International Symposium on Artificial Intelligence and Mathematics. Florida: ［s. n.］, 1996: 166179.
［4］ STALLMAN R, SUSSMAN G. Forward reasoning and dependency directed backtracking in a system for computer aided circuit analysis ［J］. Artificial Intelligence, 1977, 9(2): 135196.
［5］ LU F, WANG L C, CHENG K T, et al. A signal correlation guided ATPG solver and its applications for solving difficult industrial cases［C］// Proceedings of 2003 ACM/IEEE Design Automation Conference. Anaheim: ［s. n.］, 2003: 668673.
［6］ 翁延玲, 葛海通,严晓浪.等价性验证中的自动算符排序［J］.浙江大学学报：工学版,2007,41(6): 886889.
WENG Yan-ling, GE Hai-tong, YAN Xiao-lang. Automatic operand ordering for equivalence checking［J］. Journal of Zhejiang University：Engineering Science, 2007, 41(6): 886889.
［7］ PARTHASARATHY G, IYER M, CHENG K T, et al. An efficient finite-domain constraint solver for RTL circuits［C］// Proceedings of the ACM/IEEE Design Automation Conference. New York: ACM, 2004: 212217.
［8］ 郑伟伟,吴为民,边计年.基于线性规划的RTL可满足性求解和性质检验［J］.计算机辅助设计与图形学学报,2006,18(4): 538543.
ZHENG Wei-wei, WU Wei-min, BIAN Ji-nian. RTL satisfiability solving and property checking based on linear programming ［J］. Journal of Computer-Aided Design and Computer Graphics, 2006, 18(4): 538543.
［9］ FALLAH F,DEVADAS S,KEUTZER K. Functional vector generation for HDL models using linear programming and 3-satisfiabillty［C］// Proceedings of the 35th Design Automation Conference. San Francisco, CA: ACM, 1998: 528533.
［10］ FALLAH F. Coverage directed validation of hardware models［D］. Massachusetts: Massachusetts Institute of Technology,1999.
［11］ ZENG Zhi-hong, KALLA P, CIESIELSKI M. LPSAT: a unified approach to RTL satisfiability ［C］// Proceedings of the Conference on Design Automation and Test in Europe. New York: ACM, 2001: 398402.
[1] 黄凯杰, 黄凯, 马德, 王钰博, 冯炯, 葛海通, 严晓浪. 基于IP-XACT标准的SoC集成方法[J]. J4, 2013, 47(10): 1770-1776.
[2] 张洋, 王秀敏, 陈豪威. 基于FPGA的低密度奇偶校验码编码器设计[J]. J4, 2011, 45(9): 1582-1586.