2026-06-10 –, Poster Island A
The RISC-V ecosystem is expanding rapidly, with many open hardware projects now developed collaboratively on platforms such as GitHub. Yet while software enjoys mature continuous integration and deployment (CI/CD) practices, hardware design lacks equivalent automated verification: formal tools such as logic equivalence checking (LEC) stay confined to proprietary EDA solutions whose per-run license costs make them impractical to run on every pull request. This gap is now acute, as AI-assisted agents that modify RTL are emerging without fast, open tools to verify their output, sharpening the need for automated formal verification inside the development loop.
We present kepler-formal, an open-source formal equivalence checking tool that runs efficiently in CI for RISC-V projects. Built on a high-performance C++ netlist engine with a Python interface, it checks equivalence between RTL transformations and synthesized netlists. It is evolving from combinational LEC toward Sequential Equivalence Checking (SEC): since RTL contains registers, pipelines, and state machines, SEC's cycle-by-cycle modeling is the sound method for proving equivalence at the RTL level.
On open RISC-V designs (CVA6, BlackParrot, MegaBoom, up to ~3.9M primitives), checks complete within typical pull request budgets, from under two to under ten minutes. Running license-free and fast enough for per-commit use, kepler-formal delivers both the inner-loop verification AI agents need and a practical first formal gate before commercial sign-off.
The rapid growth of the RISC-V ecosystem has produced an increasing number of open hardware projects developed collaboratively through platforms such as GitHub. While software development widely benefits from automated continuous integration (CI) workflows, equivalent verification infrastructure for hardware design remains limited, particularly for formal verification tasks such as logic equivalence checking (LEC). Most industrial LEC tools are proprietary and difficult to integrate into distributed, open development environments.
This work presents kepler-formal, an open-source logic equivalence checking tool designed to operate efficiently within CI pipelines for RISC-V hardware development. Built on the Naja infrastructure for hierarchical netlist representation and analysis, it enables fast equivalence verification between synthesized and transformed netlists. Runtime experiments on open RISC-V designs show that equivalence checks complete within seconds to minutes, making them suitable for automated pull request validation.
The tool is integrated into open silicon flows such as OpenROAD, where it acts as an automated verification gate during development. By enabling lightweight formal verification in collaborative workflows, this approach helps bring modern software engineering practices to open hardware development.
With 20 years of experience in Electronic Design Automation (EDA), I began my journey with a PhD in microelectronics from Sorbonne University. In 2009, I co-founded Flexras Technologies, a startup specializing in FPGA prototyping tools, which was acquired by Mentor Graphics (now Siemens EDA) in 2015. There, I served as Chief Software Architect, leading global R&D teams and helping evolve our technology into a widely adopted product.In 2022, I co-founded a new venture: keplertech.io, an EDA startup built on the belief that Open Source can unlock innovation in one of the most closed and complex industries: integrated circuits and the tools used to design them. In a space dominated by a handful of major players, we aim to create meaningful opportunities for smaller, agile actors to thrive. I’m passionate about building complex systems from scratch and bringing ideas to life in the real world.
Noam Cohen is the Co-Founder and CTO of keplertech.io. Throughout his
corporate career, he led R&D teams at SNPS and Siemens, dedicated to compiler
development for hardware prototyping and emulation, with a focus on optimizing
solutions to NP-hard problems such as partitioning, placement, and routing, and
with an emphasis on high performance computing. After 10 years with the EDA
industry leaders, he co-founded keplertech.io with the aim of introducing innovation
in both technology and user experience to hardware design software tools.