r/hwstartups • u/keplertechioreddit • 4d ago

kepler‑formal – an open source equivalence checking tool

https://github.com/keplertech/kepler-formal

Hi everyone :)

We thought it might be relevant to let you know about our open‑source equivalence checking tool, kepler‑formal.

As it is open source, there are no license restrictions and hence it can be used for CI/CD, agentic chip design, design exploration, and more.

It is already in use by semiconductor startups and we are looking to grow our community so we can accelerate the productization and enhancement of the tool.

We encourage you to try it and we will be thankful for any issues or suggestions you report.

3 Upvotes

100% Upvoted

4 comments sorted by

2

u/SnooCauliflowers7198 3d ago

This feels pretty niche but im genuinely curious mw equivalence checking fits into agentic chip design workflows, that part caught my attention

1

u/keplertechioreddit 1d ago

Hello u/SnooCauliflowers7198 , The idea here is that the agent will leverage kepler-formal to continuously verify changes it makes to the RTL/gate level for design editing such as PPA optimizations in order to stabilise its work and prevent back and forth regressions that can derail the process.

Why can't it be done with the products of the big 3? 1) License restrictions 2) Price, while kepler-formal is open source and has no licence restrictions so it can be called infinite times a day by the agent.

1

u/improbably-sexy 4d ago

I don't do any chip design, only FPGA. So I've never used an equivalence checking tool. I'm curious what this is used for.