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

An Che Cheng, Chia Chih Yen, Celina G. Val, Sam Bayless, Alan J. Hu, Iris Hui Ru Jiang, Jing Yang Jou

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

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.

Original languageEnglish
JournalACM Transactions on Design Automation of Electronic Systems
Volume20
Issue number1
DOIs
StatePublished - 18 Nov 2014

Keywords

  • Algorithms
  • Covergroup
  • Formal methods
  • Simultaneous satisfiability
  • Verification

Fingerprint

Dive into the research topics of 'Efficient coverage-driven stimulus generation using simultaneous SAT solving, with application to SystemVerilog'. Together they form a unique fingerprint.

Cite this