How Far Does Replication Pay Off? A Throughput-Area Study of Brute-Force SAT on an ECP5 FPGA

Abstract

SAT solving is a core computational challenge across hardware verification, electronic design, and planning; an FPGA can evaluate SAT candidates at hardware clock rates without software overhead, enabling sub-microsecond solving on small instances. Yet, the throughput-area tradeoffs of parallel FPGA SAT datapaths remain undercharacterized on open-source toolchains. We implement a brute-force SAT solver on a Lattice ECP5 FPGA using Amaranth HDL, Yosys, and nextpnr, and characterize K-way candidate-level parallelism: replicating the clause-evaluation datapath K times to test K candidate solutions in parallel per clock cycle. Across K=1–128, cycle reduction is near-ideal (123.81× at K=128), while real speedup (37.37×) is bounded primarily by fmax degradation from the deepening winner-selection network. Throughput efficiency and area efficiency diverge: fmax retention falls monotonically while speedup per LUT rises, peaks near 8.22×10−4 at K=64, then declines as LUT cost outpaces speedup gain. Static timing analysis identifies the winner-selection network as the dominant timing bottleneck, with routing contributing ∼80% of critical-path delay at K=64.