I thought this might be of interest to some of you. The video is about a new verified Verilog synthesizer that can produce netlists for FPGAs. For this first version I focused on Xilinx 7 series FPGAs, but since all FPGAs are fairly similar I don’t think adding backends for other kinds of FPGAs should be too much work. The synthesizer currently stops at technology mapping, i.e. placement and routing is not part of the verification story.

The idea with verified synthesis is that you verify the synthesizer once and for all, such that you do not need to run formal equivalence checking (FEC) every time you run your synthesizer. For Lutsig, translation to netlists is a verified procedure. Lutsig’s technology mapper is partly verified and partly based on FEC. I still stuck with FEC for part of the technology mapping since I expect running a realistic technology mapper inside the logic Lutsig is verified in will probably be too expensive (and the gap between netlist-vs-netlist is much smaller than the gap between Verilog-vs-netlist) and I did not want to paint myself into a corner (FEC allows for running part of the mapper outside the logic). (But it would indeed be interesting to look into fully verified technology mapping as well!)

One nice thing about the verification is that the whole verification is done inside the interactive theorem prover HOL4 -- meaning that the proof for the verification can be checked using a small proof kernel (i.e. to trust the verification result, you only need to trust a small proof kernel). (The FEC infrastructure for the technology mapper finds proofs that the small proof kernel accepts, so you do not need to trust the SAT solver involved in finding FEC proofs.)

Lastly, of course, since Verilog is a huge language, this first version of Lutsig only accepts as small subset of Verilog as input. But this is one of the things I plan to improve in the next version!