feat: experimental LEC to resizer steps

flake.nix

@@ -22,9 +22,7 @@
   };
 
   inputs = {
-    # TEMPORARY: Until https://github.com/YosysHQ/yosys/pull/4553 is merged
-    ## DO NOT MERGE TO main WHILE WE'RE STILL ON A BRANCH OF NIX-EDA
-    nix-eda.url = github:efabless/nix-eda/yosys_python_flag;
+    nix-eda.url = github:efabless/nix-eda;
     libparse.url = github:efabless/libparse-python;
     ioplace-parser.url = github:efabless/ioplace_parser;
     volare.url = github:efabless/volare;

openlane/scripts/openroad/common/io.tcl

@@ -318,6 +318,35 @@ proc read_current_odb {args} {
     set_dont_use_cells
 }
 
+proc _populate_cells_by_class {} {
+    if { [info exists ::_cells_by_class(non_core)] } {
+        return
+    }
+
+    set ::_cells_by_class(non_core) [list]
+    set ::_cells_by_class(non_timing) [list]
+    foreach lib $::libs {
+        foreach master [$lib getMasters] {
+            if { "[$master getType]" != "CORE" || "[$master getType]" != "BLOCK" } {
+                lappend ::_cells_by_class(non_core) [$master getName]
+                if { "[$master getType]" != "CORE_ANTENNACELL" } {
+                    lappend ::_cells_by_class(non_timing) [$master getName]
+                }
+            }
+        }
+    }
+}
+
+proc get_timing_excluded_cells {args} {
+    _populate_cells_by_class
+    return $::_cells_by_class(non_timing)
+}
+
+proc get_non_core_cells {args} {
+    _populate_cells_by_class
+    return $::_cells_by_class(non_core)
+}
+
 proc write_views {args} {
     # This script will attempt to write views based on existing "SAVE_"
     # environment variables. If the SAVE_ variable exists, the script will
@@ -341,26 +370,32 @@ proc write_views {args} {
         write_verilog $::env(SAVE_NETLIST)
     }
 
+    if { [info exists ::env(SAVE_NETLIST_NO_PHYSICAL_CELLS)] } {
+        puts "Writing logical netlist to '$::env(SAVE_NETLIST_NO_PHYSICAL_CELLS)'…"
+        puts "Excluding: [get_non_core_cells]"
+        write_verilog -remove_cells "[get_non_core_cells]"\
+            $::env(SAVE_NETLIST_NO_PHYSICAL_CELLS)
+    }
+
     if { [info exists ::env(SAVE_POWERED_NETLIST)] } {
         puts "Writing powered netlist to '$::env(SAVE_POWERED_NETLIST)'…"
         write_verilog -include_pwr_gnd $::env(SAVE_POWERED_NETLIST)
     }
 
     if { [info exists ::env(SAVE_POWERED_NETLIST_SDF_FRIENDLY)] } {
-        set exclude_cells "[join $::env(FILL_CELL)] [join $::env(DECAP_CELL)] [join $::env(WELLTAP_CELL)] [join $::env(ENDCAP_CELL)]"
-        puts "Writing nofill powered netlist to '$::env(SAVE_POWERED_NETLIST_SDF_FRIENDLY)'…"
-        puts "Excluding $exclude_cells"
+        puts "Writing timing powered netlist to '$::env(SAVE_POWERED_NETLIST_SDF_FRIENDLY)'…"
+        puts "Excluding: [get_timing_excluded_cells]"
         write_verilog -include_pwr_gnd \
-            -remove_cells "$exclude_cells"\
+            -remove_cells "[get_timing_excluded_cells]"\
             $::env(SAVE_POWERED_NETLIST_SDF_FRIENDLY)
     }
 
     if { [info exists ::env(SAVE_POWERED_NETLIST_NO_PHYSICAL_CELLS)] } {
         set exclude_cells "[join [lindex [split $::env(DIODE_CELL) "/"] 0]] [join $::env(FILL_CELL)] [join $::env(DECAP_CELL)] [join $::env(WELLTAP_CELL)] [join $::env(ENDCAP_CELL)]"
-        puts "Writing nofilldiode powered netlist to '$::env(SAVE_POWERED_NETLIST_NO_PHYSICAL_CELLS)'…"
-        puts "Excluding $exclude_cells"
+        puts "Writing logical powered netlist to '$::env(SAVE_POWERED_NETLIST_NO_PHYSICAL_CELLS)'…"
+        puts "Excluding: [get_non_core_cells]"
         write_verilog -include_pwr_gnd \
-            -remove_cells "$exclude_cells"\
+            -remove_cells "[get_non_core_cells]"\
             $::env(SAVE_POWERED_NETLIST_NO_PHYSICAL_CELLS)
     }
 

openlane/state/design_format.py

@@ -65,6 +65,12 @@ class DesignFormat(Enum):
         "nl.v",
         "Verilog Netlist",
     )
+    NETLIST_NO_PHYSICAL_CELLS: DesignFormatObject = DesignFormatObject(
+        "nl-npc",
+        "nl-npc.v",
+        "Logical Verilog Netlist",
+        folder_override="nl",
+    )
     POWERED_NETLIST: DesignFormatObject = DesignFormatObject(
         "pnl",
         "pnl.v",
@@ -73,13 +79,13 @@ class DesignFormat(Enum):
     POWERED_NETLIST_SDF_FRIENDLY: DesignFormatObject = DesignFormatObject(
         "pnl-sdf-friendly",
         "pnl-sdf.v",
-        "Powered Verilog Netlist For SDF Simulation (Without Fill Cells)",
+        "Timing Verilog Netlist (No Physical Cells Except Diodes)",
         folder_override="pnl",
     )
     POWERED_NETLIST_NO_PHYSICAL_CELLS: DesignFormatObject = DesignFormatObject(
         "pnl-npc",
         "pnl-npc.v",
-        "Powered Verilog Netlist Without Physical Cells (Fill Cells and Diode Cells)",
+        "Powered Logical Verilog Netlist",
         folder_override="pnl",
     )
 

openlane/steps/common_variables.py

@@ -319,6 +319,12 @@
 ]
 
 rsz_variables = dpl_variables + [
+    Variable(
+        "RSZ_LEC",
+        bool,
+        "Experimental: attempts to formally prove the equivalence of the circuit before and after resizing if the EQY utility is installed (and supported by the PDK.)",
+        default=False,
+    ),
     Variable(
         "RSZ_DONT_TOUCH_RX",
         str,

openlane/steps/openroad.py

@@ -64,6 +64,7 @@
     grt_variables,
     routing_layer_variables,
 )
+from .yosys import _run_eqy
 
 from ..config import Variable, Macro
 from ..config.flow import option_variables
@@ -181,6 +182,7 @@ class OpenROADStep(TclStep):
         DesignFormat.SDC,
         DesignFormat.NETLIST,
         DesignFormat.POWERED_NETLIST,
+        DesignFormat.NETLIST_NO_PHYSICAL_CELLS,
     ]
 
     output_processors = [OpenROADOutputProcessor, DefaultOutputProcessor]
@@ -1992,7 +1994,22 @@ def run(
             debug(f"Liberty files for '{corner}' added: {libs}")
             count += 1
 
-        return super().run(state_in, env=env, **kwargs)
+        views, metrics = super().run(state_in, env=env, **kwargs)
+
+        if self.config.get("RSZ_LEC"):
+            try:
+                info("Verifying equivalence with EQY…")
+                _run_eqy(
+                    self,
+                    state_in,
+                    against_netlist=str(views[DesignFormat.NETLIST_NO_PHYSICAL_CELLS]),
+                )
+            except subprocess.CalledProcessError:
+                raise StepException(
+                    "OpenROAD resizing step emitted logically non-equivalent circuit: Yosys EQY reports a non-zero exit.\nPlease report this as a bug."
+                )
+
+        return views, metrics
 
 
 @Step.factory.register()

openlane/steps/pyosys.py

@@ -362,7 +362,7 @@ def run(self, state_in: State, **kwargs) -> Tuple[ViewsUpdate, MetricsUpdate]:
 
 class SynthesisCommon(VerilogStep):
     inputs = []  # The input RTL is part of the configuration
-    outputs = [DesignFormat.NETLIST]
+    outputs = [DesignFormat.NETLIST, DesignFormat.NETLIST_NO_PHYSICAL_CELLS]
 
     config_vars = PyosysStep.config_vars + [
         Variable(
@@ -562,6 +562,7 @@ def run(self, state_in: State, **kwargs) -> Tuple[ViewsUpdate, MetricsUpdate]:
             )
 
         view_updates[DesignFormat.NETLIST] = Path(out_file)
+        view_updates[DesignFormat.NETLIST_NO_PHYSICAL_CELLS] = Path(out_file)
 
         return view_updates, metric_updates