global check

Signed-off-by: Noam Cohen <noam.chn1@gmail.com>

Author: Noam Cohen

docs/user/FlowVariables.md

@@ -171,7 +171,7 @@ configuration file.
 | <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_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="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.| |
 | <a name="MACRO_EXTENSION"></a>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)

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]

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]
+}

flow/scripts/variables.json

@@ -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