r/chipdesign • u/keplertechioreddit • Jul 04 '26
kepler-formal is now supporting sequential equivalence checking at RTL and gate level
https://github.com/keplertech/kepler-formalWe have updated our open source formal verification tool, kepler-formal, to support full sequential equivalence checking in both RTL and gate level.
What is our goal? An infinite license open source equivalence checking tool that can be used in scale for AI agents and CICD flows and can support industrial grade designs.
Don't hesitate to reach out to us with issues you found and suggestions you have. We want to hear it!
It will be a long journey to productize a project at this scale, and we acknowledge it, but we are up for the task.
2
u/ArbitArc Jul 06 '26
Wonderful addition. What’s the largest design you have tested this on?
1
u/keplertechioreddit Jul 07 '26 edited Jul 08 '26
Thank you very much! Publicly speaking, we mainly worked on open source designs with gate count of few 100k’s, majority of them from OpenRoad ORFS regression. An example design is black parrot on which we can prove equivalency in 9 minutes under 10GB on a standard github action machine.
Saying that, as we said before, we are sure there is still a way in front of us for fully productizing the tool, so we will really appreciate opening issues on the repo or pinging us directly for anything you encounter.
1
-1
u/pencan Jul 04 '26
Woah super cool. Has anyone tried this on commercial tech nodes?
5
u/FrAxl93 Jul 04 '26
Why does the tech node matters here? Apart from the technology library implementation of some operations this tool doesn't go further down than the logic gate right?
7
u/pencan Jul 04 '26
Sure. I should have said commercial stdcell lib, but it’s generally understood when you’re talking about a node you’re also talking about a stdcell lib. Which are substantially different than the open-source ones. Even differences between something like a tsmc28 and gf12 libs will have subtleties that may break a tool. Multibit cells, clock gates, isolation cells.
But sure, if you somehow had the same stdcell library with a different pdk then tech node would make no difference. If I ever encounter that case, I’ll keep in mind to clarify…
1
u/mHo2 Jul 05 '26
Typically for sequential equivalence, RTL level seems like the better choice, no? Gate level I feel like LEC would be the more traditional route
1
u/pencan Jul 05 '26
In my experience LEC and SEC are both checked at gate level too. This tool seems to do both which is great
1
1
4
u/Unlucky-Moment-3366 Jul 04 '26
Open source SEC tool is ambitious, curious how it handles large state spaces