Coverage-Driven Design Verification Using a Diverse SAT Solver

Yosuke KAKIUCHI  Kiyoharu HAMAGUCHI  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E100-A   No.7   pp.1481-1487
Publication Date: 2017/07/01
Online ISSN: 1745-1337
Type of Manuscript: Special Section PAPER (Special Section on Design Methodologies for System on a Chip)
Category: 
Keyword: 
RTL verification,  coverage-driven verification,  sat solver,  auomated testbench,  

Full Text: PDF(277.9KB)
>>Buy this Article


Summary: 
Verification of logic designs has been a long-standing bottleneck in the process of hardware design, where its automation and improvement of efficiency has demanding needs. Mainly simulation-based verification has been used for this purpose, and recently, coverage-driven verification has been widely used, of which target is improvement of some metric called coverage. Our target is the metric called toggle coverage. To find input patterns which cause some toggles on each signal, a SAT solver could be used, but this is computationally costly. In this paper, we study the effect of combination of random simulation and usage of a SAT solver. In particular, we use a SAT solver which can find multiple “diverse” solutions. With this solver, we can avoid generating similar patterns, which are unlikely to improve coverage. The experimental results show that, a small number of calls of a SAT solver can improve entire toggle coverage effectively, compared with simple random simulation.