2026-06-10 –, Poster Island A
The rapid expansion of the RISC-V ecosystem has led to an increasing number of open hardware projects hosted on collaborative platforms such as GitHub. While modern software development benefits from mature continuous integration and continuous deployment (CI/CD) methodologies, equivalent automated verification infrastructure remains limited for hardware design. In particular, formal verification tools such as logic equivalence checking (LEC) remain largely restricted to proprietary EDA solutions.
This work explores the use of lightweight open-source EDA tools as scalable verification agents for open hardware development workflows. We present an open-source logic equivalence checking tool designed to operate efficiently within CI environments for RISC-V projects. Built on a high-performance C++ infrastructure for netlist representation and analysis, the tool enables rapid equivalence verification between different RTL transformations and synthesized netlists. Experimental results on open RISC-V designs demonstrate that automated equivalence checks can be integrated into CI pipelines with execution times compatible with typical pull request validation workflows. This approach provides a practical first verification gate for open hardware repositories before deeper sign-off verification using commercial tools.
The rapid growth of the RISC-V ecosystem has led to 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 remain 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 top of the Naja infrastructure for hierarchical netlist representation and analysis, the tool enables fast equivalence verification between synthesized or transformed netlists. Runtime experiments on open RISC-V designs demonstrate that equivalence checks can be executed within seconds, making them suitable for automated pull-request validation workflows.
The tool is integrated into open silicon flows including OpenROAD where it acts as an automated verification gate during development. By enabling lightweight formal verification in collaborative workflows, this approach helps bridge modern software engineering practices and 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.