HOME   PREV   NEXT (Rule-based hardware generation (BlueSpec))

Synthesis from Rules (SAT-based idea).

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.