svGolf

Golf scores on ASAP7, a predictive 7 nm library: never fabricated, and like sky130's score it counts no wires. sky130, a real 130 nm process, is the default. How ASAP7 is scored, and its quirks.

Tasks / matmul / record

Record 9fdf50f9ae02

on the Pareto frontieron the Pareto frontier scored at N = 4, W = 8, AccW = 32

Area

79 700.19µm²

79 700.1888 µm² exactly

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par
−8.6% smallermatmul_g1 · 87 173.61 µm²
on this page
smallest of 5 designs
cells
11 447
flops
802
repair
4 buffers, 0 tie cells
GE
19 022.828 extra

Performance · time

42 756ps

4 cycles × 10 689 ps; the period is the latest arrival at an output, or at a flip-flop's D plus setup, ideal clock

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
−0.1% fastermatmul_g1 · 42 784 ps
on this page
4th of 5 designs
Fmax-eq.
23.4 MHz derived
critical path
58 cells
unit depth
59 extra

Score · area × time

3 407 661µm²·ns

79 700.1888 µm² × 42 756 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
−8.6% bettermatmul_g1 · 3 729 636 µm²·ns
on this page
4th of 5 designs
board
layer 1, rank 4 of 4 by score
Pareto
on the front

On the board, of 1 other player: 0 beaten, 0 level, 1 trade off, 0 ahead.

how these numbers are measured and compared

Area: sky130 A0′, the repaired netlist.

Area, time and score are ranked (the leaderboard orders by the score); a number tagged extra, derived or research is shown, never ranked. Fmax-equivalent = 10⁶ / time in ps, for comparison with sites that quote Fmax.

The field is the ranked records of matmul's other players at this revision (1 player, 2 records), never the references, the baselines or a rejected design; each player counts once, at their best, and ties are exact at the recorded unit; advisory, recomputed at every build, never stored in a record and never used by the ranking.

On the board, another player is beaten when this design dominates every record of theirs, level when none of theirs is better and one is identical (the rest dominated), ahead when a record of theirs dominates this design, and a trade off otherwise (one of theirs better on one axis, worse on the other).

“On this page” and “Pareto” compare with the 5 designs of the area-time plot (1 reference and 4 submissions): not a ranking.

Area

1 216.745µm²

1 216.74474 µm² exactly

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par
−8.8% smallermatmul_g1 · 1 334.726 µm²
on this page
smallest of 5 designs
cells
12 889
flops
802
repair
1 buffer, 0 tie cells
GE
19 022.828 extra

Performance · time

5 992ps

4 cycles × 1 498 ps; the period is the latest arrival at an output, or at a flip-flop's D plus setup, ideal clock

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
−2.7% fastermatmul_g1 · 6 156 ps
on this page
4th of 5 designs
Fmax-eq.
166.9 MHz derived
unit depth
59 extra

Score · area × time

7291µm²·ns

1 216.74474 µm² × 5 992 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
−11.3% bettermatmul_g1 · 8217 µm²·ns
on this page
4th of 5 designs
board
layer 1, rank 4 of 4 by score
Pareto
on the front

On the board, of 1 other player: 0 beaten, 0 level, 1 trade off, 0 ahead.

how these numbers are measured and compared

Area: ASAP7 A0′ (asap7_a0_v1), the same scored netlist, each gate its least-area ASAP7 build, repaired by buffering. ASAP7: a predictive 7 nm library, never fabricated; no wires, like sky130's score (how ASAP7 is scored, and its quirks).

Area, time and score order this view's board (by the score); the records' ranked score is sky130's, the default view; a number tagged extra, derived or research is shown, never ranked. Fmax-equivalent = 10⁶ / time in ps, for comparison with sites that quote Fmax.

The field is the ranked records of matmul's other players at this revision (1 player, 2 records), never the references, the baselines or a rejected design; each player counts once, at their best, and ties are exact at the recorded unit; advisory, recomputed at every build, never stored in a record and never used by the ranking.

On the board, another player is beaten when this design dominates every record of theirs, level when none of theirs is better and one is identical (the rest dominated), ahead when a record of theirs dominates this design, and a trade off otherwise (one of theirs better on one axis, worse on the other).

“On this page” and “Pareto” compare with the 5 designs of the area-time plot (1 reference and 4 submissions): not a ranking.

The sources

f10.svdownload
// matmul G1 reference: N*N parallel multiply-accumulate units and one step counter k.
// After `start`, cycle k (k = 0 .. N-1) adds A[i][k]*B[k][j] (signed, wrapping at AccW bits) to
// C[i][j]; `done` rises after the N-th step and stays 1 (C held) until the next `start`.
// Flip-flops only (the FF-only profile): every register is written by nonblocking assignments in
// one always_ff, at a static window. `start` captures A and B into shift registers; each step
// shifts A by one entry and B by one row, so every select is static (no run-time part-select).
module matmul #(parameter int N = 4, parameter int W = 8, parameter int AccW = 32) (
  input  logic                 clk, rst,
  input  logic                 start,
  input  logic [N*N*W-1:0]     A, B,
  output logic                 done,
  output logic [N*N*AccW-1:0]  C
);
  logic [31:0]      k;
  logic             busy;
  logic [N*N*W-1:0] a_sh, b_sh;  // A >> k entries, B >> k rows: A[i][k] at row i's entry 0, B[k][j] at entry j

  // operand shifters and the step counter free-running: loaded on start, stepped in every other cycle
  always_ff @(posedge clk) begin
    if (start) begin
      a_sh <= A;
      b_sh <= B;
      k    <= 32'd0;
    end else begin
      a_sh <= a_sh >> W;
      b_sh <= b_sh >> (N*W);
      k    <= k + 32'd1;
    end
    if (rst) begin
      busy <= 1'b0;
      done <= 1'b0;
    end else if (start) begin
      busy <= 1'b1;
      done <= 1'b0;
    end else if (busy) begin
      if (k == N - 1) begin
        busy <= 1'b0;
        done <= 1'b1;
      end
    end
  end

  for (genvar i = 0; i < N; i++) begin : g_row
    for (genvar j = 0; j < N; j++) begin : g_col
      always_ff @(posedge clk)
        if (start)
          C[(i*N+j)*AccW +: AccW] <= '0;
        else
          // free-running accumulate: once the N steps are over b_sh has been shifted out (all zero),
          // so the product is 0 and C holds without a hold multiplexer
          C[(i*N+j)*AccW +: AccW] <= C[(i*N+j)*AccW +: AccW]
              + {{AccW{a_sh[i*N*W + W - 1]}}, a_sh[i*N*W +: W]}
              * {{AccW{b_sh[j*W + W - 1]}}, b_sh[j*W +: W]};
    end
  end
endmodule
S10.lean (722 code lines) 
-- svgolf-latency: 4
import Submission.Design
import LeanModels.Sv.Gen2
import LeanModels.Sv.Hier2Gen
import LeanModels.Sv.SeqProfile
import LeanModels.Sv.SeqFamily
import LeanModels.Sv.Known2
import LeanModels.Sv.Lib.BitVecArith
import LeanModels.Sv.CombViewArith
import LeanModels.Sv.Mono2
import SvGolf.SeqV2

/-!
# Variation of the `matmul` reference: free-running operand shifters, step counter and accumulators

`work/f10.sv` is the reference design (`N²` multiply-accumulate units, a step counter `k`, operand shift
registers `a_sh`, `b_sh`, latency `N`) with two architectural changes:
* the shift registers and `k` are not held while idle: they load on `start` and step in EVERY other cycle
  (reset included), so they need no hold multiplexer and `k` needs no reset;
* the accumulators have no `busy` gate either: each PE adds `a_sh[i][0] * b_sh[0][j]` in every cycle that
  has no `start`. After the `N` steps `b_sh` has been shifted out (all zero), so the product is 0 and `C`
  holds with no hold multiplexer: the `Fin` phase is the busy run's state at `t ≥ N` (`accC_ge`).
Only `busy` and `done` are controlled. The proof is the reference's with the control process, the PE
process and the phases changed:
1. `mmCtrl`, `ctrlQ`, `mmPE`, `peQ`: the processes and their evaluated updates.
2. `entry_ge`, `psum_ge`, `accC_ge`, `ctrl_idle`, `next_run`: the run past the `N` steps (`C` unchanged).
3. `next_idle`, `next_reset`: before the first start `C` accumulates whatever the registers hold (not claimed).
-/

namespace Submission

open LeanModels.Sv SvGolf

/-- The latency: `done` shows `N` snapshots after the start's. -/
def lat (N _W _AccW : Nat) : Nat := N

/-! ## 1. Agreement: the stages of `instantiate2` -/

/-- A 32-bit constant. -/
abbrev c32 (v : Int) : Expr2 := .lit (LVec.ofInt 32 v)

/-- `{{AccW{x[lo+W-1]}}, x[lo +: W]}`: entry `x[lo +: W]` sign-extended by `AccW` bits. -/
def sext (x : String) (AccW lo W : Nat) : Expr2 :=
  .concat #[.repl AccW (.concat #[.slice (.ident x) (lo + W - 1) 1]), .slice (.ident x) lo W]

/-- The PE at `(i, j)`: clear on `start`, else accumulate `a_sh[i][0] * b_sh[0][j]` in every cycle
(no `busy` gate: after the `N` steps `b_sh` is all zero, so the product is 0 and `C` holds). -/
def mmPE (N W AccW i j : Nat) : Process2 :=
  .alwaysFF "clk" (.ifStmt (.ident "start")
    (.nbaAssign (.slice "C" ((i * N + j) * AccW) AccW) (.lit (LVec.replicate AccW .l0)))
    (some (.nbaAssign (.slice "C" ((i * N + j) * AccW) AccW)
        (.resize AccW (.binary .add (.resize (AccW + W) (.slice (.ident "C") ((i * N + j) * AccW) AccW))
          (.binary .mul (sext "a_sh" AccW (i * N * W) W) (sext "b_sh" AccW (j * W) W)))))))

/-- A nonblocking write of a constant. -/
abbrev nb (n : String) (v : LVec) : Stmt2 := .nbaAssign (.ident n) (.lit v)

/-- The control: the operand shift registers and the step counter run free (loaded on `start`, stepped
in every other cycle); `busy` and `done` hold the handshake. -/
def mmCtrl (N W : Nat) : Process2 :=
  .alwaysFF "clk" (.block #[
    .ifStmt (.ident "start")
      (.block #[.nbaAssign (.ident "a_sh") (.ident "A"), .nbaAssign (.ident "b_sh") (.ident "B"),
        nb "k" (LVec.replicate 32 .l0)])
      (some (.block #[
        .nbaAssign (.ident "a_sh") (.binary (.shr false) (.ident "a_sh") (c32 W)),
        .nbaAssign (.ident "b_sh") (.binary (.shr false) (.ident "b_sh") (.binary .mul (c32 N) (c32 W))),
        .nbaAssign (.ident "k") (.binary .add (.ident "k") (c32 1))])),
    .ifStmt (.ident "rst")
      (.block #[nb "busy" ⟨#[.l0]⟩, nb "done" ⟨#[.l0]⟩])
      (some (.ifStmt (.ident "start")
        (.block #[nb "busy" ⟨#[.l1]⟩, nb "done" ⟨#[.l0]⟩])
        (some (.ifStmt (.ident "busy")
          (.block #[.ifStmt (.binary .eq (.ident "k") (.binary .sub (c32 N) (c32 1)))
            (.block #[nb "busy" ⟨#[.l0]⟩, nb "done" ⟨#[.l1]⟩]) none])
          none))))])

/-- The declarations, `A`/`B`/`a_sh`/`b_sh` at `wa` bits and `C` at `wc`. -/
def mmDecls (wa wc : Nat) : List Decl :=
  [{ name := "clk", width := 1, isInput := true }, { name := "rst", width := 1, isInput := true },
   { name := "start", width := 1, isInput := true }, { name := "A", width := wa, isInput := true },
   { name := "B", width := wa, isInput := true }, { name := "done", width := 1, isOutput := true },
   { name := "C", width := wc, isOutput := true }, { name := "k", width := 32 },
   { name := "busy", width := 1 }, { name := "a_sh", width := wa }, { name := "b_sh", width := wa }]

/-- The PEs, row-major. -/
def mmPEs (N W AccW : Nat) : List Process2 :=
  (List.range N).flatMap fun i => (List.range N).map fun j => mmPE N W AccW i j

def mmD (N W AccW : Nat) : Design2 where
  name := "matmul"
  decls := (mmDecls (N * N * W) (N * N * AccW)).toArray
  processes := (mmCtrl N W :: mmPEs N W AccW).toArray

/-! ### The stages of `instantiate2` -/

def mmScope (N W AccW : Int) : IEnv :=
  { vals := [("N", N), ("W", W), ("AccW", AccW)], pwidths := [("N", 32), ("W", 32), ("AccW", 32)] }

def mmEnv (N W AccW : Int) : IEnv :=
  { mmScope N W AccW with dims := dimTable (mmScope N W AccW) design.pdesign.decls }

theorem mm_paramEnv (N W AccW : Int) :
    design.pdesign.paramEnv2 [N, W, AccW] = .ok (mmEnv N W AccW) := rfl

def mmElems : List (String × Nat) :=
  ["clk", "rst", "start", "A", "B", "done", "C", "k", "busy", "a_sh", "b_sh"].map (·, 1)

theorem mm_decls (N W AccW : Int) :
    buildDecls (mmEnv N W AccW) design.pdesign.decls =
      .ok (mmDecls ((N * N * W - 1).natAbs + 1) ((N * N * AccW - 1).natAbs + 1)) := by
  simp [design.pdesign, buildDecls, instDecl, PType.width_packed_cons, PDim.width, evalInt,
    mmEnv, mmScope, List.lookup, mmDecls, Gen2.except_ok_bind]

theorem mm_elems (N W AccW : Int) : buildElems (mmEnv N W AccW) design.pdesign.decls = .ok mmElems := by
  simp [design.pdesign, buildElems, PType.width_packed_cons, PDim.width, evalInt, mmEnv,
    mmScope, List.lookup, mmElems, Gen2.except_ok_bind]

/-- The instantiation environment. -/
abbrev mmE (N W AccW : Nat) : IEnv :=
  (mmEnv N W AccW).withDecls (mmDecls (N * N * W) (N * N * AccW))

theorem mm_ctrl (N W AccW : Nat) :
    design.pdesign.processes.map (instProcess2 (mmE N W AccW) mmElems) = [mmCtrl N W] := by
  sv2_inst_simp [instStmt2, instStmts2, design.pdesign, mmEnv, mmScope, mmDecls, mmElems, mmCtrl,
    dimTable, dimTableStep, PType.width_packed_cons, PDim.width, ctxOpWidth2, rigidMax2,
    PExpr.ctxPropagates, PExpr.constLeaf, PExpr.negGenvarWidened, LVec.width, divOperandWidth2,
    instDivOperand2, fitDivOperand2]
  try and_intros
  all_goals first | rfl | decide

/-- The PE template (the process inside `g_row`/`g_col`). -/
def peT : PProcess :=
  match design.pdesign.generates with
  | [.genFor _ _ _ _ _ _ [.genFor _ _ _ _ _ _ [.process p]]] => p
  | _ => .alwaysFF "" (.block [])

/-- The `sv2_inst_simp` set of the PE template (with the window facts in scope). `instExpr2` tries
to constant-fold the `*` of the two sign-extending concatenations, and the fold must reduce to its
error; `sv2_inst_simp`'s default set carries the constant folder (`ctype`/`evalAt` and their
workers), so of the evaluators only `evalSized`, which is outside that set, is named here. -/
macro "pe_simp" : tactic => `(tactic| sv2_inst_simp [peT, evalSized, Gen2.except_pure,
  Lib.min_add_sub_one_self, Lib.max_add_sub_one_self, Lib.add_sub_one_sub_add_one, instStmt2, design.pdesign,
  mmEnv, mmScope, mmDecls, mmElems, mmPE, sext,
  dimTable, dimTableStep, PType.width_packed_cons, PDim.width, ctxOpWidth2, rigidMax2,
  PExpr.constLeaf, PExpr.negGenvarWidened, LVec.width, *])

theorem pe_inst (N W AccW i j : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) (hi : i < N)
    (hj : j < N) :
    instProcess2 (((mmE N W AccW).bindVal "i" i).bindVal "j" j) mmElems peT =
      mmPE N W AccW i j := by
  have pW := Nat.mul_pos (Nat.mul_pos hN hN) hW
  have pA := Nat.mul_pos (Nat.mul_pos hN hN) hA
  have hW0 : (0 : Int) < W := by omega
  have hA0 : (0 : Int) < AccW := by omega
  have hNW : (1 : Int) ≤ N * N * W := by rw [← Int.natCast_mul, ← Int.natCast_mul]; omega
  have hNA : (1 : Int) ≤ N * N * AccW := by rw [← Int.natCast_mul, ← Int.natCast_mul]; omega
  have hcA : ((N : Int) * N * W - 1).natAbs + 1 = N * N * W := by
    rw [← Int.natCast_mul, ← Int.natCast_mul]; exact Lib.natAbs_sub_one_add_one pW
  have hcC : ((N : Int) * N * AccW - 1).natAbs + 1 = N * N * AccW := by
    rw [← Int.natCast_mul, ← Int.natCast_mul]; exact Lib.natAbs_sub_one_add_one pA
  have hC := Lib.window_bounds_of_natCast (((i : Int) * N + j) * AccW) (N * N * AccW)
    (Lib.rowMajor_window_le (w := AccW) hi hj) hA (by simp) (by simp)
  have ha := Lib.window_bounds_of_natCast ((i : Int) * N * W) (N * N * W)
    (Lib.rowMajor_window_le (N := N) (w := W) (j := 0) hi (by omega)) hW (by simp) (by simp)
  have hb := Lib.window_bounds_of_natCast ((j : Int) * W) (N * N * W)
    (Lib.rowMajor_window_le (M := N) (w := W) (i := 0) (by omega) hj) hW (by simp) (by simp)
  have hA1 : 0 < AccW := hA
  have hW1 : 0 < W := hW
  have hWne : ¬ W = 0 := by omega
  have hmode : (PartMode.up == PartMode.range) = false := rfl
  have hlt1 : ¬ AccW + W < AccW := by omega
  have hle1 : ¬ AccW + W ≤ AccW := by omega
  pe_simp
  -- `simp` cannot use `instExpr2`'s `resize` equation (measured): unfold it by hand.
  repeat (unfold instExpr2; pe_simp)

/-- `for (g = 0; g < N; g++) body`. -/
def genN (lbl g : String) (body : List GenItem) : GenItem :=
  .genFor (some lbl) g (.int 0) (.binary .slt (.genvarRef g) (.paramRef "N" none))
    (.unary .inc (.genvarRef g)) (some 4) body

theorem mm_gens_src : design.pdesign.generates = [genN "g_row" "i" [genN "g_col" "j" ([peT].map .process)]] :=
  rfl

/-- **The nested generate expands to the row-major PEs** (`mul2d_pp_expand`'s route). -/
theorem mm_gens (N W AccW F : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) (hF : N < F) :
    expandList2 (mmE N W AccW) mmElems F design.pdesign.generates = .ok (mmPEs N W AccW) := by
  have hNv : (mmE N W AccW).vals.lookup "N" = some (N : Int) := rfl
  rw [mm_gens_src]
  apply expandList2_singleton_ok
  rw [genN, GenItem.expand2_genFor_ascending_flatMap (N := (N : Int))
      (f := fun v => (intRange 0 N).flatMap fun w =>
        [peT].map (instProcess2 (((mmE N W AccW).bindVal "i" v).bindVal "j" w) mmElems))
      (evalInt_int 0) (fun _ => isInt_paramRef_of (by rw [vals_lookup_bindVal_ne _ (by decide), hNv]))
      (fun _ => evalInt_paramRef_of (by rw [vals_lookup_bindVal_ne _ (by decide), hNv])) (by simpa using hF)]
  · simp only [intRange_zero, List.flatMap_map, Int.sub_zero, Int.toNat_natCast, List.map_cons,
      List.map_nil, Gen2.flatMap_singleton_map, mmPEs]
    congr 1
    simp only [List.flatMap_def]
    congr 1
    refine List.map_congr_left fun i hi => List.map_congr_left fun j hj => ?_
    exact pe_inst N W AccW i j hN hW hA (List.mem_range.mp hi) (List.mem_range.mp hj)
  · intro v _ _
    apply expandList2_singleton_ok
    have hv : ((mmE N W AccW).bindVal "i" v).vals.lookup "N" = some (N : Int) := by
      simp [IEnv.bindVal, List.lookup, hNv]
    rw [genN, GenItem.expand2_genFor_ascending_processes (N := (N : Int)) (evalInt_int 0)
      (fun _ => isInt_paramRef_of (by rw [vals_lookup_bindVal_ne _ (by decide), hv]))
      (fun _ => evalInt_paramRef_of (by rw [vals_lookup_bindVal_ne _ (by decide), hv]))
      (by simpa using hF)]
    simp

theorem mm_instantiate2 (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    design.pdesign.instantiate2 [(N : Int), W, AccW] (PDesign.surfaceFuel [(N : Int), W, AccW]) =
      .ok (design.pdesign.assemble2 (mmEnv N W AccW) (mmDecls (N * N * W) (N * N * AccW)) mmElems
        (mmPEs N W AccW)) := by
  have hd := mm_decls N W AccW
  rw [← Int.natCast_mul N N, ← Int.natCast_mul (N * N) W,
    Lib.natAbs_sub_one_add_one (Nat.mul_pos (Nat.mul_pos hN hN) hW), ← Int.natCast_mul (N * N) AccW,
    Lib.natAbs_sub_one_add_one (Nat.mul_pos (Nat.mul_pos hN hN) hA)] at hd
  refine PDesign.instantiate2_of_ok rfl (mm_paramEnv _ _ _) hd (mm_elems _ _ _)
    (mm_gens N W AccW _ hN hW hA ?_)
  simp only [PDesign.surfaceFuel, List.map, List.sum_cons, List.sum_nil, Int.natAbs_natCast]
  exact Nat.lt_of_lt_of_le (Nat.lt_of_lt_of_le (by omega) (Nat.le_mul_self _)) (Nat.le_add_right _ _)

theorem mm_processes (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    (design.pdesign.instantiateD2 [(N : Int), W, AccW]).processes.toList =
      mmCtrl N W :: mmPEs N W AccW := by
  rw [PDesign.instantiateD2_of_ok (mm_instantiate2 N W AccW hN hW hA), PDesign.assemble2_processes,
    mm_ctrl]
  simp [design.pdesign]

/-- Two PEs write disjoint windows of `C`. -/
theorem pe_disj {N W AccW i j i' j' : Nat} (h : i * N + j < i' * N + j') :
    ∀ a ∈ (mmPE N W AccW i j).procWins, ∀ b ∈ (mmPE N W AccW i' j').procWins,
      a.overlaps b = false := by
  have := rowMajor_le (K := AccW) h
  simp [mmPE, Process2.procWins, Stmt2.drvWins, Stmt2.drvWinsOpt, Lhs2.drvWins]
  omega

theorem mm_pe_mem {N W AccW : Nat} {p : Process2} (hp : p ∈ mmPEs N W AccW) :
    ∃ i j, p = mmPE N W AccW i j := by
  simp only [mmPEs, List.mem_flatMap, List.mem_map, List.mem_range] at hp
  obtain ⟨i, -, j, -, rfl⟩ := hp
  exact ⟨i, j, rfl⟩

/-- The control and the PEs drive pairwise disjoint windows. -/
theorem mm_pairwise (N W AccW : Nat) : (mmCtrl N W :: mmPEs N W AccW).Pairwise
    fun p q => ∀ a ∈ p.procWins, ∀ b ∈ q.procWins, a.overlaps b = false := by
  refine List.Pairwise.cons (fun p hp => ?_) (pairwise_flatMap_range (fun i _ => ?_) ?_)
  · obtain ⟨i, j, rfl⟩ := mm_pe_mem hp
    simp [mmCtrl, mmPE, Process2.procWins, Stmt2.drvWins, Stmt2.drvWinsOpt, Stmt2.drvWinsList,
      Lhs2.drvWins]
  · exact List.pairwise_map.mpr (List.pairwise_lt_range.imp_of_mem fun _ _ h => pe_disj (by omega))
  · intro i i' hii _ a ha b hb
    simp only [List.mem_map, List.mem_range] at ha hb
    obtain ⟨j, hj, rfl⟩ := ha
    obtain ⟨j', -, rfl⟩ := hb
    exact pe_disj (by have := rowMajor_le (K := N) hii; omega)

theorem mm_driversOk (N W AccW : Nat) :
    driversOk design.pdesign.declNames design.pdesign.inputNames (mmCtrl N W :: mmPEs N W AccW) = true := by
  apply driversOk_of_ff ?_ ?_ (mm_pairwise N W AccW)
  · intro p hp
    rcases List.mem_cons.mp hp with rfl | hp
    · exact ⟨_, _, rfl⟩
    · obtain ⟨i, j, rfl⟩ := mm_pe_mem hp; exact ⟨_, _, rfl⟩
  · simp only [List.mem_flatMap, List.mem_cons]
    rintro n ⟨p, hp | hp, hn⟩
    all_goals first | subst hp | obtain ⟨i, j, rfl⟩ := mm_pe_mem hp
    all_goals revert n; simp [mmCtrl, mmPE, Process2.procWrites, Process2.procWins, Stmt2.drvWins,
      Stmt2.drvWinsOpt, Stmt2.drvWinsList, Lhs2.drvWins]; all_goals decide

/-- **The loaded family is `mmD`**, at every `(N, W, AccW)` with positive parameters. -/
theorem mm_sem_eq (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    design.sem N W AccW = mmD N W AccW := by
  have h1 : design.sem N W AccW = design.pdesign.instantiateD2 [(N : Int), W, AccW] := by
    show design.pdesign.instantiateGD2 [(N : Int), W, AccW] = _
    exact PDesign.instantiateGD2_of_driversOk (by rw [mm_processes N W AccW hN hW hA]; exact mm_driversOk N W AccW)
  rw [h1, PDesign.instantiateD2_of_ok (mm_instantiate2 N W AccW hN hW hA)]
  simp only [PDesign.assemble2, mm_ctrl, mmD]
  simp [design.pdesign]

/-! ## 2. G0's clock step for the loaded family, at every `(N, W, AccW)` -/

/-- **`mmD` is in G0's decidable FF-only profile at every `(N, W, AccW)`** (symbolic, not `rfl`). -/
theorem mm_profile (N W AccW : Nat) : (mmD N W AccW).ffOnlyProfileB = true := by
  simp only [Design2.ffOnlyProfileB, Bool.and_eq_true]
  refine ⟨?_, ffDisjB_of_pairwise (by simpa [mmD] using mm_pairwise N W AccW)⟩
  simp [mmD, mmCtrl, mmPEs, mmPE, nb, List.all_flatMap, List.all_map, Stmt2.nbaOnly, Stmt2.optNbaOnly,
    Stmt2.listNbaOnly, Stmt2.nbaStaticB, Stmt2.optNbaStaticB, Stmt2.listNbaStaticB, Lhs2.window?,
    Design2.declWidth, Design2.inputNames, Stmt2.drvWins, Stmt2.drvWinsOpt, Stmt2.drvWinsList,
    Lhs2.drvWins, mmDecls]

/-- The 11 signals of `mmD`, in declaration order. -/
def MS (ck r s a b dn c k bz ash bsh : LVec) : SvState :=
  [("clk", ck), ("rst", r), ("start", s), ("A", a), ("B", b), ("done", dn), ("C", c), ("k", k),
    ("busy", bz), ("a_sh", ash), ("b_sh", bsh)]

theorem apply_mm (N W AccW : Nat) (e : SvState) (ck r s a b dn c k bz ash bsh : LVec) :
    applyInputs2 (mmD N W AccW) e (MS ck r s a b dn c k bz ash bsh) =
      MS (appIn e "clk" ck) (appIn e "rst" r) (appIn e "start" s) (appIn e "A" a) (appIn e "B" b)
        dn c k bz ash bsh := by
  unfold applyInputs2
  rw [← Array.foldl_toList]
  cases h1 : SvState.lookup e "clk" <;> cases h2 : SvState.lookup e "rst" <;>
    cases h3 : SvState.lookup e "start" <;> cases h4 : SvState.lookup e "A" <;>
    cases h5 : SvState.lookup e "B" <;>
    simp [mmD, mmDecls, MS, appIn, h1, h2, h3, h4, h5, SvState.set]

/-- A nonblocking write of `v` to the whole of `n` (old value `old`). -/
abbrev wr (n : String) (old v : LVec) : String × Nat × LVec := (n, 0, v.resizeU old.width)

/-- The control's updates, from the pre-edge values: the free-running registers, then the handshake. -/
def ctrlQ (N W : Nat) (r s a b dn k bz ash bsh : LVec) : NbaQueue2 :=
  (if s.condTrue then [wr "a_sh" ash a, wr "b_sh" bsh b, wr "k" k (LVec.replicate 32 .l0)]
   else [wr "a_sh" ash (ash.shr (LVec.ofInt 32 (W : Int))),
     wr "b_sh" bsh (bsh.shr ((LVec.ofInt 32 (N : Int)).mul (LVec.ofInt 32 (W : Int)))),
     wr "k" k (k.add (LVec.ofInt 32 1))]) ++
  (if r.condTrue then [wr "busy" bz ⟨#[.l0]⟩, wr "done" dn ⟨#[.l0]⟩]
   else if s.condTrue then [wr "busy" bz ⟨#[.l1]⟩, wr "done" dn ⟨#[.l0]⟩]
   else if bz.condTrue then
     if (LVec.ofLogic (k.eqLogical ((LVec.ofInt 32 (N : Int)).sub (LVec.ofInt 32 1)))).condTrue then
       [wr "busy" bz ⟨#[.l0]⟩, wr "done" dn ⟨#[.l1]⟩]
     else []
   else [])

/-- `{{AccW{v[lo+W-1]}}, v[lo +: W]}`, evaluated. -/
def sxv (v : LVec) (AccW lo W : Nat) : LVec :=
  LVec.concatMany #[LVec.replVec AccW (LVec.concatMany #[v.extract (lo + W - 1) 1]), v.extract lo W]

/-- The new accumulator `(i, j)` of a busy cycle, evaluated. -/
def peV (N W AccW i j : Nat) (c ash bsh : LVec) : LVec :=
  (((c.extract ((i * N + j) * AccW) AccW).resizeU (AccW + W)).add
    ((sxv ash AccW (i * N * W) W).mul (sxv bsh AccW (j * W) W))).resizeU AccW

/-- The PE's update, from the pre-edge values. -/
def peQ (N W AccW : Nat) (s _bz c ash bsh : LVec) (i j : Nat) : NbaQueue2 :=
  if s.condTrue then [("C", (i * N + j) * AccW, (LVec.replicate AccW .l0).resizeU AccW)]
  else [("C", (i * N + j) * AccW, (peV N W AccW i j c ash bsh).resizeU AccW)]

theorem ctrl_run (N W F : Nat) (hF : 30 ≤ F) (ck r s a b dn c k bz ash bsh : LVec) :
    runEdgeProcess2 F (MS ck r s a b dn c k bz ash bsh) [] (mmCtrl N W) =
      .ok (MS ck r s a b dn c k bz ash bsh, ctrlQ N W r s a b dn k bz ash bsh) := by
  obtain ⟨f, rfl⟩ : ∃ f, F = f + 30 := ⟨F - 30, by omega⟩
  unfold ctrlQ
  by_cases h1 : r.condTrue = true <;> by_cases h2 : s.condTrue = true <;>
    by_cases h3 : bz.condTrue = true <;>
    by_cases h4 : (LVec.ofLogic (k.eqLogical ((LVec.ofInt 32 (N : Int)).sub (LVec.ofInt 32 1)))).condTrue = true <;>
    simp [mmCtrl, nb, c32, runEdgeProcess2, execStmt2, execStmts2, evalExpr2, resolveLhs2, readSignal, MS,
      SvState.lookup, evalBinOp, wr, h1, h2, h3, h4]

theorem pe_run (N W AccW i j F : Nat) (hF : 30 ≤ F) (ck r s a b dn c k bz ash bsh : LVec) :
    runEdgeProcess2 F (MS ck r s a b dn c k bz ash bsh) [] (mmPE N W AccW i j) =
      .ok (MS ck r s a b dn c k bz ash bsh, peQ N W AccW s bz c ash bsh i j) := by
  obtain ⟨f, rfl⟩ : ∃ f, F = f + 30 := ⟨F - 30, by omega⟩
  unfold peQ
  by_cases h1 : s.condTrue = true <;> by_cases h2 : bz.condTrue = true <;>
    simp [mmPE, sext, runEdgeProcess2, execStmt2, evalExpr2, evalExprs2, resolveLhs2, readSignal, MS,
      SvState.lookup, evalBinOp, peV, sxv, h1, h2]

/-- One cycle's next state, from the pre-edge (inputs applied) values. -/
def mmNext (N W AccW : Nat) (ck r s a b dn c k bz ash bsh : LVec) : SvState :=
  commitNba2 (MS ck r s a b dn c k bz ash bsh) (ctrlQ N W r s a b dn k bz ash bsh ++
    (List.range N).flatMap fun i => (List.range N).flatMap (peQ N W AccW s bz c ash bsh i))

/-- **One cycle of the loaded design is G0's clock step**, evaluated (any schedule, any stimulus
entry, any state of the design's shape, every fuel from 30). -/
theorem mm_cycle (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) (σ : ScheduleOracle)
    (e : SvState) (ck r s a b dn c k bz ash bsh : LVec) (kk F : Nat) (hF : 30 ≤ F) :
    cycleStep2 (design.sem N W AccW) σ F e (MS ck r s a b dn c k bz ash bsh) kk =
      .ok (mmNext N W AccW (appIn e "clk" ck) (appIn e "rst" r) (appIn e "start" s) (appIn e "A" a)
        (appIn e "B" b) dn c k bz ash bsh, kk + 3) := by
  have hedge : ∀ p ∈ (mmD N W AccW).processes.toList, p.isEdgePhase = true := by
    intro p hp
    have hm : p ∈ mmCtrl N W :: mmPEs N W AccW := by simpa [mmD] using hp
    rcases List.mem_cons.mp hm with rfl | hm
    · rfl
    · obtain ⟨i, j, rfl⟩ := mm_pe_mem hm; rfl
  rw [mm_sem_eq N W AccW hN hW hA, cycleStep2_profile (mm_profile N W AccW) σ e _ kk ?_ ?_ (by omega),
    apply_mm, clockStep, flatMap_ffUpd F _ hedge]
  · simp only [mmD, List.toList_toArray, List.flatMap_cons, ctrl_run N W F hF, mmPEs, List.flatMap_assoc,
      List.flatMap_map, pe_run N W AccW _ _ F hF, mmNext]
  · intro i p hp
    rw [apply_mm]
    have hm : p ∈ mmCtrl N W :: mmPEs N W AccW :=
      List.mem_of_getElem? (by simpa [mmD] using hp : (mmCtrl N W :: mmPEs N W AccW)[i]? = some p)
    rcases List.mem_cons.mp hm with rfl | hm
    · exact ⟨_, ctrl_run N W F hF _ _ _ _ _ _ _ _ _ _ _⟩
    · obtain ⟨i, j, rfl⟩ := mm_pe_mem hm
      exact ⟨_, pe_run N W AccW i j F hF _ _ _ _ _ _ _ _ _ _ _⟩
  · rw [apply_mm]; simp [MS]

/-! ## 3. The busy cycle on known values: the invariant on `k` -/

attribute [local simp] condTrue_knownBit

/-- `Σ_{k' < t} A[i][k']·B[k'][j]` in the integers (`Tasks.Matmul.dot` at `t = N`). -/
def psum (N W : Nat) {n : Nat} (A B : BitVec n) (t i j : Nat) : Int :=
  (List.range t).foldl (fun acc k =>
    acc + Tasks.Matmul.entry W A (i * N + k) * Tasks.Matmul.entry W B (k * N + j)) 0

/-- The accumulators after `t` busy cycles: entry `(i, j)` is `psum t i j` mod `2^AccW`. -/
def accC (N W AccW : Nat) {n : Nat} (A B : BitVec n) (t : Nat) : LVec :=
  LVec.ofBitVec (packBV AccW (N * N) fun r => BitVec.ofInt AccW (psum N W A B t (r / N) (r % N)))

theorem psum_succ (N W : Nat) {n : Nat} (A B : BitVec n) (t i j : Nat) : psum N W A B (t + 1) i j =
    psum N W A B t i j + Tasks.Matmul.entry W A (i * N + t) * Tasks.Matmul.entry W B (t * N + j) := by
  simp [psum, List.range_succ, List.foldl_append]

/-- **PE `(i, j)` in a busy cycle** adds `A[i][t]·B[t][j]` to its accumulator. -/
theorem pe_step {N W AccW : Nat} (hW : 1 ≤ W) (A B : BitVec (N * N * W)) {t i j : Nat} (hi : i < N)
    (hj : j < N) (bz : LVec) : peQ N W AccW (knownBit false) bz (accC N W AccW A B t) (.ofBitVec (A >>> (t * W)))
      (.ofBitVec (B >>> (t * (N * W)))) i j = [("C", (i * N + j) * AccW,
        .ofBitVec (BitVec.ofInt AccW (psum N W A B (t + 1) ((i * N + j) / N) ((i * N + j) % N))))] := by
  have hd : (i * N + j) / N = i := by
    rw [Nat.add_comm, Nat.add_mul_div_right _ _ (by omega), Nat.div_eq_of_lt hj, Nat.zero_add]
  have hm : (i * N + j) % N = j := by rw [Nat.add_comm, Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt hj]
  have hr : i * N + j < N * N := by have := Lib.rowMajor_window_le (w := 1) hi hj; simp at this; omega
  have ha : i * N * W + W ≤ N * N * W := by
    have := Lib.rowMajor_window_le (N := N) (w := W) (j := 0) hi (by omega); simpa using this
  have hb : j * W + W ≤ N * N * W := by
    have := Lib.rowMajor_window_le (M := N) (w := W) (i := 0) (by omega) hj; simpa using this
  have hc := Lib.rowMajor_window_le (w := AccW) hi hj
  have e1 : t * W + i * N * W = (i * N + t) * W := by rw [Nat.add_mul, Nat.add_comm]
  have e2 : t * (N * W) + j * W = (t * N + j) * W := by rw [Nat.add_mul, Nat.mul_assoc]
  simp (disch := omega) only [peQ, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte, peV, sxv, accC,
    LVec.extract_ofBitVec, extractLsb'_packBV, hd, hm, LVec.concatMany_singleton, LVec.concatMany_cons_cons,
    LVec.replVec_ofBitVec, LVec.concat_ofBitVec, LVec.ofBitVec_replicate_append_eq_signExtend hW,
    LVec.mul_ofBitVec, LVec.resizeU_ofBitVec, LVec.add_ofBitVec, BitVec.setWidth_eq, Lib.setWidth_add_mul_signExtend,
    Lib.extractLsb'_ushiftRight, e1, e2, psum_succ, BitVec.ofInt_add, Tasks.Matmul.entry]

/-! ## 4. The spec's arithmetic: `product` is the packed vector of the wrapped dot products -/

theorem product_eq (N W AccW : Nat) {n : Nat} (a b : BitVec n) : Tasks.Matmul.product N W AccW a b =
    packBV AccW (N * N) fun r => BitVec.ofInt AccW (Tasks.Matmul.dot N W a b (r / N) (r % N)) :=
  (packBV_eq_ofNat ..).symm

/-- After `N` busy cycles the accumulators hold the product (`psum N` is `dot`). -/
theorem accC_N (N W AccW : Nat) {n : Nat} (A B : BitVec n) :
    accC N W AccW A B N = LVec.ofBitVec (Tasks.Matmul.product N W AccW A B) := by
  rw [product_eq]; rfl

/-- Entries past the end of a flat vector are zero. -/
theorem entry_ge {W n : Nat} (x : BitVec n) {idx : Nat} (h : n ≤ idx * W) : Tasks.Matmul.entry W x idx = 0 := by
  have h0 : x.extractLsb' (idx * W) W = 0#W := by
    apply BitVec.eq_of_getLsbD_eq
    intro i hi
    simp only [BitVec.getLsbD_extractLsb', hi, decide_true, Bool.true_and, BitVec.getLsbD_zero]
    first | exact BitVec.getLsbD_of_ge x _ (by omega) | exact BitVec.getLsbD_ge x _ (by omega)
  simp [Tasks.Matmul.entry, h0]

/-- Past `N` steps the partial sums do not change: `B` has only `N` rows. -/
theorem psum_ge (N W : Nat) (A B : BitVec (N * N * W)) (i j : Nat) : ∀ t, N ≤ t →
    psum N W A B t i j = psum N W A B N i j := by
  intro t ht
  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le ht
  induction d with
  | zero => rfl
  | succ d ih =>
    have h1 : N * N ≤ (N + d) * N + j :=
      Nat.le_trans (Nat.mul_le_mul (Nat.le_add_right N d) (Nat.le_refl N)) (Nat.le_add_right _ _)
    have h2 : N * N * W ≤ ((N + d) * N + j) * W := Nat.mul_le_mul_right W h1
    show psum N W A B (N + d + 1) i j = _
    rw [psum_succ, ih (Nat.le_add_right _ _), entry_ge B h2]
    simp

theorem accC_ge (N W AccW : Nat) (A B : BitVec (N * N * W)) {t : Nat} (ht : N ≤ t) :
    accC N W AccW A B t = accC N W AccW A B N := by
  have h : ∀ i j, psum N W A B t i j = psum N W A B N i j := fun i j => psum_ge N W A B i j t ht
  simp only [accC, h]

/-! ## 5. The registers through a cycle: the commit, then the invariant on `k` -/

section commit
variable {ck r s a b dn c k bz ash bsh : LVec} {lo : Nat} {v : LVec}
theorem nb_busy : nbaStep (MS ck r s a b dn c k bz ash bsh) ("busy", lo, v) =
    MS ck r s a b dn c k (bz.insertAt lo v) ash bsh := by simp [nbaStep, MS, SvState.lookup, SvState.set]
theorem nb_done : nbaStep (MS ck r s a b dn c k bz ash bsh) ("done", lo, v) =
    MS ck r s a b (dn.insertAt lo v) c k bz ash bsh := by simp [nbaStep, MS, SvState.lookup, SvState.set]
theorem nb_k : nbaStep (MS ck r s a b dn c k bz ash bsh) ("k", lo, v) =
    MS ck r s a b dn c (k.insertAt lo v) bz ash bsh := by simp [nbaStep, MS, SvState.lookup, SvState.set]
theorem nb_ash : nbaStep (MS ck r s a b dn c k bz ash bsh) ("a_sh", lo, v) =
    MS ck r s a b dn c k bz (ash.insertAt lo v) bsh := by simp [nbaStep, MS, SvState.lookup, SvState.set]
theorem nb_bsh : nbaStep (MS ck r s a b dn c k bz ash bsh) ("b_sh", lo, v) =
    MS ck r s a b dn c k bz ash (bsh.insertAt lo v) := by simp [nbaStep, MS, SvState.lookup, SvState.set]
end commit

/-- Committing writes of `C` only. -/
theorem commit_C {ck r s a b dn k bz ash bsh : LVec} : ∀ {q : NbaQueue2}, (∀ u ∈ q, u.1 = "C") → ∀ c,
    commitNba2 (MS ck r s a b dn c k bz ash bsh) q =
      MS ck r s a b dn (q.foldl (fun acc u => acc.insertAt u.2.1 u.2.2) c) k bz ash bsh
  | [], _, _ => rfl
  | ⟨n, lo, v⟩ :: q, h, c => by
    obtain rfl : n = "C" := h _ List.mem_cons_self
    rw [commitNba2_cons, List.foldl_cons, ← commit_C (fun u hu => h u (List.mem_cons_of_mem _ hu))]
    congr 1

/-- The PEs' updates, row-major, when PE `(i, j)` writes window `i·N + j` with `g (i·N + j)`. -/
theorem rowMajor_map {N AccW : Nat} {q : Nat → Nat → NbaQueue2} (g : Nat → LVec)
    (h : ∀ i j, i < N → j < N → q i j = [("C", (i * N + j) * AccW, g (i * N + j))]) :
    ((List.range N).flatMap fun i => (List.range N).flatMap (q i)) =
      (List.range (N * N)).map fun r => ("C", r * AccW, g r) := by
  suffices ∀ M, M ≤ N → ((List.range M).flatMap fun i => (List.range N).flatMap (q i)) =
      (List.range (M * N)).map (fun r => ("C", r * AccW, g r)) from this N (Nat.le_refl _)
  intro M; induction M with
  | zero => intro _; simp
  | succ M ih =>
    intro hM
    rw [List.range_succ, List.flatMap_append, ih (by omega), Nat.succ_mul, List.range_add,
      List.map_append, List.map_map]
    simp only [List.flatMap_cons, List.flatMap_nil, List.append_nil]
    rw [CombView.flatMap_congr' fun j hj => h M j (by omega) (List.mem_range.mp hj)]
    congr 1
    induction (List.range N) with
    | nil => rfl
    | cons a l ih' => rw [List.flatMap_cons, ih']; rfl

theorem commit_map {ck r s a b dn k bz ash bsh : LVec} (AccW : Nat) (g : Nat → LVec) (n : Nat) (c : LVec) :
    commitNba2 (MS ck r s a b dn c k bz ash bsh) ((List.range n).map fun r => ("C", r * AccW, g r)) =
      MS ck r s a b dn (LVec.insertEntries AccW g n c) k bz ash bsh := by
  rw [commit_C (by simp), List.foldl_map]; rfl

/-- The control in a busy cycle `t < N`: `k` and the shift registers step; the last one ends. -/
theorem ctrl_busy {N W : Nat} (hN : 1 ≤ N) (hW : 1 ≤ W) (hr : N * N * W < 2 ^ 31) (A B : BitVec (N * N * W))
    {t : Nat} (ht : t < N) (ck a b c : LVec) :
    commitNba2 (MS ck (knownBit false) (knownBit false) a b (knownBit false) c (.ofBitVec (BitVec.ofNat 32 t))
      (knownBit true) (.ofBitVec (A >>> (t * W))) (.ofBitVec (B >>> (t * (N * W)))))
      (ctrlQ N W (knownBit false) (knownBit false) a b (knownBit false) (.ofBitVec (BitVec.ofNat 32 t)) (knownBit true)
        (.ofBitVec (A >>> (t * W))) (.ofBitVec (B >>> (t * (N * W))))) =
    MS ck (knownBit false) (knownBit false) a b (knownBit (decide (t + 1 = N))) c (.ofBitVec (BitVec.ofNat 32 (t + 1)))
      (knownBit (decide (t + 1 ≠ N))) (.ofBitVec (A >>> (t * W + W))) (.ofBitVec (B >>> (t * (N * W) + N * W))) := by
  have h1 : N * W ≤ N * N * W := by rw [Nat.mul_assoc N N W]; exact Nat.le_mul_of_pos_left _ hN
  have hNW : N * W < 2 ^ 32 := by simp only [Nat.reducePow] at hr ⊢; omega
  have hW' : W < 2 ^ 32 := Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_left W hN) hNW
  have hN' : N < 2 ^ 32 := Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_right N hW) hNW
  have hyW : (BitVec.ofNat 32 W).toNat = W := by rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt hW']
  have hyNW : (BitVec.ofNat 32 N * BitVec.ofNat 32 W).toNat = N * W := by
    rw [BitVec.toNat_mul, BitVec.toNat_ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt hW', Nat.mod_eq_of_lt hN',
      Nat.mod_eq_of_lt hNW]
  have h1' : LVec.ofInt 32 1 = LVec.ofBitVec 1#32 := by decide
  simp only [ctrlQ, wr, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte, List.cons_append, List.nil_append,
    LVec.ofInt_eq_ofBitVec, BitVec.ofInt_natCast,
    BitVec.ofInt_ofNat, h1', LVec.mul_ofBitVec, LVec.sub_ofBitVec, LVec.eqLogical_ofBitVec, LVec.ofLogic_ofBool,
    decide_eq_true_eq, Lib.ofNat_eq_ofNat_sub_one_iff ht (Nat.le_of_lt hN'), LVec.width_ofBitVec, LVec.shr_ofBitVec,
    LVec.resizeU_ofBitVec, BitVec.setWidth_eq, hyW, hyNW, ← BitVec.shiftRight_add]
  by_cases hf : t + 1 = N <;>
    simp [hf, List.cons_append, List.nil_append, List.append_nil, commitNba2_cons, commitNba2_nil, nb_k, nb_ash, nb_bsh, nb_busy, nb_done,
      LVec.insertAt_zero_of_width_eq, LVec.resizeU_one_l0, LVec.resizeU_one_l1, BitVec.ofNat_add_ofNat]

/-- **The invariant on `k`, one step**: from the state `t < N` busy cycles after a start with
operands `A`, `B` (`acc[i][j] = Σ_{k' < t} A[i][k']·B[k'][j] mod 2^AccW`, `k = t`, the operands
shifted by `t` entries), one cycle without `start` reaches the state at `t + 1`; `done` rises (and
`busy` falls) exactly when `t + 1 = N`. -/
theorem next_step {N W AccW : Nat} (hN : 1 ≤ N) (hW : 1 ≤ W) (hr : N * N * W < 2 ^ 31)
    (A B : BitVec (N * N * W)) {t : Nat} (ht : t < N) (ck a b : LVec) :
    mmNext N W AccW ck (knownBit false) (knownBit false) a b (knownBit false) (accC N W AccW A B t)
      (.ofBitVec (BitVec.ofNat 32 t)) (knownBit true) (.ofBitVec (A >>> (t * W)))
      (.ofBitVec (B >>> (t * (N * W)))) =
    MS ck (knownBit false) (knownBit false) a b (knownBit (decide (t + 1 = N))) (accC N W AccW A B (t + 1))
      (.ofBitVec (BitVec.ofNat 32 (t + 1))) (knownBit (decide (t + 1 ≠ N))) (.ofBitVec (A >>> ((t + 1) * W)))
      (.ofBitVec (B >>> ((t + 1) * (N * W)))) := by
  have hq := rowMajor_map (N := N) (AccW := AccW) (q := peQ N W AccW (knownBit false) (knownBit true)
    (accC N W AccW A B t) (.ofBitVec (A >>> (t * W))) (.ofBitVec (B >>> (t * (N * W)))))
    (fun r => LVec.ofBitVec (BitVec.ofInt AccW (psum N W A B (t + 1) (r / N) (r % N))))
    (fun i j hi hj => pe_step hW A B hi hj _)
  rw [mmNext, commitNba2_append, ctrl_busy hN hW hr A B ht, hq, commit_map,
    LVec.insertEntries_ofBitVec _ _ (by simp [accC]), Nat.succ_mul, Nat.succ_mul]
  rfl

/-- The free-running registers in an idle cycle (`busy` = 0), from the state `t` cycles after a start. -/
theorem ctrl_idle {N W : Nat} (hN : 1 ≤ N) (hW : 1 ≤ W) (hr : N * N * W < 2 ^ 31) (A B : BitVec (N * N * W))
    (t : Nat) (ck a b dn c : LVec) :
    commitNba2 (MS ck (knownBit false) (knownBit false) a b dn c (.ofBitVec (BitVec.ofNat 32 t))
      (knownBit false) (.ofBitVec (A >>> (t * W))) (.ofBitVec (B >>> (t * (N * W)))))
      (ctrlQ N W (knownBit false) (knownBit false) a b dn (.ofBitVec (BitVec.ofNat 32 t)) (knownBit false)
        (.ofBitVec (A >>> (t * W))) (.ofBitVec (B >>> (t * (N * W))))) =
    MS ck (knownBit false) (knownBit false) a b dn c (.ofBitVec (BitVec.ofNat 32 (t + 1)))
      (knownBit false) (.ofBitVec (A >>> (t * W + W))) (.ofBitVec (B >>> (t * (N * W) + N * W))) := by
  have h1 : N * W ≤ N * N * W := by rw [Nat.mul_assoc N N W]; exact Nat.le_mul_of_pos_left _ hN
  have hNW : N * W < 2 ^ 32 := by simp only [Nat.reducePow] at hr ⊢; omega
  have hW' : W < 2 ^ 32 := Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_left W hN) hNW
  have hN' : N < 2 ^ 32 := Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_right N hW) hNW
  have hyW : (BitVec.ofNat 32 W).toNat = W := by rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt hW']
  have hyNW : (BitVec.ofNat 32 N * BitVec.ofNat 32 W).toNat = N * W := by
    rw [BitVec.toNat_mul, BitVec.toNat_ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt hW', Nat.mod_eq_of_lt hN',
      Nat.mod_eq_of_lt hNW]
  have h1' : LVec.ofInt 32 1 = LVec.ofBitVec 1#32 := by decide
  simp only [ctrlQ, wr, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte, List.cons_append, List.nil_append,
    List.append_nil, LVec.ofInt_eq_ofBitVec, BitVec.ofInt_natCast, BitVec.ofInt_ofNat, h1', LVec.mul_ofBitVec,
    LVec.add_ofBitVec, LVec.width_ofBitVec, LVec.shr_ofBitVec, LVec.resizeU_ofBitVec, BitVec.setWidth_eq, hyW, hyNW,
    ← BitVec.shiftRight_add]
  simp [commitNba2_cons, commitNba2_nil, nb_k, nb_ash, nb_bsh, LVec.insertAt_zero_of_width_eq,
    BitVec.ofNat_add_ofNat]

/-- **An idle step after the `N` steps**: the accumulators add `A[i][t]·B[t][j]` for `t ≥ N`, i.e. zero
(`b_sh` has been shifted out), so `C` holds; `k` and the shift registers keep running. -/
theorem next_run {N W AccW : Nat} (hN : 1 ≤ N) (hW : 1 ≤ W) (hr : N * N * W < 2 ^ 31)
    (A B : BitVec (N * N * W)) (t : Nat) (ck a b dn : LVec) :
    mmNext N W AccW ck (knownBit false) (knownBit false) a b dn (accC N W AccW A B t)
      (.ofBitVec (BitVec.ofNat 32 t)) (knownBit false) (.ofBitVec (A >>> (t * W)))
      (.ofBitVec (B >>> (t * (N * W)))) =
    MS ck (knownBit false) (knownBit false) a b dn (accC N W AccW A B (t + 1))
      (.ofBitVec (BitVec.ofNat 32 (t + 1))) (knownBit false) (.ofBitVec (A >>> ((t + 1) * W)))
      (.ofBitVec (B >>> ((t + 1) * (N * W)))) := by
  have hq := rowMajor_map (N := N) (AccW := AccW) (q := peQ N W AccW (knownBit false) (knownBit false)
    (accC N W AccW A B t) (.ofBitVec (A >>> (t * W))) (.ofBitVec (B >>> (t * (N * W)))))
    (fun r => LVec.ofBitVec (BitVec.ofInt AccW (psum N W A B (t + 1) (r / N) (r % N))))
    (fun i j hi hj => pe_step hW A B hi hj _)
  rw [mmNext, commitNba2_append, ctrl_idle hN hW hr A B t, hq, commit_map,
    LVec.insertEntries_ofBitVec _ _ (by simp [accC]), Nat.succ_mul, Nat.succ_mul]
  rfl

/-! ## 6. Shape and termination -/

/-- The register widths are the declared ones. -/
def Wd (N W AccW : Nat) (dn c k bz ash bsh : LVec) : Prop :=
  dn.width = 1 ∧ c.width = N * N * AccW ∧ k.width = 32 ∧ bz.width = 1 ∧ ash.width = N * N * W ∧
    bsh.width = N * N * W

/-- A snapshot of the design's shape. -/
def I (N W AccW : Nat) (st : SvState) : Prop :=
  ∃ ck r s a b dn c k bz ash bsh, st = MS ck r s a b dn c k bz ash bsh ∧ Wd N W AccW dn c k bz ash bsh

theorem peQ_C (N W AccW : Nat) (s bz c ash bsh : LVec) :
    ∀ u ∈ (List.range N).flatMap fun i => (List.range N).flatMap (peQ N W AccW s bz c ash bsh i), u.1 = "C" := by
  intro u hu
  simp only [List.mem_flatMap] at hu
  obtain ⟨_, _, _, _, hu⟩ := hu
  unfold peQ at hu
  by_cases h1 : s.condTrue = true <;> by_cases h2 : bz.condTrue = true <;> simp_all

/-- **Every cycle keeps the design's shape** (any values, `x` included). -/
theorem mmNext_I (N W AccW : Nat) (ck r s a b dn c k bz ash bsh : LVec) (hw : Wd N W AccW dn c k bz ash bsh) :
    I N W AccW (mmNext N W AccW ck r s a b dn c k bz ash bsh) := by
  obtain ⟨h1, h2, h3, h4, h5, h6⟩ := hw
  simp only [mmNext, commitNba2_append, ctrlQ]
  by_cases c1 : r.condTrue = true <;> by_cases c2 : s.condTrue = true <;> by_cases c3 : bz.condTrue = true <;>
    by_cases c4 : (LVec.ofLogic (k.eqLogical ((LVec.ofInt 32 (N : Int)).sub (LVec.ofInt 32 1)))).condTrue = true <;>
    simp only [c1, c2, c3, c4, Bool.false_eq_true, ↓reduceIte, commitNba2_append, commitNba2_cons, commitNba2_nil, nb_busy, nb_done, nb_k,
      nb_ash, nb_bsh, wr] <;>
    rw [commit_C (peQ_C N W AccW _ _ _ _ _)] <;>
    exact ⟨_, _, _, _, _, _, _, _, _, _, _, rfl, by simp [Wd, width_foldl_insertAt, *]⟩

theorem mm_noq (N W AccW : Nat) : (mmD N W AccW).processes.toList.any Process2.hasQualifiedCase = false := by
  simp [mmD, mmCtrl, mmPEs, mmPE, nb, Process2.hasQualifiedCase, Stmt2.hasQualifiedCase,
    Stmt2.listHasQualifiedCase]

theorem mm_init (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    I N W AccW (initState2 (design.sem N W AccW)) := by
  rw [mm_sem_eq N W AccW hN hW hA]
  refine ⟨.xVec 1, .xVec 1, .xVec 1, .xVec (N * N * W), .xVec (N * N * W), .xVec 1, .xVec (N * N * AccW),
    .xVec 32, .xVec 1, .xVec (N * N * W), .xVec (N * N * W), ?_, by simp [Wd]⟩
  simp [initState2, mmD, mmDecls, MS]

/-- **Termination**: every schedule and every stimulus completes. -/
theorem mm_terminates (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    Terminates2 (design.sem N W AccW) := by
  refine Terminates2.of_invariant (I N W AccW) (mm_init N W AccW hN hW hA) (fun σ => ⟨30, ?_⟩)
    (by rw [mm_sem_eq N W AccW hN hW hA]; exact mm_noq N W AccW)
  rintro e _ kk ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, rfl, hw⟩
  exact ⟨_, _, mm_cycle N W AccW hN hW hA σ e ck r s a b dn c k bz ash bsh kk 30 (Nat.le_refl _),
    mmNext_I N W AccW _ _ _ _ _ dn c k bz ash bsh hw⟩

/-! ## 7. The protocol: the phases of `TxTask.satisfiedAt_of_phases`, and the statement -/

theorem MS_inj {ck r s a b dn c k bz ash bsh ck' r' s' a' b' dn' c' k' bz' ash' bsh' : LVec}
    (h : MS ck r s a b dn c k bz ash bsh = MS ck' r' s' a' b' dn' c' k' bz' ash' bsh') :
    dn = dn' ∧ c = c' ∧ k = k' ∧ bz = bz' ∧ ash = ash' ∧ bsh = bsh' := by
  simp only [MS, List.cons.injEq, Prod.mk.injEq, true_and, and_true] at h
  exact h.2.2.2.2.2

/-- A cycle without `rst` and `start` from `Ready` (`busy` = 0, `done` = 0): `C` is not claimed (it accumulates
whatever the operand registers hold), and the free-running registers step. -/
theorem next_idle (N W AccW : Nat) (ck a b dn c k ash bsh : LVec) :
    ∃ c' k' ash' bsh', mmNext N W AccW ck (knownBit false) (knownBit false) a b dn c k (knownBit false) ash bsh =
      MS ck (knownBit false) (knownBit false) a b dn c' k' (knownBit false) ash' bsh' := by
  simp only [mmNext, commitNba2_append, ctrlQ, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte, List.append_nil,
    wr, commitNba2_cons, commitNba2_nil, nb_k, nb_ash, nb_bsh]
  rw [commit_C (peQ_C N W AccW _ _ _ _ _)]
  exact ⟨_, _, _, _, rfl⟩

/-- A reset cycle clears `busy` and `done` (the free-running registers step or load, whatever `start` shows). -/
theorem next_reset {N W AccW : Nat} (ck s a b dn c k bz ash bsh : LVec) (hw : Wd N W AccW dn c k bz ash bsh) :
    ∃ c' k' ash' bsh', mmNext N W AccW ck (knownBit true) s a b dn c k bz ash bsh =
      MS ck (knownBit true) s a b (knownBit false) c' k' (knownBit false) ash' bsh' := by
  obtain ⟨h1, -, -, h4, -, -⟩ := hw
  by_cases hs : s.condTrue = true <;>
  simp only [mmNext, commitNba2_append, ctrlQ, hs, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte, commitNba2_cons,
    commitNba2_nil, nb_busy, nb_done, nb_k, nb_ash, nb_bsh, wr, h1, h4, LVec.resizeU_one_l0] <;>
  rw [commit_C (peQ_C N W AccW _ _ _ _ _)] <;>
  exact ⟨_, _, _, _, by rw [LVec.insertAt_zero_of_width_eq (v := dn) (p := knownBit false) (by simp [h1]),
    LVec.insertAt_zero_of_width_eq (v := bz) (p := knownBit false) (by simp [h4])]⟩

/-- A start cycle captures the operands and clears the accumulators: the state at `t = 0`. -/
theorem next_start {N W AccW : Nat} (A B : BitVec (N * N * W)) (ck dn c k bz ash bsh : LVec)
    (hw : Wd N W AccW dn c k bz ash bsh) :
    mmNext N W AccW ck (knownBit false) (knownBit true) (.ofBitVec A) (.ofBitVec B) dn c k bz ash bsh =
      MS ck (knownBit false) (knownBit true) (.ofBitVec A) (.ofBitVec B) (knownBit false) (accC N W AccW A B 0)
        (.ofBitVec (BitVec.ofNat 32 0)) (knownBit true) (.ofBitVec (A >>> (0 * W)))
        (.ofBitVec (B >>> (0 * (N * W)))) := by
  obtain ⟨h1, h2, h3, h4, h5, h6⟩ := hw
  have hq := rowMajor_map (N := N) (AccW := AccW) (q := peQ N W AccW (knownBit true) bz c ash bsh)
    (fun r => LVec.ofBitVec (BitVec.ofInt AccW (psum N W A B 0 (r / N) (r % N))))
    (fun i j _ _ => by simp [peQ, psum])
  rw [mmNext, commitNba2_append, hq]
  simp only [ctrlQ, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte, List.cons_append, List.nil_append, commitNba2_cons, commitNba2_nil, nb_busy,
    nb_done, nb_k, nb_ash, nb_bsh, wr, h1, h3, h4, h5, h6, LVec.resizeU_one_l0, LVec.resizeU_one_l1, LVec.replicate_l0,
    LVec.resizeU_ofBitVec, BitVec.setWidth_eq]
  rw [commit_map, LVec.insertEntries_ofBitVec _ _ h2, LVec.insertAt_zero_of_width_eq (by simp [h1]),
    LVec.insertAt_zero_of_width_eq (by simp [h3]), LVec.insertAt_zero_of_width_eq (by simp [h4]),
    LVec.insertAt_zero_of_width_eq (by simp [h5]), LVec.insertAt_zero_of_width_eq (by simp [h6])]
  simp [accC]

/-- The state `t` busy cycles after a start with operands `A`, `B` (the invariant on `k`). -/
def BusyAt (N W AccW : Nat) (A B : BitVec (N * N * W)) (t : Nat) (st : SvState) : Prop :=
  ∃ ck r s a b, st = MS ck r s a b (knownBit false) (accC N W AccW A B t) (.ofBitVec (BitVec.ofNat 32 t))
    (knownBit true) (.ofBitVec (A >>> (t * W))) (.ofBitVec (B >>> (t * (N * W))))

/-- Finished with `A`, `B`: `done` = 1 and `C` the product. -/
def FinAt (N W AccW : Nat) (A B : BitVec (N * N * W)) (st : SvState) : Prop :=
  ∃ t, N ≤ t ∧ ∃ ck r s a b, st = MS ck r s a b (knownBit true) (accC N W AccW A B N)
    (.ofBitVec (BitVec.ofNat 32 t)) (knownBit false) (.ofBitVec (A >>> (t * W))) (.ofBitVec (B >>> (t * (N * W))))

/-- One cycle from a state of the shape, evaluated (`mm_cycle`). -/
def Stp (N W AccW : Nat) (e prev st : SvState) : Prop :=
  ∃ ck r s a b dn c k bz ash bsh, prev = MS ck r s a b dn c k bz ash bsh ∧ Wd N W AccW dn c k bz ash bsh ∧
    st = mmNext N W AccW (appIn e "clk" ck) (appIn e "rst" r) (appIn e "start" s) (appIn e "A" a)
      (appIn e "B" b) dn c k bz ash bsh

theorem ops_appIn {N W AccW : Nat} {e : SvState} {x : Tasks.Matmul.task.Ops (N, W, AccW)}
    (h : HoldAll e (Tasks.Matmul.task.operands (N, W, AccW)) x) (a b : LVec) :
    appIn e "A" a = .ofBitVec x.1 ∧ appIn e "B" b = .ofBitVec x.2.1 := by
  simp only [Tasks.Matmul.task, HoldAll] at h; simp [appIn, h.1, h.2.1]

/-- **The phase model** at `(N, W, AccW)`, latency `N`: `Ready` after a reset, `Busy x m` the state
`t = N - 1 - m` busy cycles after a start, `Fin x` the product shown. -/
def model (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) (hNW : N * N * W < 2 ^ 31) :
    Tasks.Matmul.task.PhaseModel (N, W, AccW) N (design.sem N W AccW) where
  Shape := I N W AccW
  Step := Stp N W AccW
  init := mm_init N W AccW hN hW hA
  cycle := by
    rintro σ F e prev k st k' ⟨ck, r, s, a, b, dn, c, kk, bz, ash, bsh, rfl, hw⟩ hc
    exact ⟨ck, r, s, a, b, dn, c, kk, bz, ash, bsh, rfl, hw, (Prod.mk.inj (cycleStep2_det hc
      (mm_cycle N W AccW hN hW hA σ e ck r s a b dn c kk bz ash bsh k 30 (Nat.le_refl _)))).1⟩
  shape := by
    rintro e prev st - ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, -, hw, rfl⟩
    exact mmNext_I N W AccW _ _ _ _ _ dn c k bz ash bsh hw
  Ready st := ∃ ck r s a b c k ash bsh, st = MS ck r s a b (knownBit false) c k (knownBit false) ash bsh
  Busy x m st := ∃ t, t + m + 1 = N ∧ BusyAt N W AccW x.1 x.2.1 t st
  Fin x st := FinAt N W AccW x.1 x.2.1 st
  ready_done := by
    rintro st ⟨ck, r, s, a, b, c, k, ash, bsh, rfl⟩
    simp [BitIs, Tasks.Matmul.task, MS, SvState.lookup]
  busy_done := by
    rintro x m st ⟨t, -, ck, r, s, a, b, rfl⟩
    simp [BitIs, Tasks.Matmul.task, MS, SvState.lookup]
  fin_done := by
    rintro ⟨A, B, ⟨⟩⟩ st ⟨t, ht, ck, r, s, a, b, rfl⟩
    simp [BitIs, HoldAll, Tasks.Matmul.task, MS, SvState.lookup, accC_N]
  reset := by
    rintro e prev st - ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, -, hw, rfl⟩ hr
    rw [show appIn e "rst" r = knownBit true from BitIs.appIn_eq hr r]
    obtain ⟨c', k', ash', bsh', h⟩ := next_reset (appIn e "clk" ck) (appIn e "start" s) (appIn e "A" a)
      (appIn e "B" b) dn c k bz ash bsh hw
    rw [h]; exact ⟨_, _, _, _, _, _, _, _, _, rfl⟩
  start := by
    rintro e prev st x - ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, -, hw, rfl⟩ - hr hs hx
    obtain ⟨ha, hb⟩ := ops_appIn hx a b
    rw [show appIn e "rst" r = knownBit false from BitIs.appIn_eq hr r,
      show appIn e "start" s = knownBit true from BitIs.appIn_eq hs s, ha, hb, next_start _ _ _ dn c k bz ash bsh hw]
    exact .inr ⟨N - 1, by omega, 0, by omega, _, _, _, _, _, rfl⟩
  busy := by
    rintro e prev st x m - ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, rfl, -, rfl⟩ ⟨t, ht, ck', r', s', a', b', hb⟩
      hr hs -
    obtain ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ := MS_inj hb
    rw [show appIn e "rst" r = knownBit false from BitIs.appIn_eq hr r,
      show appIn e "start" s = knownBit false from BitIs.appIn_eq hs s, next_step hN hW hNW _ _ (by omega)]
    by_cases hf : t + 1 = N
    · left
      simp only [hf, decide_true, ne_eq, not_true_eq_false, decide_false]
      exact ⟨N, Nat.le_refl _, _, _, _, _, _, rfl⟩
    · right
      simp only [hf, ne_eq, not_false_eq_true, decide_true, decide_false]
      exact ⟨m - 1, by omega, t + 1, by omega, _, _, _, _, _, rfl⟩
  hold_ready := by
    rintro e prev st - ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, rfl, -, rfl⟩ ⟨ck', r', s', a', b', c', k', ash',
      bsh', hb⟩ hr hs
    obtain ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ := MS_inj hb
    rw [show appIn e "rst" r = knownBit false from BitIs.appIn_eq hr r,
      show appIn e "start" s = knownBit false from BitIs.appIn_eq hs s]
    obtain ⟨c₁, k₁, a₁, b₁, h⟩ := next_idle N W AccW (appIn e "clk" ck) (appIn e "A" a) (appIn e "B" b)
      (knownBit false) c k ash bsh
    rw [h]
    exact ⟨_, _, _, _, _, _, _, _, _, rfl⟩
  hold_fin := by
    rintro e prev st x - ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, rfl, -, rfl⟩ ⟨t, ht, ck', r', s', a', b', hb⟩ hr hs
    obtain ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ := MS_inj hb
    rw [show appIn e "rst" r = knownBit false from BitIs.appIn_eq hr r,
      show appIn e "start" s = knownBit false from BitIs.appIn_eq hs s,
      ← accC_ge N W AccW x.fst x.snd.fst ht, next_run hN hW hNW x.fst x.snd.fst t]
    exact ⟨t + 1, by omega, _, _, _, _, _, by rw [accC_ge N W AccW x.fst x.snd.fst (by omega : N ≤ t + 1)]⟩

theorem mm_interface (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    Tasks.Matmul.task.Interface (N, W, AccW) (design.sem N W AccW) := by
  rw [mm_sem_eq N W AccW hN hW hA]
  exact ⟨rfl, rfl, by
    show (["clk", "rst", "start", "A", "B", "done", "C", "k", "busy", "a_sh", "b_sh"] : List String).Nodup
    decide⟩

theorem mm_disciplined (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    Tasks.Matmul.task.Disciplined (design.sem N W AccW) := by
  rw [mm_sem_eq N W AccW hN hW hA]
  refine ⟨by simp [Tasks.Matmul.task, mmD, mmDecls, Design2.inputNames], fun p hp => ?_⟩
  have hm : p ∈ mmCtrl N W :: mmPEs N W AccW := by simpa [mmD] using hp
  rcases List.mem_cons.mp hm with rfl | hm
  · simp [Tasks.Matmul.task, mmCtrl, nb, c32, edgeClock, asyncReset, processDataNames, stmtNames,
      stmtOptNames, stmtListNames, lhsNames, exprNames]
  · obtain ⟨i, j, rfl⟩ := mm_pe_mem hm
    simp [Tasks.Matmul.task, mmPE, sext, edgeClock, asyncReset, processDataNames, stmtNames, stmtOptNames,
      lhsNames, exprNames, exprListNames]

/-! ## 8. txtask-v2: every power-up (rule 2), Moore outputs (rule 1), no x-creating construct (rule 3)

Rule 2: the phase model's shape `I` (the register widths, any values) holds at every power-up state
(`mm_powerUp`), and every obligation of the model holds from any state of the shape, so the claim holds
from every power-up (`TxTask.satisfiedAtV2_of_phases`, `SvGolf.SeqV2`); the same cycle gives
termination from every power-up (`mm_terminatesPU`). Rule 1: every process is an `always_ff`
(`mm_profile`), so the design has no combinational dependency at all (`combDeps_of_ffOnly`). Rule 3
(`mm_xsafe`): every expression is a known literal, a declared signal, an in-range constant slice
(`C`'s windows, the operand entries), a concatenation, a replication, a width conversion or `+`, `-`,
`*`, `>>`, `==` on operands of matching widths. -/

/-- **Rule 1.** -/
theorem mm_moore (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    MooreOutDep (design.sem N W AccW) [] := by
  rw [mm_sem_eq N W AccW hN hW hA]
  exact MooreOutDep.of_noComb (combDeps_of_ffOnly (FFOnly.ofProfile (mm_profile N W AccW)))
    (by simp [mmD, mmDecls, Design2.outputNames, Design2.inputNames])

/-- Every power-up state of the design has its shape. -/
theorem mm_powerUp (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) (st : SvState)
    (h : PowerUp (design.sem N W AccW) st) : I N W AccW st := by
  rw [mm_sem_eq N W AccW hN hW hA] at h
  obtain ⟨ck, r1, rfl, -, -, h1⟩ := powerUp_cons.mp h
  obtain ⟨r, r2, rfl, -, -, h2⟩ := powerUp_cons.mp h1
  obtain ⟨s, r3, rfl, -, -, h3⟩ := powerUp_cons.mp h2
  obtain ⟨a, r4, rfl, -, -, h4⟩ := powerUp_cons.mp h3
  obtain ⟨b, r5, rfl, -, -, h5⟩ := powerUp_cons.mp h4
  obtain ⟨dn, r6, rfl, w6, -, h6⟩ := powerUp_cons.mp h5
  obtain ⟨c, r7, rfl, w7, -, h7⟩ := powerUp_cons.mp h6
  obtain ⟨k, r8, rfl, w8, -, h8⟩ := powerUp_cons.mp h7
  obtain ⟨bz, r9, rfl, w9, -, h9⟩ := powerUp_cons.mp h8
  obtain ⟨ash, r10, rfl, w10, -, h10⟩ := powerUp_cons.mp h9
  obtain ⟨bsh, r11, rfl, w11, -, h11⟩ := powerUp_cons.mp h10
  obtain rfl := powerUp_nil.mp h11
  exact ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, rfl, w6, w7, w8, w9, w10, w11⟩

/-- **Termination from every power-up** (the cycle of `mm_terminates`). -/
theorem mm_terminatesPU (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    TerminatesPU (design.sem N W AccW) := by
  refine TerminatesPU.of_invariant (I N W AccW) (mm_powerUp N W AccW hN hW hA) (fun σ => ⟨30, ?_⟩)
    (by rw [mm_sem_eq N W AccW hN hW hA]; exact mm_noq N W AccW)
  rintro e _ kk ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, rfl, hw⟩
  exact ⟨_, _, mm_cycle N W AccW hN hW hA σ e ck r s a b dn c k bz ash bsh kk 30 (Nat.le_refl _),
    mmNext_I N W AccW _ _ _ _ _ dn c k bz ash bsh hw⟩

theorem lvec_l0_known : (⟨#[.l0]⟩ : LVec).allKnown = true := by
  show (LVec.ofLogic .l0).allKnown = true
  rw [LVec.ofLogic_l0]; exact LVec.allKnown_ofBitVec _

theorem lvec_l1_known : (⟨#[.l1]⟩ : LVec).allKnown = true := by
  show (LVec.ofLogic .l1).allKnown = true
  rw [LVec.ofLogic_l1]; exact LVec.allKnown_ofBitVec _

/-- The control passes rule 3. -/
theorem ctrl_xsafe (N W AccW : Nat) : xsProc (mmD N W AccW) (mmCtrl N W) = true := by
  simp [xsProc, xsStmt, xsStmts, xsOpt, xsLhs, xsWidth, binW, sigWidth, mmCtrl, nb, c32, mmD, mmDecls,
    lvec_l0_known, lvec_l1_known, LVec.replicate_l0, LVec.ofInt]

/-- A PE passes rule 3: its windows of `C` and of the operand registers are in range. -/
theorem pe_xsafe {N W AccW i j : Nat} (hW : 1 ≤ W) (hi : i < N) (hj : j < N) :
    xsProc (mmD N W AccW) (mmPE N W AccW i j) = true := by
  have hN : 0 < N := by omega
  have hC := Lib.rowMajor_window_le (M := N) (N := N) (w := AccW) hi hj
  have hA : i * N * W + W ≤ N * N * W := by
    have := Lib.rowMajor_window_le (M := N) (N := N) (w := W) hi hN
    simpa [Nat.add_zero] using this
  have hB : j * W + W ≤ N * N * W := by
    have := Lib.rowMajor_window_le (M := N) (N := N) (w := W) hN hj
    simpa using this
  have hA1 : i * N * W + W - 1 + 1 ≤ N * N * W := by omega
  have hB1 : j * W + W - 1 + 1 ≤ N * N * W := by omega
  simp [xsProc, xsStmt, xsOpt, xsLhs, xsWidth, xsWidthList, binW, sigWidth, mmPE, sext, mmD, mmDecls,
    LVec.replicate_l0, hC, hA, hB, hA1, hB1]

theorem mm_pe_mem' {N W AccW : Nat} {p : Process2} (hp : p ∈ mmPEs N W AccW) :
    ∃ i j, i < N ∧ j < N ∧ p = mmPE N W AccW i j := by
  simp only [mmPEs, List.mem_flatMap, List.mem_map, List.mem_range] at hp
  obtain ⟨i, hi, j, hj, rfl⟩ := hp
  exact ⟨i, j, hi, hj, rfl⟩

/-- **Rule 3.** -/
theorem mm_xsafe (N W AccW : Nat) (hN : 1 ≤ N) (hW : 1 ≤ W) (hA : 1 ≤ AccW) :
    XSafe (design.sem N W AccW) := by
  rw [mm_sem_eq N W AccW hN hW hA]
  refine List.all_eq_true.mpr fun p hp => ?_
  have hm : p ∈ mmCtrl N W :: mmPEs N W AccW := by simpa [mmD] using hp
  rcases List.mem_cons.mp hm with rfl | hm
  · exact ctrl_xsafe N W AccW
  · obtain ⟨i, j, hi, hj, rfl⟩ := mm_pe_mem' hm
    exact pe_xsafe hW hi hj

/-- **The reference satisfies the matmul statement (txtask-v2) at latency `N`** (`4` at the scoring
point). -/
theorem solution : Goal lat := by
  refine ⟨fun p hp => ?_, rfl⟩
  obtain ⟨N, W, AccW⟩ := p
  obtain ⟨hN, hW, hA, hNW, -⟩ := hp
  exact Tasks.Matmul.task.satisfiedAtV2_of_phases (mm_interface N W AccW hN hW hA)
    (mm_disciplined N W AccW hN hW hA) (mm_terminatesPU N W AccW hN hW hA) hN
    (model N W AccW hN hW hA hNW) (mm_powerUp N W AccW hN hW hA) (mm_moore N W AccW hN hW hA)
    (mm_xsafe N W AccW hN hW hA)

end Submission

The netlist

The netlist card shows the sky130 weighing (its cells, its critical path): the ASAP7 view changes the overview above, not this card.

Schematic

drawn at N = 2, W = 2, AccW = 4

Drawn at N = 2, W = 2, AccW = 4, a display instance; scored at N = 4, W = 8, AccW = 32. Only this drawing and the notes under it are at the smaller size: the critical path, the cells and every other number on this page are the scored netlist's.

C_reg[0] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[10] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[11] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[12] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[13] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[14] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[15] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[1] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[2] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[3] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[4] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[5] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[6] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[7] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[8] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q C_reg[9] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[0] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[10] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[11] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[12] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[13] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[14] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[15] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[16] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[17] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[18] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[19] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[1] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[20] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[21] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[22] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[23] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[24] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[25] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[26] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[27] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[28] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[29] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[2] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[30] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[31] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[3] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[4] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[5] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[6] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[7] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[8] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _0__reg[9] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _30__reg · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _31__reg[0] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _31__reg[1] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _31__reg[2] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _31__reg[3] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _31__reg[4] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _31__reg[5] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _31__reg[6] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _31__reg[7] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _32__reg[0] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _32__reg[1] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _32__reg[2] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _32__reg[3] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _32__reg[4] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _32__reg[5] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _32__reg[6] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _32__reg[7] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _336_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _337_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _338_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _339_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _340_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _341_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _342_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _343_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _344_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _345_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _346_ · sky130_fd_sc_hd__and2_1 and2_1 _347_ · sky130_fd_sc_hd__nand2_1 nand2_1 _348_ · sky130_fd_sc_hd__nor2_1 nor2_1 _349_ · sky130_fd_sc_hd__nor2_1 nor2_1 _350_ · sky130_fd_sc_hd__and2_1 and2_1 _351_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _352_ · sky130_fd_sc_hd__and2_1 and2_1 _353_ · sky130_fd_sc_hd__nand2_1 nand2_1 _354_ · sky130_fd_sc_hd__xor2_1 xor2_1 _355_ · sky130_fd_sc_hd__nand2_1 nand2_1 _356_ · sky130_fd_sc_hd__xor2_1 xor2_1 _357_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _358_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _359_ · sky130_fd_sc_hd__nand2_1 nand2_1 _360_ · sky130_fd_sc_hd__nor2_1 nor2_1 _361_ · sky130_fd_sc_hd__nor2_1 nor2_1 _362_ · sky130_fd_sc_hd__and2_1 and2_1 _363_ · sky130_fd_sc_hd__nand2_1 nand2_1 _364_ · sky130_fd_sc_hd__and2_1 and2_1 _365_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _366_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _367_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _368_ · sky130_fd_sc_hd__or2_1 or2_1 _369_ · sky130_fd_sc_hd__xor2_1 xor2_1 _370_ · sky130_fd_sc_hd__nand2_1 nand2_1 _371_ · sky130_fd_sc_hd__nor2_1 nor2_1 _372_ · sky130_fd_sc_hd__nor2_1 nor2_1 _373_ · sky130_fd_sc_hd__and2_1 and2_1 _374_ · sky130_fd_sc_hd__and2_1 and2_1 _375_ · sky130_fd_sc_hd__xor2_1 xor2_1 _376_ · sky130_fd_sc_hd__or2_1 or2_1 _377_ · sky130_fd_sc_hd__and2_1 and2_1 _378_ · sky130_fd_sc_hd__nor2_1 nor2_1 _379_ · sky130_fd_sc_hd__and2_1 and2_1 _380_ · sky130_fd_sc_hd__and2_1 and2_1 _381_ · sky130_fd_sc_hd__nand2_1 nand2_1 _382_ · sky130_fd_sc_hd__nor2_1 nor2_1 _383_ · sky130_fd_sc_hd__nor2_1 nor2_1 _384_ · sky130_fd_sc_hd__and2_1 and2_1 _385_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _386_ · sky130_fd_sc_hd__and2_1 and2_1 _387_ · sky130_fd_sc_hd__nand2_1 nand2_1 _388_ · sky130_fd_sc_hd__xor2_1 xor2_1 _389_ · sky130_fd_sc_hd__nand2_1 nand2_1 _390_ · sky130_fd_sc_hd__xor2_1 xor2_1 _391_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _392_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _393_ · sky130_fd_sc_hd__nand2_1 nand2_1 _394_ · sky130_fd_sc_hd__nor2_1 nor2_1 _395_ · sky130_fd_sc_hd__nor2_1 nor2_1 _396_ · sky130_fd_sc_hd__and2_1 and2_1 _397_ · sky130_fd_sc_hd__nand2_1 nand2_1 _398_ · sky130_fd_sc_hd__and2_1 and2_1 _399_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _400_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _401_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _402_ · sky130_fd_sc_hd__or2_1 or2_1 _403_ · sky130_fd_sc_hd__xor2_1 xor2_1 _404_ · sky130_fd_sc_hd__nand2_1 nand2_1 _405_ · sky130_fd_sc_hd__nor2_1 nor2_1 _406_ · sky130_fd_sc_hd__nor2_1 nor2_1 _407_ · sky130_fd_sc_hd__and2_1 and2_1 _408_ · sky130_fd_sc_hd__and2_1 and2_1 _409_ · sky130_fd_sc_hd__xor2_1 xor2_1 _410_ · sky130_fd_sc_hd__or2_1 or2_1 _411_ · sky130_fd_sc_hd__and2_1 and2_1 _412_ · sky130_fd_sc_hd__nor2_1 nor2_1 _413_ · sky130_fd_sc_hd__and2_1 and2_1 _414_ · sky130_fd_sc_hd__and2_1 and2_1 _415_ · sky130_fd_sc_hd__nand2_1 nand2_1 _416_ · sky130_fd_sc_hd__nor2_1 nor2_1 _417_ · sky130_fd_sc_hd__nor2_1 nor2_1 _418_ · sky130_fd_sc_hd__and2_1 and2_1 _419_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _420_ · sky130_fd_sc_hd__and2_1 and2_1 _421_ · sky130_fd_sc_hd__nand2_1 nand2_1 _422_ · sky130_fd_sc_hd__xor2_1 xor2_1 _423_ · sky130_fd_sc_hd__nand2_1 nand2_1 _424_ · sky130_fd_sc_hd__xor2_1 xor2_1 _425_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _426_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _427_ · sky130_fd_sc_hd__nand2_1 nand2_1 _428_ · sky130_fd_sc_hd__nor2_1 nor2_1 _429_ · sky130_fd_sc_hd__nor2_1 nor2_1 _430_ · sky130_fd_sc_hd__and2_1 and2_1 _431_ · sky130_fd_sc_hd__nand2_1 nand2_1 _432_ · sky130_fd_sc_hd__and2_1 and2_1 _433_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _434_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _435_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _436_ · sky130_fd_sc_hd__or2_1 or2_1 _437_ · sky130_fd_sc_hd__xor2_1 xor2_1 _438_ · sky130_fd_sc_hd__nand2_1 nand2_1 _439_ · sky130_fd_sc_hd__nor2_1 nor2_1 _440_ · sky130_fd_sc_hd__nor2_1 nor2_1 _441_ · sky130_fd_sc_hd__and2_1 and2_1 _442_ · sky130_fd_sc_hd__and2_1 and2_1 _443_ · sky130_fd_sc_hd__xor2_1 xor2_1 _444_ · sky130_fd_sc_hd__or2_1 or2_1 _445_ · sky130_fd_sc_hd__and2_1 and2_1 _446_ · sky130_fd_sc_hd__nor2_1 nor2_1 _447_ · sky130_fd_sc_hd__and2_1 and2_1 _448_ · sky130_fd_sc_hd__and2_1 and2_1 _449_ · sky130_fd_sc_hd__and2_1 and2_1 _450_ · sky130_fd_sc_hd__and2_1 and2_1 _451_ · sky130_fd_sc_hd__and2_1 and2_1 _452_ · sky130_fd_sc_hd__and2_1 and2_1 _453_ · sky130_fd_sc_hd__and2_1 and2_1 _454_ · sky130_fd_sc_hd__nor2_1 nor2_1 _455_ · sky130_fd_sc_hd__nor2_1 nor2_1 _456_ · sky130_fd_sc_hd__and2_1 and2_1 _457_ · sky130_fd_sc_hd__nor2_1 nor2_1 _458_ · sky130_fd_sc_hd__nor2_1 nor2_1 _459_ · sky130_fd_sc_hd__and2_1 and2_1 _460_ · sky130_fd_sc_hd__and2_1 and2_1 _461_ · sky130_fd_sc_hd__nor2_1 nor2_1 _462_ · sky130_fd_sc_hd__nor2_1 nor2_1 _463_ · sky130_fd_sc_hd__and2_1 and2_1 _464_ · sky130_fd_sc_hd__nor2_1 nor2_1 _465_ · sky130_fd_sc_hd__nor2_1 nor2_1 _466_ · sky130_fd_sc_hd__and2_1 and2_1 _467_ · sky130_fd_sc_hd__and2_1 and2_1 _468_ · sky130_fd_sc_hd__and2_1 and2_1 _469_ · sky130_fd_sc_hd__nor2_1 nor2_1 _470_ · sky130_fd_sc_hd__nor2_1 nor2_1 _471_ · sky130_fd_sc_hd__and2_1 and2_1 _472_ · sky130_fd_sc_hd__nor2_1 nor2_1 _473_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _474_ · sky130_fd_sc_hd__and2_1 and2_1 _475_ · sky130_fd_sc_hd__and2_1 and2_1 _476_ · sky130_fd_sc_hd__nor2_1 nor2_1 _477_ · sky130_fd_sc_hd__nor2_1 nor2_1 _478_ · sky130_fd_sc_hd__and2_1 and2_1 _479_ · sky130_fd_sc_hd__nor2_1 nor2_1 _480_ · sky130_fd_sc_hd__nor2_1 nor2_1 _481_ · sky130_fd_sc_hd__and2_1 and2_1 _482_ · sky130_fd_sc_hd__and2_1 and2_1 _483_ · sky130_fd_sc_hd__and2_1 and2_1 _484_ · sky130_fd_sc_hd__nand2_1 nand2_1 _485_ · sky130_fd_sc_hd__and2_1 and2_1 _486_ · sky130_fd_sc_hd__nor2_1 nor2_1 _487_ · sky130_fd_sc_hd__nor2_1 nor2_1 _488_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _489_ · sky130_fd_sc_hd__or2_1 or2_1 _490_ · sky130_fd_sc_hd__nor2_1 nor2_1 _491_ · sky130_fd_sc_hd__and2_1 and2_1 _492_ · sky130_fd_sc_hd__nor2_1 nor2_1 _493_ · sky130_fd_sc_hd__and2_1 and2_1 _494_ · sky130_fd_sc_hd__nor2_1 nor2_1 _495_ · sky130_fd_sc_hd__nor2_1 nor2_1 _496_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _497_ · sky130_fd_sc_hd__and2_1 and2_1 _498_ · sky130_fd_sc_hd__nor2_1 nor2_1 _499_ · sky130_fd_sc_hd__nor2_1 nor2_1 _500_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _501_ · sky130_fd_sc_hd__and2_1 and2_1 _502_ · sky130_fd_sc_hd__nor2_1 nor2_1 _503_ · sky130_fd_sc_hd__nor2_1 nor2_1 _504_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _505_ · sky130_fd_sc_hd__and2_1 and2_1 _506_ · sky130_fd_sc_hd__nor2_1 nor2_1 _507_ · sky130_fd_sc_hd__nor2_1 nor2_1 _508_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _509_ · sky130_fd_sc_hd__and2_1 and2_1 _510_ · sky130_fd_sc_hd__nor2_1 nor2_1 _511_ · sky130_fd_sc_hd__nor2_1 nor2_1 _512_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _513_ · sky130_fd_sc_hd__and2_1 and2_1 _514_ · sky130_fd_sc_hd__nor2_1 nor2_1 _515_ · sky130_fd_sc_hd__nor2_1 nor2_1 _516_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _517_ · sky130_fd_sc_hd__and2_1 and2_1 _518_ · sky130_fd_sc_hd__nor2_1 nor2_1 _519_ · sky130_fd_sc_hd__nor2_1 nor2_1 _520_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _521_ · sky130_fd_sc_hd__and2_1 and2_1 _522_ · sky130_fd_sc_hd__nor2_1 nor2_1 _523_ · sky130_fd_sc_hd__nor2_1 nor2_1 _524_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _525_ · sky130_fd_sc_hd__and2_1 and2_1 _526_ · sky130_fd_sc_hd__nor2_1 nor2_1 _527_ · sky130_fd_sc_hd__nor2_1 nor2_1 _528_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _529_ · sky130_fd_sc_hd__and2_1 and2_1 _530_ · sky130_fd_sc_hd__nor2_1 nor2_1 _531_ · sky130_fd_sc_hd__nor2_1 nor2_1 _532_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _533_ · sky130_fd_sc_hd__and2_1 and2_1 _534_ · sky130_fd_sc_hd__nor2_1 nor2_1 _535_ · sky130_fd_sc_hd__nor2_1 nor2_1 _536_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _537_ · sky130_fd_sc_hd__and2_1 and2_1 _538_ · sky130_fd_sc_hd__nor2_1 nor2_1 _539_ · sky130_fd_sc_hd__nor2_1 nor2_1 _540_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _541_ · sky130_fd_sc_hd__and2_1 and2_1 _542_ · sky130_fd_sc_hd__nor2_1 nor2_1 _543_ · sky130_fd_sc_hd__nor2_1 nor2_1 _544_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _545_ · sky130_fd_sc_hd__and2_1 and2_1 _546_ · sky130_fd_sc_hd__nor2_1 nor2_1 _547_ · sky130_fd_sc_hd__nor2_1 nor2_1 _548_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _549_ · sky130_fd_sc_hd__and2_1 and2_1 _550_ · sky130_fd_sc_hd__nor2_1 nor2_1 _551_ · sky130_fd_sc_hd__nor2_1 nor2_1 _552_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _553_ · sky130_fd_sc_hd__and2_1 and2_1 _554_ · sky130_fd_sc_hd__nor2_1 nor2_1 _555_ · sky130_fd_sc_hd__nor2_1 nor2_1 _556_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _557_ · sky130_fd_sc_hd__and2_1 and2_1 _558_ · sky130_fd_sc_hd__nor2_1 nor2_1 _559_ · sky130_fd_sc_hd__nor2_1 nor2_1 _560_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _561_ · sky130_fd_sc_hd__and2_1 and2_1 _562_ · sky130_fd_sc_hd__nor2_1 nor2_1 _563_ · sky130_fd_sc_hd__nor2_1 nor2_1 _564_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _565_ · sky130_fd_sc_hd__and2_1 and2_1 _566_ · sky130_fd_sc_hd__nor2_1 nor2_1 _567_ · sky130_fd_sc_hd__nor2_1 nor2_1 _568_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _569_ · sky130_fd_sc_hd__and2_1 and2_1 _570_ · sky130_fd_sc_hd__nor2_1 nor2_1 _571_ · sky130_fd_sc_hd__nor2_1 nor2_1 _572_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _573_ · sky130_fd_sc_hd__and2_1 and2_1 _574_ · sky130_fd_sc_hd__nor2_1 nor2_1 _575_ · sky130_fd_sc_hd__nor2_1 nor2_1 _576_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _577_ · sky130_fd_sc_hd__and2_1 and2_1 _578_ · sky130_fd_sc_hd__nor2_1 nor2_1 _579_ · sky130_fd_sc_hd__nor2_1 nor2_1 _580_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _581_ · sky130_fd_sc_hd__and2_1 and2_1 _582_ · sky130_fd_sc_hd__nor2_1 nor2_1 _583_ · sky130_fd_sc_hd__nor2_1 nor2_1 _584_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _585_ · sky130_fd_sc_hd__and2_1 and2_1 _586_ · sky130_fd_sc_hd__nor2_1 nor2_1 _587_ · sky130_fd_sc_hd__nor2_1 nor2_1 _588_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _589_ · sky130_fd_sc_hd__and2_1 and2_1 _590_ · sky130_fd_sc_hd__nor2_1 nor2_1 _591_ · sky130_fd_sc_hd__nor2_1 nor2_1 _592_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _593_ · sky130_fd_sc_hd__and2_1 and2_1 _594_ · sky130_fd_sc_hd__nor2_1 nor2_1 _595_ · sky130_fd_sc_hd__nor2_1 nor2_1 _596_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _597_ · sky130_fd_sc_hd__and2_1 and2_1 _598_ · sky130_fd_sc_hd__nor2_1 nor2_1 _599_ · sky130_fd_sc_hd__nor2_1 nor2_1 _600_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _601_ · sky130_fd_sc_hd__and2_1 and2_1 _602_ · sky130_fd_sc_hd__nor2_1 nor2_1 _603_ · sky130_fd_sc_hd__nor2_1 nor2_1 _604_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _605_ · sky130_fd_sc_hd__and2_1 and2_1 _606_ · sky130_fd_sc_hd__nor2_1 nor2_1 _607_ · sky130_fd_sc_hd__nor2_1 nor2_1 _608_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _609_ · sky130_fd_sc_hd__nand2_1 nand2_1 _610_ · sky130_fd_sc_hd__nor2_1 nor2_1 _611_ · sky130_fd_sc_hd__nor2_1 nor2_1 _612_ · sky130_fd_sc_hd__and2_1 and2_1 _613_ · sky130_fd_sc_hd__xor2_1 xor2_1 _614_ · sky130_fd_sc_hd__nor2_1 nor2_1 _615_ · sky130_fd_sc_hd__and2_1 and2_1 _616_ · sky130_fd_sc_hd__nand2_1 nand2_1 _617_ · sky130_fd_sc_hd__nor2_1 nor2_1 _618_ · sky130_fd_sc_hd__nor2_1 nor2_1 _619_ · sky130_fd_sc_hd__and2_1 and2_1 _620_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _621_ · sky130_fd_sc_hd__and2_1 and2_1 _622_ · sky130_fd_sc_hd__nand2_1 nand2_1 _623_ · sky130_fd_sc_hd__xor2_1 xor2_1 _624_ · sky130_fd_sc_hd__nand2_1 nand2_1 _625_ · sky130_fd_sc_hd__xor2_1 xor2_1 _626_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _627_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _628_ · sky130_fd_sc_hd__nand2_1 nand2_1 _629_ · sky130_fd_sc_hd__nor2_1 nor2_1 _630_ · sky130_fd_sc_hd__nor2_1 nor2_1 _631_ · sky130_fd_sc_hd__and2_1 and2_1 _632_ · sky130_fd_sc_hd__nand2_1 nand2_1 _633_ · sky130_fd_sc_hd__and2_1 and2_1 _634_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _635_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _636_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _637_ · sky130_fd_sc_hd__or2_1 or2_1 _638_ · sky130_fd_sc_hd__xor2_1 xor2_1 _639_ · sky130_fd_sc_hd__nand2_1 nand2_1 _640_ · sky130_fd_sc_hd__nor2_1 nor2_1 _641_ · sky130_fd_sc_hd__nor2_1 nor2_1 _642_ · sky130_fd_sc_hd__and2_1 and2_1 _643_ · sky130_fd_sc_hd__and2_1 and2_1 _644_ · sky130_fd_sc_hd__xor2_1 xor2_1 _645_ · sky130_fd_sc_hd__or2_1 or2_1 _646_ · sky130_fd_sc_hd__and2_1 and2_1 _647_ · sky130_fd_sc_hd__nor2_1 nor2_1 _648_ · sky130_fd_sc_hd__and2_1 and2_1 done_reg · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q A B C clk done rst start 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7

It is the same design through the same pinned flow at a smaller size (ppa.py --param), so that what it does can be seen: 379 cells here, 11 447 at the scoring point. The register-to-register critical path at N = 2, W = 2, AccW = 4 (32 cells, ending at the flip-flop input _084_ falling; a period of 5 527 ps there) is in the accent colour. Drawn by netlistsvg with svGolf's sky130 skin (derived from netlistsvg's default skin, as the drawing is: MIT licence, Copyright (c) 2016 Neil Turley, the notice): one symbol per cell function, the cell above it, the instance on hover; nor2b and nand2b are drawn with the bubble on their inverted input. The cells of the path are listed under Critical path, each a link to the cell here.

The netlist at N = 2, W = 2, AccW = 4: 379 cells, 108 nor2_1, 88 and2_1, 66 dfxtp_1, 35 nor2b_1, 26 nand2_1, 17 xor2_1, 14 mux2_1, 9 or2_1, 8 nand2b_1, 8 xnor2_1. There (measured, not ranked): 3 076.70 µm², 5 527 ps. Open the drawing on its own (SVG, 276.9 KB) to pan and zoom it with the browser's own controls.

Critical path

at N = 4, W = 8, AccW = 32 · scored

The path the ranked register-to-register period ends on, at the scoring point N = 4, W = 8, AccW = 32: 59 nets, 58 cells, to the flip-flop input _00399_ falling; the period, 10 689 ps, is the last arrival plus that flip-flop's setup time (ideal clock). Each row is a net of the repaired netlist with the arrival and the transition the STA computed there (NLDM tables, the larger transition carried; no wires). The first row is a flip-flop's Q: its arrival is the flop's clock-to-Q delay after the clock edge. From ppa.py --path (critical_path_timing); the instance names are the scored netlist's, not the schematic's (drawn at a smaller size).

In the schematic, drawn at N = 2, W = 2, AccW = 4, the critical path is 32 cells to the flip-flop input _084_ falling (a period of 5 527 ps there); each cell is a link to it in the drawing:

  1. \_0_[1]
  2. _493_ and2_1
  3. _497_ and2_1
  4. _501_ and2_1
  5. _505_ and2_1
  6. _509_ and2_1
  7. _513_ and2_1
  8. _517_ and2_1
  9. _521_ and2_1
  10. _525_ and2_1
  11. _529_ and2_1
  12. _533_ and2_1
  13. _537_ and2_1
  14. _541_ and2_1
  15. _545_ and2_1
  16. _549_ and2_1
  17. _553_ and2_1
  18. _557_ and2_1
  19. _561_ and2_1
  20. _565_ and2_1
  21. _569_ and2_1
  22. _573_ and2_1
  23. _577_ and2_1
  24. _581_ and2_1
  25. _585_ and2_1
  26. _589_ and2_1
  27. _593_ and2_1
  28. _597_ and2_1
  29. _601_ and2_1
  30. _605_ and2_1
  31. _609_ nand2_1
  32. _613_ xor2_1
  33. _614_ nor2_1
  34. _084_ flip-flop D
every stage (59 rows)
#netedgedriven bycellarrival (ps)transition (ps)stage (ps)
0\_56_[0]riseflop Q–739.4661.3
1_07980_rise_15986_and2_1984.690.8245.2
2_07983_rise_15989_xor2_11 186.3190.5201.7
3_07985_rise_15991_xor2_11 403.1190.5216.8
4_07987_rise_15993_xor2_11 621.8193.2218.7
5_07989_fall_15995_xnor2_11 709.053.687.2
6_07990_fall_15996_or2_11 913.449.5204.4
7_07993_fall_16000_and2_12 065.636.3152.2
8_08010_fall_16017_or2_12 283.049.5217.4
9_08013_fall_16021_and2_12 435.136.3152.1
10_08041_fall_16049_or2_12 652.549.5217.4
11_08044_fall_16053_and2_12 804.736.3152.2
12_08077_fall_16086_or2_13 022.149.5217.4
13_08080_fall_16090_and2_13 174.236.3152.1
14_08117_fall_16127_or2_13 391.649.5217.4
15_08120_fall_16131_and2_13 543.836.3152.2
16_08164_fall_16175_or2_13 761.249.5217.4
17_08167_fall_16179_and2_13 913.436.3152.2
18_08210_fall_16222_or2_14 130.849.5217.4
19_08213_fall_16226_and2_14 282.936.3152.1
20_08259_fall_16272_or2_14 500.349.5217.4
21_08262_fall_16276_and2_14 652.536.3152.2
22_08302_fall_16316_or2_14 869.949.5217.4
23_08305_fall_16320_and2_15 022.036.3152.1
24_08345_fall_16360_or2_15 239.449.5217.4
25_08348_fall_16364_and2_15 391.636.3152.2
26_08382_fall_16398_or2_15 609.049.5217.4
27_08385_fall_16402_and2_15 761.236.3152.2
28_08415_fall_16432_or2_15 978.649.5217.4
29_08418_fall_16436_and2_16 130.736.3152.1
30_08437_fall_16455_or2_16 348.149.5217.4
31_08440_fall_16459_and2_16 500.336.3152.2
32_08452_fall_16471_or2_16 717.749.2217.4
33_08455_fall_16475_and2_16 869.736.3152.0
34_08458_fall_16478_or2_17 087.149.2217.4
35_08461_fall_16482_and2_17 246.142.1159.0
36_08470_fall_16492_nand2b_17 370.433.9124.3
37_08471_fall_16493_and2_17 515.636.1145.2
38_08472_fall_16494_or2_17 720.654.1205.0
39_08475_rise_16498_nand2_17 812.283.391.6
40_08482_fall_16506_nand2_17 857.130.744.9
41_08483_fall_16507_and2_18 000.936.1143.8
42_08484_fall_16508_or2_18 209.556.8208.6
43_08493_fall_16519_or2_18 433.649.0224.1
44_08508_fall_16536_nand2b_18 560.835.0127.2
45_08512_fall_16540_and2_18 688.736.2127.9
46_08515_fall_16543_or2_18 915.456.4226.7
47_08524_fall_16554_or2_19 139.449.0224.0
48_08539_fall_16571_nand2b_19 266.635.0127.2
49_08543_fall_16575_and2_19 394.536.2127.9
50_08546_fall_16578_or2_19 617.753.5223.2
51_08549_rise_16582_nand2_19 709.183.391.4
52_08556_fall_16590_nand2_19 754.030.744.9
53_08557_fall_16591_and2_19 897.836.1143.8
54_08558_fall_16592_or2_110 096.949.7199.1
55_08561_fall_16596_and2_110 257.743.6160.8
56_08564_rise_16599_nor2_110 349.787.392.0
57_08565_fall_16600_nor2_110 388.0162.938.3
58_00399_fall_16601_and2_110 585.931.2197.9

Cells

at N = 4, W = 8, AccW = 32 · scored

the cells of the repaired netlist, by area12 bars; the table beside the chart lists the same numbers.and2_1: 16071.66 µm² (µm² · 2 569 cells)and2_116071.66 µm² · 2 569 cellsdfxtp_1: 16055.4 µm² (µm² · 802 cells)dfxtp_116055.4 µm² · 802 cellsxor2_1: 15616.23 µm² (µm² · 1 783 cells)xor2_115616.23 µm² · 1 783 cellsnand2_1: 13482.93 µm² (µm² · 3 592 cells)nand2_113482.93 µm² · 3 592 cellsxnor2_1: 7103.06 µm² (µm² · 811 cells)xnor2_17103.06 µm² · 811 cellsor2_1: 3203.07 µm² (µm² · 512 cells)or2_13203.07 µm² · 512 cellsmux2_1: 3085.46 µm² (µm² · 274 cells)mux2_13085.46 µm² · 274 cellsnor2_1: 2706.35 µm² (µm² · 721 cells)nor2_12706.35 µm² · 721 cellsnor2b_1: 1282.48 µm² (µm² · 205 cells)nor2b_11282.48 µm² · 205 cellsnand2b_1: 1025.98 µm² (µm² · 164 cells)nand2b_11025.98 µm² · 164 cellsinv_1: 37.54 µm² (µm² · 10 cells)inv_137.54 µm² · 10 cellsbuf_4: 30.03 µm² (µm² · 4 cells)buf_430.03 µm² · 4 cells
The area of each cell type in the repaired A0′ netlist, at the scoring point: the count times the cell's area in the pinned liberty. Their sum is the ranked area.
cellcountµm² eachµm² in allshare
and2_12 5696.256016071.664020.2%
dfxtp_180220.019216055.398420.1%
xor2_11 7838.758415616.227219.6%
nand2_13 5923.753613482.931216.9%
xnor2_18118.75847103.06248.9%
or2_15126.25603203.07204.0%
mux2_127411.26083085.45923.9%
nor2_17213.75362706.34563.4%
nor2b_12056.25601282.48001.6%
nand2b_11646.25601025.98401.3%
inv_1103.753637.53600.0%
buf_447.507230.02880.0%
total11 44779700.1888

Repair (buffer_trees_v1): 4 buffers on 1 net, 0 tie cells, 2 weighing rounds; nothing is resized.

Legality: worst load 0.967 × max_capacitance, worst transition 0.974 × max_transition; 0 timing-table reads outside the characterized grid.

the gate mix of the extra GE column (the pinned GE table, score/ge_seq.json)
gate mix: cells of each type in the scored netlist11 bars; the table beside the chart lists the same numbers.NAND: 3592 cells (3592.000 GE)NAND3592 3592.000 GEAND: 2569 cells (3424.477 GE)AND2569 3424.477 GEXOR: 1783 cells (3566.000 GE)XOR1783 3566.000 GEXNOR: 811 cells (1622.000 GE)XNOR811 1622.000 GEDFF_P: 802 cells (4277.066 GE)DFF_P802 4277.066 GENOR: 721 cells (721.000 GE)NOR721 721.000 GEOR: 512 cells (682.496 GE)OR512 682.496 GEMUX: 274 cells (639.242 GE)MUX274 639.242 GEANDNOT: 205 cells (273.265 GE)ANDNOT205 273.265 GEORNOT: 164 cells (218.612 GE)ORNOT164 218.612 GENOT: 10 cells (6.670 GE)NOT10 6.670 GE
Cells by type; area is the count weighted by the pinned GE table.
cellcountGE eachGE total
NAND35921.0003592.000
AND25691.3333424.477
XOR17832.0003566.000
XNOR8112.0001622.000
DFF_P8025.3334277.066
NOR7211.000721.000
OR5121.333682.496
MUX2742.333639.242
ANDNOT2051.333273.265
ORNOT1641.333218.612
NOT100.6676.670
total1144319022.828

The record

task
matmul
player
vacuity-check
assisted by
Claude Sonnet 5.5
submitted
2026-11-10
notes
reference architecture with free-running operand shifters, step counter and accumulators (no hold mux; C holds because b_sh is shifted out); only busy and done are controlled; latency N
scoring point
AccW = 32, N = 4, W = 8
design
f10.sv sha256 73385c65005d82ccb977d186be60dc1b7facf38d205672c688dbc4eef384cca4
proof
S10.lean sha256 fd011cd83585c5b32067fbe5f0f792324c6494ce5771f7e3cb84ea82aa1a98f8
canonical text
sha256 e429dd71608c3cda7053f0affbed59afe39dd283e92e5e3406ba14615129bce4
record hash
9fdf50f9ae02743512989dd85fb239f25cb535cbcfa873e9a6f01f678b3b5316
downloads
9fdf50f9ae02.sv 9fdf50f9ae02.lean 9fdf50f9ae02.json
previous frontier
none: no submission of this task is dated before this one; 3 other submissions are dated the same day (2026-11-10), which does not order them

The proof

code lines
722
build time
8.05 s
axioms
Classical.choice, Quot.sound, propext
tactics seen
decide, induction, omega, simp
imports
Submission.Design, LeanModels.Sv.Gen2, LeanModels.Sv.Hier2Gen, LeanModels.Sv.SeqProfile, LeanModels.Sv.SeqFamily, LeanModels.Sv.Known2, LeanModels.Sv.Lib.BitVecArith, LeanModels.Sv.CombViewArith, LeanModels.Sv.Mono2, SvGolf.SeqV2

Checker and flow

Checked under the pinned flow of this site's boards.

Yosys
Yosys 0.53 (git sha1 53c22ab7c0ced80861c7536c5dae682c30fb5834, clang++ 17.0.0 -fPIC -O3)
Verilator
Verilator 5.042 2025-11-02 rev UNKNOWN.REV
Lean toolchain
leanprover/lean4:v4.33.0-rc1
svGolf revision
892ba94b00e36c0f83e15b4acf3641cee47d43c8
lean-surfaces revision
892ba94b00e36c0f83e15b4acf3641cee47d43c8
canonicalization script
bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b
scoring script
c3874dbfc85921a87df6eacdfc6b2c9a0e2b34edd5738951e0d8bdb51f4558b2
GE table
0a1aa1147b6916efa4a41e03aa3c8c70e68c1e3fd7a0e9c9a3cbc177edefd1f6
extractor
4930696021c588c75dc890034c534c95560ad9a28a4955b87d1f8d68b5edbc0c
canonical RTLIL
8ef35b30d0f52e3159cc8c02622c0dcbb64f74a66a788c7a644290f222b2e066
the checker's files (sha256)
filesha256
check.pyb0c939438a765c2ffeb679721c83ced6213c0a96bfef84759948d3857db9f431
check/Comparator.lean936f97636d6256374eaa4435d03321eeff29e22f808a72c7781375ab648600e8
check/SvEval.leanfb51d72510b515460866c2798aad3c6f55295536e627b92854c3580af215bb91
check/clocked_rules.py73856a45905724544247ad29042bdc2f1778271ec07b15cdb3a5f214685165c1
check/envelope.py076db01a9791bcc25ee84e9b0033604a4b675f00b212eab0c864078e6a4748b7
check/postsynth.pydd89805f9e8335ab15d6bb753eea76865bce47e84ccffa7e7280c91da8131d23
lakefile.tomlf35a88404367d22906effc14d644aac9a9cad47dfd3b704ea8fec88acfaf9c4d
lean-toolchain62c2d9c0fc1ec4c67e151c11eff41ca004ef38e179cf9476c230406e6defedef
score/banlist.pyf18c14c23a14d55db63e202f42cc424dc84c1dd1c337f132ad60859dc9d5d33a
score/canon.ysbbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b
score/fourstate.py95332451ae3754226fb87b46027385b46a91121e7eb9ae25b302bce756d90475
score/ge.json6a29196a3f4b58241f4c9af650c9141e4632b737214d563a11ba142a725c4bea
score/ge_seq.json0a1aa1147b6916efa4a41e03aa3c8c70e68c1e3fd7a0e9c9a3cbc177edefd1f6
score/ppa.py912031912c3e3f6790725161753e95415df34846bd8c27dde3eb707747ddbcbe
score/ppa_mapped.ys93547b343dbac135737e98516b1004a780e1cf2f579e1bd7fed82c908c6d4125
score/ppa_mapped_pins.json4b8688ba3f4d67681658e5944afe878592adf588cd416a8b47597ebe06deb045
score/ppa_pins.jsond66a6086a37a97f5985266057051979fb6a8a3c557d3ef9c42acc1b5e41502d8
score/score.py71d2e3b82f8813ec64a58f0a46909ca23dfab377db44eda6f294b713f45ae781
score/srcgate.py11952f61058051c9e8de91a801b672d07e66a29308e978156c04ffd9f0dbef45
score/svgolf.ysea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445
score/svgolf_seq.ysc3874dbfc85921a87df6eacdfc6b2c9a0e2b34edd5738951e0d8bdb51f4558b2

Post-synthesis check

At each point below, the check ran the scored netlist and ls-sv's reading of the design 8 times, once per seed, each run from a power-up state and through a seeded stimulus of 24 transactions. Each point ran against its own latency, the solution's lat at that point (the table's latency column): every transaction had to finish within it. The check found no mismatch. The stimulus is a sample of the inputs: a guard against the two tools disagreeing, not a proof.

mode
full
points
AccW = 8, N = 2, W = 4, AccW = 32, N = 4, W = 8 (the scoring point)
seeds
8 seeds per point: seed 0 from the all-zeros power-up, every other one from a random power-up drawn from its seed (below)
stimulus
24 transactions per seed
clock cycles
2 085 in all
mismatches
0
salted
no (the default empty salt: anyone can run this exact stimulus again)
scored netlist
sha256 162dd944a1d8897a4404380b5e64d49bc17c89ef7e0cbcb9ae2b4832f3f5044b
pointlatency (cycles)seedsclock cyclestransactionsmismatchesnetlist sha256
AccW = 8, N = 2, W = 4288281920de575d31fdb1
AccW = 32, N = 4, W = 8481 2571920162dd944a1d8
every seed's run (16)

A seed's draw is sha256(salt, task, point, seed) (its first 12 digits below; check/postsynth.py seed_draw). Everything random in the seed's run comes from it: the stimulus, ls-sv's power-up (zeros for seed 0, else seed:<k>) and the netlist's Verilator randSeed, which the all-zeros power-up of seed 0 does not use.

pointseedls-sv power-upnetlist randSeedclock cyclestransactionsdraw
AccW = 8, N = 2, W = 40zeros303973935109244ed5c6f8253a
AccW = 8, N = 2, W = 41seed:676124580429290409011954383251092482e6921a1035
AccW = 8, N = 2, W = 42seed:845291531553475423391528801112242b060ddd6dc0
AccW = 8, N = 2, W = 43seed:51471915497267460041397868753972437b381d742d3
AccW = 8, N = 2, W = 44seed:38148860476664146781168828466962493e4b866922d
AccW = 8, N = 2, W = 45seed:3507955749274142316192587499102248c2d8181b840
AccW = 8, N = 2, W = 46seed:9665391063568079335688604025101247c2b8adaae80
AccW = 8, N = 2, W = 47seed:11035912927779587285825733514102241db8b9c4c23c
AccW = 32, N = 4, W = 80zeros194668934815124e3ef9e3638b5
AccW = 32, N = 4, W = 81seed:97341885920105542401063280839168242132be692d56
AccW = 32, N = 4, W = 82seed:659440922216709400088936619160240371e783230d
AccW = 32, N = 4, W = 83seed:1509103197246630322759053583815124ed721e3e3e18
AccW = 32, N = 4, W = 84seed:1708700821292366037670774572716224fcdbab7c9305
AccW = 32, N = 4, W = 85seed:1356817743346383925483414218215224ccccf631a1d2
AccW = 32, N = 4, W = 86seed:2839497944125262158125213495216224f1dc560f7767
AccW = 32, N = 4, W = 87seed:807618850060394489954790409115124831e3fb7b1cd

Area against time

µm² × ps · lower left is better · ASAP7
matmul: this design's sky130 area against time, among the task's designs5 designs by sky130 area (µm²) (x) and time (ps) (y), this one ringed; lower left is better. The table under the chart lists the same numbers.10k20k30k40k100k150k200k250ksky130 area (µm²)time (ps) · lower is betterpar's score: area × time = 3 729 636 µm²·nsthe Pareto front of the entriesmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 3 729 636 µm²·ns · Area: 87 173.6 µm² · Time: 42 784 psfanout-ferret · submission · 2026-11-10 · Score: 2 276 474 µm²·ns · Area: 241 920.8 µm² · Time: 9410 psfanout-ferret · submission · 2026-11-10 · Score: 2 511 471 µm²·ns · Area: 137 104.0 µm² · Time: 18 318 psvacuity-check · submission · 2026-11-10 · Score: 2 377 063 µm²·ns · Area: 85 260.5 µm² · Time: 27 880 psthis design · vacuity-check · submission · 2026-11-10 · Score: 3 407 661 µm²·ns · Area: 79 700.2 µm² · Time: 42 756 psparthis design
matmul: this design's sky130 area against time, among the task's designs5 designs by sky130 area (µm²) (x) and time (ps) (y), this one ringed; lower left is better. The table under the chart lists the same numbers.10k20k30k40k100k150k200k250ksky130 area (µm²)time (ps) · lower is betterpar's score: area × time = 3 729 636 µm²·nsthe Pareto front of the entriesmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 3 729 636 µm²·ns · Area: 87 173.6 µm² · Time: 42 784 psfanout-ferret · submission · 2026-11-10 · Score: 2 276 474 µm²·ns · Area: 241 920.8 µm² · Time: 9410 psfanout-ferret · submission · 2026-11-10 · Score: 2 511 471 µm²·ns · Area: 137 104.0 µm² · Time: 18 318 psvacuity-check · submission · 2026-11-10 · Score: 2 377 063 µm²·ns · Area: 85 260.5 µm² · Time: 27 880 psthis design · vacuity-check · submission · 2026-11-10 · Score: 3 407 661 µm²·ns · Area: 79 700.2 µm² · Time: 42 756 psparthis design
  • submission
  • proved reference
  • the Pareto front of the entries
  • this design
  • par's score: area × time = 3 729 636 µm²·ns
sky130 area (x) against the ranked time (y); lower left is better on both. The step line is the Pareto front of the entries (the proved references and the players' ranked records); a design under par's score curve has a better score than par. Baselines are drawn for scale: scored, never proved. Every design is in view.
the designs as numbers, by score
designkindarea (µm²)time (ps)score (µm²·ns)
fanout-ferret submission241 920.779 4102 276 474
vacuity-check submission85 260.5227 8802 377 063
fanout-ferret submission137 103.9918 3182 511 471
vacuity-check · this designsubmission79 700.1942 7563 407 661
matmul_g1 proved reference · par87 173.6142 7843 729 636
matmul: this design's ASAP7 area against time, among the task's designs5 designs by ASAP7 area (µm²) (x) and time (ps) (y), this one ringed; lower left is better. The table under the chart lists the same numbers.2000300040005000600015002000250030003500ASAP7 area (µm²)time (ps) · lower is betterpar's score: area × time = 8217 µm²·nsthe Pareto front of the entriesmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 8217 µm²·ns · Area: 1334.726 µm² · Time: 6156 psfanout-ferret · submission · 2026-11-10 · Score: 5935 µm²·ns · Area: 3661.548 µm² · Time: 1621 psfanout-ferret · submission · 2026-11-10 · Score: 6520 µm²·ns · Area: 2085.873 µm² · Time: 3126 psvacuity-check · submission · 2026-11-10 · Score: 6453 µm²·ns · Area: 1315.583 µm² · Time: 4905 psthis design · vacuity-check · submission · 2026-11-10 · Score: 7291 µm²·ns · Area: 1216.745 µm² · Time: 5992 psparthis design
matmul: this design's ASAP7 area against time, among the task's designs5 designs by ASAP7 area (µm²) (x) and time (ps) (y), this one ringed; lower left is better. The table under the chart lists the same numbers.20004000600020003000ASAP7 area (µm²)time (ps) · lower is betterpar's score: area × time = 8217 µm²·nsthe Pareto front of the entriesmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 8217 µm²·ns · Area: 1334.726 µm² · Time: 6156 psfanout-ferret · submission · 2026-11-10 · Score: 5935 µm²·ns · Area: 3661.548 µm² · Time: 1621 psfanout-ferret · submission · 2026-11-10 · Score: 6520 µm²·ns · Area: 2085.873 µm² · Time: 3126 psvacuity-check · submission · 2026-11-10 · Score: 6453 µm²·ns · Area: 1315.583 µm² · Time: 4905 psthis design · vacuity-check · submission · 2026-11-10 · Score: 7291 µm²·ns · Area: 1216.745 µm² · Time: 5992 psparthis design
  • submission
  • proved reference
  • the Pareto front of the entries
  • this design
  • par's score: area × time = 8217 µm²·ns
ASAP7 area (x) against the ASAP7 time (y); lower left is better on both. The step line is the Pareto front of the entries (the proved references and the players' ranked records); a design under par's score curve has a better score than par. Baselines are drawn for scale: scored, never proved. Every design is in view.
the designs as numbers, by score
designkindarea (µm²)time (ps)score (µm²·ns)
fanout-ferret submission3 661.5481 6215935
vacuity-check submission1 315.5834 9056453
fanout-ferret submission2 085.8733 1266520
vacuity-check · this designsubmission1 216.7455 9927291
matmul_g1 proved reference · par1 334.7266 1568217

Reproduce and verify

From svgolf/, with the pinned tools (reproduce a score lists them):

shell
# the ranked numbers, at the scoring point (from svgolf/, with the pinned Yosys and liberty)
# a clocked task: the clocked flow, --seq (the time is the register-to-register period)
python3.12 score/ppa.py 9fdf50f9ae02743512989dd85fb239f25cb535cbcfa873e9a6f01f678b3b5316.sv --task tasks/matmul --seq --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256
8ef35b30d0f52e3159cc8c02622c0dcbb64f74a66a788c7a644290f222b2e066
ppa.netlist_sha256
162dd944a1d8897a4404380b5e64d49bc17c89ef7e0cbcb9ae2b4832f3f5044b
ppa.repair.netlist_sha256
56933abd2f8ba210d2a582509cdc956dfa76a7d0ce85edef6ad1c27764d46336
ppa.area_e4um2_sky130
797001888
ppa.delay_ps_sky130
10689

The schematic and the critical-path data are site/schematics/matmul/73385c65005d82cc.json and its .svg, written by site/gen_schematics.py (the display instance is ppa.py ... --param AccW=4 --param N=2 --param W=2 --repaired-netlist, drawn by netlistsvg 1.0.2; repaired netlist sha256 65b518d638b937bc…).

From svgolf/, with the pinned tools (reproduce a score lists them):

shell
# the ASAP7 view's numbers, at the scoring point (from svgolf/, with the pinned Yosys; once:
# python3.12 score/ppa.py --pdk asap7 --fetch-liberty, the five pinned ASAP7 files into score/lib/asap7/)
python3.12 score/ppa.py 9fdf50f9ae02743512989dd85fb239f25cb535cbcfa873e9a6f01f678b3b5316.sv --task tasks/matmul --seq --pdk asap7 --no-mapped \
    --json out.json

Expect, in out.json:

ppa.netlist_sha256
162dd944a1d8897a4404380b5e64d49bc17c89ef7e0cbcb9ae2b4832f3f5044b
ppa.repair.netlist_sha256
399ab1bed57c64fb3d4cae671312deb17e75832e0b8b18eb81d1f9c0eb518793
ppa.area_e5um2_asap7
121674474
ppa.delay_ps_asap7
1498

leaderboard/asap7/matmul.json keeps these numbers; python3.12 leaderboard/leaderboard.py asap7 --rescore --task matmul weighs every design of the task again and compares, bit for bit.

Verify the record

Download the three files, then from svgolf/:

shell
# re-run the whole check on this record's files (the cost of the original check)
H=9fdf50f9ae02743512989dd85fb239f25cb535cbcfa873e9a6f01f678b3b5316
mkdir -p rec/matmul && cp "$H.json" "$H.sv" "$H.lean" rec/matmul/
python3.12 leaderboard/leaderboard.py verify --data-dir rec --task matmul --full

verify --offline checks only the hashes and the arithmetic; plain verify also rescores the design (no Lean; seconds for most designs, a minute or more for the largest), on sky130 and on ASAP7.