[oharboe]

Bumping kepler-formal becomes a one-line edit: the version in etc/kepler-formal/MODULE.bazel. You don't move a submodule, and you don't chase new system packages on each platform.

A build breakage like #4717 is fixed and tested in kepler-formal's own CI, not patched in ORFS's scripts.

What ORFS no longer maintains

• build_openroad.sh:
  • the kepler-formal section, including:
    • the -march choice per architecture;
    • the EL9 TBB define;
    • the LTO flags;
    • the build and install RPATHs (build_openroad.sh: kepler-formal is installed with an absolute RUNPATH, so a moved or re-pointed install loads another build's libraries #4717, build_openroad: install kepler-formal with a relative RUNPATH #4727);
  • the lines that enable gcc-toolset-13 on EL8.
• The submodule: tools/kepler-formal, along with the five submodules inside it.
• etc/DependencyInstaller.sh:
  • TBB and capnproto on Ubuntu, EL and Homebrew;
  • the oneTBB source build on EL8;
  • gcc-toolset-13 on EL8.
• Docker files: the kepler-formal entries in etc/DockerTag.sh and .dockerignore.

What doesn't change for users

• ./build_openroad.sh --local is run the same way.
• The binary still lands in tools/install/kepler-formal/bin/kepler-formal.
• env.sh, KEPLER_FORMAL_EXE and LEC_CHECK are unchanged.
• The Docker images are built the same way.

How

build_openroad.sh runs kepler-formal's own install target, bazelisk run //:install, from etc/kepler-formal/, the way it already builds OpenROAD. That folder pins kepler-formal and nothing else. ORFS itself does not become a Bazel project. Nothing new is needed on the host. The folder's README.md explains how to bump kepler-formal and how each step maps to what DependencyInstaller.sh did.

Why this is possible now

kepler-formal now installs this way after a number of PRs to kepler-formal and the Bazel Central Registry. Its install target, keplertech/kepler-formal#292, and its registry entry, bazelbuild/bazel-central-registry#11201, are both merged, so MODULE.bazel takes kepler-formal@0.5.0-20261026-a64adfaf from the registry with no override.

So far the way to install kepler-formal has been CMake plus host packages. That costs kepler-formal the same per-platform work it costs ORFS, so I expect kepler-formal to streamline its own install too. Each step upstream only makes this folder shorter, and the interface doesn't change.

How it was tested

CI tests build_openroad.sh on every supported platform, so locally I only ran smoke tests:

• etc/kepler-formal: bazelisk run //:install -- <prefix>, from a cold start with the registry version, installs on x86-64 Linux with no host packages. kepler-formal --version runs, including from a copy of the install in another directory.
• bash -n build_openroad.sh and bash -n etc/DependencyInstaller.sh pass.

🤖 Generated with Claude Code

[gemini-code-assist]

Code Review

This pull request replaces the manual CMake compilation of the kepler-formal tool and its dependencies with a Bazel-based installation using bazelisk. It removes the tools/kepler-formal submodule, cleans up related dependencies from etc/DependencyInstaller.sh, and introduces Bazel configuration files under etc/kepler-formal. Feedback on these changes includes ignoring Bazel build outputs in .dockerignore to keep the Docker build context small, correcting the ignored symlink name in .gitignore to match the workspace name orfs-kepler-formal, and avoiding the use of a personal fork as a Bazel registry in .bazelrc due to security and reliability risks.

[oharboe]

@vvbandeira ready for review.

The CI-Public/pr-merge failure is not from this PR. It is a regression on master that every open PR hits now, for example #4731, and pr-merge will re-run once it is fixed. pr-head doesn't matter once pr-merge is green. Jenkins fails in the OpenROAD build step, before the flow tests run:

Error downloading [https://github.com/MikePopoloski/slang/archive/f04e81565793c768b747a8fd058f3e7aeceee1b5.tar.gz]
Checksum was sha256-Pj8AVITB12EZCg7lD3wYZpuHgcexydYPQsOUh77CWqg= but wanted sha256-7SEVSm6uJ56ZBFyPoKeuLh6cpXLTl17x8iqBGomouLA=

GitHub now serves a different archive for that slang commit than the one recorded in the Bazel Central Registry entry sv-lang@10.0.1-20260316-f04e8156.

The step this PR changes passed in the same Jenkins runs. On both Ubuntu 26.04 and 24.04, the tools image ran bazelisk run //:install from etc/kepler-formal, and it printed kepler-formal installed to /OpenROAD-flow-scripts/tools/install/kepler-formal/bin/kepler-formal.

[oharboe]

@maliberty @povik @vvbandeira Regarding unrelated pr-merge/head failure with github sv lang .tar.gz updated hash.

Once we're switched to Bazel only in OpenROAD, we can get all yosys+sv-lang, etc. into bazel bcr instead of git submodules.

Then we're no longer vulnerable to hash upates on github and it is bazel idiomatic.

That's a bit of an ordeal to untangle, I only have a vague sense of all the details, but worth it as it makes life for everyone simpler going forward.

[openroad-ci]

🔍 QoR check

Metrics reflect the PR merge build — i.e. what will land on the target branch.

Commit 7b3387b · Jenkins build #7 · Baseline: build · View build on dashboard

62 design(s) checked — 0 with regression(s), 1 without a comparable baseline.

[saikatchatrg]

Checked #4732 at 2aa8f0a for the #4717 case. bazelisk run //:install from etc/kepler-formal, as build_openroad.sh runs it, built and installed in 109 s here (Ubuntu, x86-64). The installed bin/kepler-formal has only $ORIGIN-relative RUNPATH entries into bin/kepler-formal.runfiles/, and ldd resolves its two non-system libraries (libnaja_runtime.so and the bundled libpython3.11.so.1.0) there. The binary contains no build path and the install has no symlinks. I copied the install to another directory and renamed the original away: the copy loads both libraries from inside itself, and a small SystemVerilog SEC run from the copy proves an equivalent pair (exit 0) and gives a counterexample for a non-equivalent one (exit 3). So with this PR a moved or re-pointed install no longer loads another build's libraries. One leftover, outside #4717: the bundled Python's libtcl8.6.so and libtk8.6.so keep an absolute RPATH, /tools/deps/lib, from python-build-standalone; kepler-formal does not load them.

#4727 fixes the same RUNPATH with a one-line change to the CMake build this PR removes; I'll close it once this lands.

[oharboe]

Thanks for checking the #4717 case on a moved install, @saikatchatrg.

The libtcl8.6.so/libtk8.6.so RPATH comes with python-build-standalone's prebuilt Python, which the Bazel Python rules download. kepler-formal does not load Tcl/Tk through it, so I'll leave it out of this PR; if it ever matters, the fix belongs in python-build-standalone.

Agreed on closing #4727 once this lands: its RUNPATH fix is one line in a CMake build that this PR deletes.

Why this replaces the CMake build rather than patching it:

• kepler-formal is on its way into the Bazel Central Registry, kepler-formal@0.5.0-20261026-a64adfaf bazelbuild/bazel-central-registry#11201. Both kepler-formal maintainers have approved it and its presubmit is green; it is waiting on a BCR maintainer.
• The install target this PR runs, Bazel: //:install, modelled on OpenROAD's keplertech/kepler-formal#292, has merged in kepler-formal.
• OpenROAD's CMake build is deprecated and due for removal today, Nov. 1, 2026 (OpenROAD's README). ORFS already builds OpenROAD with bazelisk run //:install. Building kepler-formal the same way means ORFS no longer maintains a CMake build for it: no submodules, no per-platform packages, no RPATH flags.

CI-Public/pr-merge errors on every open PR and on master; it is not caused by this PR.

[saikatchatrg]

Thanks for the explanation and for taking this on. Building kepler-formal through its own //:install, as ORFS already builds OpenROAD, removes the whole class of problem #4717 hit rather than one flag of it.

[maliberty]

@nanocoh any concerns?

[maliberty]

292 is merged

[oharboe]

The git_override is gone: kepler-formal@0.5.0-20261026-a64adfaf comes from the BCR (bazelbuild/bazel-central-registry#11201 merged), and it has //:install. 65fab0f

[nanocoh]

@nanocoh any concerns?

Looks good as long as the regress is clean and we can occasionally use git_overide when bcr is not up to date.

[oharboe]

@nanocoh any concerns?

Looks good as long as the regress is clean and we can occasionally use git_overide when bcr is not up to date.

Yes, you still can. This can be convenient when making improvements that ORFS cares about and then using git_override() to pick them up until next release is available. You could also carry a patch in ORFS on top of an official release, which I sometimes prefer over git_override() because it is is naturally scrubbed out in a bazel bcr bump. git_override() should come with a comment as to why the release isn't being used. Which approach is better while waiting for a bazel bcr bump of a module all depends on the specifics of each circumstance; normally I'd only carry tiny patches and use git_override() if there are lots of updates.