🐧 penguin-rtl

https://penguin-rtl.arjunv.net/

This is actually an old project I fogot about, so I’m making a post to remember it.

How It Works

penguin-rtl leverages Yosys, an open-source logic synthesis tool. With YoWASP, a WebAssembly distribution of Yosys, all processing happens locally on your machine via the browser.

Where to Use Formal Verification

Across vendors, synthesis tools can have vastly different mappings for the same logic. Even with the same synthesis tool, the mapping can vary based on the way the logic was written.

I’m was software engineer at an FPGA company and had the opportunity to optimize Verilog IPs for our FPGAs. Formal verification was an essential tool in rewriting clumps of logic to better map with our toolchain without compromising on functional correctness.