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?