From 88d10b081b55a269565332411be177f935b14c51 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Tue, 12 May 2026 01:17:52 +0200 Subject: [PATCH 1/4] global check Signed-off-by: Noam Cohen --- docs/user/FlowVariables.md | 4 +++- flow/scripts/final_report.tcl | 5 +++++ flow/scripts/synth_odb.tcl | 4 ++++ flow/scripts/variables.json | 6 ++++-- flow/scripts/variables.yaml | 7 +++++-- 5 files changed, 21 insertions(+), 5 deletions(-) diff --git a/docs/user/FlowVariables.md b/docs/user/FlowVariables.md index 80d3073bc5..b6c4f30d5e 100644 --- a/docs/user/FlowVariables.md +++ b/docs/user/FlowVariables.md @@ -171,7 +171,7 @@ configuration file. | LATCH_MAP_FILE| Optional mapping file supplied to Yosys to map latches| | | LAYER_PARASITICS_FILE| Path to per layer parasitics file. Defaults to $(PLATFORM_DIR)/setRC.tcl.| | | LEC_AUX_VERILOG_FILES| Additional Verilog files (e.g. blackbox stubs) to include in LEC equivalence checks. Appended to the generated Verilog netlist before running the formal equivalence check.| | -| LEC_CHECK| Perform a formal equivalence check between before and after netlists. If this fails, report an issue to OpenROAD.| 0| +| LEC_CHECK| Perform formal equivalence checks between before and after netlists. This checks CTS repair timing and the initial synthesis netlist against the final netlist. If this fails, report an issue to OpenROAD.| 0| | LIB_FILES| A Liberty file of the standard cell library with PVT characterization, input and output characteristics, timing and power definitions for each cell.| | | MACRO_BLOCKAGE_HALO| Distance beyond the edges of a macro that will also be covered by the blockage generated for that macro. Note that the default macro blockage halo comes from the largest of the specified MACRO_PLACE_HALO x or y values. This variable overrides that calculation.| | | MACRO_EXTENSION| Sets the number of GCells added to the blockages boundaries from macros.| | @@ -342,6 +342,7 @@ configuration file. - [DFF_LIB_FILE](#DFF_LIB_FILE) - [DFF_MAP_FILE](#DFF_MAP_FILE) - [LATCH_MAP_FILE](#LATCH_MAP_FILE) +- [LEC_CHECK](#LEC_CHECK) - [MIN_BUF_CELL_AND_PORTS](#MIN_BUF_CELL_AND_PORTS) - [POST_SYNTH_TCL](#POST_SYNTH_TCL) - [PRE_SYNTH_TCL](#PRE_SYNTH_TCL) @@ -588,6 +589,7 @@ configuration file. - [CDL_FILE](#CDL_FILE) - [GDS_ALLOW_EMPTY](#GDS_ALLOW_EMPTY) - [GND_NETS_VOLTAGES](#GND_NETS_VOLTAGES) +- [LEC_CHECK](#LEC_CHECK) - [MAX_ROUTING_LAYER](#MAX_ROUTING_LAYER) - [MIN_ROUTING_LAYER](#MIN_ROUTING_LAYER) - [POST_DENSITY_FILL_TCL](#POST_DENSITY_FILL_TCL) diff --git a/flow/scripts/final_report.tcl b/flow/scripts/final_report.tcl index d81acc986e..609c7fd844 100644 --- a/flow/scripts/final_report.tcl +++ b/flow/scripts/final_report.tcl @@ -1,5 +1,6 @@ utl::set_metrics_stage "finish__{}" source $::env(SCRIPTS_DIR)/load.tcl +source $::env(SCRIPTS_DIR)/lec_check.tcl erase_non_stage_variables final load_design 6_1_fill.odb 6_1_fill.sdc source_step_tcl PRE FINAL_REPORT @@ -19,6 +20,10 @@ write_def $::env(RESULTS_DIR)/6_final.def write_verilog $::env(RESULTS_DIR)/6_final.v \ -remove_cells [find_physical_only_masters] +if { $::env(LEC_CHECK) } { + run_lec_test 6_final 1_synth_lec.v 6_final.v +} + # Run extraction and STA if { [env_var_exists_and_non_empty RCX_RULES] diff --git a/flow/scripts/synth_odb.tcl b/flow/scripts/synth_odb.tcl index d6f53cda3e..73500540e7 100644 --- a/flow/scripts/synth_odb.tcl +++ b/flow/scripts/synth_odb.tcl @@ -31,3 +31,7 @@ orfs_write_db $::env(RESULTS_DIR)/1_synth.odb # which are read in here and a canonicalized version is written # out by OpenSTA that has no dependencies. orfs_write_sdc $::env(RESULTS_DIR)/1_synth.sdc +if { $::env(LEC_CHECK) } { + write_verilog $::env(RESULTS_DIR)/1_synth_lec.v \ + -remove_cells [find_physical_only_masters] +} diff --git a/flow/scripts/variables.json b/flow/scripts/variables.json index 0c8e56ad77..19024ecf19 100644 --- a/flow/scripts/variables.json +++ b/flow/scripts/variables.json @@ -475,9 +475,11 @@ }, "LEC_CHECK": { "default": 0, - "description": "Perform a formal equivalence check between before and after netlists. If this fails, report an issue to OpenROAD.\n", + "description": "Perform formal equivalence checks between before and after netlists. This checks CTS repair timing and the initial synthesis netlist against the final netlist. If this fails, report an issue to OpenROAD.\n", "stages": [ - "cts" + "synth", + "cts", + "final" ] }, "LIB_FILES": { diff --git a/flow/scripts/variables.yaml b/flow/scripts/variables.yaml index c8cbfb7898..a6d4e2852a 100644 --- a/flow/scripts/variables.yaml +++ b/flow/scripts/variables.yaml @@ -1548,11 +1548,14 @@ WRITE_ODB_AND_SDC_EACH_STAGE: default: 1 LEC_CHECK: description: > - Perform a formal equivalence check between before and after netlists. - If this fails, report an issue to OpenROAD. + Perform formal equivalence checks between before and after netlists. + This checks CTS repair timing and the initial synthesis netlist against + the final netlist. If this fails, report an issue to OpenROAD. default: 0 stages: + - synth - cts + - final LEC_AUX_VERILOG_FILES: description: > Additional Verilog files (e.g. blackbox stubs) to include in LEC From df042b88d22e1418f3932262bf2cfd7f8f9f2c5f Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Tue, 12 May 2026 13:09:27 +0200 Subject: [PATCH 2/4] sec check Signed-off-by: Noam Cohen --- docs/user/FlowVariables.md | 7 +++- flow/scripts/cts.tcl | 2 +- flow/scripts/final_report.tcl | 12 +++++-- .../{lec_check.tcl => formal_check.tcl} | 33 +++++++++++++++++++ flow/scripts/synth_odb.tcl | 6 ++-- flow/scripts/variables.json | 14 ++++++-- flow/scripts/variables.yaml | 16 +++++++-- tools/kepler-formal | 2 +- 8 files changed, 79 insertions(+), 13 deletions(-) rename flow/scripts/{lec_check.tcl => formal_check.tcl} (62%) diff --git a/docs/user/FlowVariables.md b/docs/user/FlowVariables.md index b6c4f30d5e..3428d169a2 100644 --- a/docs/user/FlowVariables.md +++ b/docs/user/FlowVariables.md @@ -170,7 +170,7 @@ configuration file. | KLAYOUT_TECH_FILE| A mapping from LEF/DEF to GDS using the KLayout tool.| | | LATCH_MAP_FILE| Optional mapping file supplied to Yosys to map latches| | | LAYER_PARASITICS_FILE| Path to per layer parasitics file. Defaults to $(PLATFORM_DIR)/setRC.tcl.| | -| LEC_AUX_VERILOG_FILES| Additional Verilog files (e.g. blackbox stubs) to include in LEC equivalence checks. Appended to the generated Verilog netlist before running the formal equivalence check.| | +| LEC_AUX_VERILOG_FILES| Additional Verilog files (e.g. blackbox stubs) to include in generated netlists for formal equivalence checks.| | | LEC_CHECK| Perform formal equivalence checks between before and after netlists. This checks CTS repair timing and the initial synthesis netlist against the final netlist. If this fails, report an issue to OpenROAD.| 0| | LIB_FILES| A Liberty file of the standard cell library with PVT characterization, input and output characteristics, timing and power definitions for each cell.| | | MACRO_BLOCKAGE_HALO| Distance beyond the edges of a macro that will also be covered by the blockage generated for that macro. Note that the default macro blockage halo comes from the largest of the specified MACRO_PLACE_HALO x or y values. This variable overrides that calculation.| | @@ -268,6 +268,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.| 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.| | @@ -342,12 +343,14 @@ configuration file. - [DFF_LIB_FILE](#DFF_LIB_FILE) - [DFF_MAP_FILE](#DFF_MAP_FILE) - [LATCH_MAP_FILE](#LATCH_MAP_FILE) +- [LEC_AUX_VERILOG_FILES](#LEC_AUX_VERILOG_FILES) - [LEC_CHECK](#LEC_CHECK) - [MIN_BUF_CELL_AND_PORTS](#MIN_BUF_CELL_AND_PORTS) - [POST_SYNTH_TCL](#POST_SYNTH_TCL) - [PRE_SYNTH_TCL](#PRE_SYNTH_TCL) - [SDC_FILE](#SDC_FILE) - [SDC_GUT](#SDC_GUT) +- [SEC_CHECK](#SEC_CHECK) - [SLANG_PLUGIN_PATH](#SLANG_PLUGIN_PATH) - [SYNTH_ARGS](#SYNTH_ARGS) - [SYNTH_BLACKBOXES](#SYNTH_BLACKBOXES) @@ -589,6 +592,7 @@ configuration file. - [CDL_FILE](#CDL_FILE) - [GDS_ALLOW_EMPTY](#GDS_ALLOW_EMPTY) - [GND_NETS_VOLTAGES](#GND_NETS_VOLTAGES) +- [LEC_AUX_VERILOG_FILES](#LEC_AUX_VERILOG_FILES) - [LEC_CHECK](#LEC_CHECK) - [MAX_ROUTING_LAYER](#MAX_ROUTING_LAYER) - [MIN_ROUTING_LAYER](#MIN_ROUTING_LAYER) @@ -599,6 +603,7 @@ configuration file. - [PWR_NETS_VOLTAGES](#PWR_NETS_VOLTAGES) - [REPORT_CLOCK_SKEW](#REPORT_CLOCK_SKEW) - [ROUTING_LAYER_ADJUSTMENT](#ROUTING_LAYER_ADJUSTMENT) +- [SEC_CHECK](#SEC_CHECK) - [SKIP_DETAILED_ROUTE](#SKIP_DETAILED_ROUTE) - [SKIP_REPORT_METRICS](#SKIP_REPORT_METRICS) diff --git a/flow/scripts/cts.tcl b/flow/scripts/cts.tcl index f079bb5f10..0503a6f410 100644 --- a/flow/scripts/cts.tcl +++ b/flow/scripts/cts.tcl @@ -1,6 +1,6 @@ utl::set_metrics_stage "cts__{}" source $::env(SCRIPTS_DIR)/load.tcl -source $::env(SCRIPTS_DIR)/lec_check.tcl +source $::env(SCRIPTS_DIR)/formal_check.tcl erase_non_stage_variables cts load_design 3_place.odb 3_place.sdc source_step_tcl PRE CTS diff --git a/flow/scripts/final_report.tcl b/flow/scripts/final_report.tcl index 609c7fd844..c70492b72a 100644 --- a/flow/scripts/final_report.tcl +++ b/flow/scripts/final_report.tcl @@ -1,6 +1,6 @@ utl::set_metrics_stage "finish__{}" source $::env(SCRIPTS_DIR)/load.tcl -source $::env(SCRIPTS_DIR)/lec_check.tcl +source $::env(SCRIPTS_DIR)/formal_check.tcl erase_non_stage_variables final load_design 6_1_fill.odb 6_1_fill.sdc source_step_tcl PRE FINAL_REPORT @@ -20,8 +20,16 @@ write_def $::env(RESULTS_DIR)/6_final.def write_verilog $::env(RESULTS_DIR)/6_final.v \ -remove_cells [find_physical_only_masters] +if { $::env(LEC_CHECK) || $::env(SEC_CHECK) } { + write_lec_verilog 6_final_lec.v +} + if { $::env(LEC_CHECK) } { - run_lec_test 6_final 1_synth_lec.v 6_final.v + run_lec_test 6_final 1_synth_lec.v 6_final_lec.v +} + +if { $::env(SEC_CHECK) } { + run_sec_test 6_final 1_synth_lec.v 6_final_lec.v } # Run extraction and STA diff --git a/flow/scripts/lec_check.tcl b/flow/scripts/formal_check.tcl similarity index 62% rename from flow/scripts/lec_check.tcl rename to flow/scripts/formal_check.tcl index 8e1d35919a..d2434ad433 100644 --- a/flow/scripts/lec_check.tcl +++ b/flow/scripts/formal_check.tcl @@ -38,6 +38,22 @@ proc write_lec_script { step file1 file2 } { close $outfile } +proc write_sec_script { step file1 file2 } { + set outfile [open "$::env(OBJECTS_DIR)/${step}_sec_test.yml" w] + puts $outfile "format: verilog" + puts $outfile "verification: sec" + puts $outfile "sec_engine: pdr" + puts $outfile "input_paths:" + puts $outfile " - $::env(RESULTS_DIR)/${file1}" + puts $outfile " - $::env(RESULTS_DIR)/${file2}" + puts $outfile "liberty_files:" + foreach libFile $::env(LIB_FILES) { + puts $outfile " - $libFile" + } + puts $outfile "log_file: $::env(LOG_DIR)/${step}_sec_check.log" + close $outfile +} + proc run_lec_test { step file1 file2 } { write_lec_script $step $file1 $file2 # tclint-disable-next-line command-args @@ -54,3 +70,20 @@ proc run_lec_test { step file1 file2 } { puts "Repair timing output passed lec test" } } + +proc run_sec_test { step file1 file2 } { + write_sec_script $step $file1 $file2 + # tclint-disable-next-line command-args + eval exec $::env(KEPLER_FORMAL_EXE) --config $::env(OBJECTS_DIR)/${step}_sec_test.yml + try { + set count [exec grep -c "SEC found a counterexample" $::env(LOG_DIR)/${step}_sec_check.log] + } trap CHILDSTATUS {results options} { + # This block executes if grep returns a non-zero exit code + set count 0 + } + if { $count > 0 } { + error "Global output failed sec test" + } else { + puts "Global output passed sec test" + } +} diff --git a/flow/scripts/synth_odb.tcl b/flow/scripts/synth_odb.tcl index 73500540e7..c233f79b36 100644 --- a/flow/scripts/synth_odb.tcl +++ b/flow/scripts/synth_odb.tcl @@ -1,5 +1,6 @@ utl::set_metrics_stage "floorplan__{}" source $::env(SCRIPTS_DIR)/load.tcl +source $::env(SCRIPTS_DIR)/formal_check.tcl erase_non_stage_variables synth load_design 1_2_yosys.v 1_2_yosys.sdc source_step_tcl PRE SYNTH @@ -31,7 +32,6 @@ orfs_write_db $::env(RESULTS_DIR)/1_synth.odb # which are read in here and a canonicalized version is written # out by OpenSTA that has no dependencies. orfs_write_sdc $::env(RESULTS_DIR)/1_synth.sdc -if { $::env(LEC_CHECK) } { - write_verilog $::env(RESULTS_DIR)/1_synth_lec.v \ - -remove_cells [find_physical_only_masters] +if { $::env(LEC_CHECK) || $::env(SEC_CHECK) } { + write_lec_verilog 1_synth_lec.v } diff --git a/flow/scripts/variables.json b/flow/scripts/variables.json index 19024ecf19..4971b3d77c 100644 --- a/flow/scripts/variables.json +++ b/flow/scripts/variables.json @@ -468,9 +468,11 @@ "type": "string" }, "LEC_AUX_VERILOG_FILES": { - "description": "Additional Verilog files (e.g. blackbox stubs) to include in LEC equivalence checks. Appended to the generated Verilog netlist before running the formal equivalence check.\n", + "description": "Additional Verilog files (e.g. blackbox stubs) to include in generated netlists for formal equivalence checks.\n", "stages": [ - "cts" + "synth", + "cts", + "final" ] }, "LEC_CHECK": { @@ -1076,6 +1078,14 @@ "SEAL_GDS": { "description": "Seal macro to place around the design.\n" }, + "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.\n", + "default": 0, + "stages": [ + "synth", + "final" + ] + }, "SETUP_MOVE_SEQUENCE": { "description": "Passed as -sequence to repair_timing. This should be a string of move keywords separated by commas.\n", "stages": [ diff --git a/flow/scripts/variables.yaml b/flow/scripts/variables.yaml index a6d4e2852a..6f490065ec 100644 --- a/flow/scripts/variables.yaml +++ b/flow/scripts/variables.yaml @@ -1556,13 +1556,23 @@ LEC_CHECK: - synth - cts - final +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. + default: 0 + stages: + - synth + - final LEC_AUX_VERILOG_FILES: description: > - Additional Verilog files (e.g. blackbox stubs) to include in LEC - equivalence checks. Appended to the generated Verilog netlist before - running the formal equivalence check. + Additional Verilog files (e.g. blackbox stubs) to include in generated + netlists for formal equivalence checks. stages: + - synth - cts + - final REMOVE_CELLS_FOR_LEC: description: > String patterns directly passed to write_verilog -remove_cells <> for diff --git a/tools/kepler-formal b/tools/kepler-formal index b596df4121..ce68ff0515 160000 --- a/tools/kepler-formal +++ b/tools/kepler-formal @@ -1 +1 @@ -Subproject commit b596df4121f2b13ac1b6fd03920a3b2053ae80f5 +Subproject commit ce68ff0515b9a2008715bd77a228bb16c0d8581c From 5aacc6425425dfa46b9e9304189baf5355cc7cd6 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Tue, 12 May 2026 13:13:21 +0200 Subject: [PATCH 3/4] linting Signed-off-by: Noam Cohen --- flow/scripts/variables.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/flow/scripts/variables.json b/flow/scripts/variables.json index 4971b3d77c..02d0c835e1 100644 --- a/flow/scripts/variables.json +++ b/flow/scripts/variables.json @@ -1079,8 +1079,8 @@ "description": "Seal macro to place around the design.\n" }, "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.\n", "default": 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", "stages": [ "synth", "final" From ee50120bb2df0847a8c965b690c8ed2b36ffc33f Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Tue, 12 May 2026 13:59:49 +0200 Subject: [PATCH 4/4] sec check Signed-off-by: Noam Cohen --- flow/settings.mk | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/flow/settings.mk b/flow/settings.mk index 413a40682c..28a18b17e6 100644 --- a/flow/settings.mk +++ b/flow/settings.mk @@ -1,5 +1,6 @@ -# Enable LEC (Logical Equivalence Check) 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 LEC transactionally at project completion, -# not in every CI run where it wastes CI time. +# 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 ?= $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)