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 1ffe71156e90

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

Area

241 920.77µm²

241 920.7712 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
+177.5% largermatmul_g1 · 87 173.61 µm²
on this page
5th of 5 designs
cells
38 735
flops
800
repair
6 buffers, 0 tie cells
GE
57 547.772 extra

Performance · time

9 410ps

1 cycle × 9 410 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
−78.0% fastermatmul_g1 · 42 784 ps
on this page
fastest of 5 designs
Fmax-eq.
106.3 MHz derived
critical path
66 cells
unit depth
73 extra

Score · area × time

2 276 474µm²·ns

241 920.7712 µm² × 9 410 ps

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

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

3 661.548µm²

3 661.54830 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par
+174.3% largermatmul_g1 · 1 334.726 µm²
on this page
5th of 5 designs
cells
41 035
flops
800
repair
16 buffers, 0 tie cells
GE
57 547.772 extra

Performance · time

1 621ps

1 cycle × 1 621 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
−73.7% fastermatmul_g1 · 6 156 ps
on this page
fastest of 5 designs
Fmax-eq.
616.9 MHz derived
unit depth
73 extra

Score · area × time

5935µm²·ns

3 661.54830 µm² × 1 621 ps

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

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

solution.svdownload
// matmul, G4: four multiply-accumulate steps per PE per cycle.
// `start` captures A and B (zero-extended into registers with three spare entries / rows, so the
// four static windows below stay in range for every N); every busy cycle adds
//   A[i][k..k+3] . B[k..k+3][j]   (entries past N read as 0)
// to C[i][j] and shifts the captured operands by four entries (A) / four rows (B). `done` rises
// after ceil(N/4) busy cycles: latency (N+3)/4 = 1 at the scoring point N = 4.
// The shifts are written as two shifts of half the amount so that no shift amount can wrap at 32 bits.
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+3)*W-1:0]   a_sh;
  logic [(N*N+3*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'd4;
      a_sh <= (a_sh >> (2*W)) >> (2*W);
      b_sh <= (b_sh >> (2*N*W)) >> (2*N*W);
      if (k + 32'd4 >= 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]}
              + {{AccW{a_sh[(i*N+2)*W + W - 1]}}, a_sh[(i*N+2)*W +: W]}
              * {{AccW{b_sh[(2*N+j)*W + W - 1]}}, b_sh[(2*N+j)*W +: W]}
              + {{AccW{a_sh[(i*N+3)*W + W - 1]}}, a_sh[(i*N+3)*W +: W]}
              * {{AccW{b_sh[(3*N+j)*W + W - 1]}}, b_sh[(3*N+j)*W +: W]};
    end
  end
endmodule
Sol.lean (855 code lines) 
-- svgolf-latency: 1
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/4)` snapshots after the start's (1 at the scoring point). -/
def lat (N _W _AccW : Nat) : Nat := (N + 3) / 4

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

/-- Four multiply-accumulates at a wider width, truncated back (`Lib.setWidth_add_mul_signExtend` four times). -/
theorem setWidth_add4_mul_signExtend {m n w : Nat} (h : m ≤ n) (x : BitVec m)
    (a0 b0 a1 b1 a2 b2 a3 b3 : BitVec w) :
    (x.setWidth n + a0.signExtend n * b0.signExtend n + a1.signExtend n * b1.signExtend n
      + a2.signExtend n * b2.signExtend n + a3.signExtend n * b3.signExtend n).setWidth m =
    x + BitVec.ofInt m (a0.toInt * b0.toInt) + BitVec.ofInt m (a1.toInt * b1.toInt)
      + BitVec.ofInt m (a2.toInt * b2.toInt) + BitVec.ofInt m (a3.toInt * b3.toInt) := by
  rw [BitVec.setWidth_add _ _ h, BitVec.setWidth_add _ _ h, 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, 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 four-step counter test: `t < N < 2^31`, `t + 4` at 32 bits against `N`. -/
theorem ge_four_iff {t N : Nat} (ht : t < N) (hN : N < 2 ^ 31) :
    BitVec.ofNat 32 N ≤ BitVec.ofNat 32 t + 4#32 ↔ N ≤ t + 4 := 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 four `a_sh` windows `[(i·N + m)·W +: W]`, `m ≤ 3`, lie inside the `(N·N + 3)·W`-bit register. -/
theorem winA_le {N W i : Nat} (m : Nat) (hm : m ≤ 3) (hi : i < N) : (i * N + m) * W + W ≤ (N * N + 3) * 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 + 3 := 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 four `b_sh` windows `[(m·N + j)·W +: W]`, `m ≤ 3`, lie inside the `(N·N + 3·N)·W`-bit register. -/
theorem winB_le {N W j : Nat} (m : Nat) (hm : m ≤ 3) (hj : j < N) :
    (m * N + j) * W + W ≤ (N * N + 3 * N) * W := by
  have h1 : m * N ≤ 3 * 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 + 3 * 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 four products `A[i][k+m]·B[k+m][j]` (`m < 4`) 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 (.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)))
          (mulT AccW W ((i * N + 2) * W) ((2 * N + j) * W)))
          (mulT AccW W ((i * N + 3) * W) ((3 * 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 four), 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 + 3) * W) (.ident "A")),
        .nbaAssign (.ident "b_sh") (.resize ((N * N + 3 * N) * W) (.ident "B"))])
      (some (.ifStmt (.ident "busy")
        (.block #[.nbaAssign (.ident "k") (.binary .add (.ident "k") (c32 4)),
          .nbaAssign (.ident "a_sh")
            (.binary (.shr false) (.binary (.shr false) (.ident "a_sh") (amtA W)) (amtA W)),
          .nbaAssign (.ident "b_sh")
            (.binary (.shr false) (.binary (.shr false) (.ident "b_sh") (amtB N W)) (amtB N W)),
          .ifStmt (.binary .ge (.binary .add (.ident "k") (c32 4)) (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 + 3) * W) ((N * N + 3 * 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 + 3) * W - 1).natAbs + 1)
        (((N * N + 3 * 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 + 3) * W) ((N * N + 3 * 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 + 3) * W := Nat.mul_pos (by omega) hW
  have pQ : 0 < (N * N + 3 * N) * W := Nat.mul_pos (by omega) hW
  have hcP : (((N : Int) * N + 3) * W - 1).natAbs + 1 = (N * N + 3) * 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 + 3 * N) * W - 1).natAbs + 1 = (N * N + 3 * 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 + 3) * W := by
    have h : 1 ≤ (N * N + 3) * W := pP
    exact_mod_cast h
  have hNQ : (1 : Int) ≤ (N * N + 3 * N) * W := by
    have h : 1 ≤ (N * N + 3 * 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 + 3) * 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 + 3) * W)
    (winA_le (N := N) (W := W) 1 (by omega) hi) hW (by simp) (by simp)
  have ha2 := Lib.window_bounds_of_natCast (((i : Int) * N + 2) * W) ((N * N + 3) * W)
    (winA_le (N := N) (W := W) 2 (by omega) hi) hW (by simp) (by simp)
  have ha3 := Lib.window_bounds_of_natCast (((i : Int) * N + 3) * W) ((N * N + 3) * W)
    (winA_le (N := N) (W := W) 3 (by omega) hi) hW (by simp) (by simp)
  have hb0 := Lib.window_bounds_of_natCast ((j : Int) * W) ((N * N + 3 * 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 + 3 * N) * W)
    (winB_le (N := N) (W := W) 1 (by omega) hj) hW (by simp) (by simp)
  have hb2 := Lib.window_bounds_of_natCast ((2 * (N : Int) + j) * W) ((N * N + 3 * N) * W)
    (winB_le (N := N) (W := W) 2 (by omega) hj) hW (by simp) (by simp)
  have hb3 := Lib.window_bounds_of_natCast ((3 * (N : Int) + j) * W) ((N * N + 3 * N) * W)
    (winB_le (N := N) (W := W) 3 (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 + 3) * W) ((N * N + 3 * N) * W) (N * N * AccW)) mmElems
        (mmPEs N W AccW)) := by
  have hd := mm_decls N W AccW
  have pP : 0 < (N * N + 3) * W := Nat.mul_pos (by omega) hW
  have pQ : 0 < (N * N + 3 * N) * W := Nat.mul_pos (by omega) hW
  have eP : (((N : Int) * N + 3) * W - 1).natAbs + 1 = (N * N + 3) * 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 + 3 * N) * W - 1).natAbs + 1 = (N * N + 3 * 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) >> (2·W)`, evaluated. -/
def shA (W : Nat) (v : LVec) : LVec :=
  (v.shr ((LVec.ofInt 32 2).mul (LVec.ofInt 32 (W : Int)))).shr ((LVec.ofInt 32 2).mul (LVec.ofInt 32 (W : Int)))

/-- `v >> (2·N·W) >> (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)))).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 + 3) * W)),
    wr "b_sh" bsh (b.resizeU ((N * N + 3 * N) * W))]
  else if bz.condTrue then
    if (LVec.ofLogic ((k.add (LVec.ofInt 32 4)).ge (LVec.ofInt 32 (N : Int)))).condTrue then
      [wr "k" k (k.add (LVec.ofInt 32 4)), 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 4)), 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 (four 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))
  let r3 := r2.add (mulV AccW W ash bsh ((i * N + 2) * W) ((2 * N + j) * W))
  let r4 := r3.add (mulV AccW W ash bsh ((i * N + 3) * W) ((3 * N + j) * W))
  r4.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 4)).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_add4 (N W : Nat) {n : Nat} (A B : BitVec n) (t i j : Nat) : psum N W A B (t + 4) 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)
      + Tasks.Matmul.entry W A (i * N + (t + 2)) * Tasks.Matmul.entry W B ((t + 2) * N + j)
      + Tasks.Matmul.entry W A (i * N + (t + 3)) * Tasks.Matmul.entry W B ((t + 3) * 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
  have h3 : psum N W A B (t + 3) i j = _ := psum_succ N W A B (t + 2) i j
  have h4 : psum N W A B (t + 4) i j = _ := psum_succ N W A B (t + 3) i j
  rw [h4, h3, 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 + 3) * W) := A.setWidth ((N * N + 3) * W)

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

/-- The `A` window of step `t + m`, as the shifted register shows it. -/
theorem eA {t i N W : Nat} (m : Nat) : t * W + (i * N + m) * W = (i * N + (t + m)) * W := by
  rw [← Nat.add_mul]; congr 1; omega

/-- The `B` window of step `t + m`, as the shifted register shows it. -/
theorem eB {t j N W : Nat} (m : Nat) : t * (N * W) + (m * N + j) * W = ((t + m) * N + j) * W := by
  simp only [Nat.add_mul, Nat.mul_add, Nat.mul_assoc]; omega

/-- **PE `(i, j)` in a busy cycle** adds `Σ_{m<4} 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 + 4) ((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 + 3) * 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 wa2 := winA_le (N := N) (W := W) (i := i) 2 (by omega) hi
  have wa3 := winA_le (N := N) (W := W) (i := i) 3 (by omega) hi
  have wb0 : j * W + W ≤ (N * N + 3 * 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 + 3 * N) * W := by
    simpa using winB_le (N := N) (W := W) (j := j) 1 (by omega) hj
  have wb2 := winB_le (N := N) (W := W) (j := j) 2 (by omega) hj
  have wb3 := winB_le (N := N) (W := W) (j := j) 3 (by omega) hj
  have hpA : N * N * W ≤ (N * N + 3) * W := Nat.mul_le_mul_right W (by omega)
  have hpB : N * N * W ≤ (N * N + 3 * 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 := eA (t := t) (i := i) (N := N) (W := W) 1
  have eA2 := eA (t := t) (i := i) (N := N) (W := W) 2
  have eA3 := eA (t := t) (i := i) (N := N) (W := W) 3
  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
  have eB2 := eB (t := t) (j := j) (N := N) (W := W) 2
  have eB3 := eB (t := t) (j := j) (N := N) (W := W) 3
  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_add4_mul_signExtend, Lib.extractLsb'_ushiftRight, extractLsb'_setWidth_of_le,
    e1, e2, eA1, eA2, eA3, eB1, eB2, eB3, psum_add4, 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 four, the shift registers shift by four 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 + 4))) c
      (.ofBitVec (BitVec.ofNat 32 (t + 4))) (knownBit (decide (¬ N ≤ t + 4)))
      (.ofBitVec (padA N W A >>> (t * W + 2 * W + 2 * W)))
      (.ofBitVec (padB N W B >>> (t * (N * W) + 2 * 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
  have h4' : LVec.ofInt 32 4 = LVec.ofBitVec 4#32 := by decide
  simp only [ctrlQ, shA, shB, wr, condTrue_knownBit, Bool.false_eq_true, ↓reduceIte, h2', h4',
    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_four_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 + 4 <;>
    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 + 4`; `done` rises (and `busy` falls) exactly when `N ≤ t + 4`. -/
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 + 4))) (accC N W AccW A B (t + 4))
      (.ofBitVec (BitVec.ofNat 32 (t + 4))) (knownBit (decide (¬ N ≤ t + 4)))
      (.ofBitVec (padA N W A >>> ((t + 4) * W))) (.ofBitVec (padB N W B >>> ((t + 4) * (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 + 4) (r / N) (r % N))))
    (fun i j hi hj => pe_step hW A B hi hj)
  have eA4 : t * W + 2 * W + 2 * W = (t + 4) * W := by rw [Nat.add_mul]; omega
  have eB4 : t * (N * W) + 2 * N * W + 2 * N * W = (t + 4) * (N * W) := by
    simp only [Nat.add_mul, Nat.mul_assoc]; omega
  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 + 3) * W ∧
    bsh.width = (N * N + 3 * 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 4)).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 + 3) * W), .xVec ((N * N + 3 * 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 + 3) / 4) (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 = 4 * j ∧ j + m + 1 = (N + 3) / 4 ∧ 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 + 3) / 4 - 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 + 4
    · 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 + 4, 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 + 3) * 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 wa2 := winA_le (N := N) (W := W) (i := i) 2 (by omega) hi
  have wa3 := winA_le (N := N) (W := W) (i := i) 3 (by omega) hi
  have wb0 : j * W + W ≤ (N * N + 3 * N) * W := by
    simpa using winB_le (N := N) (W := W) (j := j) 0 (by omega) hj
  have wb1 := winB_le (N := N) (W := W) (j := j) 1 (by omega) hj
  have wb2 := winB_le (N := N) (W := W) (j := j) 2 (by omega) hj
  have wb3 := winB_le (N := N) (W := W) (j := j) 3 (by omega) hj
  have sa0 : i * N * W + W - 1 + 1 ≤ (N * N + 3) * W := by omega
  have sa1 : (i * N + 1) * W + W - 1 + 1 ≤ (N * N + 3) * W := by omega
  have sa2 : (i * N + 2) * W + W - 1 + 1 ≤ (N * N + 3) * W := by omega
  have sa3 : (i * N + 3) * W + W - 1 + 1 ≤ (N * N + 3) * W := by omega
  have wb1' : (N + j) * W + W ≤ (N * N + 3 * N) * W := by
    simpa using winB_le (N := N) (W := W) (j := j) 1 (by omega) hj
  have wb2' : (2 * N + j) * W + W ≤ (N * N + 3 * N) * W := winB_le (N := N) (W := W) (j := j) 2 (by omega) hj
  have wb3' : (3 * N + j) * W + W ≤ (N * N + 3 * N) * W := winB_le (N := N) (W := W) (j := j) 3 (by omega) hj
  have sb0 : j * W + W - 1 + 1 ≤ (N * N + 3 * N) * W := by omega
  have sb1 : (N + j) * W + W - 1 + 1 ≤ (N * N + 3 * N) * W := by omega
  have sb2 : (2 * N + j) * W + W - 1 + 1 ≤ (N * N + 3 * N) * W := by omega
  have sb3 : (3 * N + j) * W + W - 1 + 1 ≤ (N * N + 3 * N) * W := by omega
  have sa0 : i * N * W + W - 1 + 1 ≤ (N * N + 3) * W := by omega
  have sa1 : (i * N + 1) * W + W - 1 + 1 ≤ (N * N + 3) * W := by omega
  have sa2 : (i * N + 2) * W + W - 1 + 1 ≤ (N * N + 3) * W := by omega
  have sa3 : (i * N + 3) * W + W - 1 + 1 ≤ (N * N + 3) * W := by omega
  simp [xsProc, xsStmt, xsOpt, xsLhs, xsWidth, xsWidthList, binW, sigWidth, mmPE, mulT, sext, mmD, mmDecls,
    LVec.replicate_l0, hC, wa0, wa1, wa2, wa3, wb0, wb1', wb2', wb3', sa0, sa1, sa2, sa3, sb0, sb1, sb2, sb3]

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 + 3) / 4 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 _0586_ · sky130_fd_sc_hd__nor2_1 nor2_1 _0587_ · sky130_fd_sc_hd__or2_1 or2_1 _0588_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0589_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0590_ · sky130_fd_sc_hd__or2_1 or2_1 _0591_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0592_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0593_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0594_ · sky130_fd_sc_hd__or2_1 or2_1 _0595_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0596_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0597_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0598_ · sky130_fd_sc_hd__or2_1 or2_1 _0599_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0600_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0601_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0602_ · sky130_fd_sc_hd__or2_1 or2_1 _0603_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0604_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0605_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0606_ · sky130_fd_sc_hd__or2_1 or2_1 _0607_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0608_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0609_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0610_ · sky130_fd_sc_hd__or2_1 or2_1 _0611_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0612_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0613_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0614_ · sky130_fd_sc_hd__or2_1 or2_1 _0615_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0616_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0617_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0618_ · sky130_fd_sc_hd__or2_1 or2_1 _0619_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0620_ · sky130_fd_sc_hd__and2_1 and2_1 _0621_ · sky130_fd_sc_hd__and2_1 and2_1 _0622_ · sky130_fd_sc_hd__and2_1 and2_1 _0623_ · sky130_fd_sc_hd__and2_1 and2_1 _0624_ · sky130_fd_sc_hd__and2_1 and2_1 _0625_ · sky130_fd_sc_hd__and2_1 and2_1 _0626_ · sky130_fd_sc_hd__and2_1 and2_1 _0627_ · sky130_fd_sc_hd__and2_1 and2_1 _0628_ · sky130_fd_sc_hd__and2_1 and2_1 _0629_ · sky130_fd_sc_hd__and2_1 and2_1 _0630_ · sky130_fd_sc_hd__and2_1 and2_1 _0631_ · sky130_fd_sc_hd__and2_1 and2_1 _0632_ · sky130_fd_sc_hd__and2_1 and2_1 _0633_ · sky130_fd_sc_hd__and2_1 and2_1 _0634_ · sky130_fd_sc_hd__and2_1 and2_1 _0635_ · sky130_fd_sc_hd__and2_1 and2_1 _0636_ · sky130_fd_sc_hd__and2_1 and2_1 _0637_ · sky130_fd_sc_hd__and2_1 and2_1 _0638_ · sky130_fd_sc_hd__and2_1 and2_1 _0639_ · sky130_fd_sc_hd__and2_1 and2_1 _0640_ · sky130_fd_sc_hd__and2_1 and2_1 _0641_ · sky130_fd_sc_hd__and2_1 and2_1 _0642_ · sky130_fd_sc_hd__and2_1 and2_1 _0643_ · sky130_fd_sc_hd__and2_1 and2_1 _0644_ · sky130_fd_sc_hd__and2_1 and2_1 _0645_ · sky130_fd_sc_hd__and2_1 and2_1 _0646_ · sky130_fd_sc_hd__and2_1 and2_1 _0647_ · sky130_fd_sc_hd__and2_1 and2_1 _0648_ · sky130_fd_sc_hd__and2_1 and2_1 _0649_ · sky130_fd_sc_hd__and2_1 and2_1 _0650_ · sky130_fd_sc_hd__and2_1 and2_1 _0651_ · sky130_fd_sc_hd__and2_1 and2_1 _0652_ · sky130_fd_sc_hd__and2_1 and2_1 _0653_ · sky130_fd_sc_hd__and2_1 and2_1 _0654_ · sky130_fd_sc_hd__and2_1 and2_1 _0655_ · sky130_fd_sc_hd__and2_1 and2_1 _0656_ · sky130_fd_sc_hd__and2_1 and2_1 _0657_ · sky130_fd_sc_hd__and2_1 and2_1 _0658_ · sky130_fd_sc_hd__and2_1 and2_1 _0659_ · sky130_fd_sc_hd__and2_1 and2_1 _0660_ · sky130_fd_sc_hd__and2_1 and2_1 _0661_ · sky130_fd_sc_hd__and2_1 and2_1 _0662_ · sky130_fd_sc_hd__and2_1 and2_1 _0663_ · sky130_fd_sc_hd__and2_1 and2_1 _0664_ · sky130_fd_sc_hd__and2_1 and2_1 _0665_ · sky130_fd_sc_hd__or2_1 or2_1 _0666_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0667_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0668_ · sky130_fd_sc_hd__or2_1 or2_1 _0669_ · sky130_fd_sc_hd__nor2_1 nor2_1 _0670_ · sky130_fd_sc_hd__and2_1 and2_1 _0671_ · sky130_fd_sc_hd__and2_1 and2_1 _0672_ · sky130_fd_sc_hd__or2_1 or2_1 _0673_ · sky130_fd_sc_hd__and2_1 and2_1 _0674_ · sky130_fd_sc_hd__nor2b_1 nor2b_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__or2_1 or2_1 _0680_ · sky130_fd_sc_hd__and2_1 and2_1 _0681_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0682_ · sky130_fd_sc_hd__and2_1 and2_1 _0683_ · sky130_fd_sc_hd__and2_1 and2_1 _0684_ · sky130_fd_sc_hd__or2_1 or2_1 _0685_ · sky130_fd_sc_hd__and2_1 and2_1 _0686_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0687_ · sky130_fd_sc_hd__and2_1 and2_1 _0688_ · sky130_fd_sc_hd__or2_1 or2_1 _0689_ · sky130_fd_sc_hd__and2_1 and2_1 _0690_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0691_ · sky130_fd_sc_hd__and2_1 and2_1 _0692_ · sky130_fd_sc_hd__or2_1 or2_1 _0693_ · sky130_fd_sc_hd__and2_1 and2_1 _0694_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0695_ · sky130_fd_sc_hd__or2_1 or2_1 _0696_ · sky130_fd_sc_hd__and2_1 and2_1 _0697_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0698_ · sky130_fd_sc_hd__and2_1 and2_1 _0699_ · sky130_fd_sc_hd__and2_1 and2_1 _0700_ · sky130_fd_sc_hd__or2_1 or2_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__nor2b_1 nor2b_1 _0707_ · sky130_fd_sc_hd__or2_1 or2_1 _0708_ · sky130_fd_sc_hd__and2_1 and2_1 _0709_ · sky130_fd_sc_hd__and2_1 and2_1 _0710_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0711_ · sky130_fd_sc_hd__or2_1 or2_1 _0712_ · sky130_fd_sc_hd__and2_1 and2_1 _0713_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0714_ · sky130_fd_sc_hd__and2_1 and2_1 _0715_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0716_ · sky130_fd_sc_hd__and2_1 and2_1 _0717_ · sky130_fd_sc_hd__and2_1 and2_1 _0718_ · sky130_fd_sc_hd__and2_1 and2_1 _0719_ · sky130_fd_sc_hd__and2_1 and2_1 _0720_ · sky130_fd_sc_hd__and2_1 and2_1 _0721_ · sky130_fd_sc_hd__and2_1 and2_1 _0722_ · sky130_fd_sc_hd__and2_1 and2_1 _0723_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0724_ · sky130_fd_sc_hd__and2_1 and2_1 _0725_ · sky130_fd_sc_hd__or2_1 or2_1 _0726_ · sky130_fd_sc_hd__and2_1 and2_1 _0727_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0728_ · sky130_fd_sc_hd__and2_1 and2_1 _0729_ · sky130_fd_sc_hd__or2_1 or2_1 _0730_ · sky130_fd_sc_hd__and2_1 and2_1 _0731_ · sky130_fd_sc_hd__and2_1 and2_1 _0732_ · sky130_fd_sc_hd__and2_1 and2_1 _0733_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0734_ · sky130_fd_sc_hd__or2_1 or2_1 _0735_ · sky130_fd_sc_hd__and2_1 and2_1 _0736_ · sky130_fd_sc_hd__and2_1 and2_1 _0737_ · sky130_fd_sc_hd__and2_1 and2_1 _0738_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0739_ · sky130_fd_sc_hd__or2_1 or2_1 _0740_ · sky130_fd_sc_hd__and2_1 and2_1 _0741_ · sky130_fd_sc_hd__and2_1 and2_1 _0742_ · sky130_fd_sc_hd__and2_1 and2_1 _0743_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0744_ · sky130_fd_sc_hd__or2_1 or2_1 _0745_ · sky130_fd_sc_hd__and2_1 and2_1 _0746_ · sky130_fd_sc_hd__and2_1 and2_1 _0747_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0748_ · sky130_fd_sc_hd__or2_1 or2_1 _0749_ · sky130_fd_sc_hd__and2_1 and2_1 _0750_ · sky130_fd_sc_hd__and2_1 and2_1 _0751_ · sky130_fd_sc_hd__and2_1 and2_1 _0752_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0753_ · sky130_fd_sc_hd__or2_1 or2_1 _0754_ · sky130_fd_sc_hd__and2_1 and2_1 _0755_ · sky130_fd_sc_hd__and2_1 and2_1 _0756_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0757_ · sky130_fd_sc_hd__or2_1 or2_1 _0758_ · sky130_fd_sc_hd__and2_1 and2_1 _0759_ · sky130_fd_sc_hd__and2_1 and2_1 _0760_ · sky130_fd_sc_hd__and2_1 and2_1 _0761_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0762_ · sky130_fd_sc_hd__or2_1 or2_1 _0763_ · sky130_fd_sc_hd__and2_1 and2_1 _0764_ · sky130_fd_sc_hd__and2_1 and2_1 _0765_ · sky130_fd_sc_hd__and2_1 and2_1 _0766_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0767_ · sky130_fd_sc_hd__or2_1 or2_1 _0768_ · sky130_fd_sc_hd__and2_1 and2_1 _0769_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0770_ · sky130_fd_sc_hd__and2_1 and2_1 _0771_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0772_ · sky130_fd_sc_hd__and2_1 and2_1 _0773_ · sky130_fd_sc_hd__and2_1 and2_1 _0774_ · sky130_fd_sc_hd__and2_1 and2_1 _0775_ · sky130_fd_sc_hd__or2_1 or2_1 _0776_ · sky130_fd_sc_hd__and2_1 and2_1 _0777_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0778_ · sky130_fd_sc_hd__and2_1 and2_1 _0779_ · sky130_fd_sc_hd__or2_1 or2_1 _0780_ · sky130_fd_sc_hd__and2_1 and2_1 _0781_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0782_ · sky130_fd_sc_hd__or2_1 or2_1 _0783_ · sky130_fd_sc_hd__and2_1 and2_1 _0784_ · sky130_fd_sc_hd__and2_1 and2_1 _0785_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0786_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0787_ · sky130_fd_sc_hd__or2_1 or2_1 _0788_ · sky130_fd_sc_hd__and2_1 and2_1 _0789_ · sky130_fd_sc_hd__and2_1 and2_1 _0790_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0791_ · sky130_fd_sc_hd__and2_1 and2_1 _0792_ · sky130_fd_sc_hd__and2_1 and2_1 _0793_ · sky130_fd_sc_hd__or2_1 or2_1 _0794_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0795_ · sky130_fd_sc_hd__and2_1 and2_1 _0796_ · sky130_fd_sc_hd__and2_1 and2_1 _0797_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0798_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0799_ · sky130_fd_sc_hd__or2_1 or2_1 _0800_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0801_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0802_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0803_ · sky130_fd_sc_hd__or2_1 or2_1 _0804_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0805_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0806_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0807_ · sky130_fd_sc_hd__or2_1 or2_1 _0808_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0809_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0810_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0811_ · sky130_fd_sc_hd__or2_1 or2_1 _0812_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0813_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0814_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0815_ · sky130_fd_sc_hd__or2_1 or2_1 _0816_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0817_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0818_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0819_ · sky130_fd_sc_hd__or2_1 or2_1 _0820_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0821_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0822_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0823_ · sky130_fd_sc_hd__or2_1 or2_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__or2_1 or2_1 _0828_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0829_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0830_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0831_ · sky130_fd_sc_hd__and2_1 and2_1 _0832_ · sky130_fd_sc_hd__and2_1 and2_1 _0833_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0834_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0835_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0836_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0837_ · sky130_fd_sc_hd__or2_1 or2_1 _0838_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0839_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0840_ · sky130_fd_sc_hd__and2_1 and2_1 _0841_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0842_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0843_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0844_ · sky130_fd_sc_hd__and2_1 and2_1 _0845_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0846_ · sky130_fd_sc_hd__and2_1 and2_1 _0847_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0848_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0849_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0850_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0851_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0852_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0853_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0854_ · sky130_fd_sc_hd__and2_1 and2_1 _0855_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0856_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0857_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0858_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0859_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0860_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0861_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0862_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0863_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0864_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0865_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0866_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0867_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0868_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0869_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0870_ · sky130_fd_sc_hd__or2_1 or2_1 _0871_ · sky130_fd_sc_hd__and2_1 and2_1 _0872_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0873_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0874_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0875_ · sky130_fd_sc_hd__or2_1 or2_1 _0876_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0877_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0878_ · sky130_fd_sc_hd__xnor2_1 xnor2_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__xor2_1 xor2_1 _0883_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0884_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0885_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0886_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0887_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0888_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0889_ · sky130_fd_sc_hd__and2_1 and2_1 _0890_ · sky130_fd_sc_hd__and2_1 and2_1 _0891_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0892_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0893_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0894_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0895_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0896_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0897_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0898_ · sky130_fd_sc_hd__or2_1 or2_1 _0899_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0900_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0901_ · sky130_fd_sc_hd__and2_1 and2_1 _0902_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0903_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0904_ · sky130_fd_sc_hd__and2_1 and2_1 _0905_ · sky130_fd_sc_hd__and2_1 and2_1 _0906_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0907_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0908_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0909_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0910_ · sky130_fd_sc_hd__or2_1 or2_1 _0911_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0912_ · sky130_fd_sc_hd__and2_1 and2_1 _0913_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0914_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0915_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0916_ · sky130_fd_sc_hd__and2_1 and2_1 _0917_ · sky130_fd_sc_hd__and2_1 and2_1 _0918_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0919_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0920_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0921_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0922_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0923_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0924_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0925_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0926_ · sky130_fd_sc_hd__and2_1 and2_1 _0927_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0928_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0929_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0930_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0931_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0932_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0933_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0934_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0935_ · sky130_fd_sc_hd__or2_1 or2_1 _0936_ · sky130_fd_sc_hd__and2_1 and2_1 _0937_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0938_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0939_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0940_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0941_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0942_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0943_ · sky130_fd_sc_hd__or2_1 or2_1 _0944_ · sky130_fd_sc_hd__and2_1 and2_1 _0945_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0946_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _0947_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0948_ · sky130_fd_sc_hd__or2_1 or2_1 _0949_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0950_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0951_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0952_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0953_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0954_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0955_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0956_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0957_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0958_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0959_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0960_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0961_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0962_ · sky130_fd_sc_hd__and2_1 and2_1 _0963_ · sky130_fd_sc_hd__and2_1 and2_1 _0964_ · sky130_fd_sc_hd__and2_1 and2_1 _0965_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0966_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0967_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0968_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0969_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0970_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0971_ · sky130_fd_sc_hd__or2_1 or2_1 _0972_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0973_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0974_ · sky130_fd_sc_hd__and2_1 and2_1 _0975_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0976_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0977_ · sky130_fd_sc_hd__and2_1 and2_1 _0978_ · sky130_fd_sc_hd__and2_1 and2_1 _0979_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0980_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _0981_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0982_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0983_ · sky130_fd_sc_hd__or2_1 or2_1 _0984_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0985_ · sky130_fd_sc_hd__and2_1 and2_1 _0986_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0987_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0988_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0989_ · sky130_fd_sc_hd__and2_1 and2_1 _0990_ · sky130_fd_sc_hd__and2_1 and2_1 _0991_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0992_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0993_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0994_ · sky130_fd_sc_hd__xor2_1 xor2_1 _0995_ · sky130_fd_sc_hd__nand2_1 nand2_1 _0996_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0997_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _0998_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _0999_ · sky130_fd_sc_hd__and2_1 and2_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[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__xor2_1 xor2_1 _1001_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1002_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1003_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1004_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1005_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _1006_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1007_ · sky130_fd_sc_hd__or2_1 or2_1 _1008_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1009_ · sky130_fd_sc_hd__and2_1 and2_1 _1010_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1011_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1012_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1013_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1014_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1015_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1016_ · sky130_fd_sc_hd__or2_1 or2_1 _1017_ · sky130_fd_sc_hd__and2_1 and2_1 _1018_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _1019_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _1020_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1021_ · sky130_fd_sc_hd__or2_1 or2_1 _1022_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1023_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1024_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1025_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1026_ · sky130_fd_sc_hd__xor2_1 xor2_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__xor2_1 xor2_1 _1031_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1032_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1033_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1034_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1035_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1036_ · sky130_fd_sc_hd__and2_1 and2_1 _1037_ · sky130_fd_sc_hd__and2_1 and2_1 _1038_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1039_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _1040_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1041_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1042_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1043_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1044_ · sky130_fd_sc_hd__xnor2_1 xnor2_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__nor2b_1 nor2b_1 _1049_ · sky130_fd_sc_hd__and2_1 and2_1 _1050_ · sky130_fd_sc_hd__and2_1 and2_1 _1051_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1052_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _1053_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1054_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1055_ · sky130_fd_sc_hd__or2_1 or2_1 _1056_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1057_ · sky130_fd_sc_hd__and2_1 and2_1 _1058_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1059_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1060_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1061_ · sky130_fd_sc_hd__and2_1 and2_1 _1062_ · sky130_fd_sc_hd__and2_1 and2_1 _1063_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1064_ · sky130_fd_sc_hd__nor2b_1 nor2b_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__xnor2_1 xnor2_1 _1069_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1070_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1071_ · sky130_fd_sc_hd__and2_1 and2_1 _1072_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1073_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1074_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1075_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1076_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1077_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _1078_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1079_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1080_ · sky130_fd_sc_hd__or2_1 or2_1 _1081_ · sky130_fd_sc_hd__and2_1 and2_1 _1082_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1083_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1084_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1085_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1086_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1087_ · sky130_fd_sc_hd__nor2b_1 nor2b_1 _1088_ · sky130_fd_sc_hd__or2_1 or2_1 _1089_ · sky130_fd_sc_hd__and2_1 and2_1 _1090_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _1091_ · sky130_fd_sc_hd__nand2b_1 nand2b_1 _1092_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1093_ · sky130_fd_sc_hd__or2_1 or2_1 _1094_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1095_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1096_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1097_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1098_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1099_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1100_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1101_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1102_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1103_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1104_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1105_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1106_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1107_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1108_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1109_ · sky130_fd_sc_hd__and2_1 and2_1 _1110_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1111_ · sky130_fd_sc_hd__mux2_1 mux2_1 0 1 _1112_ · sky130_fd_sc_hd__xor2_1 xor2_1 _1113_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1114_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1115_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1116_ · sky130_fd_sc_hd__xnor2_1 xnor2_1 _1117_ · sky130_fd_sc_hd__nand2_1 nand2_1 _1118_ · sky130_fd_sc_hd__nand2_1 nand2_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: 597 cells here, 38 735 at the scoring point. The register-to-register critical path at N = 2, W = 2, AccW = 4 (14 cells, ending at the flip-flop input _0104_ falling; a period of 2 817 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: 597 cells, 157 and2_1, 156 nand2_1, 64 dfxtp_1, 62 or2_1, 53 xnor2_1, 47 nor2b_1, 36 xor2_1, 12 mux2_1, 8 nand2b_1, 2 nor2_1. There (measured, not ranked): 4 503.07 µm², 2 817 ps. Open the drawing on its own (SVG, 396.4 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: 67 nets, 66 cells, to the flip-flop input _00345_ falling; the period, 9 410 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 14 cells to the flip-flop input _0104_ falling (a period of 2 817 ps there); each cell is a link to it in the drawing:

  1. \_52_[7]
  2. _0847_ nor2b_1
  3. _0849_ xor2_1
  4. _0851_ xnor2_1
  5. _0853_ xnor2_1
  6. _0854_ and2_1
  7. _0870_ or2_1
  8. _0880_ xor2_1
  9. _0882_ xor2_1
  10. _0884_ xor2_1
  11. _0885_ nand2_1
  12. _0889_ and2_1
  13. _0899_ xnor2_1
  14. _0900_ nand2_1
  15. _0901_ and2_1
  16. _0104_ flip-flop D
every stage (67 rows)
#netedgedriven bycellarrival (ps)transition (ps)stage (ps)
0\_99_[39]riseflop Q–718.6631.6
1_07424_rise_52788_and2_11 000.7137.3282.1
2_07620_fall_52985_mux2_11 389.199.3388.4
3_07622_rise_52987_xor2_11 589.7190.8200.6
4_07624_rise_52989_xor2_11 806.5190.5216.8
5_07626_rise_52991_xor2_12 023.3190.5216.8
6_07628_rise_52993_xor2_12 240.0190.5216.7
7_07630_rise_52995_xor2_12 456.8190.5216.8
8_07632_rise_52997_xor2_12 673.6190.5216.8
9_07634_rise_52999_xor2_12 890.4190.5216.8
10_07636_fall_53001_xor2_13 005.785.7115.3
11_07637_rise_53002_nand2_13 082.246.676.5
12_07781_fall_53147_nand2_13 149.755.167.5
13_07820_rise_53186_nand2_13 205.246.655.5
14_07961_fall_53328_nand2_13 272.655.167.4
15_07997_rise_53364_nand2_13 328.146.655.5
16_08120_fall_53488_nand2_13 395.655.167.5
17_08151_rise_53519_nand2_13 451.146.655.5
18_08268_fall_53637_nand2_13 518.655.167.5
19_08297_rise_53666_nand2_13 574.146.655.5
20_08397_fall_53767_nand2_13 641.555.167.4
21_08421_rise_53791_nand2_13 697.146.655.6
22_08504_fall_53875_nand2_13 764.555.167.4
23_08521_rise_53892_nand2_13 814.139.849.6
24_08578_rise_53950_and2_14 629.81051.4815.7
25_08580_fall_53952_xnor2_14 815.5174.8185.7
26_08582_rise_53954_xnor2_15 057.5212.4242.0
27_08584_rise_53956_xor2_15 277.0190.5219.5
28_08586_rise_53958_xor2_15 493.8219.1216.8
29_08588_rise_53960_xor2_15 714.2190.5220.4
30_08590_rise_53962_xor2_15 930.9219.0216.7
31_08592_rise_53964_xor2_16 153.2193.2222.3
32_08593_fall_53965_nand2_16 218.241.265.0
33_08597_fall_53970_and2_16 371.339.9153.1
34_08616_fall_53989_or2_16 600.557.5229.2
35_08620_rise_53994_nand2_16 693.881.693.3
36_08638_fall_54012_nand2_16 743.746.349.9
37_08642_rise_54017_nand2_16 831.981.388.2
38_08660_fall_54035_nand2_16 881.746.349.8
39_08664_rise_54040_nand2_16 969.981.388.2
40_08682_fall_54058_nand2_17 014.441.244.5
41_08686_fall_54063_and2_17 167.539.9153.1
42_08705_fall_54082_or2_17 396.857.5229.3
43_08708_rise_54086_nand2_17 490.081.693.2
44_08749_fall_54128_nand2_17 539.934.949.9
45_08750_rise_54129_nand2_17 622.380.382.4
46_08751_fall_54130_nand2_17 675.653.753.3
47_08754_rise_54134_nand2_17 767.181.391.5
48_08795_fall_54176_nand2_17 817.034.849.9
49_08796_rise_54177_nand2_17 900.281.583.2
50_08797_fall_54178_nand2_17 953.854.153.6
51_08801_rise_54183_nand2_18 045.581.491.7
52_08819_fall_54201_nand2_18 095.446.349.9
53_08823_rise_54206_nand2_18 183.581.388.1
54_08841_fall_54224_nand2_18 233.446.349.9
55_08844_rise_54228_nand2_18 321.681.388.2
56_08885_fall_54270_nand2_18 371.434.849.8
57_08886_rise_54271_nand2_18 453.880.382.4
58_08887_fall_54272_nand2_18 507.153.753.3
59_08891_rise_54277_nand2_18 598.681.391.5
60_08909_fall_54295_nand2_18 648.546.349.9
61_08913_rise_54300_nand2_18 736.681.388.1
62_08931_fall_54318_nand2_18 781.141.244.5
63_08934_fall_54322_and2_18 937.342.8156.2
64_08946_rise_54334_xnor2_19 074.7110.8137.4
65_08947_fall_54335_nand2_19 129.5119.454.8
66_00345_fall_54336_and2_19 306.931.0177.4

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: 83747.82 µm² (µm² · 9 562 cells)xor2_183747.82 µm² · 9 562 cellsnand2_1: 66048.35 µm² (µm² · 17 596 cells)nand2_166048.35 µm² · 17 596 cellsand2_1: 30998.48 µm² (µm² · 4 955 cells)and2_130998.48 µm² · 4 955 cellsxnor2_1: 24453.45 µm² (µm² · 2 792 cells)xnor2_124453.45 µm² · 2 792 cellsdfxtp_1: 16015.36 µm² (µm² · 800 cells)dfxtp_116015.36 µm² · 800 cellsor2_1: 9158.78 µm² (µm² · 1 464 cells)or2_19158.78 µm² · 1 464 cellsnor2b_1: 4341.66 µm² (µm² · 694 cells)nor2b_14341.66 µm² · 694 cellsmux2_1: 4200.28 µm² (µm² · 373 cells)mux2_14200.28 µm² · 373 cellsnand2b_1: 2646.29 µm² (µm² · 423 cells)nand2b_12646.29 µm² · 423 cellsnor2_1: 168.91 µm² (µm² · 45 cells)nor2_1168.91 µm² · 45 cellsinv_1: 93.84 µm² (µm² · 25 cells)inv_193.84 µm² · 25 cellsbuf_6: 22.52 µm² (µm² · 2 cells)buf_622.52 µm² · 2 cellsbuf_4: 15.01 µm² (µm² · 2 cells)buf_415.01 µm² · 2 cellsbuf_2: 10.01 µm² (µm² · 2 cells)buf_210.01 µm² · 2 cells
The area of each cell type in the repaired A0′ netlist, at the scoring point: the count times the cell's area in the pinned liberty. Their sum is the ranked area.
cellcountµm² eachµm² in allshare
xor2_19 5628.758483747.820834.6%
nand2_117 5963.753666048.345627.3%
and2_14 9556.256030998.480012.8%
xnor2_12 7928.758424453.452810.1%
dfxtp_180020.019216015.36006.6%
or2_11 4646.25609158.78403.8%
nor2b_16946.25604341.66401.8%
mux2_137311.26084200.27841.7%
nand2b_14236.25602646.28801.1%
nor2_1453.7536168.91200.1%
inv_1253.753693.84000.0%
buf_6211.260822.52160.0%
buf_427.507215.01440.0%
buf_225.004810.00960.0%
total38 735241920.7712

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

Legality: worst load 0.985 × max_capacitance, worst transition 0.99 × 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: 17596 cells (17596.000 GE)NAND17596 17596.000 GEXOR: 9562 cells (19124.000 GE)XOR9562 19124.000 GEAND: 4955 cells (6605.015 GE)AND4955 6605.015 GEXNOR: 2792 cells (5584.000 GE)XNOR2792 5584.000 GEOR: 1464 cells (1951.512 GE)OR1464 1951.512 GEDFF_P: 800 cells (4266.400 GE)DFF_P800 4266.400 GEANDNOT: 694 cells (925.102 GE)ANDNOT694 925.102 GEORNOT: 423 cells (563.859 GE)ORNOT423 563.859 GEMUX: 373 cells (870.209 GE)MUX373 870.209 GENOR: 45 cells (45.000 GE)NOR45 45.000 GENOT: 25 cells (16.675 GE)NOT25 16.675 GE
Cells by type; area is the count weighted by the pinned GE table.
cellcountGE eachGE total
NAND175961.00017596.000
XOR95622.00019124.000
AND49551.3336605.015
XNOR27922.0005584.000
OR14641.3331951.512
DFF_P8005.3334266.400
ANDNOT6941.333925.102
ORNOT4231.333563.859
MUX3732.333870.209
NOR451.00045.000
NOT250.66716.675
total3872957547.772

The record

task
matmul
player
fanout-ferret
assisted by
Claude Sonnet 5.5
submitted
2026-11-10
notes
four multiply-accumulate steps per PE per cycle from zero-padded captured operands (a_sh, b_sh), latency ceil(N/4) = 1 at N=4; variation of the shift-register reference
scoring point
AccW = 32, N = 4, W = 8
design
solution.sv sha256 b6357f45fe9705bc9c9fabfb23bc720837ad203ff17ccb91cdf0aca5e4e8378a
proof
Sol.lean sha256 e6396e30e6ddc18f7312b5271fc9bb425e783335b5a90b83262d95872fd1c195
canonical text
sha256 c42606bf5727e11c4627ca5b479819501bf8b2735be95e487e2588b9e15376dc
record hash
1ffe71156e9098006a54a5bd9ab0eb00cd103380b962c7b31482b93853668a1d
downloads
1ffe71156e90.sv 1ffe71156e90.lean 1ffe71156e90.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
855
build time
10.72 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
4b67fca3c7fa62216d1b9c035ce3658b457665e8a11399fb90fb2cb019386e1c
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 317 in all
mismatches
0
salted
no (the default empty salt: anyone can run this exact stimulus again)
scored netlist
sha256 6b3b742b53c0cd46ae887237efc4a8466fdac91b903abfdb0b39ae6876726ef2
pointlatency (cycles)seedsclock cyclestransactionsmismatchesnetlist sha256
AccW = 8, N = 2, W = 418636192020b6953d6b71
AccW = 32, N = 4, W = 81868119206b3b742b53c0
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 = 80zeros19466893487924e3ef9e3638b5
AccW = 32, N = 4, W = 81seed:9734188592010554240106328083996242132be692d56
AccW = 32, N = 4, W = 82seed:65944092221670940008893661988240371e783230d
AccW = 32, N = 4, W = 83seed:150910319724663032275905358387924ed721e3e3e18
AccW = 32, N = 4, W = 84seed:170870082129236603767077457279024fcdbab7c9305
AccW = 32, N = 4, W = 85seed:135681774334638392548341421828024ccccf631a1d2
AccW = 32, N = 4, W = 86seed:283949794412526215812521349529024f1dc560f7767
AccW = 32, N = 4, W = 87seed:80761885006039448995479040917924831e3fb7b1cd

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 511 471 µm²·ns · Area: 137 104.0 µm² · Time: 18 318 psvacuity-check · submission · 2026-11-10 · Score: 2 377 063 µm²·ns · Area: 85 260.5 µm² · Time: 27 880 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 276 474 µm²·ns · Area: 241 920.8 µm² · Time: 9410 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 511 471 µm²·ns · Area: 137 104.0 µm² · Time: 18 318 psvacuity-check · submission · 2026-11-10 · Score: 2 377 063 µm²·ns · Area: 85 260.5 µm² · Time: 27 880 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 276 474 µm²·ns · Area: 241 920.8 µm² · Time: 9410 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 · this designsubmission241 920.779 4102 276 474
vacuity-check submission85 260.5227 8802 377 063
fanout-ferret submission137 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: 6520 µm²·ns · Area: 2085.873 µm² · Time: 3126 psvacuity-check · submission · 2026-11-10 · Score: 6453 µm²·ns · Area: 1315.583 µm² · Time: 4905 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: 5935 µm²·ns · Area: 3661.548 µm² · Time: 1621 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: 6520 µm²·ns · Area: 2085.873 µm² · Time: 3126 psvacuity-check · submission · 2026-11-10 · Score: 6453 µm²·ns · Area: 1315.583 µm² · Time: 4905 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: 5935 µm²·ns · Area: 3661.548 µm² · Time: 1621 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 · this designsubmission3 661.5481 6215935
vacuity-check submission1 315.5834 9056453
fanout-ferret submission2 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 1ffe71156e9098006a54a5bd9ab0eb00cd103380b962c7b31482b93853668a1d.sv --task tasks/matmul --seq --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256
4b67fca3c7fa62216d1b9c035ce3658b457665e8a11399fb90fb2cb019386e1c
ppa.netlist_sha256
6b3b742b53c0cd46ae887237efc4a8466fdac91b903abfdb0b39ae6876726ef2
ppa.repair.netlist_sha256
39483feb34278fe8050da9f2eb7bad97aea85adae0ca47093d1b6edf31d8ac95
ppa.area_e4um2_sky130
2419207712
ppa.delay_ps_sky130
9410

The schematic and the critical-path data are site/schematics/matmul/b6357f45fe9705bc.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 1af1be441bd645b1…).

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

Expect, in out.json:

ppa.netlist_sha256
6b3b742b53c0cd46ae887237efc4a8466fdac91b903abfdb0b39ae6876726ef2
ppa.repair.netlist_sha256
e7495556c291dd78cc3d61e359cb405014b8b58e788d4aa5568ad26b3971eed2
ppa.area_e5um2_asap7
366154830
ppa.delay_ps_asap7
1621

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=1ffe71156e9098006a54a5bd9ab0eb00cd103380b962c7b31482b93853668a1d
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.