diff --git a/flake.lock b/flake.lock index a9808123b..ca62dde07 100644 --- a/flake.lock +++ b/flake.lock @@ -100,16 +100,15 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1726132101, - "narHash": "sha256-XklZsWbAmhuCwlGSJ5qB5RS06mkhtyyTwHFY2SZAn7E=", + "lastModified": 1728469407, + "narHash": "sha256-hdft8u3U5jotXXywvX9+NT31xNlWrBrehVSULJ4JUEc=", "owner": "efabless", "repo": "nix-eda", - "rev": "ef5639cc9bbee574316e3b2b4610149912564f76", + "rev": "ff3ca8916690b2eb97223e581a702bbc868d5802", "type": "github" }, "original": { "owner": "efabless", - "ref": "yosys_python_flag", "repo": "nix-eda", "type": "github" } diff --git a/flake.nix b/flake.nix index 49bf552c5..b7ea21eee 100644 --- a/flake.nix +++ b/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; diff --git a/openlane/scripts/openroad/common/io.tcl b/openlane/scripts/openroad/common/io.tcl index a07ee3645..e2c7b1ec7 100644 --- a/openlane/scripts/openroad/common/io.tcl +++ b/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) } diff --git a/openlane/state/design_format.py b/openlane/state/design_format.py index 5c344e5ee..16d3d75ea 100644 --- a/openlane/state/design_format.py +++ b/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", ) diff --git a/openlane/steps/common_variables.py b/openlane/steps/common_variables.py index 6c24c0108..8307083cb 100644 --- a/openlane/steps/common_variables.py +++ b/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, diff --git a/openlane/steps/openroad.py b/openlane/steps/openroad.py index a358145e0..90bef3c03 100644 --- a/openlane/steps/openroad.py +++ b/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() diff --git a/openlane/steps/pyosys.py b/openlane/steps/pyosys.py index 20f52a9a9..3015bba7c 100644 --- a/openlane/steps/pyosys.py +++ b/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 diff --git a/openlane/steps/yosys.py b/openlane/steps/yosys.py index 4a905df42..871ca6805 100644 --- a/openlane/steps/yosys.py +++ b/openlane/steps/yosys.py @@ -11,7 +11,9 @@ # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. # See the License for the specific language governing permissions and # limitations under the License. +import io import os +import shutil import textwrap import subprocess from abc import abstractmethod @@ -246,13 +248,150 @@ def run(self, state_in: State, **kwargs) -> Tuple[ViewsUpdate, MetricsUpdate]: return super().run(state_in, env=env, **kwargs) +def _mk_eqy_script( + step, + fp: io.TextIOWrapper, + processed_pdk: str, + state: State, + against_netlist: Optional[str] = None, +): + def p(*args, **kwargs): + print(*args, **kwargs, file=fp) + + p("[script]") + p(_generate_read_deps(step.config, step.toolbox, tcl=False)) + p("blackbox") + p("") + + # Gold + p("[gold]") + if against_netlist is not None: + # against previous netlist + p( + f"read_verilog -formal -sv {processed_pdk} {state[DesignFormat.NETLIST_NO_PHYSICAL_CELLS]}", + ) + else: + # against RTL + p( + "read_verilog -formal -sv", + end=" ", + ) + for file in step.config["VERILOG_FILES"]: + p( + f"{file}", + end=" ", + ) + p("") + + # Gate + p("[gate]") + if after := against_netlist: + p( + f"read_verilog -formal -sv {processed_pdk} {after}", + ) + else: + p( + f"read_verilog -formal -sv {processed_pdk} {state[DesignFormat.NETLIST_NO_PHYSICAL_CELLS]}", + ) + + # Script + p("[script]") + p(f"hierarchy -top {step.config['DESIGN_NAME']}") + p("proc") + p(f"prep -top {step.config['DESIGN_NAME']} -flatten") + p("memory -nomap") + p("async2sync") + p("") + + # Write + for mode in ["gold", "gate"]: + p(f"[{mode}]") + p(f"write_verilog {step.step_dir}/{mode}.v") + + # Strats + p( + textwrap.dedent( + """ + [strategy sat] + use sat + depth 5 + + [strategy bitwuzla] + use sby + depth 2 + engine smtbmc bitwuzla + + [strategy pdr] + use sby + engine abc pdr -rfi + """ + ) + ) + + +def _run_eqy( + step: Step, + state: State, + against_netlist: Optional[str] = None, + silent: bool = False, +): + processed_pdk = os.path.join(step.step_dir, "formal_pdk.v") + + if shutil.which("eqy") is None: + info("EQY is not installed. Skipping…") + return {} + + if step.config["PDK"].startswith("sky130A"): + subprocess.check_call( + [ + "eqy.formal_pdk_proc", + "--output", + processed_pdk, + ] + + [str(model) for model in step.config["CELL_VERILOG_MODELS"]] + ) + elif step.config.get("EQY_FORCE_ACCEPT_PDK"): + subprocess.check_call( + ["iverilog", "-E", "-o", processed_pdk, "-DFUNCTIONAL"] + + [str(model) for model in step.config["CELL_VERILOG_MODELS"]] + ) + else: + info(f"PDK {step.config['PDK']} is not supported by EQY. Skipping…") + return {} + + eqy_script_path = os.path.join(step.step_dir, f"{step.config['DESIGN_NAME']}.eqy") + + with open(eqy_script_path, "w", encoding="utf8") as f: + if eqy_script := step.config.get("EQY_SCRIPT"): + for line in open(eqy_script, "r", encoding="utf8"): + f.write(line) + else: + _mk_eqy_script( + step, + f, + processed_pdk, + state, + against_netlist=against_netlist, + ) + work_dir = os.path.join(step.step_dir, "scratch") + + subprocess_result = step.run_subprocess( + ["eqy", "-f", eqy_script_path, "-d", work_dir], + log_to=os.path.join(step.step_dir, "eqy.log"), + silent=silent, + ) + + os.unlink(os.path.join(work_dir, "partition.log")) # Grows into the 10s of GBs + + return subprocess_result["generated_metrics"] + + @Step.factory.register() class EQY(Step): id = "Yosys.EQY" name = "Equivalence Check" - long_name = "RTL/Netlist Equivalence Check" - inputs = [DesignFormat.NETLIST] + inputs = [DesignFormat.NETLIST_NO_PHYSICAL_CELLS] outputs = [] config_vars = ( @@ -279,93 +418,4 @@ class EQY(Step): ) def run(self, state_in: State, **kwargs) -> Tuple[ViewsUpdate, MetricsUpdate]: - processed_pdk = os.path.join(self.step_dir, "formal_pdk.v") - - if self.config["PDK"].startswith("sky130A"): - subprocess.check_call( - [ - "eqy.formal_pdk_proc", - "--output", - processed_pdk, - ] - + [str(model) for model in self.config["CELL_VERILOG_MODELS"]] - ) - elif self.config["EQY_FORCE_ACCEPT_PDK"]: - subprocess.check_call( - ["iverilog", "-E", "-o", processed_pdk, "-DFUNCTIONAL"] - + [str(model) for model in self.config["CELL_VERILOG_MODELS"]] - ) - else: - info( - f"PDK {self.config['PDK']} is not supported by the EQY step. Skipping…" - ) - return {}, {} - - eqy_script_path = os.path.join( - self.step_dir, f"{self.config['DESIGN_NAME']}.eqy" - ) - - with open(eqy_script_path, "w", encoding="utf8") as f: - if eqy_script := self.config["EQY_SCRIPT"]: - for line in open(eqy_script, "r", encoding="utf8"): - f.write(line) - else: - script = textwrap.dedent( - """ - [script] - {dep_commands} - blackbox - - [gold] - read_verilog -formal -sv {files} - - [gate] - read_verilog -formal -sv {processed_pdk} {nl} - - [script] - hierarchy -top {design_name} - proc - prep -top {design_name} -flatten - - memory -nomap - async2sync - - [gold] - write_verilog {step_dir}/gold.v - - [gate] - write_verilog {step_dir}/gate.v - - [strategy sat] - use sat - depth 5 - - [strategy pdr] - use sby - engine abc pdr -rfi - - [strategy bitwuzla] - use sby - depth 2 - engine smtbmc bitwuzla - """ - ).format( - design_name=self.config["DESIGN_NAME"], - dep_commands=_generate_read_deps( - self.config, self.toolbox, tcl=False - ), - files=TclUtils.join( - [str(file) for file in self.config["VERILOG_FILES"]] - ), - nl=state_in[DesignFormat.NETLIST], - processed_pdk=processed_pdk, - step_dir=self.step_dir, - ) - f.write(script) - work_dir = os.path.join(self.step_dir, "scratch") - - subprocess_result = self.run_subprocess( - ["eqy", "-f", eqy_script_path, "-d", work_dir] - ) - - return {}, subprocess_result["generated_metrics"] + return {}, _run_eqy(self, state_in, None)