• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
A Scalable and Nearly Uniform Generator of SAT Witnesses.
Supratik Chakraborty, Kuldeep S. Meel and Moshe Y. Vardi.
In Proceedings of International Conference on Computer-Aided Verification (CAV), pp. 608–622, July 2013.
Functional verification constitutes one of the most challenging tasks in the development of modern hardware systems, and simulation-based verification techniques dominate the functional verification landscape. A dominant paradigm in simulation-based verification is directed random testing, where a model of the system is simulated with a set of random test stimuli that are uniformly or near-uniformly distributed over the space of all stimuli satisfying a given set of constraints. Uniform or near-uniform generation of solutions for large constraint sets is therefore a problem of theoretical and practical interest. For Boolean constraints, prior work offered heuristic approaches with no guarantee of performance, and theoretical approaches with proven guarantees, but poor performance in practice. We offer here a new approach with theoretical performance guarantees and demonstrate its practical utility on large constraint sets.
@inproceedings{CMV13a,
title={A Scalable and Nearly Uniform Generator of SAT Witnesses},
bib2html_dl_pdf={../Papers/cav13.pdf},
code={https://bitbucket.org/kuldeepmeel/unigen},
author={Chakraborty, Supratik and Meel, Kuldeep S. and Vardi, Moshe Y.},
booktitle=CAV,
pages={608-622},
year={2013},
month=jul,
bib2html_rescat={Sampling},
bib2html_pubtype={Refereed Conference},
abstract={Functional verification constitutes one of the most challenging tasks in the development of modern hardware systems, and simulation-based verification techniques dominate the functional verification landscape. A dominant paradigm in simulation-based verification is directed random testing, where a model of the system is simulated with a set of random test stimuli that are uniformly or near-uniformly distributed over the space of all stimuli satisfying a given set of constraints. Uniform or near-uniform generation of solutions for large constraint sets is therefore a problem of theoretical and practical interest. For Boolean constraints, prior work offered heuristic approaches with no guarantee of performance, and theoretical approaches with proven guarantees, but poor performance in practice. We offer here a new approach with theoretical performance guarantees and demonstrate its practical utility on large constraint sets.},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51