kepler-formal

July 7, 2026 · View on GitHub

Introduction

Kepler-Formal is an equivalence checking tool for digital designs. It operates on Verilog, SystemVerilog, and the Naja interchange format, and supports:

Gate-level combinational Logic Equivalence Checking (LEC).
Gate-level Sequential Equivalence Checking (SEC).
RTL-level Sequential Equivalence Checking (SEC), including SystemVerilog file-list flows with explicit tops.

Acknowledgement

This project is supported and funded by NLNet through the NGI0 Entrust Fund.

Supported Flows

Flow	Typical inputs	Verification mode
Gate-level LEC	Post-synthesis or implementation netlists plus Liberty libraries	`lec`
Gate-level SEC	Sequential gate-level netlists plus Liberty libraries	`sec`
RTL-level SEC	RTL Verilog/SystemVerilog sources or SystemVerilog flists	`sec`

LEC is the default verification mode. SEC is selected with verification: sec in YAML or -v sec / --verification sec on the command line. SEC-specific engines, encodings, and skipped-output reports are documented in docs/sec-flags-spec.md.

Requirements

For Verilog/SystemVerilog:

Gate-level LEC expects no change of sequential boundaries and no change in names of hierarchical instances, sequential instances and top terminals.
Gate-level SEC and RTL-level SEC compare sequential behavior through the extracted transition systems. Internal element names are not used as cross-design equivalence assumptions but assume identical top terminals names.

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

Option A: hermetic, via Bazel (any Linux distro)

Let Bazel provide the compiler (hermetic clang/libc++) and pinned library dependencies (Boost, Cap'n Proto, TBB, zlib, FlexLexer.h) for the CMake build — no compiler or library packages needed, only build tools:

sudo apt-get install cmake make pkg-config bison flex python3-dev
bazelisk run //:deps
cmake -B build -DCMAKE_TOOLCHAIN_FILE=$PWD/deps/toolchain.cmake

The exported deps/ tree (~450 MB, mostly the clang distribution) is git-ignored and regenerated on each run; the compiler and library versions are byte-identical to the ones the Bazel build uses.

Note: cadical and kissat build in-source (thirdparty/{cadical,kissat}). When switching between the system toolchain and deps/toolchain.cmake, clean those build directories first (git -C thirdparty/cadical clean -dfx and likewise for kissat) so no objects from the other compiler linger.

Option B: system packages

On Ubuntu:

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:

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:

export PATH="/opt/homebrew/opt/flex/bin:/opt/homebrew/opt/bison/bin:$PATH"

Build

CMake (primary)

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

For best runtime performance:

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"

# Single file per design
build/src/bin/kepler-formal <-verilog/-naja_if/-systemverilog/-sv/-sv2v> [options] \
  <design1> <design2> [<library-file>...]

# Multi-file Verilog
build/src/bin/kepler-formal -verilog [options] --design1 <file...> --design2 <file...> \
  [--liberty <library-file>...] [--compact] [--report-skipped-pos]

# SystemVerilog SEC with flists
build/src/bin/kepler-formal -sv -v sec \
  --sv_design1_flist <file> --sv_design1_top <top> \
  --sv_design2_flist <file> --sv_design2_top <top> \
  [--liberty <library-file>...]

Flag	Meaning
`--help`, `-h`	Print usage.
`--config <file>`, `-c <file>`	Load a YAML config. If present, the YAML file takes precedence over the rest of the CLI.
`-verilog`	Parse both designs as Verilog.
`-naja_if`	Parse both designs as Naja IF.
`-systemverilog`, `-sv`	Parse both designs as SystemVerilog. Requires SEC.
`-sv2v`	Parse design 1 as SystemVerilog and design 2 as Verilog for SEC RTL-vs-gate comparison.
`--design1 <file...>`	Explicit source list for design 1 in multi-file Verilog mode.
`--design2 <file...>`	Explicit source list for design 2 in multi-file Verilog mode.
`-sv`, `-systemverilog`	Use SystemVerilog input mode.
`--liberty <file...>`, `--lib <file...>`	Liberty library files.
`--verilog_preprocessing`	Enable preprocessing for Verilog inputs.

YAML Configuration File

# YAML config
build/src/bin/kepler-formal --config <file.yaml>

Key	Type	Meaning
`format`	string	`verilog`, `v`, `naja_if`, `systemverilog`, `sv`, or `sv2v`. Defaults to `verilog` if omitted.
`input_paths`	list	Required. Either `[design0, design1]` or `[[design0_file...], [design1_file...]]`. The nested form is for multi-file Verilog.
`liberty_files`	list[string]	Liberty libraries loaded through `SNLLibertyConstructor`.
`py_tech_files`	list[string]	Python primitive loaders loaded through `SNLPyLoader`.
`verilog_preprocessing`	bool	Enable preprocessing for Verilog inputs.
`solver`	string	`kissat` or `glucose`. Defaults to `kissat`.
`log_file`	string	Path for the miter log file. Default logs are `miter_log_<n>.txt` in the current working directory.

Yaml file example:

format: verilog
verification: lec           # Optional: lec by default, or sec
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
py_tech_files:
  - primitives.py             # Optional: Python tech loaders are YAML-only
verilog_preprocessing: true   # Optional: enables Verilog preprocessor