CISPA
Browse
smtsampler.pdf (778.6 kB)

SMTSampler: efficient stimulus generation from complex SMT constraints.

Download (778.6 kB)
conference contribution
posted on 2024-02-23, 11:07 authored by Rafael DutraRafael Dutra, Jonathan Bachrach, Koushik Sen

 
Stimulus generation is an essential part of hardware verification, being at the core of widely applied constrained-random verification techniques. However, as verification problems get more and more complex, so do the constraints which must be satisfied. In this context, it is a challenge to efficiently generate random stimuli which can achieve a good coverage of the design space. We developed a new technique SMTSAMPLER which can sample random solutions from Satisfiability Modulo Theories (SMT) formulas with bit-vectors, arrays, and uninterpreted functions. The technique uses a small number of calls to a constraint solver in order to generate up to millions of stimuli. Our evaluation on a large set of complex industrial SMT benchmarks shows that SMTSAMPLER can handle a larger class of SMT problems, outperforming state-of-the-art constraint sampling techniques in the number of samples produced and the coverage of the constraint space. 

History

Editor

Bahar I

Journal

ICCAD

Page Range

30-30

Publisher

ACM

BibTeX

@conference{Dutra:Bachrach:Sen:2018, title = "SMTSampler: efficient stimulus generation from complex SMT constraints.", author = "Dutra, Rafael" AND "Bachrach, Jonathan" AND "Sen, Koushik", editor = "Bahar, Iris", year = 2018, month = 1, journal = "ICCAD", pages = "30--30", publisher = "ACM" }

Usage metrics

    Categories

    No categories selected

    Keywords

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC