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

LEC check

Author: maliberty

.gitmodules

@@ -7,3 +7,6 @@
 [submodule "tools/yosys-slang"]
 	path = tools/yosys-slang
 	url = https://github.com/povik/yosys-slang.git
+[submodule "tools/kepler-formal"]
+	path = tools/kepler-formal
+	url = https://github.com/keplertech/kepler-formal

build_openroad.sh

@@ -291,11 +291,33 @@ __local_build()
         # CMAKE_FLAGS added to work around yosys-slang#141 (unable to build outside of git checkout)
         ${NICE} make install -C tools/yosys-slang -j "${PROC}" YOSYS_PREFIX="${INSTALL_PATH}/yosys/bin/" CMAKE_FLAGS="-DYOSYS_SLANG_REVISION=unknown -DSLANG_REVISION=unknown"
 
+        echo "[INFO FLW-0031] Compiling kepler-formal"
+        cd tools/kepler-formal
+        git submodule update --init --recursive
+
+        # if build dir does not exist, create it
+        if [ ! -d build ]; then
+        mkdir build
+        fi 
+        cd build
+
+	cmake .. \
+        -DCMAKE_BUILD_TYPE=Release \
+        -DCMAKE_CXX_FLAGS_RELEASE="-Ofast -march=native -ffast-math -flto" \
+        -DCMAKE_EXE_LINKER_FLAGS="-flto" \
+        -DCMAKE_BUILD_RPATH="${DIR}/tools/kepler-formal/build/thirdparty/naja/src/dnl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/nl/nl:${DIR}/tools/kepler-formal/build/thirdparty/naja/src/optimization" \
+        -DCMAKE_INSTALL_RPATH="${INSTALL_PATH}/kepler-formal/lib" \
+        -DCMAKE_BUILD_WITH_INSTALL_RPATH=OFF \
+        -DCMAKE_INSTALL_RPATH_USE_LINK_PATH=OFF \
+        -DCMAKE_INSTALL_PREFIX="${INSTALL_PATH}/kepler-formal"
+
+        make -j"${PROC}" install
+
+        cd ../../../
         if [ ${WITH_VERIFIC} -eq 1 ]; then
                 echo "[INFO FLW-0032] Cleaning up Verific components."
                 rm -rf verific
         fi
-
 }
 
 __update_openroad_app_remote()

env.sh

@@ -13,6 +13,7 @@ function __setpaths() {
   # developer settings go in ./dev_env.sh
   export PATH=${DIR}/tools/install/OpenROAD/bin:$PATH
   export PATH=${DIR}/tools/install/yosys/bin:$PATH
+  export PATH=${DIR}/tools/install/kepler-formal/bin:$PATH
 
   if [[ "$OSTYPE" == "darwin"* ]]; then
     export PATH="/Applications/KLayout/klayout.app/Contents/MacOS:$PATH"

etc/DependencyInstaller.sh

@@ -257,7 +257,7 @@ _installUbuntuPackages() {
 
 _installDarwinPackages() {
     brew install libffi tcl-tk ruby
-    brew install python libomp
+    brew install python libomp doxygen capnp tbb bison flex boost spdlog zlib
     brew link --force libomp
     brew install --cask klayout
     brew install docker docker-buildx
@@ -271,7 +271,10 @@ _installCI() {
         coreutils \
         curl \
         python3 \
-        software-properties-common
+        software-properties-common \
+        clang pkg-config \
+        libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \
+        libgtest-dev libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev
 }
 
 _help() {

flow/scripts/cts.tcl

@@ -1,5 +1,6 @@
 utl::set_metrics_stage "cts__{}"
 source $::env(SCRIPTS_DIR)/load.tcl
+source $::env(SCRIPTS_DIR)/lec_check.tcl
 erase_non_stage_variables cts
 load_design 3_place.odb 3_place.sdc
 
@@ -60,12 +61,19 @@ 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] } {
+    write_lec_verilog 4_before_rsz_lec.v
+  }
 
   repair_timing_helper
 
   if { $::env(EQUIVALENCE_CHECK) } {
     run_equivalence_test
   }
+  if { [env_var_exists_and_non_empty 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
+  }
 
   set result [catch { detailed_placement } msg]
   if { $result != 0 } {

flow/scripts/lec_check.tcl

@@ -0,0 +1,38 @@
+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
+  } else {
+    write_verilog $::env(RESULTS_DIR)/$filename
+  }
+}
+
+proc write_lec_script { step file1 file2 } {
+  set outfile [open "$::env(OBJECTS_DIR)/${step}_lec_test.yml" w]
+  puts $outfile "format: verilog"
+  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}_lec_check.log"
+  close $outfile
+}
+
+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
+  try {
+    set count [exec grep -c "Found difference" $::env(LOG_DIR)/${step}_lec_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"
+  } else {
+    puts "Repair timing output passed lec test"
+  }
+}