• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
On Parallel Scalable Uniform SAT Witness Generator.
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia and Moshe Y. Vardi.
In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 304–319, April 2015.
Constrained-random verification (CRV) is widely used in industry for validating hardware designs. The effectiveness of CRV depends on the uniformity of test stimuli generated from a given set of constraints. Most existing techniques sacrifice either uniformity or scalability when generating stimuli. While recent work based on random hash functions has shown that it is possible to generate almost uniform stimuli from constraints with 100,000+ variables, the performance still falls short of today's industrial requirements. In this paper, we focus on pushing the performance frontier of uniform stimulus generation further. We present a random hashing-based, easily parallelizable algorithm, UniGen2, for sampling solutions of propositional constraints. UniGen2 provides strong and relevant theoretical guarantees in the context of CRV, while also offering significantly improved performance compared to existing almost-uniform generators. Experiments on a diverse set of benchmarks show that UniGen2 achieves an average speedup of about 20X over a state-of-the-art sampling algorithm, even when running on a single core. Moreover, experiments with multiple cores show that UniGen2 achieves a near-linear speedup in the number of cores, thereby boosting performance even further.
@inproceedings{CFMSV15a,
title={On Parallel Scalable Uniform SAT Witness Generator},
bib2html_dl_pdf={../Papers/Tacas15.pdf},
code={https://bitbucket.org/kuldeepmeel/unigen},
author={
Chakraborty, Supratik and Fremont, Daniel J. and Meel, Kuldeep S. and
Seshia, Sanjit A. and Vardi, Moshe Y.
},
booktitle=TACAS,
pages={304--319},
year={2015},
month=apr,
bib2html_rescat={Sampling},
bib2html_pubtype={Refereed Conference},
abstract={
Constrained-random verification (CRV) is widely used in industry for
validating hardware designs. The effectiveness of CRV depends on the
uniformity of test stimuli generated from a given set of constraints. Most
existing techniques sacrifice either uniformity or scalability when
generating stimuli. While recent work based on random hash functions has
shown that it is possible to generate almost uniform stimuli from
constraints with 100,000+ variables, the performance still falls short of
today's industrial requirements. In this paper, we focus on pushing the
performance frontier of uniform stimulus generation further. We present a
random hashing-based, easily parallelizable algorithm, UniGen2, for sampling
solutions of propositional constraints. UniGen2 provides strong and relevant
theoretical guarantees in the context of CRV, while also offering
significantly improved performance compared to existing almost-uniform
generators. Experiments on a diverse set of benchmarks show that UniGen2
achieves an average speedup of about 20X over a state-of-the-art sampling
algorithm, even when running on a single core. Moreover, experiments with
multiple cores show that UniGen2 achieves a near-linear speedup in the
number of cores, thereby boosting performance even further.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21