Recurrent CircuitSAT Sampling for Sequential Circuits

TL;DR

This work introduces a GPU-accelerated, differentiable recurrent CircuitSAT framework for sequential circuits to support constrained random verification. By modeling gates probabilistically and applying gradient descent with backpropagation through time, the method outputs input sequences together with their required clock cycles without unrolling the circuit, enabling substantial speedups (up to $105.1\times$) over CNF-based samplers on ISCAS-89 and ITC'99. The authors provide a theoretical convergence analysis for the non-convex formulation and demonstrate practical effectiveness via backtracking to generate solutions across varying sequence lengths. Extensive experiments show superior throughput and favorable learning dynamics, validating the approach against state-of-the-art samplers and highlighting its potential for scalable verification of complex sequential hardware.

Abstract

In this work, we introduce a novel GPU-accelerated circuit satisfiability (CircuitSAT) sampling technique for sequential circuits. This work is motivated by the requirement in constrained random verification (CRV) to generate input stimuli to validate the functionality of digital hardware circuits. A major challenge in CRV is generating inputs for sequential circuits, along with the appropriate number of clock cycles required to meet design constraints. Traditional approaches often use Boolean satisfiability (SAT) samplers to generate inputs by unrolling state transitions over a fixed number of clock cycles. However, these methods do not guarantee that a solution exists for the given number of cycles. Consequently, producing input stimuli together with the required clock cycles is essential for thorough testing and verification. Our approach converts the logical constraints and temporal behavior of sequential circuits into a recurrent CircuitSAT problem, optimized via gradient descent to efficiently explore a diverse set of valid solutions, including their associated number of clock cycles. By operating directly on the circuit structure, our method reinterprets the sampling process as a supervised multi-output regression task. This differentiable framework enables independent element-wise operations on each tensor element, facilitating parallel execution during learning. As a result, we achieve GPU-accelerated sampling with substantial runtime improvements (up to 105.1x) over state-of-the-art heuristic samplers. We demonstrate the effectiveness of our method through extensive evaluations on circuit problems from the ISCAS-89 and ITC'99 benchmark suites.

Figures (5)

• Figure 1: The general form of a sequential circuit.
• Figure 2: Left: The proposed recurrent sequential model. Right: The proposed recurrent cell for sequential circuits.
• Figure 3: A log plot showing the runtime performance of our recurrent sampler in terms of throughput, measured as the number of unique satisfying solutions per second, versus the number of clock cycles across all instances from the ISCAS-89 and ITC'99 benchmark suites. The throughput values are rounded to two decimal places in this plot.
• Figure 4: A plot illustrating the percentage of unique solutions generated by our recurrent sampler over $50$ clock cycles for three representative CircuitSAT instances. The batch size for this experiment is set to $100,000$.
• Figure 5: A log plot illustrating the number of unique solutions generated by our recurrent sampler over $5$ training iterations for three representative CircuitSAT instances.