penguin-rtl 🐧

Perform circuit equivalence checking entirely locally in your browser.

Usage

Supports combinational logic implemented in structural and behavioral Verilog-2005.
Logic that infers sequential elements (flip-flops and memories) is not supported yet.
The top-level module interface (module name and ports) of the gate and gold circuits must match for the verification engine to infer equivalent ports.

Examples:

Circuit A (Gate Implementation)

module inverter (
    input in,
    output out
);
    wire a = ~in;
    wire b = ~a;
    assign out = ~b;
endmodule

Circuit B (Gold Reference)

module inverter (
    input in,
    output out
);
    assign out = ~in;
endmodule

Results Waiting for verification

Results will appear here...

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 a 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.

🐧?

Best suits a formal occasion.

ISC License Copyright (C) 2012 - 2025 Claire Xenia Wolf <claire@yosyshq.com> Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above copyright notice and this permission notice appear in all copies. THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

ISC License Copyright (C) Catherine <whitequark@whitequark.org> Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above copyright notice and this permission notice appear in all copies. THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

The MIT License (MIT) Copyright (c) 2011-2024 The Bootstrap Authors Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.