google
A demo for IR to netlist LEC
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?
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
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.