Efficient coverage-driven stimulus generation using simultaneous SAT solving, with application to SystemVerilog

NCUIR > administration > Office of Secretariat > journal & Dissertation > Item 987654321/104737

Please use this identifier to cite or link to this item: https://ir.lib.ncu.edu.tw/handle/987654321/104737

Title:	Efficient coverage-driven stimulus generation using simultaneous SAT solving, with application to SystemVerilog
Authors:	周景揚;Cheng, An-Che;Yen, Chia-Chih (Jack);Val, Celina G.;Bayless, Sam;Hu, Alan J.;Jiang, Iris Hui-Ru;Jou, Jing-Yang
Contributors:	秘書室
Keywords:	Algorithms;Benchmarking;Bins;Circuits;Complement;Design engineering;Electronic systems;Stimuli
Date:	2014-01-01
Issue Date:	2026-04-23 11:56:52 (UTC+8)
Publisher:	Association for Computing Machinery (ACM)
Abstract:	摘要： 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. 出版日期： 2014-11-18 出處： ACM transactions on design automation of electronic systems, 2014-11, Vol.20 (1), p.1-23 資源來源： ACM Digital Library Complete 識別號： ISSN: 1084-4309 識別號： EISSN: 1557-7309 識別號： DOI: 10.1145/2651400
Appears in Collections:	[Office of Secretariat] journal & Dissertation

Files in This Item:

File	Description	Size	Format
index.html		0Kb	HTML	29	View/Open

社群 sharing

Loading...