[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

A number of PRs have already been merged into kepler-formal and the Bazel Central Registry so that kepler-formal installs this way. Its registry entry, bazelbuild/bazel-central-registry#11201, is approved and should merge within a week or two. One more kepler-formal PR adds the install target, keplertech/kepler-formal#292, and I expect it to merge before this PR; until it does, MODULE.bazel overrides kepler-formal with that PR's commit.

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> 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.

Builds on #4727 and is a draft until it merges.

🤖 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.