lec: fix cell filtering and update kepler-formal

flow/designs/asap7/aes-block/rules-base.json

@@ -32,7 +32,7 @@
         "compare": ">="
     },
     "cts__timing__setup__tns": {
-        "value": -3710.0,
+        "value": -5150.0,
         "compare": ">="
     },
     "cts__timing__hold__ws": {
@@ -52,11 +52,11 @@
         "compare": ">="
     },
     "globalroute__timing__setup__tns": {
-        "value": -3650.0,
+        "value": -4295.0,
         "compare": ">="
     },
     "globalroute__timing__hold__ws": {
-        "value": -22.5,
+        "value": -25.9,
         "compare": ">="
     },
     "globalroute__timing__hold__tns": {

flow/designs/nangate45/ariane133/rules-base.json

@@ -99,4 +99,4 @@
         "value": 840911,
         "compare": "<="
     }
-}
+}

flow/designs/rapidus2hp/cva6/rules-base.json

@@ -28,11 +28,11 @@
         "compare": "<="
     },
     "cts__timing__setup__ws": {
-        "value": -0.138,
+        "value": -0.111,
         "compare": ">="
     },
     "cts__timing__setup__tns": {
-        "value": -287.0,
+        "value": -245.0,
         "compare": ">="
     },
     "cts__timing__hold__ws": {
@@ -48,7 +48,7 @@
         "compare": "<="
     },
     "globalroute__timing__setup__ws": {
-        "value": -0.255,
+        "value": -0.282,
         "compare": ">="
     },
     "globalroute__timing__setup__tns": {
@@ -64,7 +64,7 @@
         "compare": ">="
     },
     "finish__timing__setup__ws": {
-        "value": -0.255,
+        "value": -0.282,
         "compare": ">="
     },
     "finish__timing__setup__tns": {

flow/designs/rapidus2hp/cva6/rules-verific.json

@@ -28,11 +28,11 @@
         "compare": "<="
     },
     "cts__timing__setup__ws": {
-        "value": -0.157,
+        "value": -0.14,
         "compare": ">="
     },
     "cts__timing__setup__tns": {
-        "value": -518.0,
+        "value": -412.0,
         "compare": ">="
     },
     "cts__timing__hold__ws": {
@@ -52,7 +52,7 @@
         "compare": ">="
     },
     "globalroute__timing__setup__tns": {
-        "value": -650.0,
+        "value": -697.0,
         "compare": ">="
     },
     "globalroute__timing__hold__ws": {
@@ -68,7 +68,7 @@
         "compare": ">="
     },
     "finish__timing__setup__tns": {
-        "value": -650.0,
+        "value": -697.0,
         "compare": ">="
     },
     "finish__timing__hold__ws": {

flow/designs/sky130hd/chameleon/rules-base.json

@@ -44,7 +44,7 @@
         "compare": ">="
     },
     "globalroute__antenna_diodes_count": {
-        "value": 188,
+        "value": 218,
         "compare": "<="
     },
     "globalroute__timing__setup__ws": {

flow/designs/sky130hd/microwatt/rules-base.json

@@ -32,7 +32,7 @@
         "compare": ">="
     },
     "cts__timing__setup__tns": {
-        "value": -311.0,
+        "value": -352.0,
         "compare": ">="
     },
     "cts__timing__hold__ws": {
@@ -72,7 +72,7 @@
         "compare": "<="
     },
     "detailedroute__antenna__violating__nets": {
-        "value": 5,
+        "value": 6,
         "compare": "<="
     },
     "detailedroute__antenna_diodes_count": {
@@ -99,4 +99,4 @@
         "value": 5578282,
         "compare": "<="
     }
-}
+}

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"
+        }
       }
     }
   }