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?

  • 5
    \$\begingroup\$ What's SAT ? And SMT? For me SMT = surface-mount technology.. \$\endgroup\$
    – Ben
    Apr 21, 2020 at 22:12

1 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

  • \$\begingroup\$ Wow, there is quite a bit of literature. I don't know how I didn't find these before. Thank you for the tips and I guess my idea is not so original! \$\endgroup\$
    – douggard
    Apr 22, 2020 at 2:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.