Skip to content
@keplertech

keplertech

README.md

Open EDA tools. Agents drive, engineers decide.

KeplerTech builds open-source EDA tools designed to be driven by AI agents, and usable standalone by engineers. The tools contain no AI: the agent brings the reasoning, the tools bring exact, reproducible results.

  • Open source: public on GitHub and PyPI under Apache-2.0. Transparent code, auditable by your own team.
  • Agent-ready: exact, structured, bounded answers. High performance and multi-threaded, so the agent loop never stalls.
  • No AI inside: fully deterministic. Same question, same answer, every time.

The agent loop: explore, edit, verify, show

  1. Explore with naja-scope: exact, token-bounded answers on RTL and netlists.
  2. Edit with any AI agent (any model, any MCP client), which decides and edits through najaeda.
  3. Verify with kepler-formal: proves each RTL or netlist edit keeps the same behavior.
  4. Show with naja-schematic: renders the design and formal diagnoses, so an engineer can review every result.

Loop until equivalence is proven. The loop works on RTL and netlists, before place and route: the agent edits RTL or netlists (refactor, optimize, fix), and each change is proven before it is kept.

Ecosystem

Every tool is built on naja, our open-source C++ netlist engine, and najaeda, its Python package. Each tool works on its own, for engineers as well as for agents.

KeplerTech ecosystem: SystemVerilog, VHDL, gate-level Verilog, Liberty and Python inputs feed the naja netlist engine, which powers najaeda, naja-scope, kepler-formal, kepler-formal-mcp and naja-schematic

Tools

Tool What it does
naja-scope MCP server giving drivers, loads, logic cones and source lines to any MCP client. On CVA6 (RISC-V core): 17/17 correct answers vs 10/17 with grep, with about 5x fewer input tokens (182k vs 888k). Details in the naja-scope README.
kepler-formal Formal proof that two design versions behave identically, or a counterexample. RTL SEC, RTL-to-gate SEC, gate-level SEC and LEC, from SystemVerilog, gate-level Verilog and Liberty. Used by OpenROAD and in hardware CI/CD.
kepler-formal-mcp MCP server for kepler-formal with three tools (rtl_sec, gate_sec, gate_lec). It reads design files and never edits them.
kepler-formal-action GitHub Action running equivalence checks on RTL and gate-level design changes in CI.
naja-schematic Schematic viewer for netlists and formal diagnoses. Native, WebAssembly (browser) and VS Code builds.
naja + najaeda The common API. RTL and gate-level designs, hierarchy and bit-level connectivity, primitive functional models, optimization and editing.

Build your own tool

Write scripts on the same API to analyze and transform your designs and automate your flow:

pip install najaeda

Documentation: najaeda.readthedocs.io

Links

Pinned Loading

  1. naja naja Public

    Netlist API (and more) for EDA flow development

    Verilog 165 26

  2. kepler-formal kepler-formal Public

    Digital Design Equivalence Checking

    C++ 112 15

  3. naja-scope naja-scope Public

    MCP server for AI agents to explore SystemVerilog/Verilog netlists: trace connectivity, walk hierarchy, jump to source - without pasting RTL into context. Built on najaeda.

    Python 20 2

  4. naja-verilog naja-verilog Public

    A standalone structural (gate-level) verilog parser

    C++ 43 3

  5. naja-schematic naja-schematic Public

    Portable netlist schematic viewer for the naja data model

    Verilog 4

  6. naja-if naja-if Public

    C++ 3

Repositories

Showing 10 of 25 repositories
View all repositories

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Top languages

Loading…

Most used topics

Loading…