Classified by Research TopicSorted by DateClassified by Publication Type

Balancing Scalability and Uniformity in SAT-Witness Generator

Balancing Scalability and Uniformity in SAT-Witness Generator.
Supratik Chakraborty, Kuldeep S. Meel and Moshe Y. Vardi.
In Proceedings of Design Automation Conference (DAC), pp. 60:1–60:6, June 2014.

Download

[PDF] 

Abstract

Constrained-random simulation is the predominant approach used in the industry for functional verification of complex digital designs. The effectiveness of this approach depends on two key factors: the quality of constraints used to generate test vectors, and the randomness of solutions generated from a given set of constraints. In this paper, we focus on the second problem, and present an algorithm that significantly improves the state-of-the-art of (almost-)uniform generation of solutions of large Boolean constraints. Our algorithm provides strong theoretical guarantees on the uniformity of generated solutions and scales to problems involving hundreds of thousands of variables.

BibTeX

@inproceedings{CMV14,
	title={Balancing Scalability and Uniformity in SAT-Witness Generator},
  bib2html_dl_pdf={../Papers/DAC2014.pdf},
  code={https://bitbucket.org/kuldeepmeel/unigen},
  author={Chakraborty, Supratik and Meel, Kuldeep S. and Vardi, Moshe Y.},
	booktitle=DAC,
	pages = {60:1--60:6},
	year={2014},
	month=jun,
bib2html_rescat={Sampling},
  bib2html_pubtype={Refereed Conference},
  abstract={Constrained-random simulation is the predominant approach used in the industry for functional verification of complex digital designs. The effectiveness of this approach depends on two key factors: the quality of constraints used to generate test vectors, and the randomness of solutions generated from a given set of constraints. In this paper, we focus on the second problem, and present an algorithm that significantly improves the state-of-the-art of (almost-)uniform generation of solutions of large Boolean constraints. Our algorithm provides strong theoretical guarantees on the uniformity of generated solutions and scales to problems involving hundreds of thousands of variables.},
}

Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51