kepler-formal

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"

Bazel (experimental)

Bazel build notes, dependency details, release flow, 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.

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...> \
  [--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

Examples

See example tests

Contact

contact@keplertech.io