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. »LINK: 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.

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.