Tasks / mul / record

Record `5b30f35c283b`

on the Pareto frontieron the Pareto frontier scored at N = 16

Area

7 961.39µm²

7 961.3856 µm² exactly

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par: −7.0% smallermul_tree_h · 8 563.21 µm²
on this page: smallest of 10 designs

cells: 1 431
flops: 0
repair: 0 buffers, 0 tie cells
GE: 1 930.3 extra
A1′: 8 075.24 µm² research

Performance · time

5 342ps

the delay: the latest output arrival, p[30] rising

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par: −10.8% fastermul_tree_h · 5 992 ps
on this page: 2nd of 10 designs

Fmax-eq.: 187.2 MHz derived
critical path: 57 cells
unit depth: 60 extra
A1′: 6 138 ps research

Score · area × time

42 530µm²·ns

7 961.3856 µm² × 5 342 ps

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par: −17.1% bettermul_tree_h · 51 311 µm²·ns
on this page: best of 10 designs
board: layer 1, rank 1 of 2 by score
Pareto: on the front

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

how these numbers are measured and compared

Area: sky130 A0′, the repaired netlist. Time: NLDM, inputs driven by buf_8, 10 fF per output bit, no wires.

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 mul's other players at this revision (1 player, 1 record), 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 10 designs of the area-time plot (5 references, 2 submissions and 3 baselines): not a ranking.

Area

120.854µm²

120.85362 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: −5.5% smallermul_tree_h · 127.954 µm²
on this page: 2nd of 10 designs

cells: 1 463
flops: 0
repair: 0 buffers, 0 tie cells
GE: 1 930.3 extra

Performance · time

1 088ps

the delay: the latest output arrival

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par: −6.2% fastermul_tree_h · 1 160 ps
on this page: 2nd of 10 designs

Fmax-eq.: 919.1 MHz derived
unit depth: 60 extra

Score · area × time

131.5µm²·ns

120.85362 µm² × 1 088 ps

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par: −11.4% bettermul_tree_h · 148.4 µm²·ns
on this page: 2nd of 10 designs
board: layer 1, rank 1 of 2 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. Time: NLDM, inputs driven by BUFx8, 2.5 fF per output bit, no wires; a table read below its grid is read at its floor. 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.

“On this page” and “Pareto” compare with the 10 designs of the area-time plot (5 references, 2 submissions and 3 baselines): not a ranking.

The sources

solution.svdownload

// svGolf task `mul` -- reference solution 5: a log-depth carry-save TREE multiplier whose leaves each hold TWO
// partial-product rows, parametric in N, written with a LOCALPARAM.
//
// The N partial-product rows pp[j] (the shifted copies of a, gated by the bits of b) are taken two at a time:
// leaf j of H = ceil(N/2) holds the carry-save pair (S, C) = (pp[2j], pp[2j+1]), two rows being already a
// pair. The H leaves are those of one balanced binary tree in a binary-HEAP numbering: the root is node 0,
// node k has the children 2k+1 and 2k+2, the H-1 internal nodes are 0 .. H-2 and the H leaves H-1 .. 2H-2.
// EVERY internal node is a 4:2 compressor on its two children's pairs: two stacked rows of 3:2 counters
// (full adders), the first row X/Y, the second S/C; the two rows of the root go through a ripple-carry
// final adder. There is no pairing node and no constant select: a node never has to be told apart from
// its siblings, which is what the single-row tree (mul_tree.sv) needs th/nth for.
//
// The one non-affine quantity, H = ceil(N/2), is a `localparam integer` defined by a division by a literal:
// the sv_comb tactics read it as one more named constant of N (PROVING.md, section 4), so every index and
// bound stays an integer constant expression and `omega` decides the obligations (H = (N + 1) / 2 is
// known to it). `bb` is `b` zero-extended to 2H+1 bits, so the last leaf of an odd N has a zero row.
// A shifted partial product is a GATHER read of `ae`, the zero-padded copy of `a`, so no write ever
// leaves its vector. All sums are taken modulo 2^(2N), exactly the width of the product.
module mul_n #(parameter int N = 16) (
  input  logic [N-1:0]   a, b,
  output logic [2*N-1:0] p
);
  localparam integer H = (N + 1) / 2;   // leaves: ceil(N/2) pairs of partial-product rows

  logic [4*N-2:0]          ae;   // ae[x] = a[x-(2N-1)] for 2N-1 <= x < 3N-1, else 0
  logic [2*H:0]            bb;   // b zero-extended
  logic [2*H-2:0][2*N-1:0] S, C; // sum / carry row of each heap node
  logic [H-1:0][2*N-1:0]   X, Y; // first-row sum / carry of node k (row H-1 unused)
  logic [2*N:0]            R;    // final-adder carries

  assign ae[2*N-2:0]     = '0;
  assign ae[3*N-2:2*N-1] = a;
  assign ae[4*N-2:3*N-1] = '0;
  assign bb[N-1:0]       = b;
  assign bb[2*H:N]       = '0;
  assign X[H-1]          = '0;
  assign Y[H-1]          = '0;
  assign R[0]            = 1'b0;

  genvar j, k, c;
  generate
    // leaves: node H-1+j is the pair of partial-product rows 2j and 2j+1 (gather reads of ae)
    for (j = 0; j < H; j++) begin : g_leaf
      for (c = 0; c < 2*N; c++) begin : g_lc
        assign S[H-1+j][c] = bb[2*j] & ae[c + 2*N - 1 - 2*j];
        assign C[H-1+j][c] = ae[c + 2*N - 2 - 2*j] & bb[2*j+1];
      end
    end
    // internal nodes: a 4:2 compressor on the children 2k+1, 2k+2
    for (k = 0; k < H-1; k++) begin : g_node
      assign Y[k][0] = 1'b0;
      assign C[k][0] = 1'b0;
      for (c = 0; c < 2*N; c++) begin : g_col
        assign X[k][c] = (S[2*k+2][c] ^ C[2*k+1][c]) ^ S[2*k+1][c];
        assign S[k][c] = (X[k][c] ^ C[2*k+2][c]) ^ Y[k][c];
      end
      for (c = 0; c < 2*N-1; c++) begin : g_car
        assign Y[k][c+1] = (S[2*k+2][c] ^ C[2*k+1][c]) ? S[2*k+1][c] : C[2*k+1][c];
        assign C[k][c+1] = (Y[k][c] ^ C[2*k+2][c]) ? X[k][c] : C[2*k+2][c];
      end
    end
    // final carry-propagate (ripple) adder of the root's two rows
    for (c = 0; c < 2*N; c++) begin : g_fin
      assign p[c]   = S[0][c] ^ (C[0][c] ^ R[c]);
      assign R[c+1] = (C[0][c] ^ S[0][c]) ? R[c] : S[0][c];
    end
  endgenerate
endmodule

Solution.lean (360 code lines)

import Submission.Design
import SvGolf.Comb
import LeanModels.Sv.CombEqTactic
import LeanModels.Sv.CombLib

/-!
# Reference solution 5 for task `mul`: a carry-save tree with TWO-ROW leaves, proved with the `sv_comb` tactics

This is a submission file like any player's `Solution.lean`. The checker generates the module
`Submission.Design` (`Submission.design`, `Submission.Goal`); this file proves

    theorem Submission.solution : Submission.Goal

for EVERY `N ≥ 1`. The design is `reference/mul_tree_h.sv`: the `N` partial-product rows are taken
two at a time, `H = ceil(N/2)` leaves (nodes `H-1 .. 2H-2` of a binary HEAP, node `k` having the
children `2k+1`, `2k+2`, the root node 0), each leaf a carry-save pair `(S, C) = (pp[2j], pp[2j+1])`;
EVERY internal node is a 4:2 compressor, two stacked rows of full adders, on its children's pairs; the
root's two rows go through a ripple-carry adder.

The new thing is the **localparam**: `localparam integer H = (N + 1) / 2;` (the number of leaves, not
an affine function of `N`). The `sv_comb` tactics read a localparam as one more named constant of `N`
(PROVING.md, section 4); its definition is inlined into every obligation as `(↑N + 1) / 2`, which
`omega` knows (floor division by a literal). That one line replaces what the single-row heap of
`mul_tree.sv` needs four extra loops and a constant select (`th`/`nth`) for.

## Route (the file is in this order)

1. **Arithmetic** (`HeapArith`, plain Lean, no ls-sv): `csa_row`, `node_sum`, `lane_gated` as in
   `mul_tree.lean`, and `heap_mul`: the sums over the CUT `{t, …, 2t}` of the heap are invariant
   modulo `2^(2N)` while `t` runs from `H-1` (the leaves: `a · b` exactly, two rows per leaf, `b`
   zero-extended) down to `0` (the root). There is no pairing case: every internal node compresses.
2. **Structure** (`tree_struct`): `sv_structure` (`CombDesign ∧ Acyclic`); the goals compare 2-D windows and close
   by `intros; sv_rowmajor; omega`, with `H` inlined. The rank is a lexicographic key `(stage, node
   order, phase)` (`treeKey`).
3. **Ports** (`tree_interface`): `sv_interface`; the valuation of a design that has localparams
   (`Summary.val`) is the tactic's business.
4. **Equations, bridge and coverage** (`solution`): the printed equations of `sv_equations` (with
   `((N : Int) + 1) / 2` in the place of `H`) are bridged to the clean facts of `heap_mul` one
   `sv_bridge eq_x` per fact (the `Int` index forms of the netlist against the `Nat` indices of the
   arithmetic: congruence and `omega`).
5. **Coverage** (`solution`, the same theorem): the coverage goals of `sv_equations` are the heap reads;
   the closing `all_goals … sv_cover` proves them, solving the writer from the read.
-/

/-! ## 1. The arithmetic (plain Lean, `CombLib` only)

The heap-indexed 4:2 carry-save tree multiplier with two-row leaves: `heap_mul` proves `p = a * b` from
the netlist equations as clean Boolean facts about bit functions; nothing here mentions a design or a
state. -/
namespace HeapArith
open LeanModels.Sv.CombLib

theorem bfVal_false {f : Nat → Bool} {n : Nat} (h : ∀ j < n, f j = false) : bfVal f n = 0 := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp only [bfVal]
    rw [ih (fun j hj => h j (by omega)), h n (by omega)]
    simp

/-- A row of 3:2 counters, the carry row shifted one column: column `c` of `s`/`cy`, with
`sh (c+1) = cy c`. The top carry `cy (W-1)` is dropped from `sh`. -/
theorem csa_row (n : Nat) (x y z s cy sh : Nat → Bool)
    (hs : ∀ c < n + 1, s c = (x c ^^ y c ^^ z c))
    (hcy : ∀ c < n + 1, cy c = ((x c && y c) || (z c && (x c ^^ y c))))
    (hsh0 : sh 0 = false) (hsh : ∀ c, c + 1 < n + 1 → sh (c + 1) = cy c) :
    bfVal s (n + 1) + bfVal sh (n + 1) + 2 ^ (n + 1) * (cy n).toNat =
      bfVal x (n + 1) + bfVal y (n + 1) + bfVal z (n + 1) := by
  have key : ∀ m, m ≤ n + 1 →
      bfVal s m + 2 * bfVal cy m = bfVal x m + bfVal y m + bfVal z m := by
    intro m
    induction m with
    | zero => intro _; simp [bfVal]
    | succ m ih =>
      intro hm
      have ih := ih (by omega)
      have hfa := fullAdder_arith (x m) (y m) (z m)
      rw [← hs m (by omega), ← hcy m (by omega)] at hfa
      simp only [bfVal]
      have : 2 ^ m * ((s m).toNat + 2 * (cy m).toNat) =
          2 ^ m * ((x m).toNat + (y m).toNat + (z m).toNat) := by rw [hfa]
      generalize (s m).toNat = S0 at *
      generalize (cy m).toNat = C0 at *
      generalize (x m).toNat = X0 at *
      generalize (y m).toNat = Y0 at *
      generalize (z m).toNat = Z0 at *
      generalize 2 ^ m = P at *
      grind
  have hsh' : bfVal sh (n + 1) = 2 * bfVal cy n := by
    rw [bfVal_shift, hsh0]
    have : bfVal (fun j => sh (j + 1)) n = bfVal cy n :=
      bfVal_congr (fun j hj => hsh j (by omega))
    rw [this]; simp
  have hk := key (n + 1) (Nat.le_refl _)
  rw [hsh']
  simp only [bfVal, Nat.pow_succ] at hk ⊢
  generalize 2 ^ n = P at *
  generalize (cy n).toNat = C0 at *
  grind

/-- A 4:2 compressor node: two stacked rows of counters, on a window of `n+1` columns, preserves
the sum exactly up to the two dropped top carries. -/
theorem node_sum (n : Nat) (SL CL SR CR S C X Y : Nat → Bool)
    (hX : ∀ c < n + 1, X c = (SL c ^^ CL c ^^ SR c))
    (hY0 : Y 0 = false)
    (hY : ∀ c, c + 1 < n + 1 → Y (c + 1) = ((SL c && CL c) || (SR c && (SL c ^^ CL c))))
    (hS : ∀ c < n + 1, S c = (X c ^^ Y c ^^ CR c))
    (hC0 : C 0 = false)
    (hC : ∀ c, c + 1 < n + 1 → C (c + 1) = ((X c && Y c) || (CR c && (X c ^^ Y c)))) :
    ∃ q, bfVal S (n + 1) + bfVal C (n + 1) + 2 ^ (n + 1) * q =
      (bfVal SL (n + 1) + bfVal CL (n + 1)) + (bfVal SR (n + 1) + bfVal CR (n + 1)) := by
  have h1 := csa_row n SL CL SR X (fun c => (SL c && CL c) || (SR c && (SL c ^^ CL c))) Y
    hX (fun _ _ => rfl) hY0 hY
  have h2 := csa_row n X Y CR S (fun c => (X c && Y c) || (CR c && (X c ^^ Y c))) C
    hS (fun _ _ => rfl) hC0 hC
  refine ⟨(((SL n && CL n) || (SR n && (SL n ^^ CL n))).toNat) +
    ((X n && Y n) || (CR n && (X n ^^ Y n))).toNat, ?_⟩
  simp only [Nat.mul_add] at h1 h2 ⊢
  generalize 2 ^ (n + 1) = P at *
  omega


/-! ### The leaves: a gated, shifted copy of `a` -/

/-- The zero-padded copy `ae` of `a`, read at offset `2N-1-r`, is `a` shifted left by `r`
(for `r ≤ N`: nothing is cut off). -/
theorem lane_val {N : Nat} (hN : 1 ≤ N) (a : BitVec N) (ae : Nat → Bool)
    (h1 : ∀ k, k < 2 * N - 1 → ae k = false)
    (h2 : ∀ k, k < N → ae (2 * N - 1 + k) = a.getLsbD k)
    (h3 : ∀ k, k < N → ae (3 * N - 1 + k) = false)
    (r : Nat) (hr : r ≤ N) :
    bfVal (fun c => ae (c + (2 * N - 1 - r))) (2 * N) = a.toNat * 2 ^ r := by
  have hs1 := bfVal_split (fun c => ae (c + (2 * N - 1 - r))) r (2 * N - r)
  rw [show r + (2 * N - r) = 2 * N by omega] at hs1
  rw [hs1]
  have hlow : bfVal (fun c => ae (c + (2 * N - 1 - r))) r = 0 :=
    bfVal_false (fun j hj => h1 _ (by omega))
  rw [hlow]
  have hs2 := bfVal_split (fun j => ae (r + j + (2 * N - 1 - r))) N (N - r)
  rw [show N + (N - r) = 2 * N - r by omega] at hs2
  rw [hs2]
  have hmid : bfVal (fun j => ae (r + j + (2 * N - 1 - r))) N = a.toNat := by
    rw [← bfVal_bv a]
    exact bfVal_congr (fun j hj => by
      have : r + j + (2 * N - 1 - r) = 2 * N - 1 + j := by omega
      rw [this]; exact h2 j hj)
  have hhigh : bfVal (fun j => (fun j => ae (r + j + (2 * N - 1 - r))) (N + j)) (N - r) = 0 :=
    bfVal_false (fun j hj => by
      show ae (r + (N + j) + (2 * N - 1 - r)) = false
      have : r + (N + j) + (2 * N - 1 - r) = 3 * N - 1 + j := by omega
      rw [this]; exact h3 j (by omega))
  rw [hmid, hhigh]
  simp only [Nat.zero_add, Nat.mul_zero, Nat.add_zero]
  rw [Nat.mul_comm]

/-- The value of a gated lane. -/
theorem lane_gated {N : Nat} (hN : 1 ≤ N) (a : BitVec N) (ae : Nat → Bool)
    (h1 : ∀ k, k < 2 * N - 1 → ae k = false)
    (h2 : ∀ k, k < N → ae (2 * N - 1 + k) = a.getLsbD k)
    (h3 : ∀ k, k < N → ae (3 * N - 1 + k) = false)
    (r : Nat) (g : Bool) (hg : g = true → r ≤ N) :
    bfVal (fun c => ae (c + (2 * N - 1 - r)) && g) (2 * N) = g.toNat * (a.toNat * 2 ^ r) := by
  rw [bfVal_and]
  cases g with
  | false => simp
  | true => simp only [Bool.toNat_true]; rw [lane_val hN a ae h1 h2 h3 r (hg rfl)]

/-! ### Sums over a stretch of heap nodes -/

def csum (V : Nat → Nat) : Nat → Nat → Nat
  | _, 0 => 0
  | s, n + 1 => csum V s n + V (s + n)

theorem csum_front (V : Nat → Nat) (n : Nat) : ∀ s, csum V s (n + 1) = V s + csum V (s + 1) n := by
  induction n with
  | zero => intro s; simp [csum]
  | succ n ih =>
    intro s
    have e : s + 1 + n = s + (n + 1) := by omega
    have e2 : csum V (s + 1) (n + 1) = csum V (s + 1) n + V (s + 1 + n) := rfl
    rw [csum, ih s, e2, e]
    omega

/-- Leaves: `csum` of the leaf values is `a · b`, two rows (two bits of `b`) per leaf. -/
theorem csum_leaves2 (H : Nat) (a : Nat) (g : Nat → Bool) (V : Nat → Nat)
    (hV : ∀ j, j < H → V (H - 1 + j) =
      (g (2 * j)).toNat * (a * 2 ^ (2 * j)) + (g (2 * j + 1)).toNat * (a * 2 ^ (2 * j + 1))) :
    ∀ n, n ≤ H → csum V (H - 1) n = a * bfVal g (2 * n) := by
  intro n
  induction n with
  | zero => intro _; simp [csum, bfVal]
  | succ n ih =>
    intro hn
    have ih := ih (by omega)
    rw [csum, ih, hV n (by omega), show 2 * (n + 1) = 2 * n + 1 + 1 by omega]
    simp only [bfVal, Nat.pow_succ]
    generalize 2 ^ (2 * n) = P
    generalize (g (2 * n)).toNat = B0
    generalize (g (2 * n + 1)).toNat = B1
    generalize bfVal g (2 * n) = F
    grind

/-- **The whole multiplier**, from the equations of the netlist as clean Boolean facts. `H` is the
number of leaves, `N ≤ 2H ≤ N + 1`: leaf `j` of the heap (node `H - 1 + j`) holds the rows `2j`, `2j+1`
of the partial products. -/
theorem heap_mul0 {N H : Nat} (hN : 1 ≤ N) (hH1 : N ≤ 2 * H) (hH2 : 2 * H ≤ N + 1)
    (a b : BitVec N) (p : BitVec (2 * N))
    (ae bb : Nat → Bool) (S C X Y : Nat → Nat → Bool) (R : Nat → Bool)
    (hae1 : ∀ k, k < 2 * N - 1 → ae k = false)
    (hae2 : ∀ k, k < N → ae (2 * N - 1 + k) = a.getLsbD k)
    (hae3 : ∀ k, k < N → ae (3 * N - 1 + k) = false)
    (hbb1 : ∀ k, k < N → bb k = b.getLsbD k)
    (hbb2 : ∀ k, N ≤ k → k < 2 * H → bb k = false)
    (hleafS : ∀ j, j < H → ∀ c, c < 2 * N →
      S (H - 1 + j) c = (ae (c + (2 * N - 1 - 2 * j)) && bb (2 * j)))
    (hleafC : ∀ j, j < H → ∀ c, c < 2 * N →
      C (H - 1 + j) c = (ae (c + (2 * N - 1 - (2 * j + 1))) && bb (2 * j + 1)))
    (hY0 : ∀ k, k < H - 1 → Y k 0 = false)
    (hC0 : ∀ k, k < H - 1 → C k 0 = false)
    (hX : ∀ k, k < H - 1 → ∀ c, c < 2 * N →
      X k c = (S (2 * k + 1) c ^^ C (2 * k + 1) c ^^ S (2 * k + 2) c))
    (hS : ∀ k, k < H - 1 → ∀ c, c < 2 * N → S k c = (X k c ^^ Y k c ^^ C (2 * k + 2) c))
    (hY : ∀ k, k < H - 1 → ∀ c, c < 2 * N - 1 →
      Y k (c + 1) = ((S (2 * k + 1) c && C (2 * k + 1) c) ||
        (S (2 * k + 2) c && (S (2 * k + 1) c ^^ C (2 * k + 1) c))))
    (hC : ∀ k, k < H - 1 → ∀ c, c < 2 * N - 1 →
      C k (c + 1) = ((X k c && Y k c) || (C (2 * k + 2) c && (X k c ^^ Y k c))))
    (hR0 : R 0 = false)
    (hp : ∀ c, c < 2 * N → p.getLsbD c = (S 0 c ^^ C 0 c ^^ R c))
    (hR : ∀ c, c < 2 * N → R (c + 1) =
      ((S 0 c && C 0 c) || (R c && (S 0 c ^^ C 0 c)))) :
    p = BitVec.ofNat (2 * N) (a.toNat * b.toNat) := by
  obtain ⟨n, hn⟩ : ∃ n, 2 * N = n + 1 := ⟨2 * N - 1, by omega⟩
  let V : Nat → Nat := fun m => bfVal (S m) (2 * N) + bfVal (C m) (2 * N)
  -- the leaves: two shifted, gated copies of `a` per leaf
  have hleaf : ∀ j, j < H → V (H - 1 + j) =
      (bb (2 * j)).toNat * (a.toNat * 2 ^ (2 * j)) +
        (bb (2 * j + 1)).toNat * (a.toNat * 2 ^ (2 * j + 1)) := by
    intro j hj
    have e1 : bfVal (S (H - 1 + j)) (2 * N) =
        bfVal (fun c => ae (c + (2 * N - 1 - 2 * j)) && bb (2 * j)) (2 * N) :=
      bfVal_congr (fun c hc => hleafS j hj c hc)
    have e2 : bfVal (C (H - 1 + j)) (2 * N) =
        bfVal (fun c => ae (c + (2 * N - 1 - (2 * j + 1))) && bb (2 * j + 1)) (2 * N) :=
      bfVal_congr (fun c hc => hleafC j hj c hc)
    show bfVal (S (H - 1 + j)) (2 * N) + bfVal (C (H - 1 + j)) (2 * N) = _
    rw [e1, e2, lane_gated hN a ae hae1 hae2 hae3 (2 * j) (bb (2 * j)) (fun hg => by
        by_cases h : N ≤ 2 * j
        · rw [hbb2 (2 * j) h (by omega)] at hg; exact absurd hg (by simp)
        · omega),
      lane_gated hN a ae hae1 hae2 hae3 (2 * j + 1) (bb (2 * j + 1)) (fun hg => by
        by_cases h : N ≤ 2 * j + 1
        · rw [hbb2 (2 * j + 1) h (by omega)] at hg; exact absurd hg (by simp)
        · omega)]
  -- `b`, zero-extended, is the gate bits
  have hbv : bfVal bb (2 * H) = b.toNat := by
    have hs := bfVal_split bb N (2 * H - N)
    rw [show N + (2 * H - N) = 2 * H by omega] at hs
    rw [hs]
    have h1 : bfVal bb N = b.toNat := by
      rw [← bfVal_bv b]; exact bfVal_congr (fun j hj => hbb1 j hj)
    have h2 : bfVal (fun j => bb (N + j)) (2 * H - N) = 0 :=
      bfVal_false (fun j hj => hbb2 (N + j) (by omega) (by omega))
    rw [h1, h2]; simp
  have hleaves : csum V (H - 1) H = a.toNat * b.toNat := by
    rw [csum_leaves2 H a.toNat bb V hleaf H (Nat.le_refl H), hbv]
  -- the nodes: every internal node is a 4:2 compressor
  have hnode : ∀ k, k < H - 1 → ∃ q, V k + 2 ^ (2 * N) * q = V (2 * k + 1) + V (2 * k + 2) := by
    intro k hk
    obtain ⟨q, hq⟩ := node_sum n (S (2 * k + 1)) (C (2 * k + 1)) (S (2 * k + 2)) (C (2 * k + 2))
      (S k) (C k) (X k) (Y k)
      (fun c hc => hX k hk c (by omega)) (hY0 k hk)
      (fun c hc => hY k hk c (by omega))
      (fun c hc => hS k hk c (by omega))
      (hC0 k hk)
      (fun c hc => hC k hk c (by omega))
    rw [← hn] at hq
    exact ⟨q, by simp only [V]; omega⟩
  -- the cut sums
  have hcut : ∀ t, t < H - 1 → ∃ q, csum V t (t + 1) + 2 ^ (2 * N) * q = csum V (t + 1) (t + 2) := by
    intro t ht
    obtain ⟨q, hq⟩ := hnode t ht
    refine ⟨q, ?_⟩
    have f1 : csum V t (t + 1) = V t + csum V (t + 1) t := csum_front V t t
    have f2 : csum V (t + 1) (t + 2) = csum V (t + 1) t + V (t + 1 + t) + V (t + 1 + (t + 1)) := rfl
    rw [f1, f2, show t + 1 + t = 2 * t + 1 by omega, show t + 1 + (t + 1) = 2 * t + 2 by omega]
    omega
  have hdown : ∀ d, d ≤ H - 1 → csum V (H - 1 - d) (H - 1 - d + 1) % 2 ^ (2 * N) =
      (a.toNat * b.toNat) % 2 ^ (2 * N) := by
    intro d
    induction d with
    | zero =>
      intro _
      rw [show H - 1 - 0 + 1 = H by omega, Nat.sub_zero, hleaves]
    | succ d ih =>
      intro hd
      have ih := ih (by omega)
      obtain ⟨q, hq⟩ := hcut (H - 1 - (d + 1)) (by omega)
      rw [show H - 1 - (d + 1) + 1 = H - 1 - d by omega,
        show H - 1 - (d + 1) + 2 = H - 1 - d + 1 by omega] at hq
      rw [← ih, ← hq, Nat.add_mul_mod_self_left, show H - 1 - (d + 1) + 1 = H - 1 - d by omega]
  have hroot := hdown (H - 1) (Nat.le_refl _)
  rw [Nat.sub_self, show (0 : Nat) + 1 = 1 from rfl] at hroot
  have hV0 : csum V 0 1 = V 0 := by simp [csum]
  rw [hV0] at hroot
  -- the final adder
  have hrip := ripple_row (2 * N) (S 0) (C 0) (fun c => S 0 c ^^ C 0 c) p.getLsbD R
    (fun _ _ => rfl) (fun c hc => hp c hc) (fun c hc => hR c hc)
  rw [hR0, bfVal_bv] at hrip
  simp only [Bool.toNat_false, Nat.add_zero] at hrip
  have hlt : p.toNat < 2 ^ (2 * N) := p.isLt
  have hpv : p.toNat = V 0 % 2 ^ (2 * N) := by
    have := sum_split hlt (t := V 0) (q := (R (2 * N)).toNat) (by simp only [V]; omega)
    exact this.1
  apply BitVec.eq_of_toNat_eq
  rw [BitVec.toNat_ofNat, hpv, hroot]


/-! ### The player's forms of the gates

`heap_mul` is `heap_mul0` with the cells written the way THIS design writes them (the printed
equations of `sv_equations`); each is the canonical full-adder cell by a case split on its Booleans. -/

theorem heap_mul {N H : Nat} (hN : 1 ≤ N) (hH1 : N ≤ 2 * H) (hH2 : 2 * H ≤ N + 1)
    (a b : BitVec N) (p : BitVec (2 * N))
    (ae bb : Nat → Bool) (S C X Y : Nat → Nat → Bool) (R : Nat → Bool)
    (hae1 : ∀ k, k < 2 * N - 1 → ae k = false)
    (hae2 : ∀ k, k < N → ae (2 * N - 1 + k) = a.getLsbD k)
    (hae3 : ∀ k, k < N → ae (3 * N - 1 + k) = false)
    (hbb1 : ∀ k, k < N → bb k = b.getLsbD k)
    (hbb2 : ∀ k, N ≤ k → k < 2 * H → bb k = false)
    (hleafS : ∀ j, j < H → ∀ c, c < 2 * N →
      S (H - 1 + j) c = (bb (2 * j) && ae (c + (2 * N - 1 - 2 * j))))
    (hleafC : ∀ j, j < H → ∀ c, c < 2 * N →
      C (H - 1 + j) c = (ae (c + (2 * N - 1 - (2 * j + 1))) && bb (2 * j + 1)))
    (hY0 : ∀ k, k < H - 1 → Y k 0 = false)
    (hC0 : ∀ k, k < H - 1 → C k 0 = false)
    (hX : ∀ k, k < H - 1 → ∀ c, c < 2 * N →
      X k c = ((S (2 * k + 2) c ^^ C (2 * k + 1) c) ^^ S (2 * k + 1) c))
    (hS : ∀ k, k < H - 1 → ∀ c, c < 2 * N → S k c = ((X k c ^^ C (2 * k + 2) c) ^^ Y k c))
    (hY : ∀ k, k < H - 1 → ∀ c, c < 2 * N - 1 →
      Y k (c + 1) = (if (S (2 * k + 2) c ^^ C (2 * k + 1) c) = true then S (2 * k + 1) c else C (2 * k + 1) c))
    (hC : ∀ k, k < H - 1 → ∀ c, c < 2 * N - 1 →
      C k (c + 1) = (if (Y k c ^^ C (2 * k + 2) c) = true then X k c else C (2 * k + 2) c))
    (hR0 : R 0 = false)
    (hp : ∀ c, c < 2 * N → p.getLsbD c = (S 0 c ^^ (C 0 c ^^ R c)))
    (hR : ∀ c, c < 2 * N → R (c + 1) = (if (C 0 c ^^ S 0 c) = true then R c else S 0 c)) :
    p = BitVec.ofNat (2 * N) (a.toNat * b.toNat) := by
  refine heap_mul0 hN hH1 hH2 a b p ae bb S C X Y R hae1 hae2 hae3 hbb1 hbb2 ?_ hleafC hY0 hC0
    ?_ ?_ ?_ ?_ hR0 ?_ ?_
  · intro j hj c hc
    rw [hleafS j hj c hc]; exact Bool.and_comm _ _
  · intro k hk c hc
    rw [hX k hk c hc]
    generalize S (2 * k + 1) c = s1; generalize C (2 * k + 1) c = c1; generalize S (2 * k + 2) c = s2
    cases s1 <;> cases c1 <;> cases s2 <;> decide
  · intro k hk c hc
    rw [hS k hk c hc]
    generalize X k c = x; generalize Y k c = y; generalize C (2 * k + 2) c = c2
    cases x <;> cases y <;> cases c2 <;> decide
  · intro k hk c hc
    rw [hY k hk c hc]
    generalize S (2 * k + 1) c = s1; generalize C (2 * k + 1) c = c1; generalize S (2 * k + 2) c = s2
    cases s1 <;> cases c1 <;> cases s2 <;> decide
  · intro k hk c hc
    rw [hC k hk c hc]
    generalize X k c = x; generalize Y k c = y; generalize C (2 * k + 2) c = c2
    cases x <;> cases y <;> cases c2 <;> decide
  · intro c hc
    rw [hp c hc]
    generalize S 0 c = s0; generalize C 0 c = c0; generalize R c = r
    cases s0 <;> cases c0 <;> cases r <;> decide
  · intro c hc
    rw [hR c hc]
    generalize S 0 c = s0; generalize C 0 c = c0; generalize R c = r
    cases s0 <;> cases c0 <;> cases r <;> decide

end HeapArith

namespace Submission

open LeanModels.Sv LeanModels.Sv.CombView LeanModels.Sv.CombLib LeanModels.Sv.CombEq SvGolf


/-! ## 2. Structure: `sv_structure` -/

/-- The rank: `(stage, node order, phase)`. Inputs and constants first, then the leaves, then the
internal nodes from the last (deepest, highest heap index) to the root, in two phases (the first row of
counters, then the second), then the ripple final adder column by column. `H = (N + 1) / 2` is the
number of leaves. -/
def treeKey (N : Nat) : SiteId → Key
  | .plain _ => (0, 0, 0)
  | .fam "g_lc" _ _ => (1, 0, 0)
  | .fam "g_node" _ [k] => (2, (N + 1) / 2 - 1 - k.toNat, 0)
  | .fam "g_col" 0 [k, _] => (2, (N + 1) / 2 - 1 - k.toNat, 1)
  | .fam "g_col" _ [k, _] => (2, (N + 1) / 2 - 1 - k.toNat, 2)
  | .fam "g_car" 0 [k, _] => (2, (N + 1) / 2 - 1 - k.toNat, 1)
  | .fam "g_car" _ [k, _] => (2, (N + 1) / 2 - 1 - k.toNat, 2)
  | .fam "g_fin" 0 [c] => (3, c.toNat, 1)
  | .fam "g_fin" _ [c] => (3, c.toNat, 0)
  | .fam _ _ _ => (3, 0, 0)

set_option maxHeartbeats 1000000 in
/-- `CombDesign` and `Acyclic` for every `N ≥ 1`, from the lexicographic key: ONE application of the
soundness theorem and one round of obligations for both. -/
theorem tree_struct (N : Nat) (hN : 1 ≤ N) :
    CombDesign (design.sem N) ∧ Acyclic (design.sem N) ∧ SharedObl design.pdesign [N] := by
  sv_structure (lexRank := treeKey N)
  all_goals (intros; sv_rowmajor; omega)

/-! ## 3. The ports (the task's `Interface`)

`sv_interface`, for a design with a localparam: the valuation is `Summary.val` (the parameters zipped
with the arguments, then the localparams evaluated over them), which the tactic unfolds itself. -/

theorem tree_interface (N : Nat) (hN : 1 ≤ N) (hc : CombDesign (design.sem N)) :
    SvGolf.Tasks.Mul.task.Interface N (design.sem N) := by
  sv_interface


/-! ## 4. Bridge, equations and coverage of the heap reads

Every cell the tree reads must have a writer. The heap rows `[0, H-1)` are written by the node loop,
the rows `[H-1, 2H-1)` by the leaf loop; a carry row is also written in column 0 by its own assign.
`sv_cover` closes these coverage goals itself (it solves the writer's loop indices from the read's row
and column and walks the disjunction of writers, `CombCover.lean`); the number of leaves `H` is
`((N : Int) + 1) / 2`, which `omega` reads. -/

set_option maxHeartbeats 600000 in
theorem solution : Goal := by
  intro N hN
  have hN' : 1 ≤ N := hN.1
  obtain ⟨hc, ha, hso⟩ := tree_struct N hN'
  refine CombTask.satisfiedAt_of_comb (tree_interface N hN' hc) hc ha ?_
  intro st heqs hs v hv
  obtain ⟨x, y, ⟨⟩⟩ := v
  simp only [SvGolf.Tasks.Mul.task, HoldAll_cons, HoldAll_nil, and_true] at hv ⊢
  obtain ⟨hA, hB⟩ := hv
  sv_equations
  · obtain ⟨⟨vp, hvp, hvpw⟩, -⟩ := known_p_g_fin_0 0 (by omega)
    have ba : ∀ i, i < N → st.boolAt "a" i = x.getLsbD i := fun i hi => SvState.boolAt_ofBitVec hA hi
    have bb : ∀ i, i < N → st.boolAt "b" i = y.getLsbD i := fun i hi => SvState.boolAt_ofBitVec hB hi
    rw [hvp, SvState.lookup_eq_ofBitVec_bv (W := 2 * N) hvp (by omega)
      (fun k hk => (known_p_g_fin_0 k (by omega)).2)]
    congr 2
    refine HeapArith.heap_mul (H := (N + 1) / 2) hN' (by omega) (by omega) x y
      (XF.bv (2 * N) (st.boolAt "p")) (st.boolAt "ae") (st.boolAt "bb") (st.cell "S" (2 * N))
      (st.cell "C" (2 * N)) (st.cell "X" (2 * N)) (st.cell "Y" (2 * N)) (st.boolAt "R")
      ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_
    · sv_bridge eq_ae_plain_0
    · sv_bridge eq_ae_plain_1 with ba
    · sv_bridge eq_ae_plain_2
    · sv_bridge eq_bb_plain_3 with bb
    · intro k hk1 hk2
      sv_bridge (eq_bb_plain_4 (k - N) (by omega))
    · sv_bridge eq_S_g_lc_0
    · sv_bridge eq_C_g_lc_1
    · sv_bridge eq_Y_g_node_0
    · sv_bridge eq_C_g_node_1
    · sv_bridge eq_X_g_col_0
    · sv_bridge eq_S_g_col_1
    · sv_bridge eq_Y_g_car_0
    · sv_bridge eq_C_g_car_1
    · sv_bridge eq_R_plain_7
    · sv_bridge eq_p_g_fin_0 with XF.getLsbD_bv
    · sv_bridge eq_R_g_fin_1
  case inputsKnown_1 => exact inKnown_ofBitVec hA (by omega)
  case inputsKnown_2 => exact inKnown_ofBitVec hB (by omega)
  all_goals first | (intros; omega) | (intros; rfl) | sv_cover

/--
info: 'Submission.solution' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms solution

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 = 4

Drawn at N = 4, a display instance; scored at N = 16. 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.

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: 70 cells here, 1 431 at the scoring point. The critical path at N = 4 (14 cells, ending at p[6] rising, 2 206 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 = 4: 70 cells, 32 nand2_1, 16 and2_1, 9 xnor2_1, 6 xor2_1, 5 or2_1, 1 inv_1, 1 nand2b_1. There (measured, not ranked): 392.88 µm², 2 206 ps. Open the drawing on its own (SVG, 45.1 KB) to pan and zoom it with the browser's own controls.

Critical path

at N = 16 · scored

The path the ranked delay ends on, at the scoring point N = 16: 58 nets, 57 cells, to p[30] rising at 5 342 ps. 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 an input: its arrival is the input driver's own delay (buf_8 fed by a 50 ps ramp). 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 = 4, the critical path is 14 cells to p[6] rising (2 206 ps there); each cell is a link to it in the drawing:

b[1]
_191_ and2_1
_197_ xnor2_1
_198_ nand2_1
_208_ nand2_1
_211_ xor2_1
_213_ xnor2_1
_214_ nand2_1
_227_ or2_1
_237_ and2_1
_241_ or2_1
_248_ nand2_1
_249_ nand2_1
_257_ xor2_1
_258_ xnor2_1
p[6]

every stage (58 rows)

#	net	edge	driven by	cell	arrival (ps)	transition (ps)	stage (ps)
0	`b[5]`	fall	input port	–	136.4	40.7
1	`_3710_`	fall	`_3834_`	`and2_1`	305.0	54.5	168.6
2	`_3753_`	rise	`_3838_`	`xnor2_1`	515.9	202.4	210.9
3	`_3764_`	fall	`_3839_`	`nand2_1`	589.2	47.5	73.3
4	`_3775_`	rise	`_3840_`	`nand2_1`	677.2	80.1	88.0
5	`_2409_`	rise	`_3843_`	`xor2_1`	870.6	190.5	193.4
6	`_2430_`	rise	`_3845_`	`xor2_1`	1 087.4	190.5	216.8
7	`_2452_`	rise	`_3847_`	`xor2_1`	1 304.0	190.2	216.6
8	`_2604_`	fall	`_3861_`	`nand2_1`	1 370.9	53.7	66.9
9	`_3036_`	rise	`_3996_`	`nand2_1`	1 461.6	80.2	90.7
10	`_3039_`	rise	`_3999_`	`xor2_1`	1 655.1	190.5	193.5
11	`_3041_`	rise	`_4001_`	`xor2_1`	1 873.8	193.2	218.7
12	`_3042_`	fall	`_4002_`	`nand2_1`	1 938.8	50.2	65.0
13	`_3045_`	fall	`_4006_`	`and2_1`	2 095.8	39.9	157.0
14	`_3094_`	fall	`_4055_`	`or2_1`	2 314.5	49.4	218.7
15	`_3150_`	fall	`_4112_`	`and2_1`	2 465.0	51.4	150.5
16	`_3151_`	rise	`_4113_`	`nand2_1`	2 526.6	41.4	61.6
17	`_3152_`	fall	`_4115_`	`nand2_1`	2 592.4	55.0	65.8
18	`_3213_`	rise	`_4176_`	`nand2_1`	2 647.9	47.0	55.5
19	`_3214_`	fall	`_4178_`	`nand2_1`	2 715.5	55.1	67.6
20	`_3281_`	rise	`_4245_`	`nand2_1`	2 771.0	47.0	55.5
21	`_3282_`	fall	`_4247_`	`nand2_1`	2 838.6	55.1	67.6
22	`_3357_`	rise	`_4322_`	`nand2_1`	2 923.4	83.4	84.8
23	`_3441_`	fall	`_4405_`	`nand2_1`	2 973.7	46.3	50.3
24	`_3442_`	rise	`_4407_`	`nand2_1`	3 061.9	81.3	88.2
25	`_3538_`	fall	`_4494_`	`nand2_1`	3 111.7	46.3	49.8
26	`_3539_`	rise	`_4496_`	`nand2_1`	3 199.9	81.3	88.2
27	`_3632_`	fall	`_4581_`	`nand2_1`	3 249.8	46.3	49.9
28	`_3634_`	rise	`_4583_`	`nand2_1`	3 337.9	81.3	88.1
29	`_3722_`	fall	`_4663_`	`nand2_1`	3 387.8	46.3	49.9
30	`_3723_`	rise	`_4665_`	`nand2_1`	3 476.0	81.3	88.2
31	`_2410_`	fall	`_4743_`	`nand2_1`	3 525.8	46.3	49.8
32	`_2411_`	rise	`_4745_`	`nand2_1`	3 614.0	81.3	88.2
33	`_2489_`	fall	`_4816_`	`nand2_1`	3 663.8	46.3	49.8
34	`_2490_`	rise	`_4818_`	`nand2_1`	3 752.0	81.3	88.2
35	`_2563_`	fall	`_4884_`	`nand2_1`	3 801.9	46.3	49.9
36	`_2564_`	rise	`_4886_`	`nand2_1`	3 890.0	81.3	88.1
37	`_2629_`	fall	`_4945_`	`nand2_1`	3 939.9	46.3	49.9
38	`_2630_`	rise	`_4947_`	`nand2_1`	4 028.1	81.3	88.2
39	`_2687_`	fall	`_4999_`	`nand2_1`	4 077.9	46.3	49.8
40	`_2688_`	rise	`_5001_`	`nand2_1`	4 166.1	81.3	88.2
41	`_2742_`	fall	`_5050_`	`nand2_1`	4 215.9	46.3	49.8
42	`_2743_`	rise	`_5052_`	`nand2_1`	4 304.1	81.3	88.2
43	`_2790_`	fall	`_5094_`	`nand2_1`	4 354.0	46.3	49.9
44	`_2791_`	rise	`_5096_`	`nand2_1`	4 442.1	81.3	88.1
45	`_2829_`	fall	`_5131_`	`nand2_1`	4 492.0	46.3	49.9
46	`_2831_`	rise	`_5133_`	`nand2_1`	4 580.2	81.3	88.2
47	`_2866_`	fall	`_5165_`	`nand2_1`	4 630.0	46.3	49.8
48	`_2867_`	rise	`_5167_`	`nand2_1`	4 689.3	41.4	59.3
49	`_2868_`	fall	`_5168_`	`nand2_1`	4 755.1	55.0	65.8
50	`_2893_`	rise	`_5191_`	`nand2_1`	4 810.6	47.0	55.5
51	`_2895_`	fall	`_5193_`	`nand2_1`	4 878.2	55.1	67.6
52	`_2914_`	rise	`_5211_`	`nand2_1`	4 933.7	46.6	55.5
53	`_2916_`	fall	`_5213_`	`nand2_1`	5 001.1	55.1	67.4
54	`_2928_`	rise	`_5224_`	`nand2_1`	5 065.5	57.1	64.4
55	`_2935_`	fall	`_5232_`	`nand2_1`	5 117.6	37.5	52.1
56	`_2937_`	fall	`_5233_`	`nand2b_1`	5 245.8	39.3	128.2
57	`_2404_`	rise	`_5235_`	`nand2_1`	5 342.5	107.0	96.7

Cells

at N = 16 · scored

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.

cell	count	µm² each	µm² in all	share
`xor2_1`	403	8.7584	3529.6352	44.3%
`nand2_1`	854	3.7536	3205.5744	40.3%
`xnor2_1`	62	8.7584	543.0208	6.8%
`and2_1`	68	6.2560	425.4080	5.3%
`nand2b_1`	21	6.2560	131.3760	1.7%
`nor2b_1`	10	6.2560	62.5600	0.8%
`nor2_1`	6	3.7536	22.5216	0.3%
`or2_1`	3	6.2560	18.7680	0.2%
`inv_1`	3	3.7536	11.2608	0.1%
`mux2_1`	1	11.2608	11.2608	0.1%
total	1 431		7961.3856

Repair (buffer_trees_v1): 0 buffers on 0 nets, 0 tie cells, 1 weighing round; nothing is resized.

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

the gate mix of the extra GE column (the pinned GE table, score/ge.json)

Cells by type; area is the count weighted by the pinned GE table.

cell	count	GE each	GE total
`NAND`	854	1.000	854.000
`XOR`	403	2.000	806.000
`AND`	68	1.333	90.644
`XNOR`	62	2.000	124.000
`ORNOT`	21	1.333	27.993
`ANDNOT`	10	1.333	13.330
`NOR`	6	1.000	6.000
`NOT`	3	0.667	2.001
`OR`	3	1.333	3.999
`MUX`	1	2.333	2.333
total	1431		1930.300

The record

task: mul
player: late-carry
assisted by: Claude Sonnet 5.5 (Anthropic)
submitted: 2026-11-05
notes: Made by an AI agent (Claude Sonnet, Anthropic) in the maintainers' newcomer study on 2026-11-05; the agent chose the player name. The design is the reference mul_tree_h (a carry-save tree of 4:2 compressors with two-row leaves and a ripple-carry final adder) with the same dataflow and generate-block labels; only the Boolean form of the cell assigns changed (XOR association, carries written as muxes, which compressor input arrives late), chosen by a search over those forms scored with score/ppa.py. The proof is the reference proof with one added lemma that restates its arithmetic theorem for these gate forms by a Boolean case split. The header comments of both files are the reference's, unchanged. Proof ported by the maintainers for the 2026-11-06 range change; design unchanged.
scoring point: N = 16
design: solution.sv sha256 9f7eb149ac237cd89d414f5de7f9e021bae46f339b13f5db8726e6f5a635bab5
proof: Solution.lean sha256 c63b53572d1bc3d6e96ca83ca95c175743054d32d495fea945c83216917870b2
canonical text: sha256 566ad1e6139884603cd2a557aaba814a9aef7d2cb0cb33d98e941ba8266b541e
record hash: 5b30f35c283bff377e4a02300c0248f4ee89ec2ea61441000da0b896cbc64b34
downloads: 5b30f35c283b.sv 5b30f35c283b.lean 5b30f35c283b.json
previous frontier: none: no submission of this task is dated before this one; 1 other submission is dated the same day (2026-11-05), which does not order it

The proof

code lines: 360
build time: 59.63 s
axioms: Classical.choice, Quot.sound, propext
tactics seen: decide, grind, induction, omega, simp, sv_cover, sv_equations, sv_interface, sv_rowmajor, sv_structure
imports: Submission.Design, SvGolf.Comb, LeanModels.Sv.CombEqTactic, LeanModels.Sv.CombLib

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: d1f3cae6f01a088007a57b31ff8baa6b839d6f74
lean-surfaces revision: d1f3cae6f01a088007a57b31ff8baa6b839d6f74
canonicalization script: bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b
scoring script: ea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445
GE table: 6a29196a3f4b58241f4c9af650c9141e4632b737214d563a11ba142a725c4bea
extractor: 4930696021c588c75dc890034c534c95560ad9a28a4955b87d1f8d68b5edbc0c
canonical RTLIL: a07aff68c4817022e892973d23f7c11d90be5d164adfadf08dc04141bec0937e

the checker's files (sha256)

file	sha256
`check.py`	`e708084f72f955b0ae1aaabe469dba3eacc5a91484a1ed81bcc073b60f3c0b6d`
`check/Comparator.lean`	`3145eb578ca71e452eff05a398e8ad04673e6c72ca5343b234cb22e2cefe65a6`
`check/SvEval.lean`	`fb51d72510b515460866c2798aad3c6f55295536e627b92854c3580af215bb91`
`check/clocked_rules.py`	`73856a45905724544247ad29042bdc2f1778271ec07b15cdb3a5f214685165c1`
`check/envelope.py`	`076db01a9791bcc25ee84e9b0033604a4b675f00b212eab0c864078e6a4748b7`
`check/postsynth.py`	`4e1ee2110c63f24e033dd689c929ea686ddf10f4db23b9057c6fb711394c7558`
`lakefile.toml`	`f35a88404367d22906effc14d644aac9a9cad47dfd3b704ea8fec88acfaf9c4d`
`lean-toolchain`	`62c2d9c0fc1ec4c67e151c11eff41ca004ef38e179cf9476c230406e6defedef`
`score/banlist.py`	`f18c14c23a14d55db63e202f42cc424dc84c1dd1c337f132ad60859dc9d5d33a`
`score/canon.ys`	`bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b`
`score/fourstate.py`	`95332451ae3754226fb87b46027385b46a91121e7eb9ae25b302bce756d90475`
`score/ge.json`	`6a29196a3f4b58241f4c9af650c9141e4632b737214d563a11ba142a725c4bea`
`score/ge_seq.json`	`54b93ca63888009d0671c8978e8ab7bf4fb8ce303bc78d3b4e1f83d946cc3201`
`score/ppa.py`	`912031912c3e3f6790725161753e95415df34846bd8c27dde3eb707747ddbcbe`
`score/ppa_mapped.ys`	`93547b343dbac135737e98516b1004a780e1cf2f579e1bd7fed82c908c6d4125`
`score/ppa_mapped_pins.json`	`4b8688ba3f4d67681658e5944afe878592adf588cd416a8b47597ebe06deb045`
`score/ppa_pins.json`	`d66a6086a37a97f5985266057051979fb6a8a3c557d3ef9c42acc1b5e41502d8`
`score/score.py`	`71d2e3b82f8813ec64a58f0a46909ca23dfab377db44eda6f294b713f45ae781`
`score/srcgate.py`	`11952f61058051c9e8de91a801b672d07e66a29308e978156c04ffd9f0dbef45`
`score/svgolf.ys`	`ea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445`
`score/svgolf_seq.ys`	`c3874dbfc85921a87df6eacdfc6b2c9a0e2b34edd5738951e0d8bdb51f4558b2`

Post-synthesis check

ls-sv's reading of the design and the scored netlist, simulated on the same vectors, agreed on every one. The vectors are a sample of the inputs: a guard against the two tools disagreeing, not a proof.

mode: full
vectors: 330
full set: 330
mismatches: 0
point: N=16
seed: 70067cf91f3a9f9aab05172b97108564a08a3daf2873d6f5ffa9152a05378815
salted: no

Area against time

µm² × ps · lower left is better · ASAP7

the designs as numbers, by score

design	kind	area (µm²)	time (ps)	score (µm²·ns)
late-carry · this design	submission	7 961.39	5 342	42 530
`dadda_rc_16`	baseline, not proved	8 230.39	5 461	44 946
`dadda_ks_16`	baseline, not proved	8 937.32	5 148	46 009
plus-minus-two	submission	7 978.90	6 329	50 498
`mul_tree_h`	proved reference · par	8 563.21	5 992	51 311
`mul_tree`	proved reference	8 603.25	6 129	52 729
`mul_wallace`	proved reference	8 966.10	5 982	53 635
`yosys_mul`	baseline, not proved · banned operator	8 825.96	6 261	55 259
`mul_n`	proved reference	8 290.45	10 907	90 424
`mul_n_byhand`	proved reference	8 290.45	10 907	90 424

the designs as numbers, by score

design	kind	area (µm²)	time (ps)	score (µm²·ns)
`dadda_ks_16`	baseline, not proved	133.174	902	120.1
late-carry · this design	submission	120.854	1 088	131.5
`dadda_rc_16`	baseline, not proved	123.391	1 100	135.7
`mul_tree_h`	proved reference · par	127.954	1 160	148.4
`yosys_mul`	baseline, not proved · banned operator	131.789	1 139	150.1
`mul_tree`	proved reference	128.552	1 191	153.1
plus-minus-two	submission	119.746	1 307	156.5
`mul_wallace`	proved reference	133.917	1 186	158.8
`mul_n`	proved reference	123.930	1 981	245.5
`mul_n_byhand`	proved reference	123.930	1 981	245.5

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)
python3.12 score/ppa.py 5b30f35c283bff377e4a02300c0248f4ee89ec2ea61441000da0b896cbc64b34.sv --task tasks/mul --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256: a07aff68c4817022e892973d23f7c11d90be5d164adfadf08dc04141bec0937e
ppa.netlist_sha256: 543b374acc78d6623eee062b9bb8cebcae8c0c517eed5e224ec57cb6b1042247
ppa.repair.netlist_sha256: 993dd1dc69f9bbe8ec3d273856040e9774940d890592395b8d204067104dc600
ppa.area_e4um2_sky130: 79613856
ppa.delay_ps_sky130: 5342

The schematic and the critical-path data are site/schematics/mul/9f7eb149ac237cd8.json and its .svg, written by site/gen_schematics.py (the display instance is ppa.py ... --param N=4 --repaired-netlist, drawn by netlistsvg 1.0.2; repaired netlist sha256 c18c43c33b117d18…).

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 5b30f35c283bff377e4a02300c0248f4ee89ec2ea61441000da0b896cbc64b34.sv --task tasks/mul --pdk asap7 --no-mapped \
    --json out.json

Expect, in out.json:

ppa.netlist_sha256: 543b374acc78d6623eee062b9bb8cebcae8c0c517eed5e224ec57cb6b1042247
ppa.repair.netlist_sha256: 540f9ff763d63b371f98e7f1ee6d30ec774af971d78e9c0cb11cf91d360b1095
ppa.area_e5um2_asap7: 12085362
ppa.delay_ps_asap7: 1088

leaderboard/asap7/mul.json keeps these numbers; python3.12 leaderboard/leaderboard.py asap7 --rescore --task mul 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=5b30f35c283bff377e4a02300c0248f4ee89ec2ea61441000da0b896cbc64b34
mkdir -p rec/mul && cp "$H.json" "$H.sv" "$H.lean" rec/mul/
python3.12 leaderboard/leaderboard.py verify --data-dir rec --task mul --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.