Enable Kepler-formal LEC for multiple designs by openroad-ci · Pull Request #3985 · The-OpenROAD-Project/OpenROAD-flow-scripts

openroad-ci · 2026-03-12T08:55:03Z

Bump kepler-formal (inout port issue fix) keplertech/kepler-formal@e8675f3
Enable kepler-formal for multiple designs - Previously, KF for those designs were disabled due to KF & OR issues

Signed-off-by: Jaehyun Kim <[email protected]>

- Previously, KF for those designs were disabled due to KF & OR issues Signed-off-by: Jaehyun Kim <[email protected]>

Signed-off-by: Jaehyun Kim <[email protected]>

Add LEC_AUX_VERILOG_FILES support to lec_check.tcl so that auxiliary Verilog files (e.g., blackbox module stubs) are concatenated into LEC netlists before Kepler Formal runs. For sky130hd/chameleon, provide clean blackbox stubs for DFFRAM_4K, DMC_32x16HC, ibex_wrapper, and apb_sys_0 so KF can resolve these macro modules during CTS LEC. Signed-off-by: Jaehyun Kim <[email protected]>

…ate/OpenROAD-flow-scripts into secure-enable-kf-lec-check Signed-off-by: Jaehyun Kim <[email protected]>

Update OpenROAD to 9b0caf1a52 which includes the unified makeNewNetName fix, resolving wire collision for hierarchical designs (e.g., microwatt CTS LEC "wire collision for net net"). Signed-off-by: Jaehyun Kim <[email protected]>

KF crashes with assertion failure in SNLLogicCloud.cpp:349: "Iso have no drivers and more than one reader, not supported" Both base and verific variants affected. Signed-off-by: Jaehyun Kim <[email protected]>

Widen globalroute and finish setup TNS thresholds from -697 to -750 to accommodate timing change from OR 9b0caf1a52 (makeNewNetName). Actual: -727.5 (4.4% regression). Signed-off-by: Jaehyun Kim <[email protected]>

Widen area and TNS thresholds for gcd, ibex, ethmac, jpeg to accommodate changes from OR 9b0caf1a52 (makeNewNetName). Signed-off-by: Jaehyun Kim <[email protected]>

cva6/verific: widen stdcell count (173997→183000), CTS WS (-0.14→-0.15) hercules_idecode/verific: widen CTS/GRT/finish TNS thresholds for timing regression from OR 9b0caf1a52. Signed-off-by: Jaehyun Kim <[email protected]>

Empty commit to retrigger sync and Jenkins PR-merge build. Signed-off-by: Jaehyun Kim <[email protected]>

…ate/OpenROAD-flow-scripts into secure-enable-kf-lec-check Signed-off-by: Jaehyun Kim <[email protected]>

Signed-off-by: Jaehyun Kim <[email protected]>

The bumped kepler-formal still has bugs for these designs: - nangate45/mempool_group: assertion crash in SNLLogicCloud.cpp:349 "Iso have no drivers and more than one reader, not supported" - rapidus2hp/cva6: netlist loading failure bus net "icache_areq_o" cannot be found in ALU module Signed-off-by: Jaehyun Kim <[email protected]>

designs/rapidus2hp/cva6/rules-base.json updates: | Metric | Old | New | Type | | ------ | --- | --- | ---- | | globalroute__timing__setup__tns | -452.0 | -463.0 | Failing | | finish__timing__setup__tns | -452.0 | -463.0 | Failing | designs/rapidus2hp/cva6/rules-verific.json updates: | Metric | Old | New | Type | | ------ | --- | --- | ---- | | placeopt__design__instance__count__stdcell | 201058 | 200149 | Tighten | | cts__timing__setup__ws | -0.136 | -0.167 | Failing | | finish__timing__setup__tns | -550.0 | -738.0 | Failing | Signed-off-by: Jaehyun Kim <[email protected]>

designs/nangate45/swerv_wrapper/rules-base.json updates: | Metric | Old | New | Type | | ------ | --- | --- | ---- | | cts__timing__setup__ws | -0.197 | -0.466 | Failing | | cts__timing__setup__tns | -84.6 | -290.0 | Failing | | globalroute__timing__setup__tns | -86.3 | -211.0 | Failing | | detailedroute__route__wirelength | 5546498 | 4367567 | Tighten | | finish__timing__setup__tns | -88.2 | -198.0 | Failing | Signed-off-by: Jaehyun Kim <[email protected]>

Signed-off-by: Jaehyun Kim <[email protected]>

…ate/OpenROAD-flow-scripts into secure-enable-kf-lec-check Signed-off-by: Jaehyun Kim <[email protected]>

Signed-off-by: Jaehyun Kim <[email protected]>

jhkim-pii · 2026-03-21T11:17:34Z

Key changes in this PR

Remove LEC_CHECK=0 for all designs
[sky130hd/chameleon] Add a new .v to specify black-box modules to run KF successfully.

There are no verilog module for some modules (e.g., DFFRAM_4K, ...), which causes an error in KF.
So I add a new flow/designs/sky130hd/chameleon/lec_blackbox_stubs.v‎ file for KF.

[rapidus2hp/cva6] cva6 RTL has uninitialized signals, which causes KF value. Initialize those signals to 0
Bump OR (CTS bug fix) to resolve the undriven input port issue in [nangate45/mempool_group], which was found by KF.
Bump Kepler-formal (multiple bug fixes).

jhkim-pii · 2026-03-21T11:18:57Z

flow/designs/sky130hd/chameleon/config.mk

 export CORE_MARGIN            = 2

 export chameleon_DIR = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)
+export LEC_AUX_VERILOG_FILES = $(chameleon_DIR)/lec_blackbox_stubs.v


Add a new .v to specify black-box modules to run KF successfully.

There are no verilog module (has .lef only) for some modules (e.g., DFFRAM_4K, ...), which causes an error in KF.

So I add a new flow/designs/sky130hd/chameleon/lec_blackbox_stubs.v‎ file for KF.

jhkim-pii · 2026-03-21T11:19:52Z

flow/designs/src/cva6/core/cache_subsystem/hpdcache/rtl/src/hwpf_stride/hwpf_stride.sv

           hpdcache_req_o.pma.uncacheable = 1'b0,
-           hpdcache_req_o.pma.io          = 1'b0;
+           hpdcache_req_o.pma.io          = 1'b0,
+           hpdcache_req_o.pma.wr_policy_hint = HPDCACHE_WR_POLICY_AUTO;


cva6 RTL has uninitialized signals, which causes KF value. Initialized those signals properly.

jhkim-pii · 2026-03-21T11:20:20Z

tools/OpenROAD

Undriven input port was found by KF. Handled by CTS bug fixing in OR (bump OR).

jhkim-pii · 2026-03-21T11:20:40Z

tools/kepler-formal

Bump Kepler-formal (multiple bug fixes).

jhkim-pii · 2026-03-21T11:29:03Z

@vvbandeira The secure CI of this PR suffers from the following build fail.

http://secure-ci:8080/job/SB/job/secure-enable-kf-lec-check/25/stages/

[2026-03-21T09:19:59.139Z] [ 94%] ABC: `` Compiling: /src/aig/ivy/ivyShow.c
[2026-03-21T09:19:59.139Z] [ 94%] ABC: `` Compiling: /src/aig/ivy/ivyTable.c
[2026-03-21T09:19:59.139Z] /usr/bin/ld: /platforms/verific/Dec25/util/util-linux.a(Strings.o): in function `Verific::Strings::atoul(char const*, unsigned int*)':
[2026-03-21T09:19:59.139Z] Strings.cpp:(.text+0x623): undefined reference to `__isoc23_strtoull'
[2026-03-21T09:19:59.139Z] /usr/bin/ld: Strings.cpp:(.text+0x67b): undefined reference to `__isoc23_strtoul'
[2026-03-21T09:19:59.139Z] /usr/bin/ld: /platforms/verific/Dec25/util/util-linux.a(Strings.o): in function `Verific::Strings::atoi(char const*, unsigned int*)':
[2026-03-21T09:19:59.139Z] Strings.cpp:(.text+0xefa): undefined reference to `__isoc23_strtoull'
[2026-03-21T09:19:59.139Z] /usr/bin/ld: Strings.cpp:(.text+0xf84): undefined reference to `__isoc23_strtoul'
[2026-03-21T09:19:59.139Z] /usr/bin/ld: /platforms/verific/Dec25/util/util-linux.a(SaveRestore.o): in function `Verific::SaveRestore::GetDesignName(char const*, unsigned int)':
[2026-03-21T09:19:59.139Z] SaveRestore.cpp:(.text+0xd5a): undefined reference to `__isoc23_sscanf'
[2026-03-21T09:19:59.139Z] [ 94%] ABC: `` Compiling: /src/aig/ivy/ivyUtil.c
[2026-03-21T09:19:59.139Z] [ 94%] ABC: `` Compiling: /src/aig/hop/hopBalance.c

Is it related to /platforms/verific/Dec25 for Secure-Branch? Secure-Run-GCP uses /platforms/verific/Feb26 (newer).

Secure-Branch build log: [2026-03-21T09:06:56.093Z] + nice ./build_openroad.sh --local --no_init --clean-force --with-verific /platforms/verific/Dec25 -> Build fail
Secure-Run-GCP build log: [2026-03-21T00:59:33.954Z] + nice ./build_openroad.sh --local --no_init --with-verific /platforms/verific/Feb26 -> Build OK

jhkim-pii added 5 commits March 12, 2026 10:12

Bump kepler-formal (inout port issue fix)

c91679f

Signed-off-by: Jaehyun Kim <[email protected]>

Enable kepler-formal for multiple designs

eaa6576

- Previously, KF for those designs were disabled due to KF & OR issues Signed-off-by: Jaehyun Kim <[email protected]>

Disable kepler-formal LEC for rapidus2hp cva6

6b81b89

Signed-off-by: Jaehyun Kim <[email protected]>

cva6: drive optional outputs explicitly

837beb5

Signed-off-by: Jaehyun Kim <[email protected]>

rapidus2hp/cva6: restore default KF LEC

ed998cb

Signed-off-by: Jaehyun Kim <[email protected]>

openroad-ci assigned jhkim-pii Mar 12, 2026

jhkim-pii added 3 commits March 17, 2026 11:02

Merge branch 'master' of https://github.com/The-OpenROAD-Project-priv…

4c5d746

…ate/OpenROAD-flow-scripts into secure-enable-kf-lec-check Signed-off-by: Jaehyun Kim <[email protected]>

Bump OR: fix net name collision in write_verilog

f6508cc

Update OpenROAD to 9b0caf1a52 which includes the unified makeNewNetName fix, resolving wire collision for hierarchical designs (e.g., microwatt CTS LEC "wire collision for net net"). Signed-off-by: Jaehyun Kim <[email protected]>

openroad-ci force-pushed the secure-enable-kf-lec-check branch from 69ef0a2 to f6508cc Compare March 17, 2026 08:49

jhkim-pii added 10 commits March 17, 2026 19:33

Disable kepler-formal LEC for rapidus2hp cva6

d84eec3

KF crashes with assertion failure in SNLLogicCloud.cpp:349: "Iso have no drivers and more than one reader, not supported" Both base and verific variants affected. Signed-off-by: Jaehyun Kim <[email protected]>

Update rapidus2hp/cva6 verific TNS metrics for OR bump

d40042b

Widen globalroute and finish setup TNS thresholds from -697 to -750 to accommodate timing change from OR 9b0caf1a52 (makeNewNetName). Actual: -727.5 (4.4% regression). Signed-off-by: Jaehyun Kim <[email protected]>

Update rapidus2hp metrics for OR bump

d2e2dc7

Widen area and TNS thresholds for gcd, ibex, ethmac, jpeg to accommodate changes from OR 9b0caf1a52 (makeNewNetName). Signed-off-by: Jaehyun Kim <[email protected]>

Update rapidus2hp cva6/hercules_idecode metrics for OR bump

15e16d8

cva6/verific: widen stdcell count (173997→183000), CTS WS (-0.14→-0.15) hercules_idecode/verific: widen CTS/GRT/finish TNS thresholds for timing regression from OR 9b0caf1a52. Signed-off-by: Jaehyun Kim <[email protected]>

Trigger CI rebuild

4c65f97

Empty commit to retrigger sync and Jenkins PR-merge build. Signed-off-by: Jaehyun Kim <[email protected]>

Merge branch 'master' of https://github.com/The-OpenROAD-Project-priv…

89da805

…ate/OpenROAD-flow-scripts into secure-enable-kf-lec-check Signed-off-by: Jaehyun Kim <[email protected]>

Enable KF LEC for nangate45/mempool_group and rapidus2hp/cva6

b61b1a8

Signed-off-by: Jaehyun Kim <[email protected]>

jhkim-pii mentioned this pull request Mar 19, 2026

CTS: clock_tree_synthesis leaves clock gating cell clock pins unconnected The-OpenROAD-Project/OpenROAD#9816

Open

jhkim-pii added 4 commits March 21, 2026 17:53

Bump OR (Fix cloned ICG location collision in CTS)

f9f7b5e

Signed-off-by: Jaehyun Kim <[email protected]>

Rebump OR

4cac046

Signed-off-by: Jaehyun Kim <[email protected]>

Merge branch 'master' of https://github.com/The-OpenROAD-Project-priv…

ee85cc0

…ate/OpenROAD-flow-scripts into secure-enable-kf-lec-check Signed-off-by: Jaehyun Kim <[email protected]>

Enable KF (LEC_CHECK=1) for nangate45/mempool_group and rapidus2hp/cva6

59c0410

Signed-off-by: Jaehyun Kim <[email protected]>

jhkim-pii reviewed Mar 21, 2026

View reviewed changes

tools/OpenROAD

Copy link

Contributor

jhkim-pii Mar 21, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Undriven input port was found by KF. Handled by CTS bug fixing in OR (bump OR).

jhkim-pii reviewed Mar 21, 2026

View reviewed changes

tools/kepler-formal

Copy link

Contributor

jhkim-pii Mar 21, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Bump Kepler-formal (multiple bug fixes).

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Enable Kepler-formal LEC for multiple designs#3985

Enable Kepler-formal LEC for multiple designs#3985
openroad-ci wants to merge 22 commits intoThe-OpenROAD-Project:masterfrom
The-OpenROAD-Project-staging:secure-enable-kf-lec-check

openroad-ci commented Mar 12, 2026

Uh oh!

jhkim-pii commented Mar 21, 2026 •

edited

Loading

Uh oh!

jhkim-pii Mar 21, 2026

Uh oh!

jhkim-pii Mar 21, 2026

Uh oh!

jhkim-pii Mar 21, 2026

Uh oh!

jhkim-pii Mar 21, 2026

Uh oh!

jhkim-pii commented Mar 21, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

openroad-ci commented Mar 12, 2026

Uh oh!

jhkim-pii commented Mar 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Key changes in this PR

Uh oh!

jhkim-pii Mar 21, 2026

Choose a reason for hiding this comment

Uh oh!

jhkim-pii Mar 21, 2026

Choose a reason for hiding this comment

Uh oh!

jhkim-pii Mar 21, 2026

Choose a reason for hiding this comment

Uh oh!

jhkim-pii Mar 21, 2026

Choose a reason for hiding this comment

Uh oh!

jhkim-pii commented Mar 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jhkim-pii commented Mar 21, 2026 •

edited

Loading

jhkim-pii commented Mar 21, 2026 •

edited

Loading