# kepler-formal

**Repository Path**: flyr01/kepler-formal

## Basic Information

- **Project Name**: kepler-formal
- **Description**: No description available
- **Primary Language**: C++
- **License**: GPL-3.0
- **Default Branch**: main
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2026-03-16
- **Last Updated**: 2026-03-16

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# kepler-formal

[![codecov](https://codecov.io/gh/keplertech/kepler-formal/branch/main/graph/badge.svg?token=59ZKZ74HFP)](https://codecov.io/gh/keplertech/kepler-formal)

## Introduction

Kepler-Formal is a logic equivalence checking (LEC) tool that operates on verilog and the naja interchange format(https://github.com/najaeda/naja-if) and focuses today on combinational equivalence checking only — sequential boundary changes are not supported yet and remain planned work.

### Acknowledgement

[<img src="https://nlnet.nl/logo/banner.png" width=100>](https://nlnet.nl/project/Naja)
[<img src="https://nlnet.nl/image/logos/NGI0Entrust_tag.svg" width=100>](https://nlnet.nl/project/Naja)

This project is supported and funded by NLNet through the [NGI0 Entrust](https://nlnet.nl/entrust) Fund.

## Requirements 

### For Verilog:

- No change of sequential boundaries. 
- No change in names of hierarchical instances, sequential instances and top terminals.

### For Naja IF:

The Kepler‑Formal Naja IF flow is intended to verify incremental modifications generated by the najaeda Python package(https://pypi.org/project/najaeda/) or by any process that maintains stable indices across edits, ensuring that corresponding design elements retain consistent identifiers.
The property of stable indices is employed to localize the scopes affected by edits and helps the Naja IF flow to achieve superior performance relative to the Verilog flow when handling incremental modifications.

## Dependencies

On Ubuntu:

```bash
sudo apt-get install g++ libboost-dev python3.9-dev capnproto libcapnp-dev libtbb-dev pkg-config bison flex doxygen libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev
```

On macOS, using [Homebrew](https://brew.sh/):

```bash
brew install cmake doxygen capnp tbb bison flex boost spdlog zlib
```

Ensure the versions of `bison` and `flex` installed via Homebrew take precedence over the macOS defaults by modifying your $PATH environment variable as follows:

```bash
export PATH="/opt/homebrew/opt/flex/bin:/opt/homebrew/opt/bison/bin:$PATH"
```
## Build

### CMake (primary)

```bash
git clone --recurse-submodules https://github.com/keplertech/kepler-formal.git
cd kepler-formal
mkdir build
cd build
cmake ..
make
```

For best runtime performance:

```bash
cmake .. \
  -DCMAKE_BUILD_TYPE=Release \
  -DCMAKE_CXX_STANDARD=20 \
  -DCMAKE_CXX_FLAGS="-O3 -march=native -ffast-math -flto -DNDEBUG" \
  -DCMAKE_CXX_FLAGS_RELEASE="-Ofast -march=native -ffast-math -flto -DNDEBUG" \
  -DCMAKE_EXE_LINKER_FLAGS="-flto"
```

### Bazel (experimental)

Bazel build support is available alongside CMake. It uses [bzlmod](https://bazel.build/external/overview#bzlmod) (MODULE.bazel) and pulls most dependencies from the [Bazel Central Registry](https://registry.bazel.build/).

```bash
git clone --recurse-submodules https://github.com/keplertech/kepler-formal.git
cd kepler-formal
bazel build //src/bin:kepler-formal
```

Run tests:

```bash
bazel test //test/...
```

**Dependency strategy:**
- **BCR**: yaml-cpp, googletest, zlib, spdlog, oneTBB (pulled automatically by Bazel)
- **Native BUILD files**: kissat and glucose SAT solvers (simple C/C++ libraries)
- **rules_foreign_cc** (cmake wrapper): naja (too complex for native BUILD files — uses flex/bison codegen, Cap'n Proto, nested submodules)
- **System packages still required**: Boost headers, Cap'n Proto, Python3 (used by naja's cmake build inside the rules_foreign_cc sandbox)

### Future work: bazel-orfs integration

Once kepler-formal is fully buildable with Bazel, it can be consumed directly by [bazel-orfs](https://github.com/The-OpenROAD-Project/bazel-orfs) as a proper Bazel dependency instead of the current `$PATH`-based wrapper ([bazel-orfs#523](https://github.com/The-OpenROAD-Project/bazel-orfs/pull/523)). This enables:

- **`bazel_dep` or `git_override`** in bazel-orfs MODULE.bazel to pin kepler-formal to a specific version or commit
- **Hermetic LEC tests** in bazel-orfs CI without requiring a pre-installed kepler-formal binary
- **Remote caching** of kepler-formal build artifacts shared across bazel-orfs users
- **Eventual BCR publication** of kepler-formal as a first-class Bazel module

## Usage

```bash
# Classic (single file per design)
build/src/bin/kepler-formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]

# Multi-file Verilog designs
build/src/bin/kepler-formal -verilog --design1 <file...> --design2 <file...> \
  [--liberty <liberty-file>...]

# Through yaml config file
build/src/bin/kepler-formal --config <yaml file>
```

### YAML Input Paths

The YAML `input_paths` field accepts either:

- A flat list of two files (one per design), or
- A nested list with one list of files per design (multi-file Verilog).

Example:

```yaml
format: verilog
input_paths:
  - [design0_part1.v, design0_part2.v] # design 0
  - [design1_part1.v, design1_part2.v] # design 1
liberty_files:
  - library_file0.lib
  - library_file1.lib
```

## Example 

https://github.com/keplertech/kepler-formal/tree/main/example

## Contact

contact@keplertech.io