Crazy idea ?
If we program an FPGA we are generating a bit vector.
SAT solvers produce bit vectors that conform to a conjunction of constraints.
Let's specify the design as a set of constraints over a fictional FPGA...
We can also convert structural and behavioural design expressions to very-tight constraints and add those in.
The SAT solution wires up the FPGA and we can then apply logic trimming.
SAT Logic Synthesis (Greaves)
Main poblem: how large an FPGA to start with? Redundant logic might need a bi-simulation erosion to remove it.
Seems to work for generating small custom protocols.