Skip to content
Open

c2rtl #152

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
eed5606
Embed XLS C2RTL flow
nanocoh Jul 10, 2026
1056dde
fixes
nanocoh Jul 11, 2026
50117e1
Optimize lazy SEC cone materialization
nanocoh Jul 12, 2026
4a198eb
Revert "Optimize lazy SEC cone materialization"
nanocoh Jul 12, 2026
5f438b0
legacy -> pdr
nanocoh Jul 12, 2026
b1516a6
Reapply "Optimize lazy SEC cone materialization"
nanocoh Jul 12, 2026
7139166
Trim embedded XLS C2RTL build surface
nanocoh Jul 13, 2026
a23312d
sec in cc flow
nanocoh Jul 13, 2026
78f665c
deps fix in wfs
nanocoh Jul 13, 2026
1679a38
Merge branch 'main' into cc2rtl
nanocoh Jul 13, 2026
ddf0c60
Fix macOS Glucose build
nanocoh Jul 13, 2026
7a03f4c
Merge branch 'cc2rtl' of https://github.com/keplertech/kepler-formal …
nanocoh Jul 13, 2026
820f96d
update configs
nanocoh Jul 13, 2026
9949ec5
update configs
nanocoh Jul 13, 2026
419cdca
fix build
nanocoh Jul 13, 2026
bee5221
Fix C2RTL CMake CI builds
nanocoh Jul 13, 2026
6d0a274
build fix
nanocoh Jul 13, 2026
8a1b5d1
build fix
nanocoh Jul 13, 2026
6535b4b
build fix
nanocoh Jul 13, 2026
236c0f1
build fix
nanocoh Jul 13, 2026
3f455e9
build fix
nanocoh Jul 13, 2026
77537c0
build fix
nanocoh Jul 13, 2026
a307658
build fix
nanocoh Jul 13, 2026
96dd92d
build fix
nanocoh Jul 13, 2026
3ad766f
build fix
nanocoh Jul 13, 2026
5e3f783
build fix
nanocoh Jul 13, 2026
c67d2ad
build fix
nanocoh Jul 14, 2026
2acd809
build fix
nanocoh Jul 14, 2026
017c703
build fix
nanocoh Jul 14, 2026
fd6a61b
build fix
nanocoh Jul 14, 2026
60e8766
build fix
nanocoh Jul 14, 2026
4868fe9
build fix
nanocoh Jul 14, 2026
f721521
build fix
nanocoh Jul 14, 2026
54ddbd9
build fix
nanocoh Jul 14, 2026
b2db376
build fix
nanocoh Jul 14, 2026
8fc9c2a
Wire XLS C2RTL Bazel dependencies
nanocoh Jul 26, 2026
3988b1a
Merge main into cc2rtl
nanocoh Jul 26, 2026
a4b0036
Optimize C2RTL preprocessing and ancestry loop checks
nanocoh Jul 27, 2026
fbf2c0e
Optimize compact SEC extraction and self-comparison
nanocoh Aug 2, 2026
a17325c
Merge remote-tracking branch 'origin/main' into cc2rtl
nanocoh Aug 2, 2026
3cd7e87
Fix CaDiCaL LTO builds and document CMake dependencies
nanocoh Aug 2, 2026
b4c4b9e
Complete embedded XLS C2RTL Bazel integration
nanocoh Aug 2, 2026
bcb8fd1
Reduce compact SEC memory and proof construction cost
nanocoh Aug 3, 2026
7a00cad
Fix stateless PDR equivalence checking
nanocoh Aug 3, 2026
79b9135
Merge remote-tracking branch 'origin/main' into cc2rtl
nanocoh Aug 10, 2026
b8c677e
Fix xls_c2rtl consumer dependency build
nanocoh Aug 10, 2026
56f2a3d
Update Naja for divmod truth table support
nanocoh Aug 10, 2026
2c89735
Fix consumer and Clang 22 dependency builds
nanocoh Aug 10, 2026
22c6f08
Preserve assignment topology during SEC extraction
nanocoh Aug 10, 2026
99ece4f
Preserve C2RTL reference output names
nanocoh Aug 11, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions .bazelrc
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,12 @@ build --host_cxxopt=-std=c++20
common:linux --repo_env=BAZEL_DO_NOT_DETECT_CPP_TOOLCHAIN=1
build:linux --dynamic_mode=off

# rules_foreign_cc invokes host tools such as cmake from sandboxed actions.
# On macOS those tools usually live under Homebrew, which is not always present
# in Bazel's default action PATH.
build:macos --action_env=PATH=/opt/homebrew/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin
build:macos --repo_env=PATH=/opt/homebrew/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin

# Force C11 for host tools to work around rules_foreign_cc pkg-config
# bootstrap failure: bundled glib uses 'bool' as a struct field name,
# which is a keyword in GCC 15's default C23 mode.
Expand Down
159 changes: 159 additions & 0 deletions .github/scripts/install-cmake-deps-ubuntu.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,159 @@
#!/usr/bin/env bash
# Copyright 2026 keplertech.io
# SPDX-License-Identifier: GPL-3.0-only

set -euo pipefail

llvm_version="${KEPLER_LLVM_VERSION:-22}"
# shellcheck disable=SC1091
source /etc/os-release
ubuntu_codename="${VERSION_CODENAME:-jammy}"
llvm_keyring="/usr/share/keyrings/llvm-snapshot.gpg"
llvm_list="/etc/apt/sources.list.d/llvm-toolchain-${ubuntu_codename}-${llvm_version}.list"

sudo apt-get update
sudo apt-get install -yq ca-certificates curl gnupg lsb-release

if [[ ! -f "${llvm_keyring}" ]]; then
curl -fsSL https://apt.llvm.org/llvm-snapshot.gpg.key \
| sudo gpg --dearmor -o "${llvm_keyring}"
fi
printf 'deb [signed-by=%s] https://apt.llvm.org/%s/ llvm-toolchain-%s-%s main\n' \
"${llvm_keyring}" "${ubuntu_codename}" "${ubuntu_codename}" "${llvm_version}" \
| sudo tee "${llvm_list}" >/dev/null

sudo apt-get update
sudo apt-get install -yq \
build-essential cmake ninja-build pkg-config curl ca-certificates \
bison flex doxygen python3-dev \
"clang-${llvm_version}" "clang-tools-${llvm_version}" \
"llvm-${llvm_version}-dev" \
"libclang-${llvm_version}-dev" "libclang-cpp${llvm_version}-dev" \
libboost-dev libboost-iostreams-dev libfl-dev \
capnproto libcapnp-dev libtbb-dev libspdlog-dev libfmt-dev \
libgtest-dev libssl-dev \
libz3-dev zlib1g-dev \
"$@"

absl_version="20260107.0"
protobuf_version="${KEPLER_PROTOBUF_VERSION:-35.1}"
re2_version="${KEPLER_RE2_VERSION:-2025-11-05}"
ortools_version="${KEPLER_ORTOOLS_VERSION:-9.15}"
absl_prefix="/usr/local"
absl_config="${absl_prefix}/lib/cmake/absl/abslConfig.cmake"

if [[ ! -f "${absl_config}" ]]; then
work_dir="${RUNNER_TEMP:-/tmp}/abseil-cpp-${absl_version}"
src_dir="${work_dir}/src"
build_dir="${work_dir}/build"

rm -rf "${work_dir}"
mkdir -p "${work_dir}"
curl -L "https://github.com/abseil/abseil-cpp/archive/refs/tags/${absl_version}.tar.gz" \
-o "${work_dir}/abseil-cpp.tar.gz"
tar -xzf "${work_dir}/abseil-cpp.tar.gz" -C "${work_dir}"
mv "${work_dir}/abseil-cpp-${absl_version}" "${src_dir}"

cmake -S "${src_dir}" -B "${build_dir}" \
-DCMAKE_BUILD_TYPE=Release \
-DCMAKE_CXX_STANDARD=20 \
-DCMAKE_C_COMPILER="clang-${llvm_version}" \
-DCMAKE_CXX_COMPILER="clang++-${llvm_version}" \
-DCMAKE_POSITION_INDEPENDENT_CODE=ON \
-DABSL_BUILD_TESTING=OFF \
-DABSL_ENABLE_INSTALL=ON \
-DABSL_PROPAGATE_CXX_STD=ON \
-DCMAKE_INSTALL_PREFIX="${absl_prefix}"
cmake --build "${build_dir}" -j "$(nproc)"
sudo cmake --install "${build_dir}"
sudo ldconfig
fi

re2_prefix="/usr/local"
re2_header="${re2_prefix}/include/re2/re2.h"

if [[ ! -f "${re2_header}" ]]; then
work_dir="${RUNNER_TEMP:-/tmp}/re2-${re2_version}"
src_dir="${work_dir}/src"
build_dir="${work_dir}/build"

rm -rf "${work_dir}"
mkdir -p "${work_dir}"
curl -L "https://github.com/google/re2/archive/refs/tags/${re2_version}.tar.gz" \
-o "${work_dir}/re2.tar.gz"
tar -xzf "${work_dir}/re2.tar.gz" -C "${work_dir}"
mv "${work_dir}/re2-${re2_version}" "${src_dir}"

cmake -S "${src_dir}" -B "${build_dir}" \
-DCMAKE_BUILD_TYPE=Release \
-DCMAKE_CXX_STANDARD=20 \
-DCMAKE_C_COMPILER="clang-${llvm_version}" \
-DCMAKE_CXX_COMPILER="clang++-${llvm_version}" \
-DCMAKE_POSITION_INDEPENDENT_CODE=ON \
-DRE2_BUILD_TESTING=OFF \
-DCMAKE_PREFIX_PATH="${absl_prefix}" \
-DCMAKE_INSTALL_PREFIX="${re2_prefix}"
cmake --build "${build_dir}" -j "$(nproc)"
sudo cmake --install "${build_dir}"
sudo ldconfig
fi

protobuf_prefix="/usr/local"
protobuf_config="${protobuf_prefix}/lib/cmake/protobuf/protobuf-config.cmake"

if [[ ! -f "${protobuf_config}" ]]; then
work_dir="${RUNNER_TEMP:-/tmp}/protobuf-${protobuf_version}"
src_dir="${work_dir}/src"
build_dir="${work_dir}/build"

rm -rf "${work_dir}"
mkdir -p "${work_dir}"
curl -L "https://github.com/protocolbuffers/protobuf/releases/download/v${protobuf_version}/protobuf-${protobuf_version}.tar.gz" \
-o "${work_dir}/protobuf.tar.gz"
tar -xzf "${work_dir}/protobuf.tar.gz" -C "${work_dir}"
mv "${work_dir}/protobuf-${protobuf_version}" "${src_dir}"

cmake -S "${src_dir}" -B "${build_dir}" \
-DCMAKE_BUILD_TYPE=Release \
-DCMAKE_CXX_STANDARD=20 \
-DCMAKE_C_COMPILER="clang-${llvm_version}" \
-DCMAKE_CXX_COMPILER="clang++-${llvm_version}" \
-DCMAKE_POSITION_INDEPENDENT_CODE=ON \
-Dprotobuf_BUILD_TESTS=OFF \
-DBUILD_SHARED_LIBS=ON \
-Dprotobuf_BUILD_SHARED_LIBS=ON \
-Dprotobuf_ABSL_PROVIDER=package \
-Dprotobuf_BUILD_PROTOC_BINARIES=ON \
-Dprotobuf_INSTALL=ON \
-DCMAKE_PREFIX_PATH="${absl_prefix}" \
-DCMAKE_INSTALL_PREFIX="${protobuf_prefix}"
cmake --build "${build_dir}" -j "$(nproc)"
sudo cmake --install "${build_dir}"
sudo ldconfig
fi

ortools_prefix="/usr/local"
ortools_header="${ortools_prefix}/include/ortools/graph/graph.h"

if [[ ! -f "${ortools_header}" ]]; then
work_dir="${RUNNER_TEMP:-/tmp}/or-tools-${ortools_version}"
src_dir="${work_dir}/src"

rm -rf "${work_dir}"
mkdir -p "${src_dir}"
curl -L \
"https://github.com/google/or-tools/releases/download/v${ortools_version}/or-tools-${ortools_version}.tar.gz" \
-o "${work_dir}/or-tools.tar.gz"
tar -xzf "${work_dir}/or-tools.tar.gz" \
-C "${src_dir}" \
--strip-components=1

sudo mkdir -p "${ortools_prefix}/include"
sudo cp -R "${src_dir}/ortools" "${ortools_prefix}/include/"
fi

if [[ -n "${GITHUB_ENV:-}" ]]; then
echo "CPATH=${ortools_prefix}/include${CPATH:+:${CPATH}}" >> "${GITHUB_ENV}"
echo "CPLUS_INCLUDE_PATH=${ortools_prefix}/include${CPLUS_INCLUDE_PATH:+:${CPLUS_INCLUDE_PATH}}" >> "${GITHUB_ENV}"
echo "CXXFLAGS=-I${ortools_prefix}/include${CXXFLAGS:+ ${CXXFLAGS}}" >> "${GITHUB_ENV}"
fi
9 changes: 6 additions & 3 deletions .github/workflows/bazel.yml
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,16 @@ jobs:

steps:
- uses: actions/checkout@v4
# No submodules needed — Bazel fetches deps via http_archive
with:
submodules: true
# Bazel fetches most deps via http_archive/BCR, but the C2RTL overlay
# deliberately builds from the pinned thirdparty/xls checkout.

- name: Cache Bazel outputs
uses: actions/cache@v4
with:
path: ~/.cache/bazel
key: bazel-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/deps.bzl', 'bazel/*.BUILD.bazel') }}
key: bazel-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/deps.bzl', 'bazel/*.BUILD.bazel', 'bazel/*.bzl') }}
restore-keys: |
bazel-${{ runner.os }}-

Expand All @@ -28,7 +31,7 @@ jobs:
sudo apt-get update
sudo apt-get install -yq \
build-essential pkg-config \
bison flex python3-dev
bison cmake flex ninja-build python3-dev

- name: Build kepler-formal
run: bazelisk build //src/bin:kepler-formal
Expand Down
12 changes: 2 additions & 10 deletions .github/workflows/c-cpp.yml
Original file line number Diff line number Diff line change
Expand Up @@ -18,25 +18,17 @@ jobs:
- uses: actions/checkout@v4
with:
submodules: true
# install dependencies
- name: Install GoogleTest
run: sudo apt-get update && sudo apt-get install -y libgtest-dev cmake
- name: Checkout submodules
run: git submodule update --init --recursive

- name: Install system dependencies
run: |
sudo apt-get update
sudo apt-get install -yq \
build-essential cmake ninja-build clang pkg-config \
libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \
libgtest-dev libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev
run: bash .github/scripts/install-cmake-deps-ubuntu.sh

- name: Configure CMake
working-directory: ${{github.workspace}}/
run: |
rm -rf build
cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang-22 -DCMAKE_CXX_COMPILER=clang++-22 -DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" -DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20


- name: Build
Expand Down
10 changes: 6 additions & 4 deletions .github/workflows/consumer.yml
Original file line number Diff line number Diff line change
Expand Up @@ -19,20 +19,22 @@ jobs:

steps:
- uses: actions/checkout@v4
with:
submodules: true
# The C2RTL overlay copies the pinned thirdparty/xls checkout, so the
# dependency smoke test needs the same submodule checkout as root builds.

- name: Cache Bazel outputs
uses: actions/cache@v4
with:
path: ~/.cache/bazel
key: bazel-consumer-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/deps.bzl', 'bazel/*.BUILD.bazel') }}
restore-keys: |
bazel-consumer-${{ runner.os }}-
key: bazel-consumer-${{ runner.os }}-${{ hashFiles('MODULE.bazel', '.github/consumer-test/MODULE.bazel', '.github/workflows/consumer.yml', 'bazel/deps.bzl', 'bazel/*.BUILD.bazel', 'bazel/*.bzl') }}

- name: Install system dependencies
run: |
sudo apt-get update
sudo apt-get install -yq \
build-essential pkg-config \
build-essential pkg-config cmake ninja-build \
bison flex python3-dev

- name: Build kepler-formal as a dependency
Expand Down
16 changes: 4 additions & 12 deletions .github/workflows/coverage.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,19 +20,11 @@ jobs:
fetch-depth: 0
submodules: true

# install dependencies
- name: Install GoogleTest
run: sudo apt-get update && sudo apt-get install -y libgtest-dev cmake
- name: Checkout submodules
run: git submodule update --init --recursive

- name: Install system dependencies
run: |
sudo apt-get update
sudo apt-get install -yq \
build-essential cmake ninja-build clang pkg-config \
libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \
libgtest-dev libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev lcov
run: bash .github/scripts/install-cmake-deps-ubuntu.sh lcov

- name: Configure CMake
# Configure CMake in a 'build' subdirectory. `CMAKE_BUILD_TYPE` is only required if you are using a single-configuration generator such as make.
Expand All @@ -41,14 +33,14 @@ jobs:
GIT_CONFIG_COUNT: "1"
GIT_CONFIG_KEY_0: core.abbrev
GIT_CONFIG_VALUE_0: "7"
run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -DCODE_COVERAGE=ON -DLONG_TESTS=ON
run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -DCMAKE_C_COMPILER=clang-22 -DCMAKE_CXX_COMPILER=clang++-22 -DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" -DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 -DCODE_COVERAGE=ON -DLONG_TESTS=ON -DCMAKE_CXX_STANDARD=20

- name: Build
# Build your program with the given configuration
run: cmake --build ${{github.workspace}}/build -j 4 --config ${{env.BUILD_TYPE}}
env:
CC: clang
CXX: clang++
CC: clang-22
CXX: clang++-22

- name: Generate Naja IF test inputs with the local Naja checkout
working-directory: ${{github.workspace}}/example
Expand Down
11 changes: 5 additions & 6 deletions .github/workflows/cva6imc.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,7 @@ jobs:
submodules: true

- name: Install dependencies
run: |
sudo apt-get update
sudo apt-get install -y \
libgtest-dev cmake pkg-config libboost-dev libfl-dev \
capnproto libcapnp-dev ninja-build libtbb-dev libspdlog-dev \
libboost-iostreams-dev zlib1g-dev
run: bash .github/scripts/install-cmake-deps-ubuntu.sh

- name: Checkout submodules
run: git submodule update --init --recursive
Expand All @@ -31,6 +26,10 @@ jobs:
run: |
cmake -B ${{github.workspace}}/build \
-GNinja \
-DCMAKE_C_COMPILER=clang-22 \
-DCMAKE_CXX_COMPILER=clang++-22 \
-DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" \
-DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 \
-DPYTHON_INTERFACE=OFF \
-DCMAKE_BUILD_TYPE=Release \
-DCMAKE_CXX_STANDARD=20 \
Expand Down
11 changes: 5 additions & 6 deletions .github/workflows/cva6ki.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,7 @@ jobs:
submodules: true

- name: Install dependencies
run: |
sudo apt-get update
sudo apt-get install -y \
libgtest-dev cmake pkg-config libboost-dev libfl-dev \
capnproto libcapnp-dev ninja-build libtbb-dev libspdlog-dev \
libboost-iostreams-dev zlib1g-dev
run: bash .github/scripts/install-cmake-deps-ubuntu.sh

- name: Checkout submodules
run: git submodule update --init --recursive
Expand All @@ -31,6 +26,10 @@ jobs:
run: |
cmake -B ${{github.workspace}}/build \
-GNinja \
-DCMAKE_C_COMPILER=clang-22 \
-DCMAKE_CXX_COMPILER=clang++-22 \
-DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" \
-DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 \
-DPYTHON_INTERFACE=OFF \
-DCMAKE_BUILD_TYPE=Release \
-DCMAKE_CXX_STANDARD=20 \
Expand Down
11 changes: 5 additions & 6 deletions .github/workflows/cva6pdr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,7 @@ jobs:
submodules: true

- name: Install dependencies
run: |
sudo apt-get update
sudo apt-get install -y \
libgtest-dev cmake pkg-config libboost-dev libfl-dev \
capnproto libcapnp-dev ninja-build libtbb-dev libspdlog-dev \
libboost-iostreams-dev zlib1g-dev
run: bash .github/scripts/install-cmake-deps-ubuntu.sh

- name: Checkout submodules
run: git submodule update --init --recursive
Expand All @@ -31,6 +26,10 @@ jobs:
run: |
cmake -B ${{github.workspace}}/build \
-GNinja \
-DCMAKE_C_COMPILER=clang-22 \
-DCMAKE_CXX_COMPILER=clang++-22 \
-DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" \
-DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 \
-DPYTHON_INTERFACE=OFF \
-DCMAKE_BUILD_TYPE=Release \
-DCMAKE_CXX_STANDARD=20 \
Expand Down
Loading
Loading