AUTO_MEMORIES: stop when a module to blackbox is not a black box

flow/scripts/memories/check_blackboxed.tcl

@@ -0,0 +1,34 @@
+# AUTO_MEMORIES: stop when a module synthesis was told to blackbox is not
+# a black box of the design.
+#
+# read_slang's --blackboxed-module ignores a name it does not know. A
+# name in blackboxes.txt that is not the module's definition -- a slang
+# per-instance name, a typo, a module the sources no longer have -- leaves
+# the memory's behavioral body in place, and the flow says so only much
+# later, as a memory over SYNTH_MEMORY_MAX_BITS with no hint of why. Run
+# after the sources are read; `names` is the blackboxes.txt list.
+proc auto_memories_check_blackboxed { names } {
+  if { [llength $names] == 0 } {
+    return
+  }
+  # yosys lists an escaped module with its leading backslash (`\1d_ram`);
+  # blackboxes.txt names it as read_slang takes it (`1d_ram`).
+  set blackboxed {}
+  foreach m [split [tee -q -s result.string select -list-mod =A:blackbox] "\n"] {
+    set m [string trim $m]
+    if { $m ne "" } {
+      lappend blackboxed [regsub {^\\} $m {}]
+    }
+  }
+  set missing {}
+  foreach m $names {
+    if { [lsearch -exact $blackboxed $m] < 0 } {
+      lappend missing $m
+    }
+  }
+  if { [llength $missing] > 0 } {
+    error "AUTO_MEMORIES: not a black box of the design after reading the\
+      sources, so its behavioral body would be synthesized:\
+      [join $missing {, }]"
+  }
+}

flow/scripts/synth_preamble.tcl

@@ -48,6 +48,8 @@ proc read_checkpoint { file } {
 # um^2. The list is produced by scripts/memories/gen_memories.py before
 # canonicalization, one `<module> <area>` per line; see
 # docs/user/AutoMemories.md.
+source $::env(SCRIPTS_DIR)/memories/check_blackboxed.tcl
+
 proc auto_memories_areas { } {
   if { ![env_var_equals AUTO_MEMORIES 1] } {
     return {}
@@ -142,6 +144,7 @@ proc read_design_sources { } {
     lappend slang_args {*}$::env(SYNTH_SLANG_ARGS)
 
     yosys read_slang {*}$slang_args
+    auto_memories_check_blackboxed [auto_memories_blackboxes]
 
     # Workaround for yosys-slang#119
     setattr -unset init
@@ -192,6 +195,8 @@ proc read_design_sources { } {
     set auto_blackboxes [auto_memories_blackboxes]
     if { [llength $auto_blackboxes] > 0 } {
       hierarchy -top $::env(DESIGN_NAME)
+      # Not checked with auto_memories_check_blackboxed: slang is the
+      # supported frontend for AUTO_MEMORIES.
       foreach m $auto_blackboxes {
         blackbox $m
       }

flow/test/test_auto_memories_blackboxed.py

@@ -0,0 +1,114 @@
+#!/usr/bin/env python3
+"""AUTO_MEMORIES stops synthesis when a module it asks read_slang to
+blackbox is not a black box of the design.
+
+read_slang's --blackboxed-module ignores a name it does not know, and
+slang names a module per instance, `<definition>$<instance path>`. Only
+the definition's name blackboxes the memory; any other name must stop
+the flow right after the sources are read, naming the module.
+
+Skipped when no yosys with read_slang is available: YOSYS_EXE or yosys on
+PATH, with the plugin from SLANG_PLUGIN_PATH when read_slang is not built
+in.
+"""
+
+import os
+import shutil
+import subprocess
+import tempfile
+import unittest
+
+CHECK_TCL = os.path.join(
+    os.path.dirname(os.path.abspath(__file__)),
+    "..",
+    "scripts",
+    "memories",
+    "check_blackboxed.tcl",
+)
+
+DESIGN = """\
+module ram (input clk, input we, input [5:0] addr, input [15:0] d,
+            output logic [15:0] q);
+  logic [15:0] mem [0:63];
+  always_ff @(posedge clk) begin
+    if (we) mem[addr] <= d;
+    q <= mem[addr];
+  end
+endmodule
+module \\1d_ram (input clk, input we, input [5:0] addr, input [15:0] d,
+                output logic [15:0] q);
+  logic [15:0] mem [0:63];
+  always_ff @(posedge clk) begin
+    if (we) mem[addr] <= d;
+    q <= mem[addr];
+  end
+endmodule
+module top (input clk, input we, input [5:0] addr, input [15:0] d,
+            output [15:0] q0, q1, q2);
+  ram u0 (.clk, .we, .addr, .d, .q(q0));
+  ram u1 (.clk, .we, .addr, .d, .q(q1));
+  \\1d_ram  u2 (.clk, .we, .addr, .d, .q(q2));
+endmodule
+"""
+
+
+def yosys_command():
+    yosys = os.environ.get("YOSYS_EXE") or shutil.which("yosys")
+    if not yosys:
+        return None
+    cmd = [yosys, "-q"]
+    plugin = os.environ.get("SLANG_PLUGIN_PATH")
+    if plugin:
+        cmd += ["-m", plugin]
+    probe = subprocess.run(cmd + ["-p", "help read_slang"], capture_output=True)
+    return cmd if probe.returncode == 0 else None
+
+
+class TestAutoMemoriesBlackboxed(unittest.TestCase):
+    def run_check(self, names):
+        cmd = yosys_command()
+        if cmd is None:
+            self.skipTest("no yosys with read_slang")
+        with tempfile.TemporaryDirectory() as tmp:
+            design = os.path.join(tmp, "top.sv")
+            with open(design, "w") as f:
+                f.write(DESIGN)
+            braced = [f"{{{n}}}" for n in names]
+            blackboxed = " ".join(f"--blackboxed-module {n}" for n in braced)
+            script = os.path.join(tmp, "check.tcl")
+            with open(script, "w") as f:
+                f.write(
+                    "yosys -import\n"
+                    f"source {{{CHECK_TCL}}}\n"
+                    f"yosys read_slang --keep-hierarchy --top top {blackboxed}"
+                    f" {{{design}}}\n"
+                    f"auto_memories_check_blackboxed [list {' '.join(braced)}]\n"
+                )
+            result = subprocess.run(
+                cmd + ["-c", script], capture_output=True, text=True
+            )
+        return result.returncode, result.stdout + result.stderr
+
+    def test_definition_name_is_blackboxed(self):
+        returncode, output = self.run_check(["ram"])
+        self.assertEqual(returncode, 0, output)
+
+    def test_escaped_definition_name_is_blackboxed(self):
+        # read_slang takes `\1d_ram` as `1d_ram`; yosys lists it escaped
+        returncode, output = self.run_check(["ram", "1d_ram"])
+        self.assertEqual(returncode, 0, output)
+
+    def test_per_instance_name_stops_the_flow(self):
+        returncode, output = self.run_check(["ram$top.u0", "ram$top.u1"])
+        self.assertNotEqual(returncode, 0, output)
+        self.assertIn("not a black box of the design", output)
+        self.assertIn("ram$top.u0, ram$top.u1", output)
+
+    def test_unknown_name_stops_the_flow(self):
+        returncode, output = self.run_check(["no_such_module"])
+        self.assertNotEqual(returncode, 0, output)
+        self.assertIn("no_such_module", output)
+
+
+if __name__ == "__main__":
+    unittest.main()