Merge pull request #3880 from keplertech/signoff-single-commit

maliberty · web-flow · commit 01bc23cdff2e · 2026-02-17T17:59:06.000Z
enable lec check
diff --git a/docs/user/FlowVariables.md b/docs/user/FlowVariables.md
@@ -161,6 +161,7 @@ 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_CHECK"></a>LEC_CHECK| Perform a formal equivalence check between before and after netlists.| 1|
 | <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.| |
@@ -196,6 +197,7 @@ configuration file.
 | <a name="RECOVER_POWER"></a>RECOVER_POWER| Specifies how many percent of paths with positive slacks can be slowed for power savings [0-100].| 0|
 | <a name="REMOVE_ABC_BUFFERS"></a>REMOVE_ABC_BUFFERS (deprecated)| Remove abc buffers from the netlist. If timing repair in floorplanning is taking too long, use a SETUP/HOLD_SLACK_MARGIN to terminate timing repair early instead of using REMOVE_ABC_BUFFERS or set SKIP_LAST_GASP=1.| 0|
 | <a name="REMOVE_CELLS_FOR_EQY"></a>REMOVE_CELLS_FOR_EQY| String patterns directly passed to write_verilog -remove_cells <> for equivalence checks.| |
+| <a name="REMOVE_CELLS_FOR_LEC"></a>REMOVE_CELLS_FOR_LEC| String patterns directly passed to write_verilog -remove_cells <> for lec checks.| |
 | <a name="REPAIR_PDN_VIA_LAYER"></a>REPAIR_PDN_VIA_LAYER| Remove power grid vias which generate DRC violations after detailed routing.| |
 | <a name="REPORT_CLOCK_SKEW"></a>REPORT_CLOCK_SKEW| Report clock skew as part of reporting metrics, starting at CTS, before which there is no clock skew. This metric can be quite time-consuming, so it can be useful to disable.| 1|
 | <a name="ROUTING_LAYER_ADJUSTMENT"></a>ROUTING_LAYER_ADJUSTMENT| Adjusts routing layer capacities to manage congestion and improve detailed routing. High values ease detailed routing but risk excessive detours and long global routing times, while low values reduce global routing failure but can complicate detailed routing. The global routing running time normally reduces dramatically (entirely design specific, but going from hours to minutes has been observed) when the value is low (such as 0.10). Sometimes, global routing will succeed with lower values and fail with higher values. Exploring results with different values can help shed light on the problem. Start with a too low value, such as 0.10, and bisect to value that works by doing multiple global routing runs. As a last resort, `make global_route_issue` and using the tools/OpenROAD/etc/deltaDebug.py can be useful to debug global routing errors. If there is something specific that is impossible to route, such as a clock line over a macro, global routing will terminate with DRC errors routes that could have been routed were it not for the specific impossible routes. deltaDebug.py should weed out the possible routes and leave a minimal failing case that pinpoints the problem.| 0.5|
@@ -421,6 +423,7 @@ configuration file.
 - [DETAILED_METRICS](#DETAILED_METRICS)
 - [EQUIVALENCE_CHECK](#EQUIVALENCE_CHECK)
 - [HOLD_SLACK_MARGIN](#HOLD_SLACK_MARGIN)
+- [LEC_CHECK](#LEC_CHECK)
 - [MATCH_CELL_FOOTPRINT](#MATCH_CELL_FOOTPRINT)
 - [MAX_REPAIR_TIMING_ITER](#MAX_REPAIR_TIMING_ITER)
 - [POST_CTS_TCL](#POST_CTS_TCL)
@@ -539,6 +542,7 @@ configuration file.
 - [PROCESS](#PROCESS)
 - [RCX_RULES](#RCX_RULES)
 - [RECOVER_POWER](#RECOVER_POWER)
+- [REMOVE_CELLS_FOR_LEC](#REMOVE_CELLS_FOR_LEC)
 - [REPAIR_PDN_VIA_LAYER](#REPAIR_PDN_VIA_LAYER)
 - [RUN_LOG_NAME_STEM](#RUN_LOG_NAME_STEM)
 - [RUN_SCRIPT](#RUN_SCRIPT)
diff --git a/flow/designs/asap7/aes-mbff/config.mk b/flow/designs/asap7/aes-mbff/config.mk
@@ -16,3 +16,4 @@ export TNS_END_PERCENT          = 100
 
 export CLUSTER_FLOPS            = 1
 export ENABLE_DPO               = 0
+
diff --git a/flow/designs/asap7/aes/config.mk b/flow/designs/asap7/aes/config.mk
@@ -30,4 +30,3 @@ else ifeq ($(FLOW_VARIANT),combine)
 	 $(WORK_HOME)/results/$(PLATFORM)/$(DESIGN_NICKNAME)/blackbox/1_synth.v
 endif
 
-export LEC_CHECK = 1
diff --git a/flow/designs/asap7/aes_lvt/config.mk b/flow/designs/asap7/aes_lvt/config.mk
@@ -17,3 +17,5 @@ export TNS_END_PERCENT        = 100
 export ASAP7_USE_VT           = LVT
 
 export RECOVER_POWER          = 100
+
+
diff --git a/flow/designs/asap7/cva6/config.mk b/flow/designs/asap7/cva6/config.mk
@@ -108,3 +108,4 @@ export CTS_LIB_NAME = asap7sc7p5t_INVBUF_SLVT_FF_nldm_211120
 
 # Remove rvfi_probes_o interface
 export SYNTH_CANONICALIZE_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NAME)/canonicalize.tcl
+
diff --git a/flow/designs/asap7/ethmac/config.mk b/flow/designs/asap7/ethmac/config.mk
@@ -10,3 +10,4 @@ export CORE_UTILIZATION       = 70
 export CORE_ASPECT_RATIO      = 1
 export CORE_MARGIN            = 2
 export PLACE_DENSITY          = 0.75
+
diff --git a/flow/designs/asap7/ethmac_lvt/config.mk b/flow/designs/asap7/ethmac_lvt/config.mk
@@ -15,3 +15,4 @@ export PLACE_DENSITY          = 0.60
 export ASAP7_USE_VT           = LVT
 
 export RECOVER_POWER          = 1
+
diff --git a/flow/designs/asap7/gcd/config.mk b/flow/designs/asap7/gcd/config.mk
@@ -14,3 +14,4 @@ export PLACE_DENSITY          = 0.35
 # a smoketest for this option, there are a
 # few last gasp iterations
 export SKIP_LAST_GASP ?= 1
+
diff --git a/flow/designs/asap7/ibex/config.mk b/flow/designs/asap7/ibex/config.mk
@@ -30,3 +30,6 @@ export TNS_END_PERCENT        = 100
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+export LEC_CHECK = 0
+
diff --git a/flow/designs/asap7/jpeg/config.mk b/flow/designs/asap7/jpeg/config.mk
@@ -16,3 +16,7 @@ export PLACE_DENSITY          = 0.75
 export TNS_END_PERCENT        = 100
 export EQUIVALENCE_CHECK     ?=   1
 export REMOVE_CELLS_FOR_EQY   = TAPCELL*
+
+export LEC_CHECK = 0
+
+
diff --git a/flow/designs/asap7/jpeg_lvt/config.mk b/flow/designs/asap7/jpeg_lvt/config.mk
@@ -18,4 +18,3 @@ export RECOVER_POWER          = 100
 
 export ASAP7_USE_VT           = LVT
 
-
diff --git a/flow/designs/asap7/mock-alu/config.mk b/flow/designs/asap7/mock-alu/config.mk
@@ -10,3 +10,6 @@ export ROUTING_LAYER_ADJUSTMENT = 0.45
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+export LEC_CHECK = 0
+
diff --git a/flow/designs/asap7/mock-cpu/config.mk b/flow/designs/asap7/mock-cpu/config.mk
@@ -13,3 +13,4 @@ export PLACE_DENSITY            = 0.71
 export TNS_END_PERCENT          = 100
 
 export IO_CONSTRAINTS        = designs/asap7/mock-cpu/io.tcl
+
diff --git a/flow/designs/asap7/riscv32i-mock-sram/config.mk b/flow/designs/asap7/riscv32i-mock-sram/config.mk
@@ -2,3 +2,4 @@ export DESIGN_NICKNAME = riscv32i-mock-sram
 export BLOCKS=fakeram7_256x32
 
 include designs/asap7/riscv32i/config.mk
+
diff --git a/flow/designs/asap7/riscv32i-mock-sram/fakeram7_256x32/config.mk b/flow/designs/asap7/riscv32i-mock-sram/fakeram7_256x32/config.mk
@@ -17,3 +17,4 @@ export PLACE_PINS_ARGS = -min_distance 6 -min_distance_in_tracks
 export IO_CONSTRAINTS  = $(DESIGN_HOME)/asap7/riscv32i-mock-sram/fakeram7_256x32/io.tcl
 
 export PDN_TCL                = $(PLATFORM_DIR)/openRoad/pdn/BLOCK_grid_strategy.tcl
+
diff --git a/flow/designs/asap7/riscv32i/config.mk b/flow/designs/asap7/riscv32i/config.mk
@@ -29,3 +29,4 @@ export CTS_CLUSTER_DIAMETER = 50
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
diff --git a/flow/designs/asap7/swerv_wrapper/config.mk b/flow/designs/asap7/swerv_wrapper/config.mk
@@ -61,3 +61,6 @@ export ROUTING_LAYER_ADJUSTMENT = 0.2
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+export LEC_CHECK = 0
+
diff --git a/flow/designs/asap7/uart/config.mk b/flow/designs/asap7/uart/config.mk
@@ -18,4 +18,3 @@ export REMOVE_CELLS_FOR_EQY   = TAPCELL*
 export SKIP_GATE_CLONING      = 1
 export VERILOG_TOP_PARAMS     = DATA_WIDTH 8
 export SYNTH_HDL_FRONTEND     = slang
-export LEC_CHECK = 1
diff --git a/flow/designs/gf180/ibex/config.mk b/flow/designs/gf180/ibex/config.mk
@@ -17,3 +17,6 @@ export PLACE_DENSITY_LB_ADDON = 0.1
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+export LEC_CHECK = 0
+
diff --git a/flow/designs/gf180/uart-blocks/config.mk b/flow/designs/gf180/uart-blocks/config.mk
@@ -22,3 +22,6 @@ export PLACE_DENSITY          = 0.60
 export TAPCELL_TCL ?= $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)/tapcell.tcl
 export MACRO_ROWS_HALO_X = 14
 export MACRO_ROWS_HALO_Y = 14
+
+export LEC_CHECK = 0
+
diff --git a/flow/designs/ihp-sg13g2/i2c-gpio-expander/I2cDeviceCtrl/config.mk b/flow/designs/ihp-sg13g2/i2c-gpio-expander/I2cDeviceCtrl/config.mk
@@ -18,3 +18,6 @@ export PLACE_DENSITY = 0.75
 export CORNERS = slow typ fast
 
 export PDN_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(TOP_DESIGN_NICKNAME)/${DESIGN_NAME}/pdn.tcl
+
+export LEC_CHECK = 0
+
diff --git a/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk b/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk
@@ -22,3 +22,6 @@ export FOOTPRINT_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)/pad.tcl
 export PDN_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)/pdn.tcl
 
 export BLOCKS = I2cDeviceCtrl
+
+export LEC_CHECK = 0
+
diff --git a/flow/designs/ihp-sg13g2/ibex/config.mk b/flow/designs/ihp-sg13g2/ibex/config.mk
@@ -22,3 +22,6 @@ export CTS_BUF_DISTANCE = 60
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+export LEC_CHECK = 0
+
diff --git a/flow/designs/nangate45/bp_be_top/config.mk b/flow/designs/nangate45/bp_be_top/config.mk
@@ -30,3 +30,5 @@ export CTS_CLUSTER_DIAMETER = 50
 export SYNTH_MINIMUM_KEEP_SIZE = 3000
 
 export FASTROUTE_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NAME)/fastroute.tcl
+
+export LEC_CHECK = 0
diff --git a/flow/designs/nangate45/bp_multi_top/config.mk b/flow/designs/nangate45/bp_multi_top/config.mk
@@ -35,3 +35,6 @@ export SKIP_GATE_CLONING      = 1
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+export LEC_CHECK = 0
+
diff --git a/flow/designs/sky130hd/aes/config.mk b/flow/designs/sky130hd/aes/config.mk
@@ -23,3 +23,4 @@ export CTS_CLUSTER_DIAMETER = 50
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
diff --git a/flow/designs/sky130hd/chameleon/config.mk b/flow/designs/sky130hd/chameleon/config.mk
@@ -50,4 +50,5 @@ export FP_PDN_RAIL_WIDTH  = 0.48
 export FP_PDN_RAIL_OFFSET = 0
 export TNS_END_PERCENT    = 100
 
+export LEC_CHECK = 0
 
diff --git a/flow/designs/sky130hd/gcd/config.mk b/flow/designs/sky130hd/gcd/config.mk
@@ -11,4 +11,3 @@ export CORE_UTILIZATION = 40
 export TNS_END_PERCENT = 100
 export EQUIVALENCE_CHECK   ?=   1
 export REMOVE_CELLS_FOR_EQY = sky130_fd_sc_hd__tapvpwrvgnd*
-export LEC_CHECK = 1
diff --git a/flow/designs/sky130hd/ibex/config.mk b/flow/designs/sky130hd/ibex/config.mk
@@ -28,3 +28,6 @@ export CTS_CLUSTER_DIAMETER = 50
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+
+export LEC_CHECK = 0
diff --git a/flow/designs/sky130hd/jpeg/config.mk b/flow/designs/sky130hd/jpeg/config.mk
@@ -13,3 +13,4 @@ export TNS_END_PERCENT = 100
 export FASTROUTE_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)/fastroute.tcl
 
 export REMOVE_ABC_BUFFERS = 1
+
diff --git a/flow/designs/sky130hd/microwatt/config.mk b/flow/designs/sky130hd/microwatt/config.mk
@@ -51,3 +51,5 @@ endif
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+export LEC_CHECK = 0
diff --git a/flow/designs/sky130hd/riscv32i/config.mk b/flow/designs/sky130hd/riscv32i/config.mk
@@ -12,3 +12,4 @@ export REMOVE_ABC_BUFFERS = 1
 
 #export SWAP_ARITH_OPERATORS = 1
 #export OPENROAD_HIERARCHICAL = 1
+
diff --git a/flow/designs/sky130hs/aes/config.mk b/flow/designs/sky130hs/aes/config.mk
@@ -19,3 +19,4 @@ export CTS_CLUSTER_DIAMETER = 50
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
diff --git a/flow/designs/sky130hs/gcd/config.mk b/flow/designs/sky130hs/gcd/config.mk
@@ -13,7 +13,6 @@ export PLACE_DENSITY_LB_ADDON = 0.1
 export TNS_END_PERCENT        = 100
 export EQUIVALENCE_CHECK     ?=   1
 export REMOVE_CELLS_FOR_EQY   = sky130_fd_sc_hs__tapvpwrvgnd*
-export LEC_CHECK = 1
 
 #export SYNTH_HDL_FRONTEND ?= slang
 #export OPENROAD_HIERARCHICAL ?= 1
diff --git a/flow/designs/sky130hs/ibex/config.mk b/flow/designs/sky130hs/ibex/config.mk
@@ -17,3 +17,4 @@ export PLACE_DENSITY_LB_ADDON = 0.2
 export TNS_END_PERCENT = 100
 
 export REMOVE_ABC_BUFFERS = 1
+
diff --git a/flow/designs/sky130hs/jpeg/config.mk b/flow/designs/sky130hs/jpeg/config.mk
@@ -19,3 +19,4 @@ export CTS_CLUSTER_DIAMETER = 50
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
diff --git a/flow/designs/sky130hs/riscv32i/config.mk b/flow/designs/sky130hs/riscv32i/config.mk
@@ -17,3 +17,4 @@ export REMOVE_ABC_BUFFERS = 1
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
diff --git a/flow/platforms/asap7/config.mk b/flow/platforms/asap7/config.mk
@@ -213,3 +213,5 @@ export IR_DROP_LAYER ?= M1
 
 # Allow empty GDS cell
 export GDS_ALLOW_EMPTY ?= fakeram.*
+
+export REMOVE_CELLS_FOR_LEC   = TAPCELL*
diff --git a/flow/platforms/sky130hd/config.mk b/flow/platforms/sky130hd/config.mk
@@ -150,3 +150,4 @@ export KLAYOUT_DRC_FILE = $(PLATFORM_DIR)/drc/$(PLATFORM).lydrc
 #LVS Check
 export CDL_FILE = $(PLATFORM_DIR)/cdl/$(PLATFORM).cdl
 export KLAYOUT_LVS_FILE = $(PLATFORM_DIR)/lvs/$(PLATFORM).lylvs
+export REMOVE_CELLS_FOR_LEC = sky130_fd_sc_hd__tapvpwrvgnd*
diff --git a/flow/platforms/sky130hs/config.mk b/flow/platforms/sky130hs/config.mk
@@ -105,3 +105,4 @@ export RCX_RULES = $(PLATFORM_DIR)/rcx_patterns.rules
 export PWR_NETS_VOLTAGES  ?= VDD 1.8
 export GND_NETS_VOLTAGES  ?= VSS 0.0
 export IR_DROP_LAYER ?= met1
+export REMOVE_CELLS_FOR_LEC = sky130_fd_sc_hs__tapvpwrvgnd*
diff --git a/flow/scripts/cts.tcl b/flow/scripts/cts.tcl
@@ -61,7 +61,7 @@ if { !$::env(SKIP_CTS_REPAIR_TIMING) } {
   if { $::env(EQUIVALENCE_CHECK) } {
     write_eqy_verilog 4_before_rsz.v
   }
-  if { [env_var_exists_and_non_empty LEC_CHECK] } {
+  if { $::env(LEC_CHECK) } {
     write_lec_verilog 4_before_rsz_lec.v
   }
 
@@ -70,7 +70,7 @@ if { !$::env(SKIP_CTS_REPAIR_TIMING) } {
   if { $::env(EQUIVALENCE_CHECK) } {
     run_equivalence_test
   }
-  if { [env_var_exists_and_non_empty LEC_CHECK] } {
+  if { $::env(LEC_CHECK) } {
     write_lec_verilog 4_after_rsz_lec.v
     run_lec_test 4_rsz 4_before_rsz_lec.v 4_after_rsz_lec.v
   }
diff --git a/flow/scripts/lec_check.tcl b/flow/scripts/lec_check.tcl
@@ -1,6 +1,6 @@
 proc write_lec_verilog { filename } {
-  if { [env_var_exists_and_non_empty REMOVE_CELLS_FOR_EQY] } {
-    write_verilog -remove_cells $::env(REMOVE_CELLS_FOR_EQY) $::env(RESULTS_DIR)/$filename
+  if { [env_var_exists_and_non_empty REMOVE_CELLS_FOR_LEC] } {
+    write_verilog -remove_cells $::env(REMOVE_CELLS_FOR_LEC) $::env(RESULTS_DIR)/$filename
   } else {
     write_verilog $::env(RESULTS_DIR)/$filename
   }
diff --git a/flow/scripts/variables.yaml b/flow/scripts/variables.yaml
@@ -1295,3 +1295,14 @@ WRITE_ODB_AND_SDC_EACH_STAGE:
   stages:
     - All stages
   default: 1
+LEC_CHECK:
+  description: >
+    Perform a formal equivalence check between before and after netlists.
+  default: 1
+  stages:
+    - cts
+REMOVE_CELLS_FOR_LEC:
+  description: >
+    String patterns directly passed to write_verilog -remove_cells <> for
+    lec checks.
+  type: string
diff --git a/tools/kepler-formal b/tools/kepler-formal
@@ -1 +1 @@
-Subproject commit 44f6ad6b075c0b98a38e042d5c4347765e250f05
+Subproject commit d609591a1c7a0620565ecb13f751969f638d845c

Original file line number	Diff line number	Diff line change
`@@ -16,3 +16,4 @@ export TNS_END_PERCENT = 100`
`16`	`16`
`17`	`17`	`export CLUSTER_FLOPS = 1`
`18`	`18`	`export ENABLE_DPO = 0`
	`19`	`+`
Original file line number	Diff line number	Diff line change
`@@ -30,4 +30,3 @@ else ifeq ($(FLOW_VARIANT),combine)`
`30`	`30`	`$(WORK_HOME)/results/$(PLATFORM)/$(DESIGN_NICKNAME)/blackbox/1_synth.v`
`31`	`31`	`endif`
`32`	`32`
`33`		`-export LEC_CHECK = 1`
Original file line number	Diff line number	Diff line change
`@@ -108,3 +108,4 @@ export CTS_LIB_NAME = asap7sc7p5t_INVBUF_SLVT_FF_nldm_211120`
`108`	`108`
`109`	`109`	`# Remove rvfi_probes_o interface`
`110`	`110`	`export SYNTH_CANONICALIZE_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NAME)/canonicalize.tcl`
	`111`	`+`
Original file line number	Diff line number	Diff line change
`@@ -15,3 +15,4 @@ export PLACE_DENSITY = 0.60`
`15`	`15`	`export ASAP7_USE_VT = LVT`
`16`	`16`
`17`	`17`	`export RECOVER_POWER = 1`
	`18`	`+`