Fixes

.github/workflows/c-cpp.yml

@@ -30,7 +30,7 @@ jobs:
         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
+          libgtest-dev libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev
 
     - name: Configure CMake
       working-directory: ${{github.workspace}}/

.github/workflows/coverage.yml

@@ -0,0 +1,71 @@
+name: coverage
+
+on:
+  push:
+    branches: [ main ]
+  pull_request:
+    branches: [ main ]
+  workflow_dispatch:
+
+env:
+  BUILD_TYPE: Debug
+
+jobs:
+  build:
+    runs-on: ubuntu-22.04
+
+    steps:
+    - uses: actions/checkout@v5
+      with:
+        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
+
+    - 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.
+      # See https://cmake.org/cmake/help/latest/variable/CMAKE_BUILD_TYPE.html?highlight=cmake_build_type
+      run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -DCODE_COVERAGE=ON -DLONG_TESTS=ON
+
+    - 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++
+
+    - name: Test
+      working-directory: ${{github.workspace}}/build
+      env:
+        PYTHONMALLOC: malloc
+      run: ctest -VV -E ".*[p|P]ython.*" -C ${{ env.BUILD_TYPE }}
+    - name: lcov
+      working-directory: ${{github.workspace}}/build
+      run: |
+           lcov --directory . --capture --output-file coverage.info
+           lcov --remove coverage.info --output-file coverage.info '/usr/*' '*/test/*' '*/kepler-formal/thirdparty/*'
+
+    - name: Upload coverage to Codecov
+      uses: codecov/codecov-action@v4
+      env:
+        CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}
+      with:
+        fail_ci_if_error: true
+        file: ${{github.workspace}}/build/coverage.info
+        disable_search: true
+        files: coverage.info
+        flags: unittests
+        name: codecov-umbrella
+        verbose: true

.github/workflows/macOS.yml

@@ -27,7 +27,7 @@ jobs:
       run: git submodule update --init --recursive
     # install dependencies
     - name: Install dependencies
-      run: brew install cmake doxygen capnp tbb bison flex boost spdlog
+      run: brew install cmake doxygen capnp tbb bison flex boost spdlog zlib
     - name: set env variable
       run: |
         echo "/usr/local/opt/flex/bin" >> $GITHUB_PATH; echo "/usr/local/opt/bison/bin" >> $GITHUB_PATH;

.github/workflows/regress.yml

@@ -30,7 +30,7 @@ jobs:
     - name: Checkout submodules
       run: git submodule update --init --recursive
     - name: Install boost & capnproto
-      run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libspdlog-dev 
+      run: sudo apt-get update && sudo apt-get install -y pkg-config libboost-dev libfl-dev capnproto libcapnp-dev ninja-build clang libtbb-dev libspdlog-dev libboost-iostreams-dev zlib1g-dev
 
     - name: Configure CMake
       run: 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
@@ -51,7 +51,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal -naja_if \
+        ./build/src/bin/kepler-formal -naja_if \
           ./example/tinyrocket_naja.if \
           ./example/tinyrocket_naja.if \
           ./example/NangateOpenCellLibrary_typical.lib \
@@ -63,7 +63,7 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ./build/src/bin/kepler_formal -verilog \
+        ./build/src/bin/kepler-formal -verilog \
           ./example/tinyrocket.v \
           ./example/tinyrocket.v \
           ./example/NangateOpenCellLibrary_typical.lib \
@@ -82,14 +82,14 @@ jobs:
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ../build/src/bin/kepler_formal --config test_config_naja_if.yaml
+        ../build/src/bin/kepler-formal --config test_config_naja_if.yaml
 
     - name: Run on verilog edited
       working-directory: ${{github.workspace}}/example
       run: |
         mkdir -p regress-output
         # Run kepler-formal on the example files (files are in example/)
-        ../build/src/bin/kepler_formal --config test_config_verilog.yaml
+        ../build/src/bin/kepler-formal --config test_config_verilog.yaml
 
 
 

.gitignore

@@ -0,0 +1,4 @@
+# Copyright 2024-2026 keplertech.io
+# SPDX-License-Identifier: GPL-3.0-only
+build
+

CMakeLists.txt

@@ -24,11 +24,23 @@ set(CMAKE_CXX_STANDARD 20 CACHE STRING "C++ standard" FORCE)
 add_subdirectory(src)
 add_subdirectory(thirdparty)
 
-option(ENABLE_UNIT_TESTS ON)
-if(ENABLE_UNIT_TESTS)
-  include(CTest)
-  add_subdirectory(test)
-endif()
+# option(ENABLE_UNIT_TESTS ON)
+# if(ENABLE_UNIT_TESTS)
+include(CTest)
+enable_testing()
+add_subdirectory(test)
+# endif()
+
+option(CODE_COVERAGE "Enable coverage reporting" OFF)
+if(CODE_COVERAGE)
+  # Add required flags (GCC & LLVM/Clang)
+  target_compile_options(coverage_config INTERFACE
+    -O0        # no optimization
+    -g         # generate debug info
+    --coverage # sets all required flags
+  )
+  target_link_options(coverage_config INTERFACE --coverage)
+endif(CODE_COVERAGE)
 
 find_package(TBB REQUIRED)
 
@@ -42,3 +54,9 @@ target_include_directories(formal_structures
 target_link_libraries(formal_structures
   PRIVATE TBB::tbb
 )
+
+option(ENABLE_COVERAGE "Enable coverage flags" ON)
+if(ENABLE_COVERAGE AND (CMAKE_CXX_COMPILER_ID MATCHES "GNU|Clang"))
+  add_compile_options(--coverage -g)
+  add_link_options(--coverage)
+endif()

README.md

@@ -28,13 +28,13 @@ The property of stable indices is employed to localize the scopes affected by ed
 On Ubuntu:
 
 ```bash
-sudo apt-get install g++ libboost-dev python3.9-dev capnproto libcapnp-dev libtbb-dev pkg-config bison flex doxygen libspdlog-dev 
+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](https://brew.sh/):
 
 ```bash
-brew install cmake doxygen capnp tbb bison flex boost spdlog
+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:
@@ -54,19 +54,21 @@ make
 ```
 
 ```bash
-# For optimized performance use: 
-cmake .. -DCMAKE_BUILD_TYPE=Release \
-  -DCMAKE_CXX_FLAGS_RELEASE="-Ofast -march=native \
-  -ffast-math -flto" -DCMAKE_EXE_LINKER_FLAGS="-flto"
+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
 
 ```bash
 # Classic 
-"build/src/bin/kepler_formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]"
+"build/src/bin/kepler-formal <-verilog/-naja_if> <netlist1> <netlist2> [<liberty-file>...]"
 # Through yaml config file
-"build/src/bin/kepler_formal --config <yaml file>"
+"build/src/bin/kepler-formal --config <yaml file>"
 ```
 
 ## Example 

example/README.md

@@ -7,10 +7,10 @@ cd example
 pip install najaeda
 python edit.py
 # For naja_if
-../build/src/bin/kepler_formal -naja_if tinyrocket_naja.if tinyrocket_naja_edited.if NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib
+../build/src/bin/kepler-formal -naja_if tinyrocket_naja.if tinyrocket_naja_edited.if NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib
 # For verilog
-../build/src/bin/kepler_formal -verilog tinyrocket_pre_edited.v tinyrocket_edited.v NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib /example/fakeram45_64x32.lib
+../build/src/bin/kepler-formal -verilog tinyrocket_pre_edited.v tinyrocket_edited.v NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib /example/fakeram45_64x32.lib
 # Through config file
-../build/src/bin/kepler_formal --config test_config_naja_if.yaml
-../build/src/bin/kepler_formal --config test_config_verilog.yaml 
+../build/src/bin/kepler-formal --config test_config_naja_if.yaml
+../build/src/bin/kepler-formal --config test_config_verilog.yaml 
 ```