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.
|58: (C) 2012-18, DJ Greaves, University of Cambridge, Computer Laboratory.|