標題: Efficient Coverage-Driven Stimulus Generation Using Simultaneous SAT Solving, with Application to SystemVerilog
作者: Cheng, An-Che
Yen, Chia-Chih (Jack)
Val, Celina G.
Bayless, Sam
Hu, Alan J.
Jiang, Iris Hui-Ru
Jou, Jing-Yang
電子工程學系及電子研究所
Department of Electronics Engineering and Institute of Electronics
關鍵字: Algorithms;Verification;Formal methods;covergroup;simultaneous satisfiability
公開日期: 1-十一月-2014
摘要: SystemVerilog provides powerful language constructs for verification, and one of them is the covergroup functional coverage model. This model is designed as a complement to assertion verification, that is, it has the advantage of defining cross-coverage over multiple coverage points. In this article, a coverage-driven verification (CDV) approach is formulated as a simultaneous Boolean satisfiability (SAT) problem that is based on covergroups. The coverage bins defined by the functional model are converted into Conjunction Normal Form (CNF) and then solved together by our proposed simultaneous SAT algorithm PLNSAT to generate stimuli for improving coverage. The basic PLNSAT algorithm is then extended in our second proposed algorithm GPLNSAT, which exploits additional information gleaned from the structure of SystemVerilog covergroups. Compared to generating stimuli separately, the simultaneous SAT approaches can share learned knowledge across each coverage target, thus reducing the overall solving time drastically. Experimental results on a UART circuit and the largest ITC benchmark circuits show that the proposed algorithms can achieve 10.8x speedup on average and outperform state-of-the-art techniques in most of the benchmarks.
URI: http://dx.doi.org/10.1145/2651400
http://hdl.handle.net/11536/123922
ISSN: 1084-4309
DOI: 10.1145/2651400
期刊: ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS
Volume: 20
顯示於類別:期刊論文


文件中的檔案:

  1. 000345523400007.pdf