diff --git a/.dockerignore b/.dockerignore index e1a31f4e72..75e99b1d85 100644 --- a/.dockerignore +++ b/.dockerignore @@ -1,6 +1,11 @@ # Build working directories tools/OpenROAD/build/ -tools/kepler-formal/build/ +# A checkout from before kepler-formal moved to etc/kepler-formal keeps +# the old submodule tree; keep it out of the image and its licenses. +tools/kepler-formal/ +# Local Bazel outputs; the image builds its own. +etc/kepler-formal/bazel-* +etc/kepler-formal/MODULE.bazel.lock # Build files build_openroad.log diff --git a/.gitignore b/.gitignore index 84d1e39569..afa12adbe8 100644 --- a/.gitignore +++ b/.gitignore @@ -104,6 +104,8 @@ bazel-out bazel-OpenROAD-flow-scripts bazel-testlogs MODULE.bazel.lock +# etc/kepler-formal +bazel-kepler-formal # python venv venv/ diff --git a/.gitmodules b/.gitmodules index 20440a806e..bcda953424 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,6 +4,3 @@ [submodule "tools/OpenROAD"] path = tools/OpenROAD url = ../OpenROAD.git -[submodule "tools/kepler-formal"] - path = tools/kepler-formal - url = https://github.com/keplertech/kepler-formal diff --git a/build_openroad.sh b/build_openroad.sh index 0eef046bd5..3ccfd38842 100755 --- a/build_openroad.sh +++ b/build_openroad.sh @@ -385,7 +385,9 @@ __local_build() source /opt/rh/devtoolset-8/enable set -u fi - # EL8: the default GCC 8 is too old for kepler-formal. + # EL8: the default GCC 8 is too old for Yosys, which needs C++20. + # It stays active for kepler-formal, which uses the host compiler + # where no downloaded clang is registered (aarch64). if [[ -f "/opt/rh/gcc-toolset-13/enable" ]]; then set +u source /opt/rh/gcc-toolset-13/enable @@ -423,27 +425,20 @@ __local_build() ${YOSYS_ARGS} ${NICE} cmake --build tools/yosys/build --target install -j "${PROC}" - echo "[INFO FLW-0031] Compiling kepler-formal" - # -march=x86-64-v3 is valid only for x86 compilers. On Arm, use the - # Armv8-A baseline, so that the binary runs on any aarch64 machine. - # EL9 ships TBB 2020, where concurrent_map needs - # TBB_PREVIEW_CONCURRENT_ORDERED_CONTAINERS; oneTBB ignores it. - # EL installs libraries in lib64 by default; the RPATH points to lib. - case "$(uname -m)" in - aarch64|arm64) KEPLER_MARCH="-march=armv8-a" ;; - *) KEPLER_MARCH="-march=x86-64-v3" ;; - esac - ${NICE} cmake -B tools/kepler-formal/build tools/kepler-formal \ - -DCMAKE_BUILD_TYPE=Release \ - -DCMAKE_CXX_FLAGS_RELEASE="-Ofast ${KEPLER_MARCH} -ffast-math -flto -DTBB_PREVIEW_CONCURRENT_ORDERED_CONTAINERS=1" \ - -DCMAKE_EXE_LINKER_FLAGS="-flto" \ - -DCMAKE_BUILD_RPATH="${DIR}/tools/kepler-formal/build/thirdparty/naja/src/dnl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/nl/nl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/optimization" \ - -DCMAKE_INSTALL_RPATH="${INSTALL_PATH}/kepler-formal/lib" \ - -DCMAKE_INSTALL_LIBDIR=lib \ - -DCMAKE_BUILD_WITH_INSTALL_RPATH=OFF \ - -DCMAKE_INSTALL_RPATH_USE_LINK_PATH=OFF \ - -DCMAKE_INSTALL_PREFIX="${INSTALL_PATH}/kepler-formal" - ${NICE} cmake --build tools/kepler-formal/build --target install -j "${PROC}" + echo "[INFO FLW-0031] Installing kepler-formal" + # etc/kepler-formal pins kepler-formal; Bazel downloads it, its + # dependencies and the compiler. See etc/kepler-formal/README.md. + if ! command -v bazelisk &> /dev/null; then + echo "[ERROR FLW-0034] kepler-formal needs bazelisk; run etc/DependencyInstaller.sh -common." >&2 + exit 1 + fi + KEPLER_PREFIX="${INSTALL_PATH}/kepler-formal" + if [[ "${KEPLER_PREFIX}" != /* ]]; then + KEPLER_PREFIX="$(pwd)/${KEPLER_PREFIX}" + fi + (cd "${DIR}/etc/kepler-formal" && \ + ${NICE} bazelisk run --jobs="${PROC}" //:install -- "${KEPLER_PREFIX}" && \ + ./install_licenses.sh "${KEPLER_PREFIX}") if [ ${WITH_VERIFIC} -eq 1 ]; then echo "[INFO FLW-0032] Cleaning up Verific components." diff --git a/docker/Dockerfile.builder b/docker/Dockerfile.builder index 3673cfb649..5c4aa78d07 100644 --- a/docker/Dockerfile.builder +++ b/docker/Dockerfile.builder @@ -30,6 +30,7 @@ FROM orfs-builder-base AS orfs-tools-builder # Exclude install so a local build's output (e.g. tools/install/OpenROAD) # cannot leak into the image; the build below starts from an empty install. COPY --link --exclude=OpenROAD --exclude=AutoTuner --exclude=install tools tools +COPY --link etc/kepler-formal etc/kepler-formal ARG numThreads=$(nproc) ARG verificPath="" diff --git a/etc/DependencyInstaller.sh b/etc/DependencyInstaller.sh index d98925a0a3..309c7dbf81 100755 --- a/etc/DependencyInstaller.sh +++ b/etc/DependencyInstaller.sh @@ -26,7 +26,7 @@ _versionCompare() { test $a "$2" $b } -# Yosys and kepler-formal are built with CMake. Yosys needs CMake >= 3.28, +# Yosys is built with CMake and needs CMake >= 3.28, # newer than Ubuntu 22.04 ships, so fetch a release from Kitware when the # one on PATH is too old. cmakeMinVersion=3.28 @@ -108,36 +108,6 @@ _installBison() { rm -rf "${workDir}" } -# kepler-formal needs oneTBB and its CMake package. EL8 ships TBB 2018, which -# has neither, so build oneTBB there. Build it static, because the -# kepler-formal RPATH does not include the prefix. -tbbVersion=2021.13.0 -tbbChecksum=3ad5dd08954b39d113dc5b3f8a8dc6dc1fd5250032b7c491eb07aed5c94133e1 - -_installTbb() { - local prefix=${PREFIX:-"/usr/local"} - if compgen -G "${prefix}/lib*/cmake/TBB/TBBConfig.cmake" > /dev/null; then - echo "oneTBB found in ${prefix}, skipping install" - return - fi - local tarball="oneTBB-${tbbVersion}.tar.gz" - local workDir - workDir=$(mktemp -d) - ( - # _installCmake may have put CMake in a prefix that is not on PATH. - export PATH="${prefix}/bin:${PATH}" - cd "${workDir}" - wget -q -O "${tarball}" "https://github.com/uxlfoundation/oneTBB/archive/refs/tags/v${tbbVersion}.tar.gz" - sha256sum -c <(echo "${tbbChecksum} ${tarball}") - tar xzf "${tarball}" - cmake -S "oneTBB-${tbbVersion}" -B build -DCMAKE_BUILD_TYPE=Release \ - -DTBB_TEST=OFF -DBUILD_SHARED_LIBS=OFF -DCMAKE_INSTALL_PREFIX="${prefix}" - cmake --build build -j "${numThreads}" - cmake --install build - ) - rm -rf "${workDir}" -} - _installORDependencies() { if [[ ${YOSYS_VER} == "" ]]; then YOSYS_VER=v$(grep 'yosys_ver =' tools/yosys/docs/source/conf.py | awk -F'"' '{print $2}') @@ -236,14 +206,12 @@ _install_EL8_EL9_Packages() { # EL8 and EL9 use `dnf`, instead of `yum` dnf -y update - # EPEL has tcl-tclreadline and capnproto. + # EPEL has tcl-tclreadline. dnf -y install "https://dl.fedoraproject.org/pub/epel/epel-release-latest-${elVersion}.noarch.rpm" - # The rest builds Yosys and kepler-formal. + # The rest builds Yosys. dnf -y install \ bison \ boost-devel \ - capnproto \ - capnproto-devel \ findutils \ flex \ gcc \ @@ -264,7 +232,7 @@ _install_EL8_EL9_Packages() { wget \ zlib-devel - # kepler-formal and the pip lock files need Python 3.10 or newer, which + # The pip lock files need Python 3.10 or newer, which # is newer than the EL8 and EL9 defaults. dnf -y install python3.12 python3.12-devel python3.12-pip update-alternatives --install /usr/bin/python3 python3 "$(command -v python3.12)" 50 @@ -276,13 +244,11 @@ _install_EL8_EL9_Packages() { readline-devel \ tcl-tclreadline \ tcl-tclreadline-devel - # The default GCC 8 is too old for kepler-formal. + # The default GCC 8 is too old for Yosys, which needs C++20. dnf -y install gcc-toolset-13 fi if [[ "${elVersion}" == "9" ]]; then - # EL8 builds oneTBB instead, in -common. - dnf -y install tbb-devel dnf -y install \ https://mirror.stream.centos.org/9-stream/AppStream/x86_64/os/Packages/readline-devel-8.1-4.el9.x86_64.rpm fi @@ -349,13 +315,11 @@ _installUbuntuPackages() { bison \ build-essential \ ca-certificates \ - capnproto \ curl \ flex \ git \ help2man \ libboost-iostreams-dev \ - libcapnp-dev \ libffi-dev \ libfl-dev \ libfl2 \ @@ -368,7 +332,6 @@ _installUbuntuPackages() { libqt5svg5-dev \ libqt5xmlpatterns5-dev \ libreadline-dev \ - libtbb-dev \ libz-dev \ perl \ pkg-config \ @@ -471,7 +434,7 @@ _installUbuntuPackages() { _installDarwinPackages() { brew install libffi tcl-tk ruby - brew install python libomp doxygen capnp tbb bison flex boost spdlog zlib cmake + brew install python libomp doxygen bison flex boost spdlog zlib cmake brew link --force libomp brew install --cask klayout brew install docker docker-buildx @@ -701,9 +664,6 @@ case "${os}" in if [[ "${option}" == "common" || "${option}" == "all" ]]; then _installCmake _installBison - if [[ "${elVersion}" == "8" ]]; then - _installTbb - fi _installPipCommon fi ;; diff --git a/etc/DockerTag.sh b/etc/DockerTag.sh index 315392c44d..2f10d8d81f 100755 --- a/etc/DockerTag.sh +++ b/etc/DockerTag.sh @@ -16,7 +16,8 @@ if [[ "$@" == "-dev" ]]; then elif [[ "$@" == "-tools" ]]; then # Everything the orfs-tools target of Dockerfile.builder depends on: # the dev image, the build scripts, the ignore file that filters the - # build context, and the checked-out tools except OpenROAD. + # build context, the checked-out tools except OpenROAD, and the + # pinned kepler-formal. ignore_file=./docker/Dockerfile.builder.dockerignore if [[ ! -f "${ignore_file}" ]]; then ignore_file=./.dockerignore @@ -26,9 +27,11 @@ elif [[ "$@" == "-tools" ]]; then cat ./build_openroad.sh ./dev_env.sh ./etc/setup_compiler_wrappers.sh cat "${ignore_file}" # Drop the trailing describe output, which depends on fetched tags. - git submodule status tools/yosys tools/kepler-formal | awk '{print $1, $2}' + git submodule status tools/yosys | awk '{print $1, $2}' git ls-tree HEAD tools/ | grep -v -e 'tools/OpenROAD$' -e 'tools/AutoTuner$' \ - -e 'tools/yosys$' -e 'tools/kepler-formal$' + -e 'tools/yosys$' + # The kepler-formal version and the Bazel settings that install it. + git ls-tree -r HEAD etc/kepler-formal } | sha256sum | awk '{print substr($1, 1, 6)}' elif [[ "$@" == "-master" ]]; then git fetch --tags >&2 diff --git a/etc/kepler-formal/.bazelrc b/etc/kepler-formal/.bazelrc new file mode 100644 index 0000000000..9b9d949212 --- /dev/null +++ b/etc/kepler-formal/.bazelrc @@ -0,0 +1,14 @@ +common --registry=https://bcr.bazel.build/ + +# kepler-formal and naja do not set the C++ standard on their targets, +# so the build sets it, as their registry presubmits do. OpenROAD +# requires C++20 too. +build --cxxopt=-std=c++20 +build --host_cxxopt=-std=c++20 +build -c opt + +# As kepler-formal's own .bazelrc: link statically on Linux. The clang +# toolchain is chosen by register_toolchains in MODULE.bazel, on x86-64 +# Linux only. +common --enable_platform_specific_config +build:linux --dynamic_mode=off diff --git a/etc/kepler-formal/.bazelversion b/etc/kepler-formal/.bazelversion new file mode 100644 index 0000000000..acd405b1d6 --- /dev/null +++ b/etc/kepler-formal/.bazelversion @@ -0,0 +1 @@ +8.6.0 diff --git a/etc/kepler-formal/BUILD.bazel b/etc/kepler-formal/BUILD.bazel new file mode 100644 index 0000000000..4e4dc28d27 --- /dev/null +++ b/etc/kepler-formal/BUILD.bazel @@ -0,0 +1,5 @@ +# bazelisk run //:install -- +alias( + name = "install", + actual = "@kepler-formal//:install", +) diff --git a/etc/kepler-formal/MODULE.bazel b/etc/kepler-formal/MODULE.bazel new file mode 100644 index 0000000000..607087bc21 --- /dev/null +++ b/etc/kepler-formal/MODULE.bazel @@ -0,0 +1,30 @@ +"""Pins the kepler-formal that build_openroad.sh installs. + +ORFS is not a Bazel project: this module exists only to install +kepler-formal into tools/install/kepler-formal. See README.md. +""" + +module(name = "orfs-kepler-formal") + +# To bump kepler-formal, change this version. +bazel_dep(name = "kepler-formal", version = "1.0.0-20261105-6870bd1a") + +# kepler-formal builds with a downloaded clang on x86-64 Linux. It +# registers that toolchain for its own builds only, a dev_dependency by +# design, so a module that depends on it registers it too, at the same +# version, as kepler-formal's .github/consumer-test does. Elsewhere the +# host compiler is used. +bazel_dep(name = "llvm", version = "0.8.26") + +llvm_toolchains = use_extension("@llvm//extensions:toolchain.bzl", "toolchain") +llvm_toolchains.exec( + arch = "x86_64", + os = "linux", +) +llvm_toolchains.target( + arch = "x86_64", + os = "linux", +) +use_repo(llvm_toolchains, "llvm_toolchains") + +register_toolchains("@llvm_toolchains//:all") diff --git a/etc/kepler-formal/README.md b/etc/kepler-formal/README.md new file mode 100644 index 0000000000..62e16601aa --- /dev/null +++ b/etc/kepler-formal/README.md @@ -0,0 +1,39 @@ +# kepler-formal + +To bump kepler-formal, change the version in `MODULE.bazel`. + +`build_openroad.sh --local` installs kepler-formal into +`tools/install/kepler-formal/bin/kepler-formal` from this folder: + +```shell +cd etc/kepler-formal +bazelisk run //:install -- "$(pwd)/../../tools/install/kepler-formal" +``` + +ORFS is not a Bazel project. This folder only pins kepler-formal; the +install is kepler-formal's own `//:install` target. + +That target installs only kepler-formal's own license. `build_openroad.sh` +then runs `install_licenses.sh` with the same prefix, which copies the +license notices of every module linked into the binary or shipped in its +runfiles to `share/kepler-formal/licenses//`: + +```shell +./install_licenses.sh "$(pwd)/../../tools/install/kepler-formal" +``` + +## How this maps to `DependencyInstaller.sh` + +`DependencyInstaller.sh` downloads a pinned CMake from Kitware when the +one the OS ships is too old, and checks it against a checksum. Bazel +does the same for kepler-formal and every library it needs, from the +[Bazel Central Registry](https://registry.bazel.build/), which keeps the +URL, the checksum and the build file of each version: + +| `DependencyInstaller.sh`, `build_openroad.sh` | Here | +| --- | --- | +| oneTBB and capnproto from the OS, or built from a pinned tarball | `bazel_dep` versions in kepler-formal's `MODULE.bazel` | +| A pinned CMake when the OS's is too old | bazelisk runs the Bazel named in `.bazelversion` | +| `gcc-toolset-13` on EL8, because GCC 8 is too old | A pinned clang is downloaded on x86-64 Linux; elsewhere the host compiler is used, `gcc-toolset-13` on EL8, which Yosys still needs | +| `tools/kepler-formal` and the submodules inside it | The version in `MODULE.bazel`; sources are checked against their checksums and cached in `~/.cache/bazel` | +| An RPATH that points at the install's `lib/` | The binary finds its libraries next to itself, in `bin/kepler-formal.runfiles/` | diff --git a/etc/kepler-formal/install_licenses.sh b/etc/kepler-formal/install_licenses.sh new file mode 100755 index 0000000000..d41774b925 --- /dev/null +++ b/etc/kepler-formal/install_licenses.sh @@ -0,0 +1,54 @@ +#!/usr/bin/env bash +# Usage: install_licenses.sh +# +# Copies the license notices of every module that goes into the +# kepler-formal binary and its runfiles (naja, yaml-cpp, spdlog, kissat, +# the embedded Python, the statically linked libc++, ...) into +# /share/kepler-formal/licenses//. kepler-formal's +# //:install ships only its own LICENSE.rst and LICENSES/. +# +# The modules are the repositories cquery finds in the binary's target +# configuration; build tools such as bison run in the exec configuration +# and are left out. Run it after `bazelisk run //:install`, from this +# folder, so that the repositories are fetched. +set -euo pipefail + +if [[ $# -ne 1 ]]; then + echo "Usage: $0 " >&2 + exit 1 +fi +dest="$(cd "$1" && pwd)/share/kepler-formal/licenses" +binary=@kepler-formal//src/bin:kepler-formal + +cd "$(dirname "$0")" +external="$(bazelisk info output_base)/external" +config="$(bazelisk cquery "${binary}" | awk '{print $NF}')" +repos="$(bazelisk cquery --consistent_labels "deps(${binary})" \ + | awk -v c="${config}" '$NF == c' \ + | sed -n 's|^@@\([^/]*\)//.*|\1|p' | sort -u)" + +rm -rf "${dest}" +count=0 +for repo in ${repos}; do + [[ -n "${repo}" ]] || continue + # Some modules unpack into a subdirectory (zlib-1.3.2/, slang-12.0/), + # and the llvm-project one keeps libc++'s notice in libcxx/. The + # embedded Python keeps its own in lib/python3.X/. + files="$(cd "${external}/${repo}" && find . -maxdepth 3 \ + \( \( -iname 'LICENSE*' -o -iname 'LICENCE*' -o -iname 'COPYING*' \ + -o -iname 'NOTICE*' -o -iname 'COPYRIGHT*' \) \ + \( -path './*' -a ! -path './*/*/*' \ + -o -path './lib/python*/LICENSE.txt' \) \) \ + -print -prune)" + [[ -n "${files}" ]] || continue + mkdir -p "${dest}/${repo}" + while IFS= read -r f; do + (cd "${external}/${repo}" && cp -rL --parents "${f}" "${dest}/${repo}/") + done <<< "${files}" + count=$((count + 1)) +done +if [[ ${count} -eq 0 ]]; then + echo "[ERROR] no license notices found for ${binary} in ${external}" >&2 + exit 1 +fi +echo "Installed the license notices of ${count} modules in ${dest}" diff --git a/tools/kepler-formal b/tools/kepler-formal deleted file mode 160000 index f70c2e3859..0000000000 --- a/tools/kepler-formal +++ /dev/null @@ -1 +0,0 @@ -Subproject commit f70c2e38592d704c8cccf68433b091e82c8118f0