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

Turn on LEC for asap7_jpeg asap7_uart sky130hd_gcd sky130hs_gcd

Author: maliberty

flow/designs/asap7/aes/config.mk

@@ -29,3 +29,5 @@ else ifeq ($(FLOW_VARIANT),combine)
 	 $(WORK_HOME)/results/$(PLATFORM)/$(DESIGN_NICKNAME)/blackbox/1_synth.v \
 	 $(WORK_HOME)/results/$(PLATFORM)/$(DESIGN_NICKNAME)/blackbox/1_synth.v
 endif
+
+export LEC_CHECK = 1

flow/designs/asap7/uart/config.mk

@@ -18,3 +18,4 @@ 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

flow/designs/sky130hd/gcd/config.mk

@@ -11,3 +11,4 @@ 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

flow/designs/sky130hs/gcd/config.mk

@@ -13,6 +13,7 @@ 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

flow/scripts/lec_check.tcl

@@ -23,7 +23,7 @@ proc write_lec_script { step file1 file2 } {
 proc run_lec_test { step file1 file2 } {
   write_lec_script $step $file1 $file2
   # tclint-disable-next-line command-args
-  eval exec kepler-formal --config $::env(OBJECTS_DIR)/${step}_lec_test.yml
+  eval exec $::env(KEPLER_FORMAL_EXE) --config $::env(OBJECTS_DIR)/${step}_lec_test.yml
   try {
     set count [exec grep -c "Found difference" $::env(LOG_DIR)/${step}_lec_check.log]]
   } trap CHILDSTATUS {results options} {

flow/scripts/variables.mk

@@ -117,6 +117,9 @@ YOSYS_IS_VALID := $(if $(YOSYS_EXE),$(shell test -x $(YOSYS_EXE) && echo "true")
 KLAYOUT_DIR = $(abspath $(FLOW_HOME)/../tools/install/klayout/)
 KLAYOUT_BIN_FROM_DIR = $(KLAYOUT_DIR)/klayout
 
+KEPLER_FORMAL_EXE ?= $(abspath $(FLOW_HOME)/../tools/install/kepler-formal/bin/kepler-formal)
+export KEPLER_FORMAL_EXE := $(KEPLER_FORMAL_EXE)
+
 ifeq ($(wildcard $(KLAYOUT_BIN_FROM_DIR)), $(KLAYOUT_BIN_FROM_DIR))
 export KLAYOUT_CMD ?= sh -c 'LD_LIBRARY_PATH=$(dir $(KLAYOUT_BIN_FROM_DIR)) $$0 "$$@"' $(KLAYOUT_BIN_FROM_DIR)
 else