DEMOTIC: A Differentiable Sampler for Multi-Level Digital Circuits

TL;DR

The paper tackles the bottleneck of generating diverse, satisfying assignments for CircuitSAT by introducing Demotic, a differentiable sampler that reframes CircuitSAT as a multi-output regression problem on a probabilistic gate model. By using gradient descent on a circuit-centric, differentiable representation, Demotic enables parallel, GPU-accelerated sampling without converting circuits to CNF, addressing scalability and throughput limitations of CNF-based SAT solvers. Empirical results on the ISCAS-85 benchmark show Demotic considerably outperforms state-of-the-art samplers in most cases, with linear scaling and significant speedups, while exploring learning dynamics, hyperparameter effects, and memory considerations. The approach offers a scalable, high-throughput tool for circuit verification and CRV tasks, reducing reliance on CPU-bound heuristics and CNF blow-ups.

Abstract

Efficient sampling of satisfying formulas for circuit satisfiability (CircuitSAT), a well-known NP-complete problem, is essential in modern front-end applications for thorough testing and verification of digital circuits. Generating such samples is a hard computational problem due to the inherent complexity of digital circuits, size of the search space, and resource constraints involved in the process. Addressing these challenges has prompted the development of specialized algorithms that heavily rely on heuristics. However, these heuristic-based approaches frequently encounter scalability issues when tasked with sampling from a larger number of solutions, primarily due to their sequential nature. Different from such heuristic algorithms, we propose a novel differentiable sampler for multi-level digital circuits, called {\sc Demotic}, that utilizes gradient descent (GD) to solve the CircuitSAT problem and obtain a wide range of valid and distinct solutions. {\sc Demotic} leverages the circuit structure of the problem instance to learn valid solutions using GD by re-framing the CircuitSAT problem as a supervised multi-output regression task. This differentiable approach allows bit-wise operations to be performed independently on each element of a tensor, enabling parallel execution of learning operations, and accordingly, GPU-accelerated sampling with significant runtime improvements compared to state-of-the-art heuristic samplers. We demonstrate the superior runtime performance of {\sc Demotic} in the sampling task across various CircuitSAT instances from the ISCAS-85 benchmark suite. Specifically, {\sc Demotic} outperforms the state-of-the-art sampler by more than two orders of magnitude in most cases.

Figures (6)

• Figure 1: An overview of Demotic is shown. Demotic takes a Verilog instance describing a combinational circuit and parse it into its corresponding probabilistic model described in PyTorch. The embedding layer converts the learnable real-value inputs into probabilities. The $\ell_2$-loss function is calculated in each training iteration and the input variables are updated using GD.
• Figure 2: Log-Log plot of runtime in millisecond against the count of unique satisfying solutions found within that run time across all the CircuitSAT problems from the ISCAS-85 benchmark. Dotted lines denote the trend of the runtime performance for each sampler.
• Figure 3: Log learning plot of Demotic showing the number of unique satisfying solutions across different iterations for the CircuitSAT problems from the ISCAS-85 benchmark.
• Figure 4: Log learning plot of Demotic showing the number of unique satisfying solutions across different iterations and learning rates for the CircuitSAT problem of "c$2670$".
• Figure 5: Log plot of the throughput of Demotic, measured by the number of unique satisfying solutions per second across different iterations for the CircuitSAT problems from the ISCAS-85 benchmark.