On Parallel Scalable Uniform SAT Witness Generation

摘要: Constrained-random verification CRV is widely used in industry for validating hardware designs. The effectiveness of depends on the uniformity test stimuli generated from a given set constraints. Most existing techniques sacrifice either or scalability when generating stimuli. While recent work based random hash functions has shown that it possible to generate almost uniform constraints with 100,000+ variables, performance still falls short today's industrial requirements. In this paper, we focus pushing frontier stimulus generation further. We present hashing-based, easily parallelizable algorithm, UniGen2, sampling solutions propositional UniGen2 provides strong and relevant theoretical guarantees context CRV, while also offering significantly improved compared almost-uniform generators. Experiments diverse benchmarks show achieves an average speedup about 20× over state-of-the-art even running single core. Moreover, experiments multiple cores near-linear number cores, thereby boosting