Formal Acceleration on FPGA. Innovation in Verification

Extending hardware acceleration to formal verification is a powerful idea to extend hardware acceleration to a verification domain that has not got much attention for acceleration. Paul Cunningham (GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and lecturer at Stanford, EE292A) and I continue our series on research ideas. As always, feedback welcome.

The Innovation

This month’s pick is SAT-Accel: A Modern SAT Solver on a FPGA. The authors are from UCLA. The paper was published in the ACM/SIGDA International Symposium on FPGAs in 2025 and has 4 citations.

CPU-based SAT solvers have advanced on many fronts over the years, enabling larger problems to be addressed but not noticeably taking advantage of hardware acceleration so far. This paper introduces work enabling interesting performance enhancement though FPGA implementations.

Paul’s view

It is hard to pick an algorithm more fundamental to verification than SAT, which lies at the heart of formal verification and constrained random stimulus generation. This paper from UCLA looks at accelerating SAT on FPGA. The authors argue that modern SAT solvers implement many strategies that deliver orders of magnitude in speed-up on real world use cases. However, prior art for SAT on FPGA neglects to incorporate these strategies, resulting in poor performance. They propose a new accelerator, SAT-Accel, that implements many of these strategies and achieves 800x speed-up over the best previous FPGA-based SAT solver, SAT-Hard.

A SAT solver begins with a boolean expression in CNF, since any circuit can be quickly converted to a CNF expression in linear time and memory. It then performs a depth first search over variables in the expression, assigning values to each variable in turn until the expression is satisfied. Where if expression becomes false, the search is rolled back and different variable assignments are tried. Modern solvers then deploy various strategies to avoid redundant or dead-end searches, make intelligent choices about which variable to try assigning a value to next, and to optimize memory access patterns.

SAT-Accel has an elegant architecture comprising of a specialized memory access unit, an array of processing elements to parallelize propagating variable assignments through the expression, and a dedicated unit to perform on-the-fly clause minimization and search rollback. Compared to Kissat, a current state-of-the-art open source SAT solver running on a 64-core AMD Epyc, SAT-Accel averages a 3x speed-up. It’s main challenge and the authors’ focus for further research is capacity: SAT-Accel works only with SRAM on the FPGA, which limits it to 32k variables and 131k clauses. To be of commercial value, capacity needs to be in the millions of variables and clauses. Either off-chip DRAM with some form of caching scheme is needed, or the solver needs to distribute across multiple FPGAs. Nice paper, I look forward to seeing what this team at UCLA will publish next.

Raúl’s view

SAT (Boolean satisfiability: given a Boolean formula, is there an assignment to its variables that makes it evaluate to true?) is NP-complete, yet many practical algorithms have been developed, and it is widely used in EDA applications such as equivalence checking, bounded model checking, ATPG, and logic optimization.

This paper presents SAT-Accel, the first FPGA-based SAT solver that implements many of the algorithmic innovations found in modern CPU SAT solvers (e.g., Kissat and MiniSat). Its central contribution is an algorithm-hardware co-design that adapts SAT algorithms to FPGA hardware through new memory structures and data representations. As a result, SAT-Accel achieves roughly an 800x speedup over the previous FPGA state of the art (SAT-Hard) while supporting significantly larger problem sizes. Compared with software solvers, however, the picture is different: it is 17.9x faster than MiniSat and 2.8x faster than Kissat, but supports much smaller problems—only 32K variables and 131K clauses. Benchmarks that could not fit into the FPGA’s on-chip memory were excluded from the comparison. By contrast, industrial SAT instances routinely contain millions of variables. For example, verifying a design with 500,000 flip-flops, 5 million logic gates, and 200 clock cycles of unrolling can easily produce Boolean formulas with tens of millions of variables.

SAT-Accel implements the following algorithms: Conflict-Driven Clause Learning (CDCL), Clause Minimization, Clause Deletion, Solver Restart Policy, Phase Saving, Variable Decision Heuristics, and Efficient Clause Checking (ECC). The authors acknowledge that solvers like Kissat include numerous additional heuristics not implemented in SAT-Accel, like advanced phase selection, chronological backtracking, and variable and clause elimination.

Perhaps the most interesting aspect of the work is its memory management. SAT solving is memory-bound. Variables are accessed in an irregular order, making execution memory-latency bound, with cache misses dominating runtime while arithmetic units remain mostly idle. To address this, the authors introduce a page-based memory manager in which pages can be immediately recycled without compaction. They also maintain two representations of the SAT instance: a conventional clause-oriented representation for learning and minimization, and a transposed variable-oriented representation used for propagation. Maintaining two specialized memory organizations increases storage requirements but significantly reduces memory access latency. This largely eliminates the memory bottleneck, but the FPGA’s limited on-chip memory (~107 MB on the U55C) constrains the size of problems that can be solved.

In summary, SAT-Accel is a compelling architectural proof of concept for domain-specific acceleration, such as the quantum compilation benchmarks highlighted by the authors, where problems fit within its fixed memory footprint. However, for the multi-million-variable SAT instances common in industrial EDA, software solvers implementing Kissat-like algorithms on CPUs remain the practical solution.