kepler-formal

September 16, 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`
RTL to Gate SEC	SystemVerilog design 1 and Verilog design 2, plus Liberty libraries	`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.

Distribution

Install Nix using the official installation instructions.

Enable the keplertech Cachix binary cache, then install the CLI (Nix 2.35+ with nix-command and flakes enabled):

nix run nixpkgs#cachix -- use keplertech
nix profile install 'git+https://github.com/keplertech/kepler-formal?ref=main&submodules=1#kepler-formal'

On NixOS, run sudo nixos-rebuild switch between these two commands.

Build Instructions

CMake

Dependencies

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

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"

Bazel (experimental)

On Ubuntu, install the required host tools:

sudo apt-get install build-essential pkg-config bison flex python3-dev

Build and test with Bazelisk:

bazelisk build //src/bin:kepler-formal
bazelisk test //test/...

Additional notes and the BCR publication roadmap are tracked in docs/bcr-roadmap.md.

Usage

The full binary and YAML flag reference is tracked in docs/flags-spec.md. SEC-specific flags, engine behavior, encoding defaults, and skipped-output reports are documented in docs/sec-flags-spec.md.

Custom Python Primitives

Custom technology primitives can be defined in Python and loaded through the YAML py_tech_files option. See Custom Python Primitives for setup and deployment and the Xilinx FPGA example for the use model.

SEC Result Codes

Result	Exit code	Meaning
Proved	`0`	All checked outputs were proved equivalent.
Partially proved	`1`	Some outputs were proved; all remaining outputs are inconclusive.
Inconclusive	`2`	SEC produced neither a proof nor a counterexample.
Counterexample found	`3`	A definitive mismatch was found.
Exported (`dump_only`)	`0`	BTOR2 was written; proof was not run.

The export-only result is not an equivalence verdict. Configuration, input, or runtime errors are execution failures rather than SEC verdicts.

Binary Flags

# 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...> \
  [--verilog_design1_top <top>] [--verilog_design2_top <top>] \
  [--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.
`--version`, `-V`	Print Kepler Formal and Naja versions and build Git hashes, then exit.
`--config <file>`, `-c <file>`	Load a YAML config. Config mode cannot be combined with other CLI options.
`--verification <lec\|sec>`, `-v <lec\|sec>`	Select combinational LEC or sequential SEC. Defaults to `lec`.
`--dump-btor2 <file>`	Export the prepared SEC equivalence problem as BTOR2 before solving.
`--dump-only`	Stop after BTOR2 export without a proof verdict; requires `--dump-btor2`.
`--allow-boundary-mismatch`	Allow LEC to continue when top-level inputs or sequential-element outputs do not match by name. By default, such a mismatch stops the run before SAT solving.
`-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.
`--verilog_design1_top <top>`, `--verilog_design2_top <top>`	Select the top module for each Verilog design. In `sv2v` mode, only design 2 is Verilog.
`-sv`, `-systemverilog`	Use SystemVerilog input mode.
`--liberty <file...>`, `--lib <file...>`	Liberty library files.
`--verilog_preprocessing`	Enable preprocessing for Verilog inputs.

To intentionally compare designs with different LEC boundaries:

build/src/bin/kepler-formal -verilog --allow-boundary-mismatch \
  design1.v design2.v cells.lib

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.
`verification`	string	`lec` or `sec`. Defaults to `lec`.
`btor2_export`	bool	Enable BTOR2 export before solving; SEC only. Defaults to `false`.
`btor2_export_path`	string	BTOR2 destination; defaults to `miter.btor2` when enabled. Requires `btor2_export: true`.
`dump_only`	bool	Stop after export without solving. Defaults to `false`; requires `btor2_export: true`.
`allow-boundary-mismatch`	bool	Allow an LEC boundary mismatch. Defaults to `false`; ignored for SEC.
`input_paths`	list	Required. Either `[design0, design1]` or `[[design0_file...], [design1_file...]]`. The nested form is for multi-file Verilog.
`verilog_design1_top`, `verilog_design2_top`	string	Select the top module for each Verilog design. In `sv2v` mode, only `verilog_design2_top` is valid.
`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