The-OpenROAD-Project · nanocoh · May 11, 2026 · May 12, 2026 · May 12, 2026 · May 12, 2026
diff --git a/docs/user/FlowVariables.md b/docs/user/FlowVariables.md
@@ -171,8 +171,8 @@ configuration file.
 | <a name="KLAYOUT_TECH_FILE"></a>KLAYOUT_TECH_FILE| A mapping from LEF/DEF to GDS using the KLayout tool.| |
 | <a name="LATCH_MAP_FILE"></a>LATCH_MAP_FILE| Optional mapping file supplied to Yosys to map latches| |
 | <a name="LAYER_PARASITICS_FILE"></a>LAYER_PARASITICS_FILE| Path to per layer parasitics file. Defaults to $(PLATFORM_DIR)/setRC.tcl.| |
-| <a name="LEC_AUX_VERILOG_FILES"></a>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.| |
-| <a name="LEC_CHECK"></a>LEC_CHECK| Perform a formal equivalence check between before and after netlists. If this fails, report an issue to OpenROAD.| 0|
+| <a name="LEC_AUX_VERILOG_FILES"></a>LEC_AUX_VERILOG_FILES| Additional Verilog files (e.g. blackbox stubs) to include in generated netlists for formal equivalence checks.| |
+| <a name="LEC_CHECK"></a>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|
 | <a name="LIB_FILES"></a>LIB_FILES| A Liberty file of the standard cell library with PVT characterization, input and output characteristics, timing and power definitions for each cell.| |
 | <a name="LIB_MODEL"></a>LIB_MODEL| Selects between NLDM and CCS timing models for the ASAP7 platform. Valid values: NLDM (default), CCS. Used in flow/platforms/asap7/config.mk to pick the LIB_DIR subdirectory and accumulate the corresponding $(CORNER)_$(LIB_MODEL)_LIB_FILES list, and in flow/scripts/load.tcl to gate CCS-specific Tcl branches.| NLDM|
 | <a name="MACRO_BLOCKAGE_HALO"></a>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.| |
@@ -269,6 +269,7 @@ configuration file.
 | <a name="SDC_FILE"></a>SDC_FILE| The path to design constraint (SDC) file.| |
 | <a name="SDC_GUT"></a>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.| |
 | <a name="SEAL_GDS"></a>SEAL_GDS| Seal macro to place around the design.| |
+| <a name="SEC_CHECK"></a>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|
 | <a name="SETUP_MOVE_SEQUENCE"></a>SETUP_MOVE_SEQUENCE| Passed as -sequence to repair_timing. This should be a string of move keywords separated by commas.| |
 | <a name="SETUP_SLACK_MARGIN"></a>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|
 | <a name="SET_RC_TCL"></a>SET_RC_TCL| Metal & Via RC definition file path.| |
@@ -344,11 +345,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)
 - [SKIP_REPORT_METRICS](#SKIP_REPORT_METRICS)
 - [SLANG_PLUGIN_PATH](#SLANG_PLUGIN_PATH)
 - [SYNTH_ARGS](#SYNTH_ARGS)
@@ -591,6 +595,8 @@ 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)
 - [POST_DENSITY_FILL_TCL](#POST_DENSITY_FILL_TCL)
@@ -600,6 +606,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/Makefile b/flow/Makefile
@@ -412,6 +412,14 @@ endif
 
 $(RESULTS_DIR)/1_synth.sdc: $(RESULTS_DIR)/1_synth.odb
 
+FORMAL_CHECK_DEPS =
+ifneq ($(filter 1,$(LEC_CHECK) $(SEC_CHECK)),)
+FORMAL_CHECK_DEPS += $(RESULTS_DIR)/1_synth_lec.v
+endif
+
+$(RESULTS_DIR)/1_synth_lec.v: $(RESULTS_DIR)/1_synth.odb $(RESULTS_DIR)/1_synth.sdc
+	$(UNSET_AND_MAKE) do-1_synth
+
 $(eval $(call do-step,2_1_floorplan,$(RESULTS_DIR)/1_synth.odb $(RESULTS_DIR)/1_synth.sdc $(TECH_LEF) $(SC_LEF) $(ADDITIONAL_LEFS) $(FOOTPRINT) $(SIG_MAP_FILE) $(FOOTPRINT_TCL) $(LIB_FILES) $(IO_CONSTRAINTS),floorplan))
 
 $(eval $(call do-copy,2_floorplan,2_1_floorplan.sdc,,.sdc))
@@ -616,7 +624,7 @@ $(eval $(call do-copy,6_1_fill,5_route.sdc,,.sdc))
 
 $(eval $(call do-copy,6_final,5_route.sdc,,.sdc))
 
-$(eval $(call do-step,6_report,$(RESULTS_DIR)/6_1_fill.odb $(RESULTS_DIR)/6_1_fill.sdc,final_report,.log,$(LOG_DIR)))
+$(eval $(call do-step,6_report,$(RESULTS_DIR)/6_1_fill.odb $(RESULTS_DIR)/6_1_fill.sdc $(FORMAL_CHECK_DEPS),final_report,.log,$(LOG_DIR)))
 
 $(RESULTS_DIR)/6_final.def: $(LOG_DIR)/6_report.log
 

diff --git 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
@@ -1,5 +1,6 @@
 utl::set_metrics_stage "finish__{}"
 source $::env(SCRIPTS_DIR)/load.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
@@ -19,6 +20,18 @@ 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_lec.v
+}
+
+if { $::env(SEC_CHECK) } {
+  run_sec_test 6_final 1_synth_lec.v 6_final_lec.v
+}
+
 # Run extraction and STA
 if {
   [env_var_exists_and_non_empty RCX_RULES]

diff --git a/flow/scripts/lec_check.tcl → flow/scripts/formal_check.tcl b/flow/scripts/lec_check.tcl → flow/scripts/formal_check.tcl
@@ -46,6 +46,29 @@ 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 formal_check_label { step } {
+  if { [string equal $step 4_rsz] } {
+    return "Repair timing output"
+  }
+  return "Global output"
+}
+
 proc run_lec_test { step file1 file2 } {
   write_lec_script $step $file1 $file2
   # tclint-disable-next-line command-args
@@ -56,9 +79,27 @@ proc run_lec_test { step file1 file2 } {
     # This block executes if grep returns a non-zero exit code
     set count 0
   }
+  set label [formal_check_label $step]
+  if { $count > 0 } {
+    error "$label failed lec test"
+  } else {
+    puts "$label 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 "Repair timing output failed lec test"
+    error "Global output failed sec test"
   } else {
-    puts "Repair timing output passed lec test"
+    puts "Global output passed sec test"
   }
 }
diff --git a/flow/scripts/synth_odb.tcl b/flow/scripts/synth_odb.tcl
@@ -1,5 +1,6 @@
 utl::set_metrics_stage "synth__{}"
 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
@@ -34,3 +35,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) || $::env(SEC_CHECK) } {
+  write_lec_verilog 1_synth_lec.v
+}
diff --git a/flow/scripts/synth_syn.tcl b/flow/scripts/synth_syn.tcl
@@ -1,5 +1,6 @@
 utl::set_metrics_stage "synth__{}"
 source $::env(SCRIPTS_DIR)/load.tcl
+source $::env(SCRIPTS_DIR)/formal_check.tcl
 erase_non_stage_variables synth
 
 source_env_var_if_exists PLATFORM_TCL
@@ -74,3 +75,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) || $::env(SEC_CHECK) } {
+  write_lec_verilog 1_synth_lec.v
+}
diff --git a/flow/scripts/variables.json b/flow/scripts/variables.json
diff --git a/flow/scripts/variables.yaml b/flow/scripts/variables.yaml
@@ -1570,18 +1570,31 @@ 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
+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/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)
diff --git a/tools/kepler-formal b/tools/kepler-formal