计算机技术﹑电信技术 |
|
|
|
|
一种基于混合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) |
[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. |
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|