SMTSampler: Efficient Stimulus Generation from Complex SMT Constraints
SMTSampler: Efficient Stimulus Generation from Complex SMT Constraints
复制标题
DOI：
10.1145/3240765.3240848
复制
发表时间：
2018-11
期刊：
影响因子：
--
通讯作者：
Rafael Dutra;J. Bachrach;Koushik Sen
中科院分区：
文献类型：
--
作者：
Rafael Dutra;J. Bachrach;Koushik Sen
激励产生是硬件验证的重要组成部分，是广泛应用的约束随机验证技术的核心。然而，随着验证问题变得越来越复杂，必须满足的约束也越来越复杂。在这种情况下，它是一个挑战，有效地产生随机刺激，可以实现良好的覆盖设计空间。我们开发了一种新的技术SMTSampler，它可以从可满足性模理论（SMT）公式的位向量，数组和未解释的函数的随机解的样本。该技术使用少量的调用约束求解器，以生成多达数百万的刺激。我们对一组复杂的工业SMT基准测试的评估表明，SMTSampler可以处理更大类的SMT问题，在产生的样本数量和约束空间的覆盖范围方面优于最先进的约束采样技术。
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.