From 4035de1b1797382bedadf2d031b4076e0ad06f4a Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Fri, 3 Jul 2026 13:59:46 +0200 Subject: [PATCH 01/23] sec global check Signed-off-by: Noam Cohen --- flow/settings.mk | 4 ++-- tools/kepler-formal | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/flow/settings.mk b/flow/settings.mk index 4ed65a99a6..28a18b17e6 100644 --- a/flow/settings.mk +++ b/flow/settings.mk @@ -1,6 +1,6 @@ -# Enable LEC only if kepler-formal is installed. +# Enable formal checks only if kepler-formal is installed. # kepler-formal is primarily an OpenROAD/ORFS developer tool, not an end-user # tool. End-users would typically run these checks transactionally at project # completion, not in every CI run where it wastes CI time. export LEC_CHECK ?= $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0) -export SEC_CHECK ?= 0 +export SEC_CHECK ?= $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0) diff --git a/tools/kepler-formal b/tools/kepler-formal index 0bc2a79c38..8f48712546 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit 0bc2a79c3897a6093aa44bcececcdca75c329d63 +Subproject commit 8f4871254639fa88450a3f917a3ca555562271bb From 16df2be311ba4ee0c83c036f983981d5fcf33be6 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Fri, 3 Jul 2026 14:37:30 +0200 Subject: [PATCH 02/23] kf update Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index 8f48712546..ca4c9cd2fa 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit 8f4871254639fa88450a3f917a3ca555562271bb +Subproject commit ca4c9cd2fa8ff732d2704cd6d77809fb24f70069 From 7908753c75c7b6bbd5efab977d8479a6792f66fc Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Fri, 3 Jul 2026 19:49:07 +0200 Subject: [PATCH 03/23] kf update Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index ca4c9cd2fa..59a41cb77a 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit ca4c9cd2fa8ff732d2704cd6d77809fb24f70069 +Subproject commit 59a41cb77acb8a2c2766a77520cf2a123f664f6d From 8dfdc20a818395def0de9049f1edf83d120d6abe Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Fri, 9 Oct 2026 20:30:33 +0200 Subject: [PATCH 04/23] bump kf Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index f025fa2f25..91e00fda45 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit f025fa2f254efd6c702cef004e55995c1f13a11a +Subproject commit 91e00fda45648918b51c3cc7bcf967b3541fbbb8 From 88e722384afdfdee8e6597b887efc4b45c0a9f93 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 15 Oct 2026 13:02:51 +0200 Subject: [PATCH 05/23] opt fixes Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index 91e00fda45..d9f24b0093 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit 91e00fda45648918b51c3cc7bcf967b3541fbbb8 +Subproject commit d9f24b00934a1bac8293a835e0a2e6586f9c7798 From 094f07cbff997e15704b7e226639278468a83fb0 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 15 Oct 2026 15:44:34 +0200 Subject: [PATCH 06/23] BLOCKS as boundary Signed-off-by: Noam Cohen --- docs/user/FlowVariables.md | 2 +- flow/scripts/formal_check.tcl | 35 +++++++++++++++++++++++++++++++++++ flow/scripts/variables.json | 2 +- flow/scripts/variables.yaml | 6 ++++-- tools/OpenROAD | 2 +- tools/yosys | 2 +- 6 files changed, 43 insertions(+), 6 deletions(-) diff --git a/docs/user/FlowVariables.md b/docs/user/FlowVariables.md index d1d62544e9..a25082eeba 100644 --- a/docs/user/FlowVariables.md +++ b/docs/user/FlowVariables.md @@ -277,7 +277,7 @@ configuration file. | SDC_FILE| The path to design constraint (SDC) file.| | | SDC_GUT| Load design and remove all internal logic before doing synthesis. This is useful when creating a mock .lef abstract that has a smaller area than the amount of logic would allow. bazel-orfs uses this to mock SRAMs, for instance.| | | SEAL_GDS| Seal macro to place around the design.| | -| SEC_CHECK| Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. If this fails, report an issue to OpenROAD.| $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)| +| SEC_CHECK| Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. Hardened sub-blocks listed in BLOCKS are checked as black boxes (proof boundaries), since their abstracts carry no logic. If this fails, report an issue to OpenROAD.| $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)| | SETUP_MOVE_SEQUENCE| Passed as -sequence to repair_timing. This should be a string of move keywords separated by commas.| | | SETUP_SLACK_MARGIN| Specifies a time margin for the slack when fixing setup violations. This option allows you to overfix or underfix(negative value, terminate retiming before 0 or positive slack). See HOLD_SLACK_MARGIN for more details.| 0| | SET_RC_TCL| Metal & Via RC definition file path.| | diff --git a/flow/scripts/formal_check.tcl b/flow/scripts/formal_check.tcl index 930b59b00d..d2f3a00053 100644 --- a/flow/scripts/formal_check.tcl +++ b/flow/scripts/formal_check.tcl @@ -67,6 +67,30 @@ proc write_lec_script { step file1 file2 } { close $outfile } +# Hardened sub-blocks (BLOCKS) enter the parent netlist as timing-only +# abstracts with no logic model, so a formal check would treat every output +# cone that reaches one as opaque. Return the instance paths of all block +# instances in the loaded design; both netlists come from the same run, so the +# same path exists in both and each instance can be paired with itself. +proc formal_block_instance_paths { } { + set paths {} + if { ![env_var_exists_and_non_empty BLOCKS] } { + return $paths + } + set block [ord::get_db_block] + foreach inst [$block getInsts] { + set master [[$inst getMaster] getName] + if { [lsearch -exact $::env(BLOCKS) $master] >= 0 } { + lappend paths [$inst getName] + } + } + return [lsort $paths] +} + +proc formal_yaml_quote { text } { + return "\"[string map {\\ \\\\ \" \\\"} $text]\"" +} + proc write_sec_script { step file1 file2 } { set outfile [open "$::env(OBJECTS_DIR)/${step}_sec_test.yml" w] puts $outfile "format: verilog" @@ -79,6 +103,17 @@ proc write_sec_script { step file1 file2 } { foreach libFile $::env(LIB_FILES) { puts $outfile " - $libFile" } + # Each block instance becomes a proof boundary: its input pins are compared + # across the two netlists and its output pins are shared free inputs, so the + # block is checked as a black box instead of hiding the cones behind it. + set boundaries [formal_block_instance_paths] + if { [llength $boundaries] > 0 } { + puts $outfile "set_as_boundary:" + foreach path $boundaries { + set quoted [formal_yaml_quote $path] + puts $outfile " - \[$quoted, $quoted\]" + } + } puts $outfile "log_file: $::env(LOG_DIR)/${step}_sec_check.log" close $outfile } diff --git a/flow/scripts/variables.json b/flow/scripts/variables.json index d311173a1a..3bf72b880b 100644 --- a/flow/scripts/variables.json +++ b/flow/scripts/variables.json @@ -1134,7 +1134,7 @@ }, "SEC_CHECK": { "default": "$(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)", - "description": "Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. If this fails, report an issue to OpenROAD.\n", + "description": "Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. Hardened sub-blocks listed in BLOCKS are checked as black boxes (proof boundaries), since their abstracts carry no logic. If this fails, report an issue to OpenROAD.\n", "stages": [ "synth", "final" diff --git a/flow/scripts/variables.yaml b/flow/scripts/variables.yaml index c2e11a639c..c565e84eb7 100644 --- a/flow/scripts/variables.yaml +++ b/flow/scripts/variables.yaml @@ -1637,8 +1637,10 @@ LEC_CHECK: SEC_CHECK: description: > Perform a sequential equivalence check between the initial synthesis - netlist and final netlist with the Kepler Formal PDR engine. If this - fails, report an issue to OpenROAD. + netlist and final netlist with the Kepler Formal PDR engine. Hardened + sub-blocks listed in BLOCKS are checked as black boxes (proof boundaries), + since their abstracts carry no logic. If this fails, report an issue to + OpenROAD. default: $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0) stages: - synth diff --git a/tools/OpenROAD b/tools/OpenROAD index 943a4d2c92..4c26918f5a 160000 --- a/tools/OpenROAD +++ b/tools/OpenROAD @@ -1 +1 @@ -Subproject commit 943a4d2c9284cce991a916b67937157d890fe133 +Subproject commit 4c26918f5a77392910939b51b9c2490b7e7e3201 diff --git a/tools/yosys b/tools/yosys index a5af9d690a..8449dd4700 160000 --- a/tools/yosys +++ b/tools/yosys @@ -1 +1 @@ -Subproject commit a5af9d690a43744bf6b2cc3dea2717c16b54621c +Subproject commit 8449dd4700821ea021b241a6addaaf8ccd171dfc From d24de5f36d7e7a2d1b11d8b64135c3d72e108ebe Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 15 Oct 2026 16:53:25 +0200 Subject: [PATCH 07/23] fix deps Signed-off-by: Noam Cohen --- tools/OpenROAD | 2 +- tools/yosys | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/OpenROAD b/tools/OpenROAD index 4c26918f5a..943a4d2c92 160000 --- a/tools/OpenROAD +++ b/tools/OpenROAD @@ -1 +1 @@ -Subproject commit 4c26918f5a77392910939b51b9c2490b7e7e3201 +Subproject commit 943a4d2c9284cce991a916b67937157d890fe133 diff --git a/tools/yosys b/tools/yosys index 8449dd4700..a5af9d690a 160000 --- a/tools/yosys +++ b/tools/yosys @@ -1 +1 @@ -Subproject commit 8449dd4700821ea021b241a6addaaf8ccd171dfc +Subproject commit a5af9d690a43744bf6b2cc3dea2717c16b54621c From 7b1bc61a1f13b245b93c00f14cc42a0437c97f42 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 15 Oct 2026 19:02:57 +0200 Subject: [PATCH 08/23] fix resolve instance Signed-off-by: Noam Cohen --- flow/scripts/formal_check.tcl | 52 ++++++++++++++++++++++++++++++++++- tools/kepler-formal | 2 +- 2 files changed, 52 insertions(+), 2 deletions(-) diff --git a/flow/scripts/formal_check.tcl b/flow/scripts/formal_check.tcl index d2f3a00053..8417c31db6 100644 --- a/flow/scripts/formal_check.tcl +++ b/flow/scripts/formal_check.tcl @@ -72,6 +72,56 @@ proc write_lec_script { step file1 file2 } { # cone that reaches one as opaque. Return the instance paths of all block # instances in the loaded design; both netlists come from the same run, so the # same path exists in both and each instance can be paired with itself. +# Escapes every unescaped `/` in an instance name as `\/`, the OpenSTA SDC +# convention kepler-formal reads: `/` separates hierarchy levels and `\/` is a +# literal slash inside one name. Existing escapes are kept as they are. +proc formal_escape_slashes { name } { + set escaped "" + set length [string length $name] + for { set i 0 } { $i < $length } { incr i } { + set ch [string index $name $i] + if { $ch eq "\\" } { + incr i + append escaped "\\" [string index $name $i] + } elseif { $ch eq "/" } { + append escaped "\\/" + } else { + append escaped $ch + } + } + return $escaped +} + +# Mirrors dbNetwork::stripParentPrefix: in a hierarchical database write_verilog +# names a leaf by what follows the last unescaped `/` of its database name. +proc formal_strip_parent_prefix { name } { + set pos [string last "/" $name] + while { $pos >= 0 } { + if { $pos == 0 || [string index $name [expr { $pos - 1 }]] ne "\\" } { + return [string range $name [expr { $pos + 1 }] end] + } + set pos [string last "/" $name [expr { $pos - 2 }]] + } + return $name +} + +# Boundary path of a block instance exactly as write_verilog names it: in a flat +# database the whole instance name is one leaf (`\u0/r0 ` in Verilog, so the +# path is `u0\/r0`); in a hierarchical database the leaf keeps its module +# instance path and loses the parent prefix. Paths are never reinterpreted. +proc formal_boundary_path { inst } { + set name [$inst getName] + set prefix "" + if { [[ord::get_db] hasHierarchy] } { + set mod_inst [[$inst getModule] getModInst] + if { $mod_inst != "NULL" } { + set prefix "[$mod_inst getHierarchicalName]/" + } + set name [formal_strip_parent_prefix $name] + } + return "$prefix[formal_escape_slashes $name]" +} + proc formal_block_instance_paths { } { set paths {} if { ![env_var_exists_and_non_empty BLOCKS] } { @@ -81,7 +131,7 @@ proc formal_block_instance_paths { } { foreach inst [$block getInsts] { set master [[$inst getMaster] getName] if { [lsearch -exact $::env(BLOCKS) $master] >= 0 } { - lappend paths [$inst getName] + lappend paths [formal_boundary_path $inst] } } return [lsort $paths] diff --git a/tools/kepler-formal b/tools/kepler-formal index d9f24b0093..8eb34e22ee 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit d9f24b00934a1bac8293a835e0a2e6586f9c7798 +Subproject commit 8eb34e22eeee5955a046c55942cabcdffc17252c From 92e8ec0f6896571f28b6a10043cfba829497d1fc Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 15 Oct 2026 20:44:51 +0200 Subject: [PATCH 09/23] ingore unconnected inputs at boundary Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index 8eb34e22ee..d9c7584961 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit 8eb34e22eeee5955a046c55942cabcdffc17252c +Subproject commit d9c75849612ba7ed64e44b6330dbad9dd7b11b7a From e2261e6fbf5f37caae1eaecb7c8bb27bd36e04bb Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Tue, 20 Oct 2026 22:31:00 +0200 Subject: [PATCH 10/23] binary relation learning round Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index d9c7584961..08d53403d1 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit d9c75849612ba7ed64e44b6330dbad9dd7b11b7a +Subproject commit 08d53403d1d699538b92928a8fab1faeda389ed8 From 55c59f59f42c40fcffb24ba60b10df91fa0d01ff Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Tue, 20 Oct 2026 23:53:25 +0200 Subject: [PATCH 11/23] fix ihp cells filtering Signed-off-by: Noam Cohen --- flow/platforms/ihp-sg13g2/config.mk | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flow/platforms/ihp-sg13g2/config.mk b/flow/platforms/ihp-sg13g2/config.mk index 1cbb86c560..8293bbbb18 100644 --- a/flow/platforms/ihp-sg13g2/config.mk +++ b/flow/platforms/ihp-sg13g2/config.mk @@ -174,7 +174,7 @@ export KLAYOUT_DRC_FILE ?= $(PLATFORM_DIR)/drc/sg13g2_minimal.lydrc export CDL_FILE ?= $(PLATFORM_DIR)/cdl/sg13g2_stdcell.cdl #export KLAYOUT_LVS_FILE = $(PLATFORM_DIR)/lvs/$(PLATFORM).lylvs -export REMOVE_CELLS_FOR_LEC ?= "bondpad_70* sg13g2*" +export REMOVE_CELLS_FOR_LEC ?= "bondpad_70*" # --------------------------------------------------------- # Final From 4410239cfd5ffe4c5d07b4d0419dcfa0b2e0991c Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 21 Oct 2026 11:04:44 +0200 Subject: [PATCH 12/23] add modeling for word level in kf Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index 08d53403d1..d2ca853bcb 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit 08d53403d1d699538b92928a8fab1faeda389ed8 +Subproject commit d2ca853bcba97f61d5cab908e6671974ee954671 From aaa9502ce36ab99c15a9b81e023f5d96ac2c3857 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 21 Oct 2026 16:44:06 +0200 Subject: [PATCH 13/23] rom support Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index d2ca853bcb..b178b3e0a4 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit d2ca853bcba97f61d5cab908e6671974ee954671 +Subproject commit b178b3e0a46ee96c264860d5cd46c55b80819e6e From 6f5b2c68a3ed954a4f6d4ff911e2cac7e76464f4 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 22 Oct 2026 02:08:11 +0200 Subject: [PATCH 14/23] partition relation study Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index b178b3e0a4..2c6d2fe062 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit b178b3e0a46ee96c264860d5cd46c55b80819e6e +Subproject commit 2c6d2fe0625afa999d04e4b3a4ab04e4fa53fa13 From 60aac58987242e623d6193f0d35d65e0105c5f1f Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 22 Oct 2026 16:02:50 +0200 Subject: [PATCH 15/23] further latch support Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index 2c6d2fe062..32a58dfca2 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit 2c6d2fe0625afa999d04e4b3a4ab04e4fa53fa13 +Subproject commit 32a58dfca2d669b6068e595cf6faf6d5b62a31f3 From 22247a9b9b30e705f6b74c8b0d4dac7d11840503 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Fri, 23 Oct 2026 11:45:42 +0200 Subject: [PATCH 16/23] relation study speedup Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index 32a58dfca2..a868a12f7d 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit 32a58dfca2d669b6068e595cf6faf6d5b62a31f3 +Subproject commit a868a12f7d99d1731caea151fa3a68a0472cf82f From 1dd520ab64bb7d9117ebc4837f4b1f1ca430c5c3 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Fri, 23 Oct 2026 19:55:24 +0200 Subject: [PATCH 17/23] update Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index a868a12f7d..a669e56945 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit a868a12f7d99d1731caea151fa3a68a0472cf82f +Subproject commit a669e569452f5cff9865aad4a4fcb42e16124dd6 From d585487235f80dfa69ac411af1328fafdce58883 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Tue, 27 Oct 2026 01:03:48 +0100 Subject: [PATCH 18/23] update kf Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index a669e56945..dce6dc467c 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit a669e569452f5cff9865aad4a4fcb42e16124dd6 +Subproject commit dce6dc467cd2f5f19a8dd65d24105d97ec212413 From 6b423b9dc089e885efd9da9f8c53e9bb393cbb6a Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Tue, 27 Oct 2026 23:01:28 +0100 Subject: [PATCH 19/23] update kf Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index dce6dc467c..cff1975356 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit dce6dc467cd2f5f19a8dd65d24105d97ec212413 +Subproject commit cff19753569cfdffa2fab86872c75b3dfe927f72 From 66ecbcaf28cc160a65fa087fb3e5469dabb57de3 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 28 Oct 2026 11:46:02 +0100 Subject: [PATCH 20/23] disable sec step when needed Signed-off-by: Noam Cohen --- flow/designs/asap7/chi_async_bridge/config.mk | 4 ++++ flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk | 4 ++++ flow/designs/nangate45/mempool_group/config.mk | 4 ++++ flow/designs/sky130hd/chameleon/config.mk | 4 ++++ flow/designs/sky130hd/microwatt/config.mk | 4 +++- tools/kepler-formal | 2 +- 6 files changed, 20 insertions(+), 2 deletions(-) diff --git a/flow/designs/asap7/chi_async_bridge/config.mk b/flow/designs/asap7/chi_async_bridge/config.mk index 1f9e2cda64..934cbadcc6 100644 --- a/flow/designs/asap7/chi_async_bridge/config.mk +++ b/flow/designs/asap7/chi_async_bridge/config.mk @@ -37,3 +37,7 @@ export VERILOG_TOP_PARAMS = REQ_W 32 RSP_W 16 DAT_W 64 SNP_W 24 DEPTH 4 else ifeq ($(FLOW_VARIANT),medium) export VERILOG_TOP_PARAMS = DEPTH 4 endif + +# Temporary disabling: the asynchronous clock-domain crossings are outside +# the sequential check. +export SEC_CHECK = 0 diff --git a/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk b/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk index 53f618cb07..24fbdc6b83 100644 --- a/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk +++ b/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk @@ -55,3 +55,7 @@ export PDN_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)/pdn.tcl export BLOCKS = I2cDeviceCtrl + +# Temporary disabling: the bidirectional IO pads are outside the sequential +# check. +export SEC_CHECK = 0 diff --git a/flow/designs/nangate45/mempool_group/config.mk b/flow/designs/nangate45/mempool_group/config.mk index 8cca19fda0..8be9e2bcf9 100644 --- a/flow/designs/nangate45/mempool_group/config.mk +++ b/flow/designs/nangate45/mempool_group/config.mk @@ -78,3 +78,7 @@ export CORE_AREA = 10 12 1090 1090 export RTLMP_MIN_CHANNEL_SIZE = 20 20 export SYNTH_HDL_FRONTEND = slang + +# Temporary disabling: the hierarchical netlist leaves memory write-mask pins +# undriven, which the sequential check cannot verify. +export SEC_CHECK = 0 diff --git a/flow/designs/sky130hd/chameleon/config.mk b/flow/designs/sky130hd/chameleon/config.mk index 6bbe14781d..2d68f462c5 100644 --- a/flow/designs/sky130hd/chameleon/config.mk +++ b/flow/designs/sky130hd/chameleon/config.mk @@ -50,3 +50,7 @@ export FP_PDN_RAIL_OFFSET = 0 export TNS_END_PERCENT = 100 export RTLMP_MIN_CHANNEL_SIZE = 70 70 + +# Temporary disabling: the hard macros carry no logic in their Liberty, which +# leaves no output for the sequential check to verify. +export SEC_CHECK = 0 diff --git a/flow/designs/sky130hd/microwatt/config.mk b/flow/designs/sky130hd/microwatt/config.mk index f2da973056..d008df4820 100644 --- a/flow/designs/sky130hd/microwatt/config.mk +++ b/flow/designs/sky130hd/microwatt/config.mk @@ -51,5 +51,7 @@ endif export SWAP_ARITH_OPERATORS = 1 export OPENROAD_HIERARCHICAL = 1 -# Temporary disabling +# Temporary disabling: the hierarchical netlist is rejected by the +# equivalence checker (duplicate wire declaration). export LEC_CHECK = 0 +export SEC_CHECK = 0 diff --git a/tools/kepler-formal b/tools/kepler-formal index cff1975356..b242c10a76 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit cff19753569cfdffa2fab86872c75b3dfe927f72 +Subproject commit b242c10a765270a770fe93aa3f66fb3ac6855d4c From 1c297d560dc305e7d11a1cce0f58671ee660f786 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Wed, 28 Oct 2026 13:51:24 +0100 Subject: [PATCH 21/23] use set_boundary for BLOCKS Signed-off-by: Noam Cohen --- docs/user/FlowVariables.md | 2 +- flow/scripts/formal_check.tcl | 18 ++++++++++++------ flow/scripts/variables.json | 2 +- flow/scripts/variables.yaml | 9 +++++---- 4 files changed, 19 insertions(+), 12 deletions(-) diff --git a/docs/user/FlowVariables.md b/docs/user/FlowVariables.md index 07481b00d8..8d10cf1436 100644 --- a/docs/user/FlowVariables.md +++ b/docs/user/FlowVariables.md @@ -275,7 +275,7 @@ configuration file. | SC_LEF| Path to technology standard cell LEF file.| | | SDC_FILE| The path to design constraint (SDC) file.| | | SEAL_GDS| Seal macro to place around the design.| | -| SEC_CHECK| Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. Hardened sub-blocks listed in BLOCKS are checked as black boxes (proof boundaries), since their abstracts carry no logic. If this fails, report an issue to OpenROAD.| $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)| +| SEC_CHECK| Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. Hard macros, the sub-blocks listed in BLOCKS and every BLOCK-class cell such as SRAM macros, are checked as black boxes (proof boundaries): they are the same cells in both netlists and their abstracts carry no logic. If this fails, report an issue to OpenROAD.| $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)| | SETUP_MOVE_SEQUENCE| Passed as -sequence to repair_timing. This should be a string of move keywords separated by commas.| | | SETUP_SLACK_MARGIN| Specifies a time margin for the slack when fixing setup violations. This option allows you to overfix or underfix(negative value, terminate retiming before 0 or positive slack). See HOLD_SLACK_MARGIN for more details.| 0| | SKIP_ANTENNA_REPAIR| Skips antenna repair entirely.| 0| diff --git a/flow/scripts/formal_check.tcl b/flow/scripts/formal_check.tcl index 079f7adc56..e5d079c882 100644 --- a/flow/scripts/formal_check.tcl +++ b/flow/scripts/formal_check.tcl @@ -122,15 +122,21 @@ proc formal_boundary_path { inst } { return "$prefix[formal_escape_slashes $name]" } +# Hard macros are proof boundaries: the instances of the masters listed in +# BLOCKS, and every instance of a BLOCK-class master (SRAM macros, hardened +# sub-blocks). A macro is the same cell in both netlists, so only its +# connections need checking; expanding its contents into state would only make +# the proof slower. proc formal_block_instance_paths { } { set paths {} - if { ![env_var_exists_and_non_empty BLOCKS] } { - return $paths + set blocks {} + if { [env_var_exists_and_non_empty BLOCKS] } { + set blocks $::env(BLOCKS) } set block [ord::get_db_block] foreach inst [$block getInsts] { - set master [[$inst getMaster] getName] - if { [lsearch -exact $::env(BLOCKS) $master] >= 0 } { + set master [$inst getMaster] + if { [$master isBlock] || [lsearch -exact $blocks [$master getName]] >= 0 } { lappend paths [formal_boundary_path $inst] } } @@ -153,9 +159,9 @@ proc write_sec_script { step file1 file2 } { foreach libFile $::env(LIB_FILES) { puts $outfile " - $libFile" } - # Each block instance becomes a proof boundary: its input pins are compared + # Each macro instance becomes a proof boundary: its input pins are compared # across the two netlists and its output pins are shared free inputs, so the - # block is checked as a black box instead of hiding the cones behind it. + # macro is checked as a black box instead of hiding the cones behind it. set boundaries [formal_block_instance_paths] if { [llength $boundaries] > 0 } { puts $outfile "set_as_boundary:" diff --git a/flow/scripts/variables.json b/flow/scripts/variables.json index 0bddc137fd..c7beade0f6 100644 --- a/flow/scripts/variables.json +++ b/flow/scripts/variables.json @@ -1139,7 +1139,7 @@ }, "SEC_CHECK": { "default": "$(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)", - "description": "Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. Hardened sub-blocks listed in BLOCKS are checked as black boxes (proof boundaries), since their abstracts carry no logic. If this fails, report an issue to OpenROAD.\n", + "description": "Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. Hard macros, the sub-blocks listed in BLOCKS and every BLOCK-class cell such as SRAM macros, are checked as black boxes (proof boundaries): they are the same cells in both netlists and their abstracts carry no logic. If this fails, report an issue to OpenROAD.\n", "stages": [ "synth", "final" diff --git a/flow/scripts/variables.yaml b/flow/scripts/variables.yaml index 057c447d53..27d9b47ff3 100644 --- a/flow/scripts/variables.yaml +++ b/flow/scripts/variables.yaml @@ -1677,10 +1677,11 @@ LEC_CHECK: SEC_CHECK: description: > Perform a sequential equivalence check between the initial synthesis - netlist and final netlist with the Kepler Formal PDR engine. Hardened - sub-blocks listed in BLOCKS are checked as black boxes (proof boundaries), - since their abstracts carry no logic. If this fails, report an issue to - OpenROAD. + netlist and final netlist with the Kepler Formal PDR engine. Hard macros, + the sub-blocks listed in BLOCKS and every BLOCK-class cell such as SRAM + macros, are checked as black boxes (proof boundaries): they are the same + cells in both netlists and their abstracts carry no logic. If this fails, + report an issue to OpenROAD. default: $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0) stages: - synth From 0c51cd60e9ee6b3d6c01e2a4ac48da7a99dcc9b2 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 29 Oct 2026 19:05:51 +0100 Subject: [PATCH 22/23] fix clock extraction Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index b242c10a76..1c6edfc09a 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit b242c10a765270a770fe93aa3f66fb3ac6855d4c +Subproject commit 1c6edfc09a7782f7d92aa2ad77b8c4df57686a74 From 0ca7f2f4e3bec2c38de5b613ce49afb93068128e Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Fri, 30 Oct 2026 17:27:54 +0100 Subject: [PATCH 23/23] fix clock extraction Signed-off-by: Noam Cohen --- tools/kepler-formal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/kepler-formal b/tools/kepler-formal index 1c6edfc09a..611158ec92 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit 1c6edfc09a7782f7d92aa2ad77b8c4df57686a74 +Subproject commit 611158ec92e52e690a7f09fbdd2231ce7b7cc564