Balancing Scalability and Uniformity in SAT Witness Generator

被引：38

作者：

Chakraborty, Supratik ^{[1
]}

Meel, Kuldeep S. ^{[2
]}

Vardi, Moshe Y. ^{[2
]}

机构：

[1] Indian Inst Technol, Bombay 400076, Maharashtra, India

[2] Rice Univ, Houston, TX 77251 USA

来源：

2014 51ST ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC) | 2014年

关键词：

D O I：

10.1145/2593069.2593097

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Constrained-random simulation is the predominant, approach used in the industry for functional verification of complex digital designs. The effectiveness or 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.

引用

页数：6