docs: visualize RTL saturation evidence

Author: Labeeb2339

README.md

@@ -68,6 +68,16 @@ exact_sum = sum(a[i] * b[i] for i in 0 .. VEC_LEN-1)
 result    = clamp(exact_sum, -2^(OUT_W-1), 2^(OUT_W-1)-1)
 ```
 
+<p align="center">
+  <img src="assets/rtl-saturation-evidence.svg" width="100%" alt="Signed 16-bit saturation curve with six named deterministic RTL vectors">
+</p>
+
+I generate this boundary plot from the same named vectors and bit-exact Python
+model used by the self-checking RTL regression. It shows the wide accumulator
+value before clamping and the emitted 16-bit result, including exact limits,
+one-step overflow cases, and both signed extremes. It is arithmetic evidence,
+not a timing, area, or power result.
+
 Lane 0 occupies bits `[7:0]` of each packed input bus. Accumulation does not
 wrap with the default parameters; saturation happens once, after the final
 lane. See [Architecture](docs/architecture.md) for timing and width details.
@@ -80,7 +90,7 @@ lane. See [Architecture](docs/architecture.md) for timing and width details.
 | `model/dot_product_model.py` | Bit-exact reference arithmetic and packing |
 | `tb/tb_int8_dot_product.sv` | Self-checking ready/valid testbench |
 | `tools/run_regression.py` | Vector generation, compile, and simulation harness |
-| `tools/render_readme_assets.py` | Rebuilds and checks the README evidence figure |
+| `tools/render_readme_assets.py` | Rebuilds and checks both README evidence figures |
 | `tests/` | Python unit tests for the arithmetic contract |
 | `docs/` | Architecture and verification notes |
 

assets/rtl-saturation-evidence.svg

@@ -6,11 +6,12 @@
 import argparse
 from pathlib import Path
 
-from run_regression import corner_cases
+from run_regression import corner_cases, dot_product_int8
 
 
 ROOT = Path(__file__).resolve().parents[1]
 OUTPUT = ROOT / "assets" / "rtl-regression.svg"
+SATURATION_OUTPUT = ROOT / "assets" / "rtl-saturation-evidence.svg"
 SCENARIOS = ((1, 40), (8, 200), (17, 100))
 
 
@@ -94,21 +95,157 @@ def render() -> str:
 '''
 
 
+def render_saturation() -> str:
+    cases = {case.name: case for case in corner_cases(vec_len=8)}
+    names = (
+        "max_negative",
+        "one_below_negative_limit",
+        "exact_negative_limit",
+        "exact_positive_limit",
+        "one_above_positive_limit",
+        "max_positive",
+    )
+    expected = {
+        "max_negative": (-130_048, -32_768),
+        "one_below_negative_limit": (-32_769, -32_768),
+        "exact_negative_limit": (-32_768, -32_768),
+        "exact_positive_limit": (32_767, 32_767),
+        "one_above_positive_limit": (32_768, 32_767),
+        "max_positive": (129_032, 32_767),
+    }
+    labels = {
+        "max_negative": "max negative",
+        "one_below_negative_limit": "one below limit",
+        "exact_negative_limit": "exact negative limit",
+        "exact_positive_limit": "exact positive limit",
+        "one_above_positive_limit": "one above limit",
+        "max_positive": "max positive",
+    }
+
+    rows: list[tuple[str, int, int]] = []
+    for name in names:
+        case = cases[name]
+        exact_sum = sum(a * b for a, b in zip(case.vector_a, case.vector_b, strict=True))
+        emitted = dot_product_int8(case.vector_a, case.vector_b)
+        if (exact_sum, emitted) != expected[name]:
+            raise ValueError(f"named saturation vector drifted: {name}")
+        rows.append((name, exact_sum, emitted))
+
+    plot_left = 104
+    plot_top = 154
+    plot_width = 676
+    plot_height = 350
+    exact_min = -140_000
+    exact_max = 140_000
+    output_min = -32_768
+    output_max = 32_767
+
+    def map_x(value: int) -> float:
+        return plot_left + (value - exact_min) * plot_width / (exact_max - exact_min)
+
+    def map_y(value: int) -> float:
+        return plot_top + (output_max - value) * plot_height / (output_max - output_min)
+
+    points = []
+    table_rows = []
+    for index, (name, exact_sum, emitted) in enumerate(rows):
+        x = map_x(exact_sum)
+        y = map_y(emitted)
+        clamped = exact_sum != emitted
+        points.append(
+            f'''<circle cx="{x:.2f}" cy="{y:.2f}" r="8" fill="{"#e39a32" if clamped else "#2f827f"}" stroke="#fbf6ec" stroke-width="3">
+  <title>{labels[name]}: exact accumulator {exact_sum:,}, emitted {emitted:,}</title>
+</circle>'''
+        )
+        row_y = 180 + index * 55
+        table_rows.append(
+            f'''<text x="856" y="{row_y}" class="case">{labels[name]}</text>
+<text x="1160" y="{row_y}" text-anchor="end" class="numbers">{exact_sum:,} -&gt; {emitted:,}</text>
+<text x="1190" y="{row_y}" class="{"clamp" if clamped else "exact"}">{"CLAMP" if clamped else "EXACT"}</text>'''
+        )
+
+    lower_y = map_y(output_min)
+    upper_y = map_y(output_max)
+    lower_x = map_x(output_min)
+    upper_x = map_x(output_max)
+    zero_x = map_x(0)
+    zero_y = map_y(0)
+
+    return f'''<svg xmlns="http://www.w3.org/2000/svg" width="1280" height="650" viewBox="0 0 1280 650" role="img" aria-labelledby="sat-title sat-desc">
+  <title id="sat-title">Edge AI RTL Lab signed 16-bit saturation evidence</title>
+  <desc id="sat-desc">The clamp transfer curve and six named deterministic vectors show exact accumulator sums mapped to signed 16-bit outputs. Four vectors clamp and two remain exactly on the boundaries.</desc>
+  <style>
+    .title {{ font: 700 31px ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; fill: #13253b; }}
+    .subtitle,.axis,.footer {{ font: 15px system-ui, sans-serif; fill: #5f6974; }}
+    .axis {{ font-size: 13px; }}
+    .case {{ font: 600 14px system-ui, sans-serif; fill: #253c55; }}
+    .numbers {{ font: 600 14px ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; fill: #13253b; }}
+    .clamp {{ font: 700 12px ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; fill: #b66317; }}
+    .exact {{ font: 700 12px ui-monospace, SFMono-Regular, Menlo, Consolas, monospace; fill: #2f827f; }}
+    .grid {{ stroke: #e5dac5; stroke-width: 1; }}
+    .curve {{ fill: none; stroke: #203c5b; stroke-width: 5; stroke-linejoin: round; }}
+  </style>
+  <rect width="1280" height="650" rx="28" fill="#fbf6ec"/>
+  <path d="M0 92H1280" stroke="#e6dac3"/>
+  <text x="62" y="54" class="title">SIGNED SATURATION / NAMED RTL VECTORS</text>
+  <text x="62" y="80" class="subtitle">Exact wide accumulator -&gt; signed 16-bit output / VEC_LEN=8</text>
+
+  <g>
+    <path d="M{plot_left} {upper_y:.2f}H{plot_left + plot_width}" class="grid"/>
+    <path d="M{plot_left} {zero_y:.2f}H{plot_left + plot_width}" class="grid"/>
+    <path d="M{plot_left} {lower_y:.2f}H{plot_left + plot_width}" class="grid"/>
+    <path d="M{zero_x:.2f} {plot_top}V{plot_top + plot_height}" class="grid"/>
+    <polyline points="{plot_left},{lower_y:.2f} {lower_x:.2f},{lower_y:.2f} {upper_x:.2f},{upper_y:.2f} {plot_left + plot_width},{upper_y:.2f}" class="curve"/>
+    {"".join(points)}
+    <text x="{plot_left - 16}" y="{upper_y + 5:.2f}" text-anchor="end" class="axis">32,767</text>
+    <text x="{plot_left - 16}" y="{zero_y + 5:.2f}" text-anchor="end" class="axis">0</text>
+    <text x="{plot_left - 16}" y="{lower_y + 5:.2f}" text-anchor="end" class="axis">-32,768</text>
+    <text x="{plot_left}" y="536" text-anchor="middle" class="axis">-140k</text>
+    <text x="{lower_x:.2f}" y="536" text-anchor="middle" class="axis">-32,768</text>
+    <text x="{zero_x:.2f}" y="536" text-anchor="middle" class="axis">0</text>
+    <text x="{upper_x:.2f}" y="536" text-anchor="middle" class="axis">32,767</text>
+    <text x="{plot_left + plot_width}" y="536" text-anchor="middle" class="axis">140k</text>
+    <text x="{plot_left + plot_width / 2}" y="570" text-anchor="middle" class="subtitle">exact accumulator sum</text>
+    <text transform="translate(30 {plot_top + plot_height / 2}) rotate(-90)" text-anchor="middle" class="subtitle">emitted output</text>
+  </g>
+
+  <path d="M824 132V516" stroke="#e6dac3"/>
+  <text x="856" y="140" class="subtitle">named deterministic vectors</text>
+  {"".join(table_rows)}
+  <circle cx="868" cy="536" r="7" fill="#2f827f"/><text x="886" y="541" class="footer">exact boundary</text>
+  <circle cx="1026" cy="536" r="7" fill="#e39a32"/><text x="1044" y="541" class="footer">saturated</text>
+  <path d="M62 592H1218" stroke="#e6dac3"/>
+  <text x="62" y="622" class="footer">Derived from corner_cases(8) and the bit-exact Python model; the same named vectors feed the self-checking RTL regression. No timing, area, or power claim.</text>
+</svg>
+'''
+
+
 def main() -> None:
     parser = argparse.ArgumentParser(description=__doc__)
     parser.add_argument("--check", action="store_true", help="fail if the committed SVG is stale")
     args = parser.parse_args()
-    expected = render()
+    expected_outputs = {
+        OUTPUT: render(),
+        SATURATION_OUTPUT: render_saturation(),
+    }
 
     if args.check:
-        if not OUTPUT.exists() or OUTPUT.read_text(encoding="utf-8") != expected:
-            raise SystemExit(f"stale generated asset: {OUTPUT.relative_to(ROOT)}")
-        print(f"up to date: {OUTPUT.relative_to(ROOT)}")
+        stale = [
+            path
+            for path, expected in expected_outputs.items()
+            if not path.exists() or path.read_text(encoding="utf-8") != expected
+        ]
+        if stale:
+            paths = ", ".join(str(path.relative_to(ROOT)) for path in stale)
+            raise SystemExit(f"stale generated assets: {paths}")
+        for path in expected_outputs:
+            print(f"up to date: {path.relative_to(ROOT)}")
         return
 
-    OUTPUT.parent.mkdir(parents=True, exist_ok=True)
-    OUTPUT.write_text(expected, encoding="utf-8")
-    print(f"wrote {OUTPUT.relative_to(ROOT)}")
+    for path, expected in expected_outputs.items():
+        path.parent.mkdir(parents=True, exist_ok=True)
+        path.write_text(expected, encoding="utf-8")
+        print(f"wrote {path.relative_to(ROOT)}")
 
 
 if __name__ == "__main__":