| 一种基于混合SAT求解器的RTL验证方法 |
| |
| 引用本文： | 葛海通,翁延玲,严晓浪. 一种基于混合SAT求解器的RTL验证方法[J]. 浙江大学学报(工学版), 2010, 44(2): 289-293. DOI: 10.3785/j.issn.1008-973X.2010.02.014 |
| |
| 作者姓名： | 葛海通 翁延玲 严晓浪 |
| |
| 作者单位： | （浙江大学 超大规模集成电路设计研究所,浙江 杭州 310027） |
| |
| 基金项目： | 国家自然科学基金资助项目（90207002）. |
| |
| 摘 要： | 为了提高集成电路验证系统的性能,提出一种面向Verilog描述的寄存器传输级（RTL）电路验证方法.该方法将验证问题转化为RTL可满足性问题,并采用基于混合布尔可满足性问题（SAT）的求解器.与传统方法相比,其综合引擎取消了算术电路逻辑的实现,保留了电路特性及其优化信息.因为所需的待验证模型的抽象层次较高,综合系统所花的综合时间较少,尤其是验证引擎不需要处理较低级别的验证细节,由此大大提升了系统性能.不同规模的加法器实验结果表明,基于混合SAT引擎的RTL验证流程较传统流程有明显优势,对复杂电路的验证时间甚至可减少99%.
|
| 关 键 词： | 集成电路设计 逻辑综合 等价性验证 混合SAT求解器 |
Register transfer level verification system based on hybrid satisfiability engine |
| |
| GE Hai-tong,WENG Yan-ling,YAN Xiao-lang. Register transfer level verification system based on hybrid satisfiability engine[J]. Journal of Zhejiang University(Engineering Science), 2010, 44(2): 289-293. DOI: 10.3785/j.issn.1008-973X.2010.02.014 |
| |
| Authors: | GE Hai-tong WENG Yan-ling YAN Xiao-lang |
| |
| Affiliation: | (Institute of VLSI Design, Zhejiang University, Hangzhou 310027, China) |
| |
| Abstract: | |
| |
| Keywords: | integrate circuit design logic synthesis equivalence checking hybrid SAT engine |
|
| 点击此处可从《浙江大学学报(工学版)》浏览原始摘要信息 |
|
点击此处可从《浙江大学学报(工学版)》下载全文 |
|
