Can you use an FPGA / verilog to accelerate SAT / SMT solving?

Question

I am aware that SAT and SMT are widely used in hardware verification. This would tell me intuitively that trying every input on a circuit is slower than porting the circuit to a solver. However, we have ASICs for computing SHA256 faster in mining Bitcoin, so my thought is why not for SAT?

I would like to build something that takes CNF SAT expressions (later on SMTLIB) and generates Verilog for them. I am not sure if it would be faster to pipe test inputs back and forth over USB or write a little harness to run within the Verilog. Either way, I'd like to offload the expression testing onto an FPGA. I figure generation + device programming time will be fixed (say, 20 seconds) so it will only make sense for longer running solves.

Is this feasible or is there something about SAT solving / FPGAs I don't understand?

Answer 1

Yes, you can certainly use FPGAs to do this kind of work, there’s lots of literature pointing to it. Examples - [1] [2] [3] [4]

SMT = Satisfiable Modulo Theory

SAT is Boolean Satisfiable Problem, nicknamed a ‘SAT’ for short.

More about this stuff here: https://people.eecs.berkeley.edu/~sseshia/pubdir/SMT-BookChapter.pdf

My suggestion is to address the bitstream loading time. Some FPGAs support what Xilinx calls ‘tandem’ configuration, where a large FPGA first has a smaller bitstream loaded locally that’s enough to light up PCI Express, then the rest of the bitstream is loaded at high speed over the PCIe link.

More here: https://www.xilinx.com/Attachment/Xilinx_Answer_51950.pdf