Tasks / mul / record

Record `a24c91127116`

reference: par, not an entryreference: par, not an entry scored at N = 16

Recorded by the maintainers from the proved reference mul_tree_h: its design and its proof mul_tree_h.lean (307 code lines). A carry-save tree whose leaves each hold two partial-product rows, every node a 4:2 compressor, with a ripple final adder. The record shows that reference passing the whole checker. It is par, the bar to beatpar, the bar to beat, not a player's entry, and it is not ranked among the submissions (proved references).

Area

8 563.21µm²

8 563.2128 µm² exactly

Beats 0% · matches 0%

0 of 2 other players beaten, 0 equal.

vs par: this design is par
on this page: 6th of 10 designs

cells: 1 450
flops: 0
repair: 0 buffers, 0 tie cells
GE: 2 025.905 extra
A1′: 8 134.05 µm² research

Performance · time

5 992ps

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

Beats 50% · matches 0%

1 of 2 other players beaten, 0 equal.

vs par: this design is par
on this page: 5th of 10 designs

Fmax-eq.: 166.9 MHz derived
critical path: 56 cells
unit depth: 62 extra
A1′: 6 217 ps research

Score · area × time

51 311µm²·ns

8 563.2128 µm² × 5 992 ps

Beats 0% · matches 0%

0 of 2 other players beaten, 0 equal.

vs par: this design is par
on this page: 5th of 10 designs
board: par, the bar to beat: never ranked
Pareto: dominated on this page by late-carry and dadda_rc_16

On the board, of 2 other players: 0 beaten, 0 level, 1 trade off, 1 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 (2 players, 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 10 designs of the area-time plot (5 references, 2 submissions and 3 baselines): not a ranking.

Area

127.954µm²

127.95408 µm² exactly

Beats 0% · matches 0%

0 of 2 other players beaten, 0 equal.

vs par: this design is par
on this page: 6th of 10 designs

cells: 1 451
flops: 0
repair: 0 buffers, 0 tie cells
GE: 2 025.905 extra

Performance · time

1 160ps

the delay: the latest output arrival

Beats 50% · matches 0%

1 of 2 other players beaten, 0 equal.

vs par: this design is par
on this page: 5th of 10 designs

Fmax-eq.: 862.1 MHz derived
unit depth: 62 extra

Score · area × time

148.4µm²·ns

127.95408 µm² × 1 160 ps

Beats 50% · matches 0%

1 of 2 other players beaten, 0 equal.

vs par: this design is par
on this page: 4th of 10 designs
board: par, the bar to beat: never ranked
Pareto: dominated on this page by late-carry and dadda_rc_16

On the board, of 2 other players: 0 beaten, 0 level, 1 trade off, 1 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

mul_tree_h.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] = ae[c + 2*N - 1 - 2*j] & bb[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+1][c] ^ C[2*k+1][c] ^ S[2*k+2][c];
        assign S[k][c] = X[k][c] ^ Y[k][c] ^ C[2*k+2][c];
      end
      for (c = 0; c < 2*N-1; c++) begin : g_car
        assign 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]));
        assign C[k][c+1] = (X[k][c] & Y[k][c]) | (C[2*k+2][c] & (X[k][c] ^ Y[k][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] = (S[0][c] & C[0][c]) | (R[c] & (S[0][c] ^ C[0][c]));
    end
  endgenerate
endmodule

mul_tree_h.lean (307 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_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 = (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]

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: 64 cells here, 1 450 at the scoring point. The critical path at N = 4 (11 cells, ending at p[6] rising, 1 777 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: 64 cells, 27 nand2_1, 18 and2_1, 16 xor2_1, 3 xnor2_1. There (measured, not ranked): 380.36 µm², 1 777 ps. Open the drawing on its own (SVG, 41.7 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: 57 nets, 56 cells, to p[30] rising at 5 992 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 11 cells to p[6] rising (1 777 ps there); each cell is a link to it in the drawing:

a[3]
_244_ and2_1
_247_ xnor2_1
_249_ xor2_1
_251_ xor2_1
_253_ xor2_1
_254_ and2_1
_269_ nand2_1
_271_ nand2_1
_279_ nand2_1
_281_ nand2_1
_287_ xor2_1
p[6]

every stage (57 rows)

#	net	edge	driven by	cell	arrival (ps)	transition (ps)	stage (ps)
0	`a[8]`	fall	input port	–	128.1	33.5
1	`_3974_`	fall	`_6077_`	`and2_1`	290.6	51.7	162.5
2	`_4027_`	rise	`_6131_`	`xor2_1`	491.3	190.5	200.7
3	`_4029_`	rise	`_6133_`	`xor2_1`	708.0	190.5	216.7
4	`_4031_`	rise	`_6135_`	`xor2_1`	924.8	190.5	216.8
5	`_4033_`	rise	`_6137_`	`xor2_1`	1 141.6	190.5	216.8
6	`_4035_`	rise	`_6139_`	`xor2_1`	1 358.4	190.5	216.8
7	`_4037_`	rise	`_6141_`	`xor2_1`	1 575.1	190.5	216.7
8	`_4039_`	rise	`_6143_`	`xor2_1`	1 791.9	190.5	216.8
9	`_4041_`	rise	`_6145_`	`xor2_1`	2 008.7	190.5	216.8
10	`_4043_`	rise	`_6147_`	`xor2_1`	2 225.4	190.5	216.7
11	`_4045_`	rise	`_6149_`	`xor2_1`	2 430.5	174.5	205.1
12	`_4047_`	rise	`_6151_`	`xor2_1`	2 645.3	190.5	214.8
13	`_4049_`	rise	`_6153_`	`xor2_1`	2 862.0	190.5	216.7
14	`_4050_`	fall	`_6154_`	`nand2_1`	2 933.8	45.9	71.8
15	`_4051_`	rise	`_6156_`	`nand2_1`	3 021.0	80.1	87.2
16	`_4108_`	fall	`_4763_`	`nand2_1`	3 070.6	45.9	49.6
17	`_4109_`	rise	`_4765_`	`nand2_1`	3 157.8	80.1	87.2
18	`_4172_`	fall	`_4828_`	`nand2_1`	3 207.4	45.9	49.6
19	`_4173_`	rise	`_4830_`	`nand2_1`	3 294.6	80.1	87.2
20	`_4242_`	fall	`_4899_`	`nand2_1`	3 344.1	45.9	49.5
21	`_4243_`	rise	`_4901_`	`nand2_1`	3 431.3	80.1	87.2
22	`_4319_`	fall	`_4977_`	`nand2_1`	3 480.9	45.9	49.6
23	`_4320_`	rise	`_4979_`	`nand2_1`	3 568.1	80.1	87.2
24	`_4404_`	fall	`_5061_`	`nand2_1`	3 617.7	45.9	49.6
25	`_4405_`	rise	`_5063_`	`nand2_1`	3 704.9	80.1	87.2
26	`_4500_`	fall	`_5150_`	`nand2_1`	3 754.5	45.9	49.6
27	`_4501_`	rise	`_5152_`	`nand2_1`	3 841.7	80.1	87.2
28	`_4595_`	fall	`_5238_`	`nand2_1`	3 891.2	45.9	49.5
29	`_4596_`	rise	`_5240_`	`nand2_1`	3 978.4	80.1	87.2
30	`_4684_`	fall	`_5320_`	`nand2_1`	4 028.0	45.9	49.6
31	`_4685_`	rise	`_5322_`	`nand2_1`	4 115.2	80.1	87.2
32	`_3353_`	fall	`_5400_`	`nand2_1`	4 164.8	45.9	49.6
33	`_3354_`	rise	`_5402_`	`nand2_1`	4 252.0	80.1	87.2
34	`_3432_`	fall	`_5473_`	`nand2_1`	4 301.6	45.9	49.6
35	`_3433_`	rise	`_5475_`	`nand2_1`	4 388.8	80.1	87.2
36	`_3503_`	fall	`_5540_`	`nand2_1`	4 438.4	45.9	49.6
37	`_3504_`	rise	`_5542_`	`nand2_1`	4 525.5	80.1	87.1
38	`_3568_`	fall	`_5600_`	`nand2_1`	4 575.1	45.9	49.6
39	`_3569_`	rise	`_5602_`	`nand2_1`	4 662.3	80.1	87.2
40	`_3631_`	fall	`_5658_`	`nand2_1`	4 711.9	45.9	49.6
41	`_3632_`	rise	`_5660_`	`nand2_1`	4 799.1	80.1	87.2
42	`_3686_`	fall	`_5709_`	`nand2_1`	4 848.7	45.9	49.6
43	`_3687_`	rise	`_5711_`	`nand2_1`	4 935.9	80.1	87.2
44	`_3734_`	fall	`_5754_`	`nand2_1`	4 985.5	45.9	49.6
45	`_3735_`	rise	`_5756_`	`nand2_1`	5 072.6	80.1	87.1
46	`_3774_`	fall	`_5791_`	`nand2_1`	5 122.2	45.9	49.6
47	`_3775_`	rise	`_5793_`	`nand2_1`	5 209.4	80.1	87.2
48	`_3809_`	fall	`_5825_`	`nand2_1`	5 259.0	45.9	49.6
49	`_3810_`	rise	`_5827_`	`nand2_1`	5 346.2	80.1	87.2
50	`_3838_`	fall	`_5852_`	`nand2_1`	5 395.8	45.9	49.6
51	`_3839_`	rise	`_5854_`	`nand2_1`	5 483.0	80.1	87.2
52	`_3860_`	fall	`_5873_`	`nand2_1`	5 532.6	45.9	49.6
53	`_3861_`	rise	`_5875_`	`nand2_1`	5 619.8	80.1	87.2
54	`_3874_`	fall	`_5887_`	`nand2_1`	5 669.3	45.9	49.5
55	`_3876_`	rise	`_5889_`	`nand2_1`	5 756.5	80.1	87.2
56	`_3332_`	rise	`_5899_`	`xor2_1`	5 991.8	247.2	235.3

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`	464	8.7584	4063.8976	47.5%
`nand2_1`	684	3.7536	2567.4624	30.0%
`and2_1`	284	6.2560	1776.7040	20.7%
`xnor2_1`	17	8.7584	148.8928	1.7%
`nand2b_1`	1	6.2560	6.2560	0.1%
total	1 450		8563.2128

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`	684	1.000	684.000
`XOR`	464	2.000	928.000
`AND`	284	1.333	378.572
`XNOR`	17	2.000	34.000
`ORNOT`	1	1.333	1.333
total	1450		2025.905

The record

task: mul
player: svgolf-reference
assisted by: Claude (Anthropic)
submitted: 2026-11-07
notes: reference solution
scoring point: N = 16
design: mul_tree_h.sv sha256 f77fcae9b71e648b5d7e30fa4c429b86f75c5315ddd543d6e875b94aa33c3f65
proof: mul_tree_h.lean sha256 4cdd0e0cea2cdcedbefd01705fc6632421a6a13cef1dbd7e97960a1198e091a6: the proof of the reference mul_tree_h (mul_tree_h.lean, 307 code lines)
canonical text: sha256 9da951fcd81f0c35011f053686751f21337389747292eb955e58c5e9398cd4b9
record hash: a24c91127116e87437b1cbbfcdd5d5607d34eb89f3c0e72c26f7bfe9a87f2fba
downloads: a24c91127116.sv a24c91127116.lean a24c91127116.json

The proof

code lines: 307
build time: 34.09 s
axioms: Classical.choice, Quot.sound, propext
tactics seen: 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: 60ebf526fff291b303d5926cece6ff6451e3b1171acd6f8d48b0c944fa8dd6fe

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: c4b1312dcaed2472d21eb03834d60c9b24a5a5c5b862ec4c35eac709e3dbd673
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	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` · this design	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	submission	120.854	1 088	131.5
`dadda_rc_16`	baseline, not proved	123.391	1 100	135.7
`mul_tree_h` · this design	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 tasks/mul/reference/mul_tree_h.sv --task tasks/mul --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256: 60ebf526fff291b303d5926cece6ff6451e3b1171acd6f8d48b0c944fa8dd6fe
ppa.netlist_sha256: 127b7cdd2871845693bd4fab68573b2a9e0f50607dfe336196481aab29557bc5
ppa.repair.netlist_sha256: 58bb983dfaa1ad4865d275f70b5d27aeb9768134e4fd4ae1f1609025c5f2c3a8
ppa.area_e4um2_sky130: 85632128
ppa.delay_ps_sky130: 5992

The schematic and the critical-path data are site/schematics/mul/f77fcae9b71e648b.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 2e1b05730680e17e…).

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

Expect, in out.json:

ppa.netlist_sha256: 127b7cdd2871845693bd4fab68573b2a9e0f50607dfe336196481aab29557bc5
ppa.repair.netlist_sha256: 4ffa243bda30e7f96a2fb3dd760541b437579e6f2e7a265090b62c9bb8b15555
ppa.area_e5um2_asap7: 12795408
ppa.delay_ps_asap7: 1160

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