A demo for IR to netlist LEC

[Aaronchan-sz]

Readme of solver says: That Verilog is then compiled by an external tool, which, if successful, will output a "netlist" - a set of standard cells (think AND, OR, NOT, flops, etc.) and wires connecting them that realizes the design

is there an example show how to convert a verilog file generated by codegen_main to netlist that can be consumed by lec solver?

[cdleary]

We've been meaning to make one against the open PDKs (e.g. sky130 and OpenROAD) but we don't have one of those in the repo yet.

If you're interested in taking a try at it you need to provide the IR file, the gate-level netlist file, and the liberty file from the PDK to this binary: https://github.com/google/xls/blob/7f53fd34b69285ace2611500530ba02b5b947b13/xls/tools/lec_main.cc#L49

It converts the IR operations to SMTLib (e.g. Z3), converts the gate-level netlist connectivity to SMTLib by using the boolean formulas described in the liberty file, and then tries to find a counterexample to those being equivalent. There's also functionality for extracting logic clouds between flop stages in a pipeline but the simplest example would likely be something combinational.

synthesize_rtl rules should product gate-level netlists as one of their artifacts -- here's an example of using the synthesize_rtl rule for sky130 https://github.com/google/xls/blob/7f53fd34b69285ace2611500530ba02b5b947b13/xls/modules/rle/BUILD#L111

[cdleary]

Aside: marking as "good first issue" in the sense it'd be interesting for a contributor to put those pieces together, though notably there's a few pieces there (described in the above) to find / put together.