lec: fix cell filtering and update kepler-formal

- Enhance find_physical_only_masters to auto-detect cells with no
  signal pins and no liberty cell (e.g., CDMMTYPE2 marker cells)
- Add REMOVE_CELLS_FOR_LEC support to write_lec_verilog in lec_check.tcl
- Update kepler-formal to 093a7b5 (fix for missing bus direction)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>

Author: jhkim-pii

flow/scripts/lec_check.tcl

@@ -1,9 +1,9 @@
 proc write_lec_verilog { filename } {
+  set remove_cells [find_physical_only_masters]
   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
+    lappend remove_cells {*}$::env(REMOVE_CELLS_FOR_LEC)
   }
+  write_verilog -remove_cells $remove_cells $::env(RESULTS_DIR)/$filename
 }
 
 proc write_lec_script { step file1 file2 } {
@@ -25,7 +25,7 @@ proc run_lec_test { step file1 file2 } {
   # tclint-disable-next-line command-args
   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]]
+    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

flow/scripts/util.tcl

@@ -229,6 +229,27 @@ proc is_physical_only_master { master } {
   return 0
 }
 
+# Returns 1 if the master has no signal pins (only power/ground or none).
+proc has_signal_pins { master } {
+  foreach mterm [$master getMTerms] {
+    set sig_type [$mterm getSigType]
+    if { $sig_type != "POWER" && $sig_type != "GROUND" } {
+      return 1
+    }
+  }
+  return 0
+}
+
+# Returns 1 if the master has a corresponding liberty cell.
+proc has_liberty_cell { master } {
+  set master_name [$master getName]
+  set lib_cells [get_lib_cells -quiet */$master_name]
+  if { $lib_cells == {} } {
+    return 0
+  }
+  return 1
+}
+
 # Finds all physical-only masters in the current database and
 # returns their names.
 proc find_physical_only_masters { } {
@@ -237,8 +258,19 @@ proc find_physical_only_masters { } {
   set physical_only_masters [list]
   foreach lib $libs {
     foreach master [$lib getMasters] {
+      set master_name [$master getName]
       if { [is_physical_only_master $master] } {
-        lappend physical_only_masters [$master getName]
+        lappend physical_only_masters $master_name
+        continue
+      }
+
+      # Consider cells with no signal pins and no liberty cell as physical-only
+      if { [has_liberty_cell $master] == 0 } {
+        if { [has_signal_pins $master] == 0 } {
+          lappend physical_only_masters $master_name
+        } else {
+          puts "Warning: master $master_name has signal pins but no liberty cell"
+        }
       }
     }
   }