From 61c850d49ecafcaaa9151d2d7b6e7b188a6c3de9 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 12 Aug 2026 11:25:51 +0200 Subject: [PATCH 1/8] Clarify primary CMake build instructions --- README.md | 49 ++++++++++++++++++++++++++----------------------- 1 file changed, 26 insertions(+), 23 deletions(-) diff --git a/README.md b/README.md index ec4e3083..70bfc499 100644 --- a/README.md +++ b/README.md @@ -51,28 +51,7 @@ The property of stable indices is employed to localize the scopes affected by ed ## 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: - -```bash -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 +### CMake dependencies (primary) On Ubuntu: @@ -91,6 +70,28 @@ Ensure the versions of `bison` and `flex` installed via Homebrew take precedence ```bash export PATH="/opt/homebrew/opt/flex/bin:/opt/homebrew/opt/bison/bin:$PATH" ``` + +### Bazel-provided CMake toolchain (experimental, Linux) + +As a secondary, experimental option, Bazel can provide the compiler +(hermetic clang/libc++) and pinned library dependencies (Boost, Cap'n Proto, +TBB, zlib, FlexLexer.h) for the CMake build. Only build tools are needed: + +```bash +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. + ## Build ### CMake (primary) @@ -117,7 +118,9 @@ cmake .. \ ### Bazel (experimental) -Bazel build notes, dependency details, release flow, and the BCR publication roadmap are tracked in [docs/bcr-roadmap.md](docs/bcr-roadmap.md). +The Bazel build is a secondary, experimental option. Build notes, dependency +details, release flow, and the BCR publication roadmap are tracked in +[docs/bcr-roadmap.md](docs/bcr-roadmap.md). ## Usage From fa2b61b7353e72fc4e21cc3270aab623e6625a70 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 12 Aug 2026 11:31:59 +0200 Subject: [PATCH 2/8] Reorganize build documentation by build system --- README.md | 52 +++++++++++++++++++++++++--------------------------- 1 file changed, 25 insertions(+), 27 deletions(-) diff --git a/README.md b/README.md index 70bfc499..9747ed9a 100644 --- a/README.md +++ b/README.md @@ -49,9 +49,9 @@ in [docs/sec-flags-spec.md](docs/sec-flags-spec.md). 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 +## CMake -### CMake dependencies (primary) +### Dependencies On Ubuntu: @@ -71,30 +71,7 @@ Ensure the versions of `bison` and `flex` installed via Homebrew take precedence export PATH="/opt/homebrew/opt/flex/bin:/opt/homebrew/opt/bison/bin:$PATH" ``` -### Bazel-provided CMake toolchain (experimental, Linux) - -As a secondary, experimental option, Bazel can provide the compiler -(hermetic clang/libc++) and pinned library dependencies (Boost, Cap'n Proto, -TBB, zlib, FlexLexer.h) for the CMake build. Only build tools are needed: - -```bash -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. - -## Build - -### CMake (primary) +### Build ```bash git clone --recurse-submodules https://github.com/keplertech/kepler-formal.git @@ -116,12 +93,33 @@ cmake .. \ -DCMAKE_EXE_LINKER_FLAGS="-flto" ``` -### Bazel (experimental) +## Bazel (experimental) The Bazel build is a secondary, experimental option. Build notes, dependency details, release flow, and the BCR publication roadmap are tracked in [docs/bcr-roadmap.md](docs/bcr-roadmap.md). +### CMake toolchain (Linux) + +As a secondary, experimental option, Bazel can provide the compiler +(hermetic clang/libc++) and pinned library dependencies (Boost, Cap'n Proto, +TBB, zlib, FlexLexer.h) for the CMake build. Only build tools are needed: + +```bash +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. + ## Usage The full binary and YAML flag reference is tracked in [docs/flags-spec.md](docs/flags-spec.md). SEC-specific flags, engine behavior, encoding defaults, and skipped-output reports are documented in [docs/sec-flags-spec.md](docs/sec-flags-spec.md). From a83c1315af8adf62f1f057b122e197c32067bec5 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 12 Aug 2026 11:47:35 +0200 Subject: [PATCH 3/8] Clarify CMake and Bazel build instructions --- README.md | 27 +++++++++------------------ 1 file changed, 9 insertions(+), 18 deletions(-) diff --git a/README.md b/README.md index 9747ed9a..17b90ec9 100644 --- a/README.md +++ b/README.md @@ -95,30 +95,21 @@ cmake .. \ ## Bazel (experimental) -The Bazel build is a secondary, experimental option. Build notes, dependency -details, release flow, and the BCR publication roadmap are tracked in -[docs/bcr-roadmap.md](docs/bcr-roadmap.md). +On Ubuntu, install the required host tools: -### CMake toolchain (Linux) +```bash +sudo apt-get install build-essential pkg-config bison flex python3-dev +``` -As a secondary, experimental option, Bazel can provide the compiler -(hermetic clang/libc++) and pinned library dependencies (Boost, Cap'n Proto, -TBB, zlib, FlexLexer.h) for the CMake build. Only build tools are needed: +Build and test with Bazelisk: ```bash -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 +bazelisk build //src/bin:kepler-formal +bazelisk test //test/... ``` -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. +Additional notes and the BCR publication roadmap are tracked in +[docs/bcr-roadmap.md](docs/bcr-roadmap.md). ## Usage From 553663f6111d7cb8928d022d69612c523d1ba172 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 12 Aug 2026 11:50:42 +0200 Subject: [PATCH 4/8] Group build instructions by build system --- README.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 17b90ec9..d3d849d2 100644 --- a/README.md +++ b/README.md @@ -49,9 +49,11 @@ in [docs/sec-flags-spec.md](docs/sec-flags-spec.md). 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. -## CMake +## Build Instructions -### Dependencies +### CMake + +#### Dependencies On Ubuntu: @@ -71,7 +73,7 @@ Ensure the versions of `bison` and `flex` installed via Homebrew take precedence export PATH="/opt/homebrew/opt/flex/bin:/opt/homebrew/opt/bison/bin:$PATH" ``` -### Build +#### Build ```bash git clone --recurse-submodules https://github.com/keplertech/kepler-formal.git @@ -93,7 +95,7 @@ cmake .. \ -DCMAKE_EXE_LINKER_FLAGS="-flto" ``` -## Bazel (experimental) +### Bazel (experimental) On Ubuntu, install the required host tools: From 4a01f85d5c28acc2ceb3ab8c1a124e820d1e2be0 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 12 Aug 2026 11:53:10 +0200 Subject: [PATCH 5/8] Link Python primitive examples --- README.md | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index d3d849d2..4bf0c31b 100644 --- a/README.md +++ b/README.md @@ -120,12 +120,9 @@ The full binary and YAML flag reference is tracked in [docs/flags-spec.md](docs/ ### Custom Python Primitives Custom technology primitives can be defined in Python and loaded with the YAML -`py_tech_files` option. Kepler-formal automatically makes an adjacent `naja.so` -available while preserving the user's existing `PYTHONPATH`. When relocating -the executable, copy its complete directory, including `naja.so`, or set -`PYTHONPATH` to another compatible module. See -[Custom Python Primitives](docs/python-primitives.md) for the file format, -lookup behavior, and deployment instructions. +`py_tech_files` option. See [Custom Python Primitives](docs/python-primitives.md) +for setup and deployment, and the [Xilinx examples](examples/xilinx) for +working models and configurations. ### SEC Result Codes From edc5c63830ffc9661a69323065f199f4a85cd2ca Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 12 Aug 2026 12:01:53 +0200 Subject: [PATCH 6/8] Refine Python primitive documentation --- README.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 4bf0c31b..0eff2ed4 100644 --- a/README.md +++ b/README.md @@ -119,10 +119,10 @@ The full binary and YAML flag reference is tracked in [docs/flags-spec.md](docs/ ### Custom Python Primitives -Custom technology primitives can be defined in Python and loaded with the YAML -`py_tech_files` option. See [Custom Python Primitives](docs/python-primitives.md) -for setup and deployment, and the [Xilinx examples](examples/xilinx) for -working models and configurations. +Custom technology primitives can be defined in Python and loaded through the +YAML `py_tech_files` option. See +[Custom Python Primitives](docs/python-primitives.md) for setup and deployment +and the [Xilinx FPGA example](examples/xilinx) for the use model. ### SEC Result Codes From 1616f6900d599207d83dd763ccf322b6f97413da Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Fri, 14 Aug 2026 00:34:03 +0200 Subject: [PATCH 7/8] allow : in liberty identifiers in naja --- thirdparty/naja | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/thirdparty/naja b/thirdparty/naja index abe47a6d..83f3c95d 160000 --- a/thirdparty/naja +++ b/thirdparty/naja @@ -1 +1 @@ -Subproject commit abe47a6d0ff1c9392e08834440a5f3b50da134af +Subproject commit 83f3c95d0d26438240ee852e6d5b2ddd0e2bd9cb From ec73e59495002e99220e8ae02c835f6c377faf32 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Fri, 14 Aug 2026 01:10:33 +0200 Subject: [PATCH 8/8] Update Naja dependency revision --- bazel/deps.bzl | 4 ++-- thirdparty/naja | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/bazel/deps.bzl b/bazel/deps.bzl index 4ae3c741..1c0e3594 100644 --- a/bazel/deps.bzl +++ b/bazel/deps.bzl @@ -33,7 +33,7 @@ _FLEX_VERSION = "2.6.4" _CADICAL_COMMIT = "7b99c07f0bcab5824a5a3ce62c7066554017f641" _GLUCOSE_COMMIT = "7f887abba7cf13636a5ac2d28653668a20a91b25" _KISSAT_COMMIT = "8af8e56f174b778aef3aa45af9f739b2a5f492c2" -_NAJA_COMMIT = "abe47a6d0ff1c9392e08834440a5f3b50da134af" +_NAJA_COMMIT = "c96e1b18bf6e411a9ed5273eac0d4cea1c79c73f" _NAJA_VERILOG_COMMIT = "5da040bb34f0e4e5bb8d67223b999a0132fb401f" _NAJA_IF_COMMIT = "099677d9f52c0db11b12c08d03e32543eebc7888" _SLANG_COMMIT = "512c327c209d3043aa98ecfd02d06a1b73fcd5fb" @@ -156,7 +156,7 @@ def _deps_impl(_module_ctx): http_archive( name = "naja", url = "https://github.com/nanocoh/naja/archive/{}.tar.gz".format(_NAJA_COMMIT), - sha256 = "d7121316309a47f8fd39fe07efa308ca3e935c3ad8f0131443c3666a96d6bb17", + sha256 = "055337bc81b41cf6f10720950d99afed7c4ae7c328f42ec28d9185d392f33f13", strip_prefix = "naja-{}".format(_NAJA_COMMIT), build_file = Label("//bazel:naja.BUILD.bazel"), patch_args = ["-p0", "-f"], diff --git a/thirdparty/naja b/thirdparty/naja index 83f3c95d..c96e1b18 160000 --- a/thirdparty/naja +++ b/thirdparty/naja @@ -1 +1 @@ -Subproject commit 83f3c95d0d26438240ee852e6d5b2ddd0e2bd9cb +Subproject commit c96e1b18bf6e411a9ed5273eac0d4cea1c79c73f