To enable LEC'ing FPGA designs, we need a means of translating, e.g., LUT4-based designs into AND/OR/NOT/etc.-defined netlists, since that's the language our LEC tools currently speak.

julianviera@ started on this work during his internship, and demonstrated some good proof-of-concept work, so it'd be good to fully flesh out the work. IIRC, the necessary steps are:

ID the functionality of each LUT config ("init"?) in terms of AND/OR/NOT, etc.
Rewrite each LUT in terms of those operations (may require declaring add'l cells/wires)

...that's really it. I don't know that it makes sense to define a Bazel macro to do this, since the LUT mapping is potentially per-target, unless we make some default option that can be overridden by a config flag...but I'm not actually sure if that's possible.

I'll initially assign the issue to me, to make sure it doesn't get lost, but this can be picked up by anyone. It's really a decent starter project.

An update on the status of this work and next steps:

219 adds support for iCE40 LUTs by hardcoding the netlist parser to handle cells called `SB_LUT4`. It handles the LUTs by creating a new `CellLibraryEntry` with a `StateTable` that matches the LUT mask (or retrieving it if it exists already), instead of looking it up in a provided `CellLibrary` which is the direction suggested in the description above.

The next steps could go in two (somewhat related) directions:

There are more cells beyond SB_LUT4 that need to be supported for the iCE40, though I think just implementing SB_DFF would enable a full LEC flow to work with XLS (e.g. with the add1_8b.x program). I'm not sure if it would make more sense to create these cells in the netlist parser at runtime, like we do for LUTs in #219, or to specify a separate iCE40 cell library similar to fake_cell_library.
As support for these cells (as well as possibly cells for other FPGAs) are implemented, it might make sense to disentangle the cell name resolution/lookup code from the netlist parser code, i.e. separate the netlist parsing and the cell name lookup (which are both done as part of xls::netlist::rtl::Parser::ParseNetlist). In this way, we could have multiple cell name resolution "backends" that each know how to resolve cells for a specific vendor. The hardcoding of handling SB_LUT4 could then be moved out of the parsing step.

google / xls

Create FPGA LUT-to-Z3 translator #142