global LEC check

docs/user/FlowVariables.md

@@ -173,8 +173,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.| $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,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.| |
@@ -271,6 +271,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)
 - [SYNTH_ARGS](#SYNTH_ARGS)
 - [SYNTH_BLACKBOXES](#SYNTH_BLACKBOXES)
@@ -589,6 +593,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)
@@ -598,6 +604,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)
 

flow/Makefile

@@ -369,7 +369,7 @@ $(eval $(call OPEN_GUI_SHORTCUT,$(1),$(1).odb))
 endif
 
 .PHONY: do-$(1)
-do-$(1): $(OBJECTS_DIR)/copyright.txt
+do-$(1): $(DO_STEP_DEPS_$(1)) $(OBJECTS_DIR)/copyright.txt
 	$(SCRIPTS_DIR)/flow.sh $(1) $(3)
 endef
 
@@ -412,6 +412,26 @@ 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
+
+.PHONY: check-kepler-formal
+check-kepler-formal:
+	@if [ ! -x "$(KEPLER_FORMAL_EXE)" ]; then \
+		echo "Error: Kepler Formal not found. Install Kepler Formal or set KEPLER_FORMAL_EXE."; \
+		echo "Hint: Kepler Formal is needed when LEC_CHECK=1 or SEC_CHECK=1."; \
+		exit 1; \
+	fi
+
+$(RESULTS_DIR)/1_synth_lec.v: $(RESULTS_DIR)/1_synth.odb $(RESULTS_DIR)/1_synth.sdc
+	$(UNSET_AND_MAKE) do-1_synth
+
+ifneq ($(filter 1,$(LEC_CHECK) $(SEC_CHECK)),)
+$(RESULTS_DIR)/1_synth_lec.v: | check-kepler-formal
+endif
+
 $(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))
@@ -510,8 +530,16 @@ cts: $(RESULTS_DIR)/4_cts.odb \
 
 # Run TritonCTS
 # ------------------------------------------------------------------------------
+ifeq ($(LEC_CHECK),1)
+DO_STEP_DEPS_4_1_cts += check-kepler-formal
+endif
+
 $(eval $(call do-step,4_1_cts,$(RESULTS_DIR)/3_place.odb $(RESULTS_DIR)/3_place.sdc,cts))
 
+ifeq ($(LEC_CHECK),1)
+$(RESULTS_DIR)/4_1_cts.odb: | check-kepler-formal
+endif
+
 $(RESULTS_DIR)/4_cts.sdc: $(RESULTS_DIR)/4_cts.odb
 
 $(eval $(call do-copy,4_cts,4_1_cts.odb))
@@ -616,7 +644,15 @@ $(eval $(call do-step,6_1_fill,$(RESULTS_DIR)/5_route.odb $(RESULTS_DIR)/5_route
 
 $(eval $(call do-copy,6_1_fill,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)))
+ifneq ($(filter 1,$(LEC_CHECK) $(SEC_CHECK)),)
+DO_STEP_DEPS_6_report += check-kepler-formal
+endif
+
+$(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)))
+
+ifneq ($(filter 1,$(LEC_CHECK) $(SEC_CHECK)),)
+$(LOG_DIR)/6_report.log: | check-kepler-formal
+endif
 
 # final_report writes 6_final.sdc alongside 6_final.odb (constraints are
 # unchanged during finishing), mirroring how synth writes 1_synth.sdc.

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

flow/scripts/final_outputs.tcl

@@ -1,11 +1,24 @@
 # Delete routing obstructions for final DEF
+source $::env(SCRIPTS_DIR)/formal_check.tcl
 source $::env(SCRIPTS_DIR)/deleteRoutingObstructions.tcl
 deleteRoutingObstructions
 
 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]

flow/scripts/lec_check.tcl → flow/scripts/formal_check.tcl

@@ -1,9 +1,18 @@
+proc check_kepler_formal { } {
+  if {
+    ![info exists ::env(KEPLER_FORMAL_EXE)]
+    || ![file executable $::env(KEPLER_FORMAL_EXE)]
+  } {
+    error "Kepler Formal not found. Install Kepler Formal or set KEPLER_FORMAL_EXE."
+  }
+}
+
 proc lec_check_enabled { } {
-  return [expr {
-    [env_var_equals LEC_CHECK 1]
-    && [info exists ::env(KEPLER_FORMAL_EXE)]
-    && [file executable $::env(KEPLER_FORMAL_EXE)]
-  }]
+  if { ![env_var_equals LEC_CHECK 1] } {
+    return 0
+  }
+  check_kepler_formal
+  return 1
 }
 
 proc write_lec_verilog { filename } {
@@ -46,7 +55,31 @@ 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 } {
+  check_kepler_formal
   write_lec_script $step $file1 $file2
   # tclint-disable-next-line command-args
   eval exec $::env(KEPLER_FORMAL_EXE) --config $::env(OBJECTS_DIR)/${step}_lec_test.yml
@@ -56,9 +89,28 @@ 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 } {
+  check_kepler_formal
+  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"
   }
 }

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
@@ -35,3 +36,6 @@ orfs_write_db $::env(RESULTS_DIR)/1_synth.odb
 # out by OpenSTA that has no dependencies. Sole writer of
 # 1_synth.sdc.
 orfs_write_sdc $::env(RESULTS_DIR)/1_synth.sdc
+if { $::env(LEC_CHECK) || $::env(SEC_CHECK) } {
+  write_lec_verilog 1_synth_lec.v
+}

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
@@ -75,3 +76,6 @@ orfs_write_db $::env(RESULTS_DIR)/1_synth.odb
 # out by OpenSTA that has no dependencies. Sole writer of
 # 1_synth.sdc.
 orfs_write_sdc $::env(RESULTS_DIR)/1_synth.sdc
+if { $::env(LEC_CHECK) || $::env(SEC_CHECK) } {
+  write_lec_verilog 1_synth_lec.v
+}

flow/scripts/variables.yaml

@@ -1566,18 +1566,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.
-  default: 0
+    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: $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,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