Create FPGA LUT-to-Z3 translator

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.