LEC check

Signed-off-by: Noam Cohen <[email protected]>

Author: nanocoh

.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,38 @@ __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
+
+        if [[ "$OSTYPE" == "darwin"* ]]; then
+        cmake .. \
+        -DCMAKE_BUILD_TYPE=Release \
+        -DCMAKE_CXX_FLAGS_RELEASE="-Ofast -march=native -ffast-math -flto" \
+        -DCMAKE_EXE_LINKER_FLAGS="-flto" \
+        -DCMAKE_INSTALL_RPATH_USE_LINK_PATH=ON \
+        -DCMAKE_INSTALL_RPATH=@executable_path/../lib
+        else
+        cmake .. \
+        -DCMAKE_BUILD_TYPE=Release \
+        -DCMAKE_CXX_FLAGS_RELEASE="-Ofast -march=native -ffast-math -flto" \
+        -DCMAKE_EXE_LINKER_FLAGS="-flto" \
+        -DCMAKE_INSTALL_RPATH_USE_LINK_PATH=ON \
+        -DCMAKE_INSTALL_RPATH=\$ORIGIN/../lib
+        fi
+        make -j4 install
+        cd ../../../
         if [ ${WITH_VERIFIC} -eq 1 ]; then
                 echo "[INFO FLW-0032] Cleaning up Verific components."
                 rm -rf verific
         fi
-
 }
 
 __update_openroad_app_remote()

etc/DependencyInstaller.sh

@@ -286,7 +286,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
@@ -300,7 +300,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

@@ -60,12 +60,18 @@ 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] } {
+    run_lec_test
+  }
 
   set result [catch { detailed_placement } msg]
   if { $result != 0 } {

flow/scripts/load.tcl

@@ -106,3 +106,40 @@ proc run_equivalence_test { } {
     puts "Repair timing output passed equivalence test"
   }
 }
+
+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 { } {
+  set outfile [open "$::env(OBJECTS_DIR)/4_lec_test.yml" w]
+  puts $outfile "format: verilog"
+  puts $outfile "input_paths:"
+  puts $outfile "  - $::env(RESULTS_DIR)/4_before_rsz_lec.v"
+  puts $outfile "  - $::env(RESULTS_DIR)/4_after_rsz_lec.v"
+  # Gold netlist
+  puts $outfile "liberty_files:"
+  foreach libFile $::env(LIB_FILES) {
+    puts $outfile " - $libFile"
+  }
+  puts $outfile "log_file: $::env(LOG_DIR)/4_lec_check.log"
+  close $outfile
+}
+
+proc run_lec_test { } {
+  write_lec_verilog 4_after_rsz_lec.v
+  write_lec_script
+  # tclint-disable-next-line command-args
+  eval exec kepler-formal --config $::env(OBJECTS_DIR)/4_lec_test.yml
+  set count \
+    [exec grep -c "Found difference" $::env(LOG_DIR)/4_lec_check.log]
+  if { $count > 0 } {
+    error "Repair timing output failed lec test"
+  } else {
+    puts "Repair timing output passed lec test"
+  }
+}