Claire Xen  🏳️‍⚧️ 🏳️‍🌈 🧙🏻‍♀️ BLM  🏴 🚩

I've been pushing for an open tool to do this for a while, and now that bitstream formats are being slowly reverse engineered we're getting closer. I want the FPGA equivalent of an ASIC LVS check and right now that simply doesn't exist.

It does exist for ice40: icebox_vlog followed by logic equivalence check against post-synth / pre-pnr netlist with Yosys. (There's no simple push button flow for equivalence checks with Yosys yet, but it can be done.)

Can you do it on a nontrivial netlist and find all of the isomorphisms between DFFs etc to make the equivalence check sanely fast? The hard part, I think, would be dealing with optimizations like state machine re-coding, register balancing, etc.

What I think is needed to handle that well is some kind of "map file" in which synthesis documents the transformations it did, and mappings from RTL to post-synthesis nets, so that the formal tool can detect the isomorphisms and verify the transformations are correct.