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 abdd0afdf025

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

Area

137 103.99µm²

137 103.9936 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
+57.3% largermatmul_g1 · 87 173.61 µm²
on this page
4th of 5 designs
cells
20 958
flops
801
repair
6 buffers, 0 tie cells
GE
32 652.081 extra

Performance · time

18 318ps

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

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par
−57.2% fastermatmul_g1 · 42 784 ps
on this page
2nd of 5 designs
Fmax-eq.
54.6 MHz derived
critical path
65 cells
unit depth
72 extra

Score · area × time

2 511 471µm²·ns

137 103.9936 µm² × 18 318 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
−32.7% bettermatmul_g1 · 3 729 636 µm²·ns
on this page
3rd of 5 designs
board
layer 1, rank 3 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

2 085.873µm²

2 085.87312 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
+56.3% largermatmul_g1 · 1 334.726 µm²
on this page
4th of 5 designs
cells
22 872
flops
801
repair
18 buffers, 0 tie cells
GE
32 652.081 extra

Performance · time

3 126ps

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

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par
−49.2% fastermatmul_g1 · 6 156 ps
on this page
2nd of 5 designs
Fmax-eq.
319.9 MHz derived
unit depth
72 extra

Score · area × time

6520µm²·ns

2 085.87312 µm² × 3 126 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
−20.6% bettermatmul_g1 · 8217 µm²·ns
on this page
3rd of 5 designs
board
layer 1, rank 3 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

solution2.svdownload
// matmul, G2: two multiply-accumulate steps per PE per cycle.
// `start` captures A and B (zero-extended into registers with one spare entry / one spare row, so
// the two static windows below stay in range for every N); every busy cycle adds
//   A[i][k], A[i][k+1] . B[k][j], B[k+1][j]   (entries past N read as 0)
// to C[i][j] and shifts the captured operands by two entries (A) / two rows (B). `done` rises
// after ceil(N/2) busy cycles: latency (N+1)/2 = 2 at the scoring point N = 4.
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+1)*W-1:0]   a_sh;
  logic [(N*N+N)*W-1:0]   b_sh;

  always_ff @(posedge clk)
    if (rst) begin
      busy <= 1'b0;
      done <= 1'b0;
      k    <= 32'd0;
    end else if (start) begin
      busy <= 1'b1;
      done <= 1'b0;
      k    <= 32'd0;
      a_sh <= A;
      b_sh <= B;
    end else if (busy) begin
      k    <= k + 32'd2;
      a_sh <= a_sh >> (2*W);
      b_sh <= b_sh >> (2*N*W);
      if (k + 32'd2 >= N) begin
        busy <= 1'b0;
        done <= 1'b1;
      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 if (busy)
          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]}
              + {{AccW{a_sh[(i*N+1)*W + W - 1]}}, a_sh[(i*N+1)*W +: W]}
              * {{AccW{b_sh[(N+j)*W + W - 1]}}, b_sh[(N+j)*W +: W]};
    end
  end
endmodule
Sol2.lean (805 code lines) 
-- svgolf-latency: 2
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

/-!
# Reference solution for task `matmul`, G1: `N²` multiply-accumulate units and one step counter

On `start`, `reference/matmul_g1.sv` captures `A`, `B` into shift registers and clears `C`; for `N`
busy cycles PE `(i, j)` adds `A[i][k]·B[k][j]` (sign-extended, mod `2^AccW`); `done` shows in the
snapshot `N` cycles after the start's (`lat = N`). Proved at every in-range `(N, W, AccW)`:
1. **Agreement** (`mm_sem_eq`): the loaded family `design.sem N W AccW` is the hand-built `mmD`.
2. **G0's clock step** (`mm_profile`, `mm_cycle`): one cycle of the loaded design, from any state
   of its shape, any schedule, is the evaluated commit `mmNext`.
3. **The invariant on `k`** (`pe_step`, `next_step`): busy cycle `t` turns every accumulator's
   `Σ_{k' < t} A[i][k']·B[k'][j]` into the sum to `t + 1`, mod `2^AccW` (`accC`).
4. **The spec's arithmetic** (`product_eq`, `accC_N`): `product` is `accC` at `t = N`.
5. **The protocol** (`model`): the phases of `TxTask.satisfiedAt_of_phases`.
6. **txtask-v2** (section 8): rule 2 (`mm_powerUp`: every power-up state has the model's shape, so
   the claim and termination hold from every power-up), rule 1 (`mm_moore`: every process an
   `always_ff`, so no combinational dependency) and rule 3 (`mm_xsafe`), then `solution`.

The design-independent lemmas are in the library: the packed view and its commit (`packBV`,
`LVec.insertEntries_ofBitVec`) in `LeanModels.Sv.SeqFamily`, the clock step (`ffDisjB_of_pairwise`,
`flatMap_ffUpd`) in `LeanModels.Sv.SeqProfile`, the window arithmetic and the datapath's `BitVec` facts in
`LeanModels.Sv.Lib.NatArith` and `LeanModels.Sv.Lib.BitVecArith`.
-/

namespace Submission

open LeanModels.Sv SvGolf

/-- The latency: `done` shows `ceil(N/2)` snapshots after the start's (2 at the scoring point). -/
def lat (N _W _AccW : Nat) : Nat := (N + 1) / 2

/-! ## 0. Small `BitVec` facts for the four-step datapath -/

theorem setWidth_signExtend_mul4 {m n w : Nat} (h : m ≤ n) (a b : BitVec w) :
    (a.signExtend n * b.signExtend n).setWidth m = BitVec.ofInt m (a.toInt * b.toInt) := by
  rw [BitVec.setWidth_mul _ _ h, Lib.setWidth_signExtend_of_le _ h, Lib.setWidth_signExtend_of_le _ h,
    BitVec.ofInt_mul]
  rfl

/-- Two multiply-accumulates at a wider width, truncated back (`Lib.setWidth_add_mul_signExtend` twice). -/
theorem setWidth_add2_mul_signExtend {m n w : Nat} (h : m ≤ n) (x : BitVec m)
    (a0 b0 a1 b1 : BitVec w) :
    (x.setWidth n + a0.signExtend n * b0.signExtend n + a1.signExtend n * b1.signExtend n).setWidth m =
    x + BitVec.ofInt m (a0.toInt * b0.toInt) + BitVec.ofInt m (a1.toInt * b1.toInt) := by
  rw [BitVec.setWidth_add _ _ h, BitVec.setWidth_add _ _ h, BitVec.setWidth_setWidth_of_le _ h,
    BitVec.setWidth_eq, setWidth_signExtend_mul4 h, setWidth_signExtend_mul4 h]

/-- Zero-extending first changes no part select. -/
theorem extractLsb'_setWidth_of_le {n n' : Nat} (h : n ≤ n') (x : BitVec n) (s l : Nat) :
    (x.setWidth n').extractLsb' s l = x.extractLsb' s l := by
  apply BitVec.eq_of_getLsbD_eq; intro i hi
  by_cases hs : s + i < n
  · simp [BitVec.getLsbD_extractLsb', BitVec.getLsbD_setWidth, hi, hs, show s + i < n' by omega]
  · simp [BitVec.getLsbD_extractLsb', BitVec.getLsbD_setWidth, hi, hs, BitVec.getLsbD_of_ge x (s + i) (by omega)]

/-- The two-step counter test: `t < N < 2^31`, `t + 2` at 32 bits against `N`. -/
theorem ge_two_iff {t N : Nat} (ht : t < N) (hN : N < 2 ^ 31) :
    BitVec.ofNat 32 N ≤ BitVec.ofNat 32 t + 2#32 ↔ N ≤ t + 2 := by
  rw [BitVec.le_def, BitVec.toNat_add, BitVec.toNat_ofNat, BitVec.toNat_ofNat, BitVec.toNat_ofNat]
  simp only [Nat.reducePow] at hN ⊢
  omega

/-- The two `a_sh` windows `[(i·N + m)·W +: W]`, `m ≤ 1`, lie inside the `(N·N + 1)·W`-bit register. -/
theorem winA_le {N W i : Nat} (m : Nat) (hm : m ≤ 1) (hi : i < N) : (i * N + m) * W + W ≤ (N * N + 1) * W := by
  have h1 : (i + 1) * N ≤ N * N := Nat.mul_le_mul_right N (by omega)
  rw [Nat.add_mul, Nat.one_mul] at h1
  have h : i * N + m + 1 ≤ N * N + 1 := by omega
  have h2 := Nat.mul_le_mul_right W h
  rw [Nat.add_mul (i * N + m) 1 W, Nat.one_mul] at h2
  exact h2

/-- The two `b_sh` windows `[(m·N + j)·W +: W]`, `m ≤ 1`, lie inside the `(N·N + N)·W`-bit register. -/
theorem winB_le {N W j : Nat} (m : Nat) (hm : m ≤ 1) (hj : j < N) :
    (m * N + j) * W + W ≤ (N * N + N) * W := by
  have h1 : m * N ≤ 1 * N := Nat.mul_le_mul_right N hm
  have h3 : N ≤ N * N := Nat.le_mul_self N
  have h : m * N + j + 1 ≤ N * N + N := by omega
  have h2 := Nat.mul_le_mul_right W h
  rw [Nat.add_mul (m * N + j) 1 W, Nat.one_mul] at h2
  exact h2

/-! ## 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]

/-- One product of the busy sum: `a_sh[la +: W]` times `b_sh[lb +: W]`, both sign-extended by `AccW` bits. -/
def mulT (AccW W la lb : Nat) : Expr2 :=
  .binary .mul (sext "a_sh" AccW la W) (sext "b_sh" AccW lb W)

/-- The PE at `(i, j)`: clear on `start`, else add two products `A[i][k+m]·B[k+m][j]` (`m < 2`) while `busy`. -/
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 (.ifStmt (.ident "busy")
      (.nbaAssign (.slice "C" ((i * N + j) * AccW) AccW)
        (.resize AccW (.binary .add (.binary .add
          (.resize (AccW + W) (.slice (.ident "C") ((i * N + j) * AccW) AccW))
          (mulT AccW W (i * N * W) (j * W)))
          (mulT AccW W ((i * N + 1) * W) ((N + j) * W)))))
      none)))

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

/-- A shift amount `2·N·W` / `2·W`, as the instantiation writes it. -/
abbrev amtA (W : Nat) : Expr2 := .binary .mul (c32 2) (c32 W)
abbrev amtB (N W : Nat) : Expr2 := .binary .mul (.binary .mul (c32 2) (c32 N)) (c32 W)

/-- The control: `busy`, `done`, the step counter `k` (steps of two), the operand shift registers. -/
def mmCtrl (N W : Nat) : Process2 :=
  .alwaysFF "clk" (.ifStmt (.ident "rst")
    (.block #[nb "busy" ⟨#[.l0]⟩, nb "done" ⟨#[.l0]⟩, nb "k" (LVec.replicate 32 .l0)])
    (some (.ifStmt (.ident "start")
      (.block #[nb "busy" ⟨#[.l1]⟩, nb "done" ⟨#[.l0]⟩, nb "k" (LVec.replicate 32 .l0),
        .nbaAssign (.ident "a_sh") (.resize ((N * N + 1) * W) (.ident "A")),
        .nbaAssign (.ident "b_sh") (.resize ((N * N + N) * W) (.ident "B"))])
      (some (.ifStmt (.ident "busy")
        (.block #[.nbaAssign (.ident "k") (.binary .add (.ident "k") (c32 2)),
          .nbaAssign (.ident "a_sh") (.binary (.shr false) (.ident "a_sh") (amtA W)),
          .nbaAssign (.ident "b_sh") (.binary (.shr false) (.ident "b_sh") (amtB N W)),
          .ifStmt (.binary .ge (.binary .add (.ident "k") (c32 2)) (c32 N))
            (.block #[nb "busy" ⟨#[.l0]⟩, nb "done" ⟨#[.l1]⟩]) none])
        none)))))

/-- The declarations: `A`/`B` at `wa` bits, `a_sh` at `wp`, `b_sh` at `wq`, `C` at `wc`. -/
def mmDecls (wa wp wq 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 := wp }, { name := "b_sh", width := wq }]

/-- 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 + 1) * W) ((N * 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 + 1) * W - 1).natAbs + 1)
        (((N * 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 + 1) * W) ((N * 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, mulT, 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 pP : 0 < (N * N + 1) * W := Nat.mul_pos (by omega) hW
  have pQ : 0 < (N * N + N) * W := Nat.mul_pos (by omega) hW
  have hcP : (((N : Int) * N + 1) * W - 1).natAbs + 1 = (N * N + 1) * W := by
    have := Lib.natAbs_sub_one_add_one pP
    first | (push_cast at this; exact this) | simpa using this | exact_mod_cast this
  have hcQ : (((N : Int) * N + N) * W - 1).natAbs + 1 = (N * N + N) * W := by
    have := Lib.natAbs_sub_one_add_one pQ
    first | (push_cast at this; exact this) | simpa using this | exact_mod_cast this
  have hNP : (1 : Int) ≤ (N * N + 1) * W := by
    have h : 1 ≤ (N * N + 1) * W := pP
    exact_mod_cast h
  have hNQ : (1 : Int) ≤ (N * N + N) * W := by
    have h : 1 ≤ (N * N + N) * W := pQ
    exact_mod_cast h
  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 ha0 := Lib.window_bounds_of_natCast ((i : Int) * N * W) ((N * N + 1) * W)
    (winA_le (N := N) (W := W) 0 (by omega) hi) hW (by simp) (by simp)
  have ha1 := Lib.window_bounds_of_natCast (((i : Int) * N + 1) * W) ((N * N + 1) * W)
    (winA_le (N := N) (W := W) 1 (by omega) hi) hW (by simp) (by simp)
  have hb0 := Lib.window_bounds_of_natCast ((j : Int) * W) ((N * N + N) * W)
    (winB_le (N := N) (W := W) 0 (by omega) hj) hW (by simp) (by simp)
  have hb1 := Lib.window_bounds_of_natCast (((N : Int) + j) * W) ((N * N + N) * W)
    (winB_le (N := N) (W := W) 1 (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 + 1) * W) ((N * N + N) * W) (N * N * AccW)) mmElems
        (mmPEs N W AccW)) := by
  have hd := mm_decls N W AccW
  have pP : 0 < (N * N + 1) * W := Nat.mul_pos (by omega) hW
  have pQ : 0 < (N * N + N) * W := Nat.mul_pos (by omega) hW
  have eP : (((N : Int) * N + 1) * W - 1).natAbs + 1 = (N * N + 1) * W := by
    have := Lib.natAbs_sub_one_add_one pP
    first | (push_cast at this; exact this) | simpa using this | exact_mod_cast this
  have eQ : (((N : Int) * N + N) * W - 1).natAbs + 1 = (N * N + N) * W := by
    have := Lib.natAbs_sub_one_add_one pQ
    first | (push_cast at this; exact this) | simpa using this | exact_mod_cast this
  rw [eP, eQ] at hd
  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)

/-- `v >> (2·W)`, evaluated. -/
def shA (W : Nat) (v : LVec) : LVec :=
  v.shr ((LVec.ofInt 32 2).mul (LVec.ofInt 32 (W : Int)))

/-- `v >> (2·N·W)`, evaluated. -/
def shB (N W : Nat) (v : LVec) : LVec :=
  v.shr (((LVec.ofInt 32 2).mul (LVec.ofInt 32 (N : Int))).mul (LVec.ofInt 32 (W : Int)))

/-- The control's updates, from the pre-edge values. -/
def ctrlQ (N W : Nat) (r s a b dn k bz ash bsh : LVec) : NbaQueue2 :=
  if r.condTrue then [wr "busy" bz ⟨#[.l0]⟩, wr "done" dn ⟨#[.l0]⟩, wr "k" k (LVec.replicate 32 .l0)]
  else if s.condTrue then [wr "busy" bz ⟨#[.l1]⟩, wr "done" dn ⟨#[.l0]⟩,
    wr "k" k (LVec.replicate 32 .l0), wr "a_sh" ash (a.resizeU ((N * N + 1) * W)),
    wr "b_sh" bsh (b.resizeU ((N * N + N) * W))]
  else if bz.condTrue then
    if (LVec.ofLogic ((k.add (LVec.ofInt 32 2)).ge (LVec.ofInt 32 (N : Int)))).condTrue then
      [wr "k" k (k.add (LVec.ofInt 32 2)), wr "a_sh" ash (shA W ash), wr "b_sh" bsh (shB N W bsh),
        wr "busy" bz ⟨#[.l0]⟩, wr "done" dn ⟨#[.l1]⟩]
    else [wr "k" k (k.add (LVec.ofInt 32 2)), wr "a_sh" ash (shA W ash), wr "b_sh" bsh (shB N W bsh)]
  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]

/-- One product of the busy sum, evaluated. -/
def mulV (AccW W : Nat) (ash bsh : LVec) (la lb : Nat) : LVec :=
  (sxv ash AccW la W).mul (sxv bsh AccW lb W)

/-- The new accumulator `(i, j)` of a busy cycle (two products), evaluated. -/
def peV (N W AccW i j : Nat) (c ash bsh : LVec) : LVec :=
  let r0 := (c.extract ((i * N + j) * AccW) AccW).resizeU (AccW + W)
  let r1 := r0.add (mulV AccW W ash bsh (i * N * W) (j * W))
  let r2 := r1.add (mulV AccW W ash bsh ((i * N + 1) * W) ((N + j) * W))
  r2.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 if bz.condTrue then [("C", (i * N + j) * AccW, (peV N W AccW i j c ash bsh).resizeU AccW)]
  else []

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.add (LVec.ofInt 32 2)).ge (LVec.ofInt 32 (N : Int)))).condTrue = true <;>
    simp [mmCtrl, nb, c32, amtA, amtB, shA, shB, 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, mulT, mulV, 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]

theorem psum_add2 (N W : Nat) {n : Nat} (A B : BitVec n) (t i j : Nat) : psum N W A B (t + 2) 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)
      + Tasks.Matmul.entry W A (i * N + (t + 1)) * Tasks.Matmul.entry W B ((t + 1) * N + j) := by
  have h1 : psum N W A B (t + 1) i j = _ := psum_succ N W A B t i j
  have h2 : psum N W A B (t + 2) i j = _ := psum_succ N W A B (t + 1) i j
  rw [h2, h1]

/-- `A` zero-extended to the `a_sh` register's width. -/
def padA (N W : Nat) (A : BitVec (N * N * W)) : BitVec ((N * N + 1) * W) := A.setWidth ((N * N + 1) * W)

/-- `B` zero-extended to the `b_sh` register's width. -/
def padB (N W : Nat) (B : BitVec (N * N * W)) : BitVec ((N * N + N) * W) := B.setWidth ((N * N + N) * W)

/-- **PE `(i, j)` in a busy cycle** adds `Σ_{m<2} A[i][t+m]·B[t+m][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) : peQ N W AccW (knownBit false) (knownBit true) (accC N W AccW A B t)
      (.ofBitVec (padA N W A >>> (t * W))) (.ofBitVec (padB N W B >>> (t * (N * W)))) i j =
      [("C", (i * N + j) * AccW,
        .ofBitVec (BitVec.ofInt AccW (psum N W A B (t + 2) ((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 hc := Lib.rowMajor_window_le (w := AccW) hi hj
  have hr : i * N + j < N * N := by
    have := Lib.rowMajor_window_le (w := 1) hi hj
    simp at this
    omega
  have wa0 : i * N * W + W ≤ (N * N + 1) * W := by
    simpa using winA_le (N := N) (W := W) (i := i) 0 (by omega) hi
  have wa1 := winA_le (N := N) (W := W) (i := i) 1 (by omega) hi
  have wb0 : j * W + W ≤ (N * N + N) * W := by
    simpa using winB_le (N := N) (W := W) (j := j) 0 (by omega) hj
  have wb1 : (N + j) * W + W ≤ (N * N + N) * W := by
    simpa using winB_le (N := N) (W := W) (j := j) 1 (by omega) hj
  have hpA : N * N * W ≤ (N * N + 1) * W := Nat.mul_le_mul_right W (by omega)
  have hpB : N * N * W ≤ (N * N + N) * W := Nat.mul_le_mul_right W (by omega)
  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]
  have eA1 : t * W + (i * N + 1) * W = (i * N + (t + 1)) * W := by
    rw [← Nat.add_mul]; congr 1; omega
  have eB1 : t * (N * W) + (N + j) * W = ((t + 1) * N + j) * W := by
    simp only [Nat.add_mul, Nat.mul_assoc, Nat.one_mul]; omega
  simp (disch := omega) only [peQ, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte, peV, mulV, sxv, accC, padA,
    padB, 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.add_ofBitVec, LVec.resizeU_ofBitVec,
    BitVec.setWidth_eq, setWidth_add2_mul_signExtend, Lib.extractLsb'_ushiftRight, extractLsb'_setWidth_of_le,
    e1, e2, eA1, eB1, psum_add2, 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

/-! ## 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

theorem toNat_mul_lt {w a b : Nat} (ha : a < 2 ^ w) (hb : b < 2 ^ w) (hab : a * b < 2 ^ w) :
    (BitVec.ofNat w a * BitVec.ofNat w b).toNat = a * b := by
  rw [BitVec.toNat_mul, BitVec.toNat_ofNat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb,
    Nat.mod_eq_of_lt hab]

theorem toNat_mul3_lt {w a b c : Nat} (ha : a < 2 ^ w) (hb : b < 2 ^ w) (hc : c < 2 ^ w)
    (hab : a * b < 2 ^ w) (habc : a * b * c < 2 ^ w) :
    (BitVec.ofNat w a * BitVec.ofNat w b * BitVec.ofNat w c).toNat = a * b * c := by
  rw [BitVec.toNat_mul, toNat_mul_lt ha hb hab, BitVec.toNat_ofNat, Nat.mod_eq_of_lt hc, Nat.mod_eq_of_lt habc]

/-- The control in a busy cycle `t < N`: `k` steps by two, the shift registers shift by two entries / rows;
the cycle that reaches `N` 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 (padA N W A >>> (t * W))) (.ofBitVec (padB N W B >>> (t * (N * W)))))
      (ctrlQ N W (knownBit false) (knownBit false) a b (knownBit false) (.ofBitVec (BitVec.ofNat 32 t)) (knownBit true)
        (.ofBitVec (padA N W A >>> (t * W))) (.ofBitVec (padB N W B >>> (t * (N * W))))) =
    MS ck (knownBit false) (knownBit false) a b (knownBit (decide (N ≤ t + 2))) c
      (.ofBitVec (BitVec.ofNat 32 (t + 2))) (knownBit (decide (¬ N ≤ t + 2)))
      (.ofBitVec (padA N W A >>> (t * W + 2 * W)))
      (.ofBitVec (padB N W B >>> (t * (N * W) + 2 * N * W))) := by
  simp only [Nat.reducePow] at hr
  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 ^ 31 := by simp only [Nat.reducePow]; omega
  have hN31 : N < 2 ^ 31 := by
    have : N ≤ N * W := Nat.le_mul_of_pos_right N hW
    simp only [Nat.reducePow]; omega
  have hW31 : W < 2 ^ 31 := by
    have : W ≤ N * W := Nat.le_mul_of_pos_left W hN
    simp only [Nat.reducePow]; omega
  have hN' : N < 2 ^ 32 := by simp only [Nat.reducePow]; omega
  have hW' : W < 2 ^ 32 := by simp only [Nat.reducePow]; omega
  have h2 : 2 < 2 ^ 32 := by decide
  have h2W : 2 * W < 2 ^ 32 := by simp only [Nat.reducePow]; omega
  have h2N : 2 * N < 2 ^ 32 := by simp only [Nat.reducePow]; omega
  have h2NW : 2 * N * W < 2 ^ 32 := by
    rw [Nat.mul_assoc]; simp only [Nat.reducePow]; omega
  have hyW : (BitVec.ofNat 32 2 * BitVec.ofNat 32 W).toNat = 2 * W := toNat_mul_lt h2 hW' h2W
  have hyNW : (BitVec.ofNat 32 2 * BitVec.ofNat 32 N * BitVec.ofNat 32 W).toNat = 2 * N * W :=
    toNat_mul3_lt h2 hN' hW' h2N h2NW
  have h2' : LVec.ofInt 32 2 = LVec.ofBitVec 2#32 := by decide
  simp only [ctrlQ, shA, shB, wr, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte, h2',
    LVec.ofInt_eq_ofBitVec, BitVec.ofInt_natCast, BitVec.ofInt_ofNat, LVec.mul_ofBitVec,
    LVec.add_ofBitVec, LVec.ge_ofBitVec, LVec.ofLogic_ofBool, decide_eq_true_eq, ge_two_iff ht hN31,
    LVec.width_ofBitVec, LVec.shr_ofBitVec, LVec.resizeU_ofBitVec, BitVec.setWidth_eq, hyW, hyNW,
    ← BitVec.shiftRight_add]
  by_cases hf : N ≤ t + 2 <;>
    simp [hf, 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` steps 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 + 2`; `done` rises (and `busy` falls) exactly when `N ≤ t + 2`. -/
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 (padA N W A >>> (t * W)))
      (.ofBitVec (padB N W B >>> (t * (N * W)))) =
    MS ck (knownBit false) (knownBit false) a b (knownBit (decide (N ≤ t + 2))) (accC N W AccW A B (t + 2))
      (.ofBitVec (BitVec.ofNat 32 (t + 2))) (knownBit (decide (¬ N ≤ t + 2)))
      (.ofBitVec (padA N W A >>> ((t + 2) * W))) (.ofBitVec (padB N W B >>> ((t + 2) * (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 (padA N W A >>> (t * W))) (.ofBitVec (padB N W B >>> (t * (N * W)))))
    (fun r => LVec.ofBitVec (BitVec.ofInt AccW (psum N W A B (t + 2) (r / N) (r % N))))
    (fun i j hi hj => pe_step hW A B hi hj)
  have eA4 : t * W + 2 * W = (t + 2) * W := by rw [Nat.add_mul]
  have eB4 : t * (N * W) + 2 * N * W = (t + 2) * (N * W) := by
    simp only [Nat.add_mul, Nat.mul_assoc]
  rw [mmNext, commitNba2_append, ctrl_busy hN hW hr A B ht, hq, commit_map,
    LVec.insertEntries_ofBitVec _ _ (by simp [accC]), eA4, eB4]
  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 + 1) * W ∧
    bsh.width = (N * 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.add (LVec.ofInt 32 2)).ge (LVec.ofInt 32 (N : Int)))).condTrue = true <;>
    simp only [c1, c2, c3, c4, Bool.false_eq_true, ↓reduceIte, 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, mulT, 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 + 1) * W), .xVec ((N * 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 an idle state (`busy` = 0) changes no register. -/
theorem next_idle (N W AccW : Nat) (ck a b dn c k ash bsh : LVec) :
    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
  have h : ((List.range N).flatMap fun i => (List.range N).flatMap
      (peQ N W AccW (knownBit false) (knownBit false) c ash bsh i)) = [] := by simp [List.flatMap_eq_nil_iff, peQ]
  rw [mmNext, h]; simp [ctrlQ]; rfl

/-- A reset cycle clears `busy` and `done`. -/
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', 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
  simp only [mmNext, commitNba2_append, ctrlQ, condTrue_knownBit, ↓reduceIte, commitNba2_cons, commitNba2_nil, nb_busy,
    nb_done, nb_k, 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 (padA N W A >>> (0 * W)))
        (.ofBitVec (padB N W 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, 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, padA, padB]

/-- 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 (padA N W A >>> (t * W))) (.ofBitVec (padB N W B >>> (t * (N * W))))

/-- Past the last real step the accumulators stay: terms with `k ≥ N` read `B` out of range, as 0. -/
theorem entry_B_zero {N W : Nat} (B : BitVec (N * N * W)) {k j : Nat} (hk : N ≤ k) :
    Tasks.Matmul.entry W B (k * N + j) = 0 := by
  have h : N * N * W ≤ (k * N + j) * W := by
    have h1 : N * N ≤ k * N + j := by
      have := Nat.mul_le_mul_right N hk
      omega
    exact Nat.mul_le_mul_right W h1
  have e : B.extractLsb' ((k * N + j) * W) W = 0#W := by
    apply BitVec.eq_of_getLsbD_eq; intro i hi
    simp [BitVec.getLsbD_extractLsb', BitVec.getLsbD_of_ge B ((k * N + j) * W + i) (by omega)]
  simp [Tasks.Matmul.entry, e]

theorem psum_ge (N W : Nat) (A B : BitVec (N * N * W)) (i j : Nat) :
    ∀ d, psum N W A B (N + d) i j = psum N W A B N i j
  | 0 => rfl
  | d + 1 => by
    rw [← Nat.add_assoc, psum_succ, psum_ge N W A B i j d, entry_B_zero B (by omega), Int.mul_zero, Int.add_zero]

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 = LVec.ofBitVec (Tasks.Matmul.product N W AccW A B) := by
  obtain ⟨d, rfl⟩ : ∃ d, t = N + d := ⟨t - N, by omega⟩
  rw [← accC_N]
  simp only [accC, psum_ge]

/-- 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 :=
  ∃ ck r s a b k ash bsh, st = MS ck r s a b (knownBit true) (.ofBitVec (Tasks.Matmul.product N W AccW A B)) k
    (knownBit false) ash bsh

/-- 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 + 1) / 2) (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 j, t = 2 * j ∧ j + m + 1 = (N + 1) / 2 ∧ 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, j, -, -, ck, r, s, a, b, rfl⟩
    simp [BitIs, Tasks.Matmul.task, MS, SvState.lookup]
  fin_done := by
    rintro ⟨A, B, ⟨⟩⟩ st ⟨ck, r, s, a, b, k, ash, bsh, rfl⟩
    simp [BitIs, HoldAll, Tasks.Matmul.task, MS, SvState.lookup]
  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', 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) / 2 - 1, by omega, 0, 0, by omega, 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, j, htj, hj, ck', r', s', a', b', hb⟩
      hr hs -
    obtain ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ := MS_inj hb
    have htN : t < N := by omega
    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 _ _ htN]
    by_cases hf : N ≤ t + 2
    · left
      simp only [hf, accC_ge N W AccW _ _ hf, decide_true, ne_eq, not_true_eq_false, decide_false]
      exact ⟨_, _, _, _, _, _, _, _, rfl⟩
    · right
      simp only [hf, ne_eq, not_false_eq_true, decide_true, decide_false]
      exact ⟨m - 1, by omega, t + 2, j + 1, by omega, 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, next_idle]
    exact ⟨_, _, _, _, _, _, _, _, _, rfl⟩
  hold_fin := by
    rintro e prev st x - ⟨ck, r, s, a, b, dn, c, k, bz, ash, bsh, rfl, -, rfl⟩ ⟨ck', r', s', a', b', 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, next_idle]
    exact ⟨_, _, _, _, _, _, _, _, rfl⟩

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, amtA, amtB, edgeClock, asyncReset, processDataNames, stmtNames,
      stmtOptNames, stmtListNames, lhsNames, exprNames]
  · obtain ⟨i, j, rfl⟩ := mm_pe_mem hm
    simp [Tasks.Matmul.task, mmPE, mulT, 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, amtA, amtB, 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 wa0 : i * N * W + W ≤ (N * N + 1) * W := by
    simpa using winA_le (N := N) (W := W) (i := i) 0 (by omega) hi
  have wa1 := winA_le (N := N) (W := W) (i := i) 1 (by omega) hi
  have wb0 : j * W + W ≤ (N * N + N) * W := by
    simpa using winB_le (N := N) (W := W) (j := j) 0 (by omega) hj
  have wb1' : (N + j) * W + W ≤ (N * N + N) * W := by
    simpa using winB_le (N := N) (W := W) (j := j) 1 (by omega) hj
  have sb0 : j * W + W - 1 + 1 ≤ (N * N + N) * W := by omega
  have sb1 : (N + j) * W + W - 1 + 1 ≤ (N * N + N) * W := by omega
  have sa0 : i * N * W + W - 1 + 1 ≤ (N * N + 1) * W := by omega
  have sa1 : (i * N + 1) * W + W - 1 + 1 ≤ (N * N + 1) * W := by omega
  simp [xsProc, xsStmt, xsOpt, xsLhs, xsWidth, xsWidthList, binW, sigWidth, mmPE, mulT, sext, mmD, mmDecls,
    LVec.replicate_l0, hC, wa0, wa1, wb0, wb1', sa0, sa1, sb0, sb1]

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)
    (show 1 ≤ (N + 1) / 2 by omega) (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 _0570_ · sky130_fd_sc_hd__nor2_1 nor2_1 _0571_ · sky130_fd_sc_hd__or2_1 or2_1 _0572_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0573_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0574_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0575_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0576_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0577_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0578_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0579_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0580_ · sky130_fd_sc_hd__and2_1 and2_1 _0581_ · sky130_fd_sc_hd__and2_1 and2_1 _0582_ · sky130_fd_sc_hd__and2_1 and2_1 _0583_ · sky130_fd_sc_hd__and2_1 and2_1 _0584_ · sky130_fd_sc_hd__and2_1 and2_1 _0585_ · sky130_fd_sc_hd__and2_1 and2_1 _0586_ · sky130_fd_sc_hd__and2_1 and2_1 _0587_ · sky130_fd_sc_hd__and2_1 and2_1 _0588_ · sky130_fd_sc_hd__and2_1 and2_1 _0589_ · sky130_fd_sc_hd__and2_1 and2_1 _0590_ · sky130_fd_sc_hd__and2_1 and2_1 _0591_ · sky130_fd_sc_hd__and2_1 and2_1 _0592_ · sky130_fd_sc_hd__and2_1 and2_1 _0593_ · sky130_fd_sc_hd__and2_1 and2_1 _0594_ · sky130_fd_sc_hd__and2_1 and2_1 _0595_ · sky130_fd_sc_hd__and2_1 and2_1 _0596_ · sky130_fd_sc_hd__and2_1 and2_1 _0597_ · sky130_fd_sc_hd__and2_1 and2_1 _0598_ · sky130_fd_sc_hd__and2_1 and2_1 _0599_ · sky130_fd_sc_hd__and2_1 and2_1 _0600_ · sky130_fd_sc_hd__and2_1 and2_1 _0601_ · sky130_fd_sc_hd__and2_1 and2_1 _0602_ · sky130_fd_sc_hd__and2_1 and2_1 _0603_ · sky130_fd_sc_hd__and2_1 and2_1 _0604_ · sky130_fd_sc_hd__and2_1 and2_1 _0605_ · sky130_fd_sc_hd__and2_1 and2_1 _0606_ · sky130_fd_sc_hd__and2_1 and2_1 _0607_ · sky130_fd_sc_hd__and2_1 and2_1 _0608_ · sky130_fd_sc_hd__and2_1 and2_1 _0609_ · sky130_fd_sc_hd__and2_1 and2_1 _0610_ · sky130_fd_sc_hd__and2_1 and2_1 _0611_ · sky130_fd_sc_hd__or2_1 or2_1 _0612_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0613_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0614_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0615_ · sky130_fd_sc_hd__or2_1 or2_1 _0616_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0617_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0618_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0619_ · sky130_fd_sc_hd__or2_1 or2_1 _0620_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0621_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0622_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0623_ · sky130_fd_sc_hd__or2_1 or2_1 _0624_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0625_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0626_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0627_ · sky130_fd_sc_hd__or2_1 or2_1 _0628_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0629_ · sky130_fd_sc_hd__nor2_1 nor2_1 _0630_ · sky130_fd_sc_hd__and2_1 and2_1 _0631_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0632_ · sky130_fd_sc_hd__and2_1 and2_1 _0633_ · sky130_fd_sc_hd__and2_1 and2_1 _0634_ · sky130_fd_sc_hd__or2_1 or2_1 _0635_ · sky130_fd_sc_hd__and2_1 and2_1 _0636_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0637_ · sky130_fd_sc_hd__or2_1 or2_1 _0638_ · sky130_fd_sc_hd__and2_1 and2_1 _0639_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0640_ · sky130_fd_sc_hd__and2_1 and2_1 _0641_ · sky130_fd_sc_hd__and2_1 and2_1 _0642_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0643_ · sky130_fd_sc_hd__and2_1 and2_1 _0644_ · sky130_fd_sc_hd__and2_1 and2_1 _0645_ · sky130_fd_sc_hd__or2_1 or2_1 _0646_ · sky130_fd_sc_hd__and2_1 and2_1 _0647_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0648_ · sky130_fd_sc_hd__and2_1 and2_1 _0649_ · sky130_fd_sc_hd__or2_1 or2_1 _0650_ · sky130_fd_sc_hd__and2_1 and2_1 _0651_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0652_ · sky130_fd_sc_hd__and2_1 and2_1 _0653_ · sky130_fd_sc_hd__or2_1 or2_1 _0654_ · sky130_fd_sc_hd__and2_1 and2_1 _0655_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0656_ · sky130_fd_sc_hd__and2_1 and2_1 _0657_ · sky130_fd_sc_hd__or2_1 or2_1 _0658_ · sky130_fd_sc_hd__and2_1 and2_1 _0659_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0660_ · sky130_fd_sc_hd__or2_1 or2_1 _0661_ · sky130_fd_sc_hd__and2_1 and2_1 _0662_ · sky130_fd_sc_hd__and2_1 and2_1 _0663_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0664_ · sky130_fd_sc_hd__or2_1 or2_1 _0665_ · sky130_fd_sc_hd__and2_1 and2_1 _0666_ · sky130_fd_sc_hd__and2_1 and2_1 _0667_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0668_ · sky130_fd_sc_hd__or2_1 or2_1 _0669_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0670_ · sky130_fd_sc_hd__and2_1 and2_1 _0671_ · sky130_fd_sc_hd__and2_1 and2_1 _0672_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0673_ · sky130_fd_sc_hd__and2_1 and2_1 _0674_ · sky130_fd_sc_hd__and2_1 and2_1 _0675_ · sky130_fd_sc_hd__and2_1 and2_1 _0676_ · sky130_fd_sc_hd__or2_1 or2_1 _0677_ · sky130_fd_sc_hd__and2_1 and2_1 _0678_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0679_ · sky130_fd_sc_hd__and2_1 and2_1 _0680_ · sky130_fd_sc_hd__or2_1 or2_1 _0681_ · sky130_fd_sc_hd__and2_1 and2_1 _0682_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0683_ · sky130_fd_sc_hd__or2_1 or2_1 _0684_ · sky130_fd_sc_hd__and2_1 and2_1 _0685_ · sky130_fd_sc_hd__and2_1 and2_1 _0686_ · sky130_fd_sc_hd__and2_1 and2_1 _0687_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0688_ · sky130_fd_sc_hd__or2_1 or2_1 _0689_ · sky130_fd_sc_hd__and2_1 and2_1 _0690_ · sky130_fd_sc_hd__and2_1 and2_1 _0691_ · sky130_fd_sc_hd__and2_1 and2_1 _0692_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0693_ · sky130_fd_sc_hd__or2_1 or2_1 _0694_ · sky130_fd_sc_hd__and2_1 and2_1 _0695_ · sky130_fd_sc_hd__and2_1 and2_1 _0696_ · sky130_fd_sc_hd__and2_1 and2_1 _0697_ · sky130_fd_sc_hd__and2_1 and2_1 _0698_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0699_ · sky130_fd_sc_hd__or2_1 or2_1 _0700_ · sky130_fd_sc_hd__and2_1 and2_1 _0701_ · sky130_fd_sc_hd__and2_1 and2_1 _0702_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0703_ · sky130_fd_sc_hd__or2_1 or2_1 _0704_ · sky130_fd_sc_hd__and2_1 and2_1 _0705_ · sky130_fd_sc_hd__and2_1 and2_1 _0706_ · sky130_fd_sc_hd__and2_1 and2_1 _0707_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0708_ · sky130_fd_sc_hd__or2_1 or2_1 _0709_ · sky130_fd_sc_hd__and2_1 and2_1 _0710_ · sky130_fd_sc_hd__and2_1 and2_1 _0711_ · sky130_fd_sc_hd__and2_1 and2_1 _0712_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0713_ · sky130_fd_sc_hd__or2_1 or2_1 _0714_ · sky130_fd_sc_hd__and2_1 and2_1 _0715_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0716_ · sky130_fd_sc_hd__and2_1 and2_1 _0717_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0718_ · sky130_fd_sc_hd__and2_1 and2_1 _0719_ · sky130_fd_sc_hd__and2_1 and2_1 _0720_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0721_ · sky130_fd_sc_hd__or2_1 or2_1 _0722_ · sky130_fd_sc_hd__and2_1 and2_1 _0723_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0724_ · sky130_fd_sc_hd__and2_1 and2_1 _0725_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0726_ · sky130_fd_sc_hd__and2_1 and2_1 _0727_ · sky130_fd_sc_hd__and2_1 and2_1 _0728_ · sky130_fd_sc_hd__and2_1 and2_1 _0729_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0730_ · sky130_fd_sc_hd__or2_1 or2_1 _0731_ · sky130_fd_sc_hd__and2_1 and2_1 _0732_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0733_ · sky130_fd_sc_hd__and2_1 and2_1 _0734_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0735_ · sky130_fd_sc_hd__and2_1 and2_1 _0736_ · sky130_fd_sc_hd__and2_1 and2_1 _0737_ · sky130_fd_sc_hd__or2_1 or2_1 _0738_ · sky130_fd_sc_hd__and2_1 and2_1 _0739_ · sky130_fd_sc_hd__and2_1 and2_1 _0740_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0741_ · sky130_fd_sc_hd__or2_1 or2_1 _0742_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0743_ · sky130_fd_sc_hd__and2_1 and2_1 _0744_ · sky130_fd_sc_hd__and2_1 and2_1 _0745_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0746_ · sky130_fd_sc_hd__and2_1 and2_1 _0747_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0748_ · sky130_fd_sc_hd__and2_1 and2_1 _0749_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0750_ · sky130_fd_sc_hd__and2_1 and2_1 _0751_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0752_ · sky130_fd_sc_hd__and2_1 and2_1 _0753_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0754_ · sky130_fd_sc_hd__and2_1 and2_1 _0755_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0756_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0757_ · sky130_fd_sc_hd__or2_1 or2_1 _0758_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0759_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0760_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0761_ · sky130_fd_sc_hd__or2_1 or2_1 _0762_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0763_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0764_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0765_ · sky130_fd_sc_hd__or2_1 or2_1 _0766_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0767_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0768_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0769_ · sky130_fd_sc_hd__or2_1 or2_1 _0770_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0771_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0772_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0773_ · sky130_fd_sc_hd__or2_1 or2_1 _0774_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0775_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0776_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0777_ · sky130_fd_sc_hd__or2_1 or2_1 _0778_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0779_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0780_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0781_ · sky130_fd_sc_hd__or2_1 or2_1 _0782_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0783_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0784_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0785_ · sky130_fd_sc_hd__or2_1 or2_1 _0786_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0787_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0788_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0789_ · sky130_fd_sc_hd__and2_1 and2_1 _0790_ · sky130_fd_sc_hd__and2_1 and2_1 _0791_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0792_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0793_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0794_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0795_ · sky130_fd_sc_hd__or2_1 or2_1 _0796_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0797_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0798_ · sky130_fd_sc_hd__and2_1 and2_1 _0799_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0800_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0801_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0802_ · sky130_fd_sc_hd__and2_1 and2_1 _0803_ · sky130_fd_sc_hd__and2_1 and2_1 _0804_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0805_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0806_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0807_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0808_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0809_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0810_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0811_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0812_ · sky130_fd_sc_hd__and2_1 and2_1 _0813_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0814_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0815_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0816_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0817_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0818_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0819_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0820_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0821_ · sky130_fd_sc_hd__or2_1 or2_1 _0822_ · sky130_fd_sc_hd__and2_1 and2_1 _0823_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0824_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0825_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0826_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0827_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0828_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0829_ · sky130_fd_sc_hd__or2_1 or2_1 _0830_ · sky130_fd_sc_hd__and2_1 and2_1 _0831_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0832_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0833_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0834_ · sky130_fd_sc_hd__or2_1 or2_1 _0835_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0836_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0837_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0838_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0839_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0840_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0841_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0842_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0843_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0844_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0845_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0846_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0847_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0848_ · sky130_fd_sc_hd__and2_1 and2_1 _0849_ · sky130_fd_sc_hd__and2_1 and2_1 _0850_ · sky130_fd_sc_hd__and2_1 and2_1 _0851_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0852_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0853_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0854_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0855_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0856_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0857_ · sky130_fd_sc_hd__or2_1 or2_1 _0858_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0859_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0860_ · sky130_fd_sc_hd__and2_1 and2_1 _0861_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0862_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0863_ · sky130_fd_sc_hd__and2_1 and2_1 _0864_ · sky130_fd_sc_hd__and2_1 and2_1 _0865_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0866_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0867_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0868_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0869_ · sky130_fd_sc_hd__or2_1 or2_1 _0870_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0871_ · sky130_fd_sc_hd__and2_1 and2_1 _0872_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0873_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0874_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0875_ · sky130_fd_sc_hd__and2_1 and2_1 _0876_ · sky130_fd_sc_hd__and2_1 and2_1 _0877_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0878_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0879_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0880_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0881_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0882_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0883_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0884_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0885_ · sky130_fd_sc_hd__and2_1 and2_1 _0886_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0887_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0888_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0889_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0890_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0891_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0892_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0893_ · sky130_fd_sc_hd__or2_1 or2_1 _0894_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0895_ · sky130_fd_sc_hd__and2_1 and2_1 _0896_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0897_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0898_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0899_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0900_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0901_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0902_ · sky130_fd_sc_hd__or2_1 or2_1 _0903_ · sky130_fd_sc_hd__and2_1 and2_1 _0904_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0905_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0906_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0907_ · sky130_fd_sc_hd__or2_1 or2_1 _0908_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0909_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0910_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0911_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0912_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0913_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0914_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0915_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0916_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0917_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0918_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0919_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0920_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0921_ · sky130_fd_sc_hd__and2_1 and2_1 _0922_ · sky130_fd_sc_hd__and2_1 and2_1 _0923_ · sky130_fd_sc_hd__and2_1 and2_1 _0924_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0925_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0926_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0927_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0928_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0929_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0930_ · sky130_fd_sc_hd__or2_1 or2_1 _0931_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0932_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0933_ · sky130_fd_sc_hd__and2_1 and2_1 _0934_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0935_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0936_ · sky130_fd_sc_hd__and2_1 and2_1 _0937_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0938_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0939_ · sky130_fd_sc_hd__or2_1 or2_1 _0940_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0941_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0942_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0943_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0944_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0945_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0946_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0947_ · sky130_fd_sc_hd__and2_1 and2_1 _0948_ · sky130_fd_sc_hd__and2_1 and2_1 _0949_ · sky130_fd_sc_hd__and2_1 and2_1 _0950_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0951_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0952_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0953_ · sky130_fd_sc_hd__and2_1 and2_1 _0954_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0955_ · sky130_fd_sc_hd__or2_1 or2_1 _0956_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0957_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0958_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0959_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0960_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0961_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0962_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0963_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0964_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0965_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0966_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0967_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0968_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0969_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0970_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0971_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0972_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0973_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0974_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0975_ · sky130_fd_sc_hd__or2_1 or2_1 _0976_ · sky130_fd_sc_hd__or2_1 or2_1 _0977_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0978_ · sky130_fd_sc_hd__and2_1 and2_1 _0979_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0980_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0981_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0982_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0983_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0984_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0985_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0986_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0987_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0988_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0989_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0990_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0991_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0992_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0993_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0994_ · sky130_fd_sc_hd__and2_1 and2_1 _0995_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0996_ · sky130_fd_sc_hd__and2_1 and2_1 _0997_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0998_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0999_ · sky130_fd_sc_hd__nand2_1 nand2_1 _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 _1000_ · sky130_fd_sc_hd__and2_1 and2_1 _1001_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1002_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1003_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1004_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1005_ · sky130_fd_sc_hd__or2_1 or2_1 _1006_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1007_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1008_ · sky130_fd_sc_hd__and2_1 and2_1 _1009_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1010_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1011_ · sky130_fd_sc_hd__and2_1 and2_1 _1012_ · sky130_fd_sc_hd__and2_1 and2_1 _1013_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1014_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _1015_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1016_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1017_ · sky130_fd_sc_hd__or2_1 or2_1 _1018_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1019_ · sky130_fd_sc_hd__and2_1 and2_1 _1020_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1021_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1022_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1023_ · sky130_fd_sc_hd__and2_1 and2_1 _1024_ · sky130_fd_sc_hd__and2_1 and2_1 _1025_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1026_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1027_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1028_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1029_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1030_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1031_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1032_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1033_ · sky130_fd_sc_hd__and2_1 and2_1 _1034_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1035_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1036_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1037_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1038_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1039_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _1040_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1041_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1042_ · sky130_fd_sc_hd__or2_1 or2_1 _1043_ · sky130_fd_sc_hd__and2_1 and2_1 _1044_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1045_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1046_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1047_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1048_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1049_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1050_ · sky130_fd_sc_hd__or2_1 or2_1 _1051_ · sky130_fd_sc_hd__and2_1 and2_1 _1052_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _1053_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _1054_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1055_ · sky130_fd_sc_hd__or2_1 or2_1 _1056_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1057_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1058_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1059_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1060_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1061_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1062_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1063_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1064_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1065_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1066_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1067_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1068_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1069_ · sky130_fd_sc_hd__and2_1 and2_1 _1070_ · sky130_fd_sc_hd__and2_1 and2_1 _1071_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1072_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _1073_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1074_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1075_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1076_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1077_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1078_ · sky130_fd_sc_hd__or2_1 or2_1 _1079_ · sky130_fd_sc_hd__and2_1 and2_1 _1080_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1081_ · sky130_fd_sc_hd__nor2_1 nor2_1 _1082_ · sky130_fd_sc_hd__nor2_1 nor2_1 _1083_ · sky130_fd_sc_hd__and2_1 and2_1 _1084_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1085_ · sky130_fd_sc_hd__or2_1 or2_1 _1086_ · sky130_fd_sc_hd__and2_1 and2_1 _50__reg · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _51__reg[0] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _51__reg[1] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _51__reg[2] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _51__reg[3] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _51__reg[4] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _51__reg[5] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _51__reg[6] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _51__reg[7] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _52__reg[0] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _52__reg[1] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _52__reg[2] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _52__reg[3] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _52__reg[4] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _52__reg[5] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _52__reg[6] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q _52__reg[7] · sky130_fd_sc_hd__dfxtp_1 dfxtp_1 D Q 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: 582 cells here, 20 958 at the scoring point. The register-to-register critical path at N = 2, W = 2, AccW = 4 (16 cells, ending at the flip-flop input _0086_ falling; a period of 2 989 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: 582 cells, 147 nand2_1, 146 and2_1, 65 dfxtp_1, 57 or2_1, 51 xnor2_1, 46 nor2b_1, 39 xor2_1, 17 mux2_1, 10 nand2b_1, 4 nor2_1. There (measured, not ranked): 4 468.04 µm², 2 989 ps. Open the drawing on its own (SVG, 401.0 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: 66 nets, 65 cells, to the flip-flop input _00108_ falling; the period, 9 159 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 16 cells to the flip-flop input _0086_ falling (a period of 2 989 ps there); each cell is a link to it in the drawing:

  1. _50_
  2. _0630_ and2_1
  3. _0633_ and2_1
  4. _0638_ and2_1
  5. _0648_ and2_1
  6. _0674_ and2_1
  7. _0675_ and2_1
  8. _0686_ and2_1
  9. _0691_ and2_1
  10. _0697_ and2_1
  11. _0706_ and2_1
  12. _0711_ and2_1
  13. _0719_ and2_1
  14. _0728_ and2_1
  15. _0730_ or2_1
  16. _0731_ and2_1
  17. _0733_ and2_1
  18. _0086_ flip-flop D
every stage (66 rows)
#netedgedriven bycellarrival (ps)transition (ps)stage (ps)
0\_99_[111]riseflop Q–737.3658.2
1_12684_rise_20640_and2_11 009.1120.0271.8
2_12686_fall_20642_nand2_11 090.5133.181.4
3_12691_fall_20647_and2_11 303.977.8213.4
4_12819_rise_20775_xor2_11 515.4190.5211.5
5_12828_rise_20784_xor2_11 732.1190.5216.7
6_12873_rise_20829_xor2_11 948.9190.5216.8
7_12889_rise_20845_xor2_12 165.7190.5216.8
8_12929_rise_20885_xor2_12 382.5190.5216.8
9_12931_rise_20887_xor2_12 599.2190.5216.7
10_12969_rise_20925_xor2_12 816.0190.5216.8
11_13031_rise_20987_xor2_13 034.7193.2218.7
12_13032_fall_20988_nand2_13 106.846.372.1
13_13033_rise_20989_nand2_13 195.081.388.2
14_13035_fall_20991_nand2_13 239.541.244.5
15_13036_fall_20992_and2_13 401.047.7161.5
16_13037_fall_20993_nand2b_13 527.742.9126.7
17_13038_fall_20994_and2_13 690.047.7162.3
18_13039_fall_20995_nand2b_13 816.742.9126.7
19_13040_fall_20996_and2_13 978.947.7162.2
20_13041_fall_20997_nand2b_14 105.642.9126.7
21_13042_fall_20998_and2_14 267.947.7162.3
22_13043_fall_20999_nand2b_14 400.248.3132.3
23_13044_rise_21000_nand2_14 489.381.389.1
24_13058_fall_21014_nand2_14 539.446.550.1
25_13067_rise_21023_nand2_15 181.6869.1642.2
26_13138_rise_21094_xor2_15 434.7233.5253.1
27_13140_rise_21096_xor2_15 656.6190.2221.9
28_13290_fall_21246_nand2_15 723.653.767.0
29_13291_rise_21247_nand2_15 814.280.290.6
30_13293_fall_21249_nand2_15 863.845.949.6
31_13294_rise_21250_nand2_15 951.180.387.3
32_13295_fall_21251_nand2_16 004.553.753.4
33_13296_rise_21252_nand2_16 095.380.390.8
34_13297_fall_21253_nand2_16 148.653.753.3
35_13298_rise_21254_nand2_16 235.775.287.1
36_13299_fall_21255_nand2_16 287.930.652.2
37_13300_rise_21256_nand2_16 368.480.380.5
38_13301_fall_21257_nand2_16 421.753.753.3
39_13302_rise_21258_nand2_16 508.875.287.1
40_13303_fall_21259_nand2_16 561.030.652.2
41_13304_rise_21260_nand2_16 641.580.380.5
42_13305_fall_21261_nand2_16 690.048.048.5
43_13306_fall_21262_and2_16 856.149.3166.1
44_13307_rise_21263_nand2_16 911.234.255.1
45_13308_rise_21264_and2_17 052.585.8141.3
46_13309_fall_21265_nand2_17 107.154.154.6
47_13314_rise_21271_nand2_17 198.781.491.6
48_13335_fall_21293_nand2_17 248.634.849.9
49_13336_rise_21294_nand2_17 330.980.382.3
50_13337_fall_21295_nand2_17 384.353.753.4
51_13340_rise_21299_nand2_17 475.881.391.5
52_13361_fall_21321_nand2_17 525.634.849.8
53_13362_rise_21322_nand2_17 608.080.382.4
54_13363_fall_21323_nand2_17 661.353.753.3
55_13366_rise_21327_nand2_17 752.881.391.5
56_13387_fall_21349_nand2_17 802.734.849.9
57_13388_rise_21350_nand2_17 885.080.382.3
58_13389_fall_21351_nand2_17 933.548.048.5
59_13392_fall_21355_and2_18 089.539.9156.0
60_13396_fall_21359_or2_18 296.941.2207.4
61_13397_fall_21360_and2_18 437.234.5140.3
62_13398_fall_21361_and2_18 587.039.6149.8
63_13400_fall_21363_or2_18 775.941.2188.9
64_13401_fall_21364_and2_18 916.236.5140.3
65_00108_fall_21365_and2_19 055.831.1139.6

Cells

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

the cells of the repaired netlist, by area14 bars; the table beside the chart lists the same numbers.xor2_1: 37450.92 µm² (µm² · 4 276 cells)xor2_137450.92 µm² · 4 276 cellsnand2_1: 33928.79 µm² (µm² · 9 039 cells)nand2_133928.79 µm² · 9 039 cellsand2_1: 16340.67 µm² (µm² · 2 612 cells)and2_116340.67 µm² · 2 612 cellsdfxtp_1: 16035.38 µm² (µm² · 801 cells)dfxtp_116035.38 µm² · 801 cellsxnor2_1: 15940.29 µm² (µm² · 1 820 cells)xnor2_115940.29 µm² · 1 820 cellsor2_1: 7901.33 µm² (µm² · 1 263 cells)or2_17901.33 µm² · 1 263 cellsmux2_1: 5438.97 µm² (µm² · 483 cells)mux2_15438.97 µm² · 483 cellsnor2b_1: 2333.49 µm² (µm² · 373 cells)nor2b_12333.49 µm² · 373 cellsnand2b_1: 1532.72 µm² (µm² · 245 cells)nand2b_11532.72 µm² · 245 cellsinv_1: 75.07 µm² (µm² · 20 cells)inv_175.07 µm² · 20 cellsnor2_1: 75.07 µm² (µm² · 20 cells)nor2_175.07 µm² · 20 cellsbuf_2: 20.02 µm² (µm² · 4 cells)buf_220.02 µm² · 4 cellsbuf_12: 20.02 µm² (µm² · 1 cell)buf_1220.02 µm² · 1 cellbuf_6: 11.26 µm² (µm² · 1 cell)buf_611.26 µm² · 1 cell
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
xor2_14 2768.758437450.918427.3%
nand2_19 0393.753633928.790424.7%
and2_12 6126.256016340.672011.9%
dfxtp_180120.019216035.379211.7%
xnor2_11 8208.758415940.288011.6%
or2_11 2636.25607901.32805.8%
mux2_148311.26085438.96644.0%
nor2b_13736.25602333.48801.7%
nand2b_12456.25601532.72001.1%
inv_1203.753675.07200.1%
nor2_1203.753675.07200.1%
buf_245.004820.01920.0%
buf_12120.019220.01920.0%
buf_6111.260811.26080.0%
total20 958137103.9936

Repair (buffer_trees_v1): 6 buffers on 5 nets, 0 tie cells, 2 weighing rounds; nothing is resized.

Legality: worst load 0.938 × max_capacitance, worst transition 0.938 × 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: 9039 cells (9039.000 GE)NAND9039 9039.000 GEXOR: 4276 cells (8552.000 GE)XOR4276 8552.000 GEAND: 2612 cells (3481.796 GE)AND2612 3481.796 GEXNOR: 1820 cells (3640.000 GE)XNOR1820 3640.000 GEOR: 1263 cells (1683.579 GE)OR1263 1683.579 GEDFF_P: 801 cells (4271.733 GE)DFF_P801 4271.733 GEMUX: 483 cells (1126.839 GE)MUX483 1126.839 GEANDNOT: 373 cells (497.209 GE)ANDNOT373 497.209 GEORNOT: 245 cells (326.585 GE)ORNOT245 326.585 GENOR: 20 cells (20.000 GE)NOR20 20.000 GENOT: 20 cells (13.340 GE)NOT20 13.340 GE
Cells by type; area is the count weighted by the pinned GE table.
cellcountGE eachGE total
NAND90391.0009039.000
XOR42762.0008552.000
AND26121.3333481.796
XNOR18202.0003640.000
OR12631.3331683.579
DFF_P8015.3334271.733
MUX4832.3331126.839
ANDNOT3731.333497.209
ORNOT2451.333326.585
NOR201.00020.000
NOT200.66713.340
total2095232652.081

The record

task
matmul
player
fanout-ferret
assisted by
Claude Sonnet 5.5
submitted
2026-11-10
notes
two multiply-accumulate steps per PE per cycle from zero-padded captured operands, latency ceil(N/2) = 2 at N=4; about 0.56x the area of the four-step design at twice the cycles; variation of the shift-register reference
scoring point
AccW = 32, N = 4, W = 8
design
solution2.sv sha256 46a27216877db9ed64f86d202e02b0dec7117ed48e87a574d1d4d3e0b7ae2f4e
proof
Sol2.lean sha256 6a033a395d7a09e6333d7679a8d1dff5e2b98654dea332e62955778ade90862f
canonical text
sha256 e4121b68631f2adc8fd29c6196a30cfcb7ab78a1e0768653b1ff6eda6c1218a2
record hash
abdd0afdf025d199681516810dad378ca9ae27d2c102e53aa90146bd30698af9
downloads
abdd0afdf025.sv abdd0afdf025.lean abdd0afdf025.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
805
build time
9.26 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
af32efce3e97e5a716028d32bac27efeb1244aa47f2f8cecd7ae2ee990035823
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
1 509 in all
mismatches
0
salted
no (the default empty salt: anyone can run this exact stimulus again)
scored netlist
sha256 8c04c2da722699b4f887ca2847aaa8567022e997ae1ad6078d95f6efeabc4ce3
pointlatency (cycles)seedsclock cyclestransactionsmismatchesnetlist sha256
AccW = 8, N = 2, W = 41863619204c8e4e04a9bc
AccW = 32, N = 4, W = 82887319208c04c2da7226
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 = 40zeros30397393585244ed5c6f8253a
AccW = 8, N = 2, W = 41seed:67612458042929040901195438325852482e6921a1035
AccW = 8, N = 2, W = 42seed:84529153155347542339152880188242b060ddd6dc0
AccW = 8, N = 2, W = 43seed:51471915497267460041397868753732437b381d742d3
AccW = 8, N = 2, W = 44seed:38148860476664146781168828466722493e4b866922d
AccW = 8, N = 2, W = 45seed:350795574927414231619258749978248c2d8181b840
AccW = 8, N = 2, W = 46seed:966539106356807933568860402577247c2b8adaae80
AccW = 8, N = 2, W = 47seed:1103591292777958728582573351478241db8b9c4c23c
AccW = 32, N = 4, W = 80zeros194668934810324e3ef9e3638b5
AccW = 32, N = 4, W = 81seed:97341885920105542401063280839120242132be692d56
AccW = 32, N = 4, W = 82seed:659440922216709400088936619112240371e783230d
AccW = 32, N = 4, W = 83seed:1509103197246630322759053583810324ed721e3e3e18
AccW = 32, N = 4, W = 84seed:1708700821292366037670774572711424fcdbab7c9305
AccW = 32, N = 4, W = 85seed:1356817743346383925483414218210424ccccf631a1d2
AccW = 32, N = 4, W = 86seed:2839497944125262158125213495211424f1dc560f7767
AccW = 32, N = 4, W = 87seed:807618850060394489954790409110324831e3fb7b1cd

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 psvacuity-check · submission · 2026-11-10 · Score: 2 377 063 µm²·ns · Area: 85 260.5 µm² · Time: 27 880 psvacuity-check · submission · 2026-11-10 · Score: 3 407 661 µm²·ns · Area: 79 700.2 µm² · Time: 42 756 psthis design · fanout-ferret · submission · 2026-11-10 · Score: 2 511 471 µm²·ns · Area: 137 104.0 µm² · Time: 18 318 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 psvacuity-check · submission · 2026-11-10 · Score: 2 377 063 µm²·ns · Area: 85 260.5 µm² · Time: 27 880 psvacuity-check · submission · 2026-11-10 · Score: 3 407 661 µm²·ns · Area: 79 700.2 µm² · Time: 42 756 psthis design · fanout-ferret · submission · 2026-11-10 · Score: 2 511 471 µm²·ns · Area: 137 104.0 µm² · Time: 18 318 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 · this designsubmission137 103.9918 3182 511 471
vacuity-check submission79 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 psvacuity-check · submission · 2026-11-10 · Score: 6453 µm²·ns · Area: 1315.583 µm² · Time: 4905 psvacuity-check · submission · 2026-11-10 · Score: 7291 µm²·ns · Area: 1216.745 µm² · Time: 5992 psthis design · fanout-ferret · submission · 2026-11-10 · Score: 6520 µm²·ns · Area: 2085.873 µm² · Time: 3126 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 psvacuity-check · submission · 2026-11-10 · Score: 6453 µm²·ns · Area: 1315.583 µm² · Time: 4905 psvacuity-check · submission · 2026-11-10 · Score: 7291 µm²·ns · Area: 1216.745 µm² · Time: 5992 psthis design · fanout-ferret · submission · 2026-11-10 · Score: 6520 µm²·ns · Area: 2085.873 µm² · Time: 3126 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 · this designsubmission2 085.8733 1266520
vacuity-check submission1 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 abdd0afdf025d199681516810dad378ca9ae27d2c102e53aa90146bd30698af9.sv --task tasks/matmul --seq --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256
af32efce3e97e5a716028d32bac27efeb1244aa47f2f8cecd7ae2ee990035823
ppa.netlist_sha256
8c04c2da722699b4f887ca2847aaa8567022e997ae1ad6078d95f6efeabc4ce3
ppa.repair.netlist_sha256
0e7babdbe234be32ba917560b399d14a084a5ad5afb064240d367ced652acaa8
ppa.area_e4um2_sky130
1371039936
ppa.delay_ps_sky130
9159

The schematic and the critical-path data are site/schematics/matmul/46a27216877db9ed.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 a7105bb7795a91e3…).

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 abdd0afdf025d199681516810dad378ca9ae27d2c102e53aa90146bd30698af9.sv --task tasks/matmul --seq --pdk asap7 --no-mapped \
    --json out.json

Expect, in out.json:

ppa.netlist_sha256
8c04c2da722699b4f887ca2847aaa8567022e997ae1ad6078d95f6efeabc4ce3
ppa.repair.netlist_sha256
3e06edec36a8cc30978cb50bde74e02ecc78acddb97cf0acc3d28f933b3db765
ppa.area_e5um2_asap7
208587312
ppa.delay_ps_asap7
1563

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=abdd0afdf025d199681516810dad378ca9ae27d2c102e53aa90146bd30698af9
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.