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

This project is supported and funded by NLNet through the NGI0 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:

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"

Usage

# Classic 
"build/src/bin/kepler-formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]"
# Through yaml config file
"build/src/bin/kepler-formal --config <yaml file>"

Example

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

Contact

contact@keplertech.io