Christophe Alexandre
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.
Session
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.