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 '20 at 22:12

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 '20 at 2:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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