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

N × N matrix multiplication, clocked matmul

Multiply two signed N × N matrices, wrapping at AccW bits, behind a start/done handshake.

open for submissions clocked, transaction scored at N = 4, W = 8, AccW = 32

Par
3 729 636µm²·nsmatmul_g1 · 87 174 µm² × 4 cycles × 10.7 ns period
Record
2 276 474µm²·nsfanout-ferret · 241 921 µm² × 1 cycle × 9.41 ns period
Under par
−39%
Par
8217µm²·nsmatmul_g1 · 1334.726 µm² × 4 cycles × 1.54 ns period
Record
5935µm²·nsfanout-ferret · 3661.548 µm² × 1 cycle × 1.62 ns period
Under par
−28%

Score

ASAP7 · area × time · µm²·ns · lower is better
matmul: the score of each entry by date5 entries by date (x) and score in µm²·ns (y); the line is the best score so far, the dashed line par. The table under the chart lists the same numbers.2.5M3M3.5M26 Oct2 Nov9 Novdate enteredscore (µm²·ns) · lower is betterpar: matmul_g1, 3 729 636 µm²·nsPAR3 729 636 · provedthe best score so farmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 3 729 636 µm²·ns · Area: 87 173.6 µm² · Time: 42 784 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 psfanout-ferret · submission · 2026-11-10 · Score: 2 511 471 µm²·ns · Area: 137 104.0 µm² · Time: 18 318 psfanout-ferret · submission · 2026-11-10 · Score: 2 276 474 µm²·ns · Area: 241 920.8 µm² · Time: 9410 ps
matmul: the score of each entry by date5 entries by date (x) and score in µm²·ns (y); the line is the best score so far, the dashed line par. The table under the chart lists the same numbers.2.5M3M3.5M26 Oct2 Nov9 Novdate enteredscore (µm²·ns) · lower is betterpar: matmul_g1, 3 729 636 µm²·nsPARthe best score so farmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 3 729 636 µm²·ns · Area: 87 173.6 µm² · Time: 42 784 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 psfanout-ferret · submission · 2026-11-10 · Score: 2 511 471 µm²·ns · Area: 137 104.0 µm² · Time: 18 318 psfanout-ferret · submission · 2026-11-10 · Score: 2 276 474 µm²·ns · Area: 241 920.8 µm² · Time: 9410 ps
  • submission
  • proved reference
  • the best score so far
  • par
Score = area × time: the sky130 cell area of the scored netlist in µm² (flip-flops included) times the latency in cycles × the register-to-register clock period in ns, from the pinned flow, so µm²·ns. Lower is better. It is the one ranked number: Par (the best proved reference's score, the bar to beat), Record (the best accepted score so far, par while no submission beats it), Under par (how far the record is below par, as a share of par's score) and the leaderboard use it. The Pareto front, area in GE (NAND2 gate equivalents), depth and the other numbers are for exploring, under compare the designs; reproduce a score says how to get the same numbers. The clock period (what score/ppa.py calls the register-to-register period) is the longest path from an input or a flip-flop to an output or a flip-flop (clock-to-Q and setup included), so paths from the inputs and to the outputs count too, not only the paths between two flip-flops. Rated with Yosys 0.53 (git 53c22ab7, the Homebrew build for macOS arm64, clang++ 17, -O3) and its yosys-abc (ABC 1.01 of 6 May 2025): the flow is deterministic on that build (measured on 52 designs). Another build of the same version can break ABC's ties differently (measured: 3 fdivp designs, up to 2.9% in delay), so a number made on another platform may differ slightly: the build and its hashes. Dots are the entries by date; the proved references are the first entries, dated by when they joined the task.
every entry by date
datedesignkindscore (µm²·ns)area × time
2026-11-03matmul_g1proved reference · par3 729 63687 174 µm² × 4 × 10.7 ns
2026-11-10fanout-ferretsubmission2 276 474241 921 µm² × 1 × 9.41 ns
2026-11-10vacuity-checksubmission2 377 06385 261 µm² × 5 × 5.58 ns
2026-11-10fanout-ferretsubmission2 511 471137 104 µm² × 2 × 9.16 ns
2026-11-10vacuity-checksubmission3 407 66179 700 µm² × 4 × 10.7 ns
matmul: the score of each entry by date5 entries by date (x) and score in µm²·ns (y); the line is the best score so far, the dashed line par. The table under the chart lists the same numbers.6000650070007500800026 Oct2 Nov9 Novdate enteredscore (µm²·ns) · lower is betterpar: matmul_g1, 8217 µm²·nsPAR8217 · provedthe best score so farmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 8217 µm²·ns · Area: 1334.726 µm² · Time: 6156 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 psfanout-ferret · submission · 2026-11-10 · Score: 6520 µm²·ns · Area: 2085.873 µm² · Time: 3126 psfanout-ferret · submission · 2026-11-10 · Score: 5935 µm²·ns · Area: 3661.548 µm² · Time: 1621 ps
matmul: the score of each entry by date5 entries by date (x) and score in µm²·ns (y); the line is the best score so far, the dashed line par. The table under the chart lists the same numbers.60007000800026 Oct2 Nov9 Novdate enteredscore (µm²·ns) · lower is betterpar: matmul_g1, 8217 µm²·nsPARthe best score so farmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 8217 µm²·ns · Area: 1334.726 µm² · Time: 6156 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 psfanout-ferret · submission · 2026-11-10 · Score: 6520 µm²·ns · Area: 2085.873 µm² · Time: 3126 psfanout-ferret · submission · 2026-11-10 · Score: 5935 µm²·ns · Area: 3661.548 µm² · Time: 1621 ps
  • submission
  • proved reference
  • the best score so far
  • par
Score = area × time: the ASAP7 cell area of the scored netlist in µm² (flip-flops included) times the latency in cycles × the register-to-register clock period in ns, from the pinned flow, so µm²·ns. Lower is better. In this view Par (the best proved reference's score, the bar to beat), Record (the best accepted score so far, par while no submission beats it), Under par (how far the record is below par, as a share of par's score) and the leaderboard use it; the records' ranked score is sky130's, the default view. The Pareto front, area in GE (NAND2 gate equivalents), depth and the other numbers are for exploring, under compare the designs; reproduce a score says how to get the same numbers. ASAP7 view. These numbers are on ASAP7 (asap7sc7p5t), a predictive 7 nm library made for research: it has never been fabricated, so no chip can confirm them. Like sky130's score they count no wires. sky130, a real 130 nm process, is the default view (how ASAP7 is scored, and its quirks). The clock period (what score/ppa.py calls the register-to-register period) is the longest path from an input or a flip-flop to an output or a flip-flop (clock-to-Q and setup included), so paths from the inputs and to the outputs count too, not only the paths between two flip-flops. Rated with Yosys 0.53 (git 53c22ab7, the Homebrew build for macOS arm64, clang++ 17, -O3) and its yosys-abc (ABC 1.01 of 6 May 2025): the flow is deterministic on that build (measured on 52 designs). Another build of the same version can break ABC's ties differently (measured: 3 fdivp designs, up to 2.9% in delay), so a number made on another platform may differ slightly: the build and its hashes. Dots are the entries by date; the proved references are the first entries, dated by when they joined the task.
every entry by date
datedesignkindscore (µm²·ns)area × time
2026-11-03matmul_g1proved reference · par82171334.726 µm² × 4 × 1.54 ns
2026-11-10fanout-ferretsubmission59353661.548 µm² × 1 × 1.62 ns
2026-11-10vacuity-checksubmission64531315.583 µm² × 5 × 0.981 ns
2026-11-10fanout-ferretsubmission65202085.873 µm² × 2 × 1.56 ns
2026-11-10vacuity-checksubmission72911216.745 µm² × 4 × 1.50 ns

First submission: How to submit

This task

Proving guide

Multiply two N × N matrices of signed W-bit entries: C = A · B, every sum wrapping at AccW bits. A handshake frames each product: the design reads A and B when start is pulsed, and after each start raises done once C holds the product. C is claimed only from the first done = 1 after a start until the next start, where it must hold the product; at every other cycle it may show anything, while done is known at every cycle from the release and 0 until the first start. The proof covers every N, W, AccW ≥ 1 with N·N·W < 2^31 and N·N·AccW < 2^31 and proves the latency the submission declares; the score is taken at N = 4, W = 8, AccW = 32.

The design is clocked by clk alone, on its rising edge, with the synchronous reset rst: no asynchronous process, and clk is never read as data. No output may depend combinationally on an input; the claims hold from every power-up value of every register, the first reset included; no construct may create an unknown value, and a register that is never loaded is refused. Every operator but run-time / % ** (banned in every task) is allowed, * included, so the task is the schedule, which the score prices: how many multipliers, how many cycles and how short a cycle. Any schedule is allowed: N² multiply-accumulate units at once, fewer units over more cycles, a systolic array. The proved reference, N² multiply-accumulate units stepping through k, takes N cycles (4 at the scoring point) for 20783.15 GE.

Interface #

Write a module with exactly this header: port names, directions, widths and order matter, and so do the module's name and its parameters.

matmul.sv
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
);
portdirectionwidth (bits)
clkinput1
rstinput1
startinput1
AinputN*N*W
BinputN*N*W
doneoutput1
CoutputN*N*AccW

The trusted statement #

A proof must establish the task's trusted statement, the constant SvGolf.Tasks.Matmul.Statement of Spec.lean (module tasks.matmul.Spec). Below it is split into the properties a circuit must have, one card each: what the property guarantees in plain words, and its exact Lean text. Every proved reference has all of them. The last tab, what does not count, lists the designs the checker rejects.

Properties

A design and its declared latency meet the trusted statement exactly when, for every (N, W, AccW) in range, they have all of the properties below. The last five are guarantees the design owes an environment that follows the protocol: after a reset is released, start is raised only while the design is idle, and A and B are held from start until done rises. Lean checks that, together, the properties say exactly what the statement says, nothing less and nothing more (the theorem statement_iff_properties).

PARAMS_IN_RANGE is the range the statement covers, not a property: every other card must hold at each value in it.

PARAMS_IN_RANGErangeThe parameters the statement covers: N, W, AccW ≥ 1, and both port widths below 2^31.

The statement covers every matrix size N ≥ 1, entry width W ≥ 1 and accumulator width AccW ≥ 1, as long as both port widths, N·N·W and N·N·AccW bits, stay below 2^31: the parameters are 32-bit ints, and in that range a real SystemVerilog tool and Lean's model agree on every width and index. One proof covers all of them; the design is scored at N = 4, W = 8, AccW = 32.

ParamsInRange
/-- The parameters the statement covers: `N, W, AccW ≥ 1`, and both port widths below `2^31`. -/
def ParamsInRange (N W AccW : Nat) : Prop :=
  1 ≤ N ∧ 1 ≤ W ∧ 1 ≤ AccW ∧ N * N * W < 2 ^ 31 ∧ N * N * AccW < 2 ^ 31
svgolf/tasks/matmul/Properties.lean:27Open in code
INTERFACEExactly these ports, in this order, with these widths; no two declarations share a name.

The module has exactly the input ports clk, rst, start (1 bit each), A and B (N·N·W bits each) and exactly the output ports done (1 bit) and C (N·N·AccW bits), with these widths, in this order. Nothing is missing and nothing is extra: an extra input could serve as a hidden mode pin, and the checker and the scoring tools drive and read the design by these names and widths. No two declarations of the module (ports or internal signals) share a name, so every port has exactly one declared width. Matrices are flat, row-major, least significant entry first: entry (i, k) of A is A[(i·N+k)·W +: W].

Interface
/-- Exactly these ports, in this order, with these widths; no two declarations share a name. -/
def Interface (N W AccW : Nat) (d : Design2) : Prop :=
  inputPorts d = [("clk", 1), ("rst", 1), ("start", 1), ("A", N * N * W), ("B", N * N * W)] ∧
    outputPorts d = [("done", 1), ("C", N * N * AccW)] ∧ (d.decls.toList.map Decl.name).Nodup
svgolf/tasks/matmul/Properties.lean:31Open in code
CLOCK_DISCIPLINEclk is an input; every process that runs at a clock edge is clocked by clk; no process has an asynchronous reset (rst is synchronous); no process reads clk as data.

The clock is the input clk: every register is clocked by it, no register has an asynchronous reset (rst is synchronous, read inside the clocked processes), and no logic reads clk as a data signal. Together these make one cycle of Lean's model exactly one rising edge of clk in the real circuit: a clock that is gated, derived from logic, tied off or never driven is ruled out. One consequence to know: the registers have to sit in the top module, because connecting clk to a child instance copies it as data.

ClockDiscipline
/-- `clk` is an input; every process that runs at a clock edge is clocked by `clk`; no process
has an asynchronous reset (`rst` is synchronous); no process reads `clk` as data. -/
def ClockDiscipline (d : Design2) : Prop :=
  "clk" ∈ d.inputNames.toList ∧
    ∀ p ∈ d.processes.toList,
      (p.isEdgePhase = true → edgeClock p = some "clk") ∧
      asyncReset p = none ∧
      "clk" ∉ processDataNames p
svgolf/tasks/matmul/Properties.lean:36Open in code
TERMINATESFrom every power-up state, under every schedule and every known stimulus, the run completes.

From every power-up state (every register and variable, 2-state ones included, holding some 0 or 1), whatever order the simulator picks for processes that are ready at the same moment (the schedule), and whatever known values the environment drives on the inputs, simulating the design completes: every clock cycle settles. A combinational loop that oscillates fails this, and so does a design the tools could not read. It is also what gives the guarantees below their teeth: they are about completed runs, and a design with no completed run would satisfy them without doing anything.

Terminates
/-- From every power-up state, under every schedule and every known stimulus, the run completes. -/
def Terminates (d : Design2) : Prop :=
  ∀ st0, PowerUp d st0 → ∀ (σ : ScheduleOracle) (stim : List SvState), KnownStim d stim →
    ∃ tr, RunsAt d σ st0 stim tr
svgolf/tasks/matmul/Properties.lean:45Open in code
LATENCY_AT_LEAST_ONEThe declared latency is at least one cycle.

Besides the design, a submission declares its latency: the number of cycles it may take to answer a start, as a function of the parameters. It must be at least one cycle. The checker pins its value at the scoring point, and the score uses it (time = latency × clock period), so declaring a larger latency than needed only costs score.

LatencyAtLeastOne
/-- The declared latency is at least one cycle. -/
def LatencyAtLeastOne (lat : Nat) : Prop :=
  1 ≤ lat
svgolf/tasks/matmul/Properties.lean:50Open in code
MOORE_OUTPUTSNo combinational path leads from an input port, rst included, to an output port (MooreOutDep with nothing exempt, txtask-v2 rule 1): done and C are functions of the registers, so every snapshot is what the wires show for the whole next period.

No combinational path leads from any input, rst included, to done and C: the outputs are functions of the registers only. The proof reads the outputs in the snapshot just after a clock edge, with that cycle's inputs still applied; on the wire the inputs change before the next edge. Without this rule an output that reads an input directly would be proved on one value and seen on another; an output gated by rst could hide a transaction's last value from a consumer when a reset follows (txtask-v2 rule 1).

MooreOutputs
/-- No combinational path leads from an input port, `rst` included, to an output port
(`MooreOutDep` with nothing exempt, txtask-v2 rule 1): `done` and `C` are functions of the
registers, so every snapshot is what the wires show for the whole next period. -/
def MooreOutputs (d : Design2) : Prop :=
  MooreOutDep d []
svgolf/tasks/matmul/Properties.lean:54Open in code
NO_X_CREATINGNo construct of the design can create an x or z from known operands (XSafe, txtask-v2 rule 3): with the power-up rule, every value of every run is known.

No construct of the design can make an unknown value out of known ones: no run-time / or % except by a nonzero constant, no ** that could be x, no run-time index that can leave its range, no slice beyond its operand, no bitwise or equality operator on operands of different widths, no x or z literal outside a casez/casex pattern. Together with the power-up rule, every value the design computes in Lean's model is then a known 0 or 1, so every if, case and ?: decides on a known value, where the hardware decides too (txtask-v2 rule 3).

NoXCreating
/-- No construct of the design can create an `x` or `z` from known operands (`XSafe`, txtask-v2
rule 3): with the power-up rule, every value of every run is known. -/
def NoXCreating (d : Design2) : Prop :=
  XSafe d
svgolf/tasks/matmul/Properties.lean:68Open in code
DONE_KNOWNdone is a known bit at every cycle from the release.

As long as the environment follows the protocol, done is a known bit, 0 or 1, in every cycle from the release of the reset on. The environment decides when to start the next transaction by watching done, so done must mean something in every cycle; never x.

DoneKnown
/-- `done` is a known bit at every cycle from the release. -/
def DoneKnown (N W AccW : Nat) (d : Design2) : Prop :=
  UnderProtocol N W AccW d fun _ tr c1 h =>
    ∀ c, c1 ≤ c → c < h → ∃ b, TraceBit tr c "done" b
svgolf/tasks/matmul/Properties.lean:73Open in code
DONE_LOW_BEFORE_FIRST_STARTdone is 0 at every cycle from the release up to the first start.

As long as the environment follows the protocol, done is 0 in every cycle after the release of the reset and before the first start. done = 1 claims a result, and before the first start there is none: a design that raises done too soon fails here, whatever C shows.

DoneLowBeforeFirstStart
/-- `done` is 0 at every cycle from the release up to the first start. -/
def DoneLowBeforeFirstStart (N W AccW : Nat) (d : Design2) : Prop :=
  UnderProtocol N W AccW d fun stim tr c1 h =>
    ∀ c, c1 ≤ c → c < h → (∀ s, c1 ≤ s → s ≤ c → ¬ StimBit stim s "start" true) →
      TraceBit tr c "done" false
svgolf/tasks/matmul/Properties.lean:78Open in code
DONE_WITHIN_LATENCYAfter every start s, done is 1 at some cycle at most lat cycles later.

As long as the environment follows the protocol, after every start, done is 1 in some cycle at most lat cycles later, counting the cycle in which start is sampled as cycle 0. Finishing earlier is fine, and the number of cycles may depend on the data, as long as it never exceeds the declared latency.

DoneWithinLatency
/-- After every start `s`, `done` is 1 at some cycle at most `lat` cycles later. -/
def DoneWithinLatency (N W AccW lat : Nat) (d : Design2) : Prop :=
  UnderProtocol N W AccW d fun stim tr c1 h =>
    ∀ s, c1 ≤ s → StimBit stim s "start" true → s + lat < h →
      ∃ c, s ≤ c ∧ c ≤ s + lat ∧ TraceBit tr c "done" true
svgolf/tasks/matmul/Properties.lean:84Open in code
DONE_HELDOnce done is 1 after a start, it stays 1 until the next start.

As long as the environment follows the protocol, once done has been 1 after a start, it stays 1 in every cycle until the next start. The result does not vanish: the environment may read it at any time before it starts the next transaction.

DoneHeld
/-- Once `done` is 1 after a start, it stays 1 until the next start. -/
def DoneHeld (N W AccW : Nat) (d : Design2) : Prop :=
  UnderProtocol N W AccW d fun stim tr c1 h =>
    ∀ s c, c < h → Finished stim tr c1 s c → TraceBit tr c "done" true
svgolf/tasks/matmul/Properties.lean:97Open in code
RESULT_IS_PRODUCTOnce done is 1 after a start with operands A and B, C holds the product A·B until the next start.

As long as the environment follows the protocol, in every cycle from the first done = 1 after a start until the next start, C holds the matrix product A·B of the operands driven when start was sampled. Entries of A and B are signed W-bit numbers, and each C[i][j] = Σ_k A[i][k]·B[k][j] is computed exactly and then wrapped to AccW bits (modulo 2^AccW, as a GPU accumulator does). Once done rises the environment may change A and B, so the design must keep the result, not recompute it from its inputs.

ResultIsProduct
/-- Once `done` is 1 after a start with operands `A` and `B`, `C` holds the product `A·B` until
the next start. -/
def ResultIsProduct (N W AccW : Nat) (d : Design2) : Prop :=
  UnderProtocol N W AccW d fun stim tr c1 h =>
    ∀ s c (A B : BitVec (N * N * W)), c < h → Finished stim tr c1 s c →
      (∃ e, stim[s]? = some e ∧ HoldAll e [("A", N * N * W), ("B", N * N * W)] (A, B, ())) →
      ∃ st, tr[c]? = some st ∧ HoldAll st [("C", N * N * AccW)] (product N W AccW A B, ())
svgolf/tasks/matmul/Properties.lean:102Open in code

Definitions

The names the properties use, each with its Lean text. Trusted text is what a proof is about; a helper of Properties.lean is not trusted: Lean checks it as part of statement_iff_properties.

This task's trusted text

productSpec.leanproduct N W AccW A B: the matrix product, each entry Σ_k A[i][k]·B[k][j] over signed W-bit entries, reduced modulo 2^AccW, packed flat and row-major.
product
/-- The product `C = A·B`, each entry reduced mod `2^AccW`, packed flat row-major. -/
def product (N W AccW : Nat) {n : Nat} (a b : BitVec n) : BitVec (N * N * AccW) :=
  BitVec.ofNat (N * N * AccW)
    ((List.range (N * N)).foldl
      (fun acc ij =>
        acc + (BitVec.ofInt AccW (dot N W a b (ij / N) (ij % N))).toNat * 2 ^ (ij * AccW))
      0)
svgolf/tasks/matmul/Spec.lean:66Open in code
dotSpec.leandot N W A B i j: the exact integer Σ_{k<N} A[i][k]·B[k][j].
dot
/-- `Σ_{k < N} A[i][k] · B[k][j]` in the integers. -/
def dot (N W : Nat) {n : Nat} (a b : BitVec n) (i j : Nat) : Int :=
  (List.range N).foldl (fun acc k => acc + entry W a (i * N + k) * entry W b (k * N + j)) 0
svgolf/tasks/matmul/Spec.lean:62Open in code
entrySpec.leanentry W x idx: entry idx of a flat vector of W-bit signed entries, as an integer.
entry
/-- Entry `idx` of a flat vector of `W`-bit signed entries, as an integer. -/
def entry (W : Nat) {n : Nat} (x : BitVec n) (idx : Nat) : Int :=
  (x.extractLsb' (idx * W) W).toInt
svgolf/tasks/matmul/Spec.lean:58Open in code
StatementSpec.leanThe trusted challenge statement that these properties restate, part by part.
Statement
/-- **The challenge statement**, for the three-parameter design family `sem N W AccW` and the
latency function `lat N W AccW`. The checker's goal is `Statement design.sem lat ∧ lat 4 8 32 = n`
with the latency `lat` the proof file defines and the declared number `n` (C3). -/
abbrev Statement (sem : Nat → Nat → Nat → LeanModels.Sv.Design2) (lat : Nat → Nat → Nat → Nat) :
    Prop :=
  task.StatementV2 (fun p => sem p.1 p.2.1 p.2.2) (fun p => lat p.1 p.2.1 p.2.2)
svgolf/tasks/matmul/Spec.lean:86Open in code
taskSpec.leanThe task as data: the parameter range, the port names and widths, and the function of a transaction.
task
/-- **The task** (C6). -/
def task : TxTask Params where
  inRange p := 1 ≤ p.1 ∧ 1 ≤ p.2.1 ∧ 1 ≤ p.2.2 ∧
    p.1 * p.1 * p.2.1 < 2 ^ 31 ∧ p.1 * p.1 * p.2.2 < 2 ^ 31
  clk := "clk"
  rst := "rst"
  start := "start"
  operands p := [("A", p.1 * p.1 * p.2.1), ("B", p.1 * p.1 * p.2.1)]
  done := "done"
  payload p := [("C", p.1 * p.1 * p.2.2)]
  result p := fun (a, b, ()) => (product p.1 p.2.1 p.2.2 a b, ())
svgolf/tasks/matmul/Spec.lean:74Open in code

Helpers in Properties.lean (proved, not trusted)

FinishedProperties.leanFinished stim tr c1 s c: s is a start after the release c1, done has been 1 in some cycle from s to c, and there is no later start up to c. These are the cycles in which the result must be shown.
Finished
/-- `Finished stim tr c1 s c`: `s` is a start after the release `c1`, `done` has been 1 at some
cycle from `s` to `c`, and there is no later start up to `c`. -/
def Finished (stim tr : List SvState) (c1 s c : Nat) : Prop :=
  c1 ≤ s ∧ StimBit stim s "start" true ∧
    (∃ c', s ≤ c' ∧ c' ≤ c ∧ TraceBit tr c' "done" true) ∧
    ∀ s', s < s' → s' ≤ c → ¬ StimBit stim s' "start" true
svgolf/tasks/matmul/Properties.lean:90Open in code
UnderProtocolProperties.leanUnderProtocol d G: in every completed run from every power-up state on every known stimulus, from every release of the reset, up to every later cycle h before which the environment followed the protocol (the task's Rely), G holds up to h. Every guarantee is stated in this frame, so a protocol violation can only void claims about later cycles.
UnderProtocol
/-- `G` holds in every completed run from every power-up state on every known stimulus, from every
release `c1` of the reset, up to every horizon `h` before which the environment kept the protocol
(`TxTask.Rely`). -/
def UnderProtocol (N W AccW : Nat) (d : Design2)
    (G : List SvState → List SvState → Nat → Nat → Prop) : Prop :=
  ModelsPU d fun stim tr =>
    ∀ c1 h, Released "rst" stim c1 h → task.Rely (N, W, AccW) stim tr c1 h → G stim tr c1 h
svgolf/tasks/matmul/Properties.lean:60Open in code

The shared trusted base

TxTask.RelyTaskSeq.leanThe environment's side of the protocol, up to a horizon: start and the operands are driven with known values in every cycle, start is 1 only while the design is idle, and the operands of a start are held until the cycle in which done first rises.
Rely
/-- **The rely, up to the horizon `h`**: from the release `c1`, every entry
before `h` drives `start` and the operands with known values; `start` is 1
only when `Idle`; and the operands of a start are held until the cycle in
which `done` first rises. -/
def Rely (p : P) (stim tr : List SvState) (c1 h : Nat) : Prop :=
  ∀ c, c1 ≤ c → c < h →
    (∃ b, StimBit stim c t.start b) ∧ (∃ x, t.OpsAt p stim c x) ∧
    (StimBit stim c t.start true → t.Idle stim tr c1 c) ∧
    ∀ s x, c1 ≤ s → s ≤ c → StimBit stim s t.start true → t.OpsAt p stim s x →
      (∀ c', s ≤ c' → c' < c → ¬ TraceBit tr c' t.done true) → t.OpsAt p stim c x
svgolf/SvGolf/TaskSeq.lean:487Open in code
TxTask.IdleTaskSeq.leanThe design is idle: every start since the release has already been answered by a cycle with done = 1.
Idle
/-- **C2, `Idle`**: from the release `c1`, every start before cycle `c` has
been followed, before `c`, by a cycle showing `done` = 1. -/
def Idle (stim tr : List SvState) (c1 c : Nat) : Prop :=
  ∀ s, c1 ≤ s → s < c → StimBit stim s t.start true →
    ∃ c', s ≤ c' ∧ c' < c ∧ TraceBit tr c' t.done true
svgolf/SvGolf/TaskSeq.lean:481Open in code
TxTask.GuarTaskSeq.leanThe trusted guarantee, one conjunction; DONE_KNOWN, DONE_LOW_BEFORE_FIRST_START, DONE_WITHIN_LATENCY, DONE_HELD and RESULT_IS_PRODUCT are its parts.
Guar
/-- **The guarantee, up to the horizon `h`** (C3, C4, C5): `done` is known at
every cycle from the release. `done` = 1 claims a result; before the first start
there is none, so `done` is 0 at every cycle from the release up to the first
start (as `out_valid` in `StreamTask.Guar`; decided 2026-11-09). For every start
`s` with operands `x`: `done` rises at a cycle `≤ s + lat` (when that cycle is
before `h`), and from the first cycle it is 1 until the next start it stays 1
with the payload equal to `result x`. -/
def Guar (p : P) (lat : Nat) (stim tr : List SvState) (c1 h : Nat) : Prop :=
  (∀ c, c1 ≤ c → c < h → ∃ b, TraceBit tr c t.done b) ∧
  (∀ c, c1 ≤ c → c < h → (∀ s, c1 ≤ s → s ≤ c → ¬ StimBit stim s t.start true) →
    TraceBit tr c t.done false) ∧
  ∀ s x, c1 ≤ s → s < h → StimBit stim s t.start true → t.OpsAt p stim s x →
    (s + lat < h → ∃ c, s ≤ c ∧ c ≤ s + lat ∧ TraceBit tr c t.done true) ∧
    ∀ c, s ≤ c → c < h → (∃ c', s ≤ c' ∧ c' ≤ c ∧ TraceBit tr c' t.done true) →
      (∀ s', s < s' → s' ≤ c → ¬ StimBit stim s' t.start true) →
      ∃ st, tr[c]? = some st ∧ BitIs st t.done true ∧ HoldAll st (t.payload p) (t.result p x)
svgolf/SvGolf/TaskSeq.lean:498Open in code
ReleasedTaskSeq.leanReleased rst stim c1 h: rst was 1 in the cycle before c1 and is 0 in every cycle from c1 up to h. Claims start at every release, so nothing may survive a reset.
Released
/-- **C1**: `c1` is a release cycle of the synchronous reset `rst` within the
first `h` entries: the entry before `c1` asserts it, every entry in `[c1, h)`
deasserts it. -/
def Released (rst : String) (stim : List SvState) (c1 h : Nat) : Prop :=
  0 < c1 ∧ StimBit stim (c1 - 1) rst true ∧ ∀ c, c1 ≤ c → c < h → StimBit stim c rst false
svgolf/SvGolf/TaskSeq.lean:424Open in code
TraceBitTaskSeq.leanTraceBit tr c n b: in cycle c the design shows the 1-bit signal n as the known bit b.
TraceBit
/-- The snapshot `c` exists and binds `n` to `b`. -/
def TraceBit (tr : List SvState) (c : Nat) (n : String) (b : Bool) : Prop :=
  ∃ st, tr[c]? = some st ∧ BitIs st n b
svgolf/SvGolf/TaskSeq.lean:420Open in code
StimBitTaskSeq.leanStimBit stim c n b: in cycle c the environment drives the 1-bit input n with the known bit b.
StimBit
/-- The stimulus entry `c` exists and binds `n` to `b`. -/
def StimBit (stim : List SvState) (c : Nat) (n : String) (b : Bool) : Prop :=
  ∃ e, stim[c]? = some e ∧ BitIs e n b
svgolf/SvGolf/TaskSeq.lean:416Open in code
ClockedByTaskSeq.leanThe trusted clock discipline that CLOCK_DISCIPLINE restates.
ClockedBy
/-- **The clock discipline** (replaces `Unclocked` for a task with a clock):
`k` is an input port of `d`; every edge-phase process (the processes ls-sv
runs at the clock edge, `Process2.isEdgePhase`) is clocked by `k`; an edge
process with an asynchronous reset uses the reset port `rst`; and no process
reads `k` as data. Under it, "one stimulus entry is one rising edge of `k`"
is the protocol, so an undriven, tied, derived or gated clock cannot occur. -/
def ClockedBy (k : String) (rst : Option String) (d : Design2) : Prop :=
  k ∈ d.inputNames.toList ∧
  ∀ p ∈ d.processes.toList,
    (p.isEdgePhase = true → edgeClock p = some k) ∧
    (∀ r, asyncReset p = some r → rst = some r) ∧
    k ∉ processDataNames p
svgolf/SvGolf/TaskSeq.lean:255Open in code
edgeClockTaskSeq.leanThe clock of a clocked process (always_ff @(posedge c) and the like); none for any other process.
edgeClock
/-- The clock of an edge process (`always_ff @(posedge c)`, `always
@(posedge c)`, `always_ff @(posedge c or negedge rn)`, `always_ff @(posedge c
or posedge r)`); `none` for every other process. -/
def edgeClock : Process2 → Option String
  | .alwaysFF c _ | .alwaysPlain c _ | .alwaysFFR c _ _ _ => some c
  | _ => none
svgolf/SvGolf/TaskSeq.lean:240Open in code
asyncResetTaskSeq.leanThe asynchronous reset of a clocked process (the rn of posedge c or negedge rn), if it has one.
asyncReset
/-- The asynchronous reset of an edge process (the `rn` of `posedge c or
negedge rn`, or the `r` of `posedge c or posedge r`), if it has one. Both
polarities name their reset, so the clock discipline below holds an
active-high reset to the task's reset port too. -/
def asyncReset : Process2 → Option String
  | .alwaysFFR _ r _ _ => some r
  | _ => none
svgolf/SvGolf/TaskSeq.lean:247Open in code
processDataNamesTaskSeq.leanEvery signal a process reads or writes as data: its body, or its assignment. The clock and reset in the event control do not count.
processDataNames
/-- The names a process mentions as DATA: everything in its body (or its
target and value). The clock and reset names in an edge process's event
control are not data. -/
def processDataNames : Process2 → List String
  | .alwaysFF _ b | .alwaysPlain _ b | .alwaysFFR _ _ b _ | .alwaysComb b => stmtNames b
  | .assign t e => lhsNames t ++ exprNames e
  | .unsupported _ _ => []
svgolf/SvGolf/TaskSeq.lean:232Open in code
inputPortsTask.leanThe design's input ports, each with its declared width, in declaration order.
inputPorts
/-- The input ports of `d` with their declared widths, in declaration order.
`instantiate2` lists the ports first, in port-list order. A declaration is
an input port iff its `isInput` flag is set. -/
def inputPorts (d : Design2) : List Sig :=
  d.decls.toList.filterMap fun dc => if dc.isInput then some (dc.name, dc.width) else none
svgolf/SvGolf/Task.lean:178Open in code
outputPortsTask.leanThe design's output ports, each with its declared width, in declaration order.
outputPorts
/-- The output ports of `d` with their declared widths, in declaration order.
A declaration is an output port iff its `isOutput` flag is set. -/
def outputPorts (d : Design2) : List Sig :=
  d.decls.toList.filterMap fun dc => if dc.isOutput then some (dc.name, dc.width) else none
svgolf/SvGolf/Task.lean:184Open in code
HoldAllTask.leanHoldAll st ports values: in the state st, every listed port holds its value as a known bit vector (no x, no z) of exactly the port's width.
HoldAll
/-- `HoldAll st sigs v`: in state `st`, every port `(n, w)` of `sigs` is bound
to the fully known `w`-bit vector that `v` assigns it. -/
def HoldAll (st : SvState) : (sigs : List Sig) → Vals (sigs.map Prod.snd) → Prop
  | [], _ => True
  | (n, _) :: sigs, v => SvState.lookup st n = some (LVec.ofBitVec v.1) ∧ HoldAll st sigs v.2
svgolf/SvGolf/Task.lean:197Open in code
ScheduleOracleSemantics.leanA legal schedule: the order in which the simulator runs the processes that are ready at the same moment. The statement quantifies over all of them.
ScheduleOracle
/-- A legal schedule: at invocation `k`, orders the ready process list.
`choose_perm` is the legality proof — every invocation is a permutation of
the ready list — so `∀ σ : ScheduleOracle` ranges over exactly the legal
schedules. See the module docstring for the invocation-counter protocol. -/
structure ScheduleOracle where
  /-- Invocation counter and ready process indices in, execution order out. -/
  choose : Nat → List Nat → List Nat
  /-- Every invocation yields a permutation of the ready list. -/
  choose_perm : ∀ (k : Nat) (ready : List Nat), (choose k ready).Perm ready
LeanModels/Sv/Semantics.lean:151Open in code
Process2.isEdgePhaseSem2.leanTrue for the processes that run at the clock edge: always_ff, always @(posedge …) and asynchronous-reset blocks.
isEdgePhase
/-- Edge-phase processes: every posedge-clocked block, INCLUDING the
async-reset ones (the posedge fires with reset asserted too — the body's
reset branch is what holds the state, pin3 CYCLE 4). -/
def Process2.isEdgePhase : Process2 → Bool
  | .alwaysFF _ _ | .alwaysPlain _ _ | .alwaysFFR _ _ _ _ => true
  | _ => false
LeanModels/Sv/Sem2.lean:650Open in code
MooreOutDepTaskSeq.leanThe trusted rule 1 of txtask-v2 that MOORE_OUTPUTS restates: a set of signals that holds every input port outside the exempt list (here the list is empty: every input port, rst included), is closed along every combinational dependency and holds no output port.
MooreOutDep
/-- **Rule 1, Moore outputs**: no combinational path leads from an input port outside `exempt`
to an output port. `S` is a set of signals that contains every such input, is closed along the
combinational dependencies (if an assignment depends on a signal in `S`, every signal it writes
is in `S`) and contains no output port. Every v2 statement exempts nothing (`SeqTask`'s from the
start; `TxTask`'s and `StreamTask`'s since 2026-11-09, see `TxTask.SatisfiedAtV2`). -/
def MooreOutDep (d : Design2) (exempt : List String) : Prop :=
  ∃ S : String → Prop,
    (∀ n ∈ d.inputNames.toList, n ∉ exempt → S n) ∧
    (∀ e ∈ combDeps d, (∃ r ∈ e.2, S r) → S e.1) ∧
    ∀ o ∈ d.outputNames.toList, ¬ S o
svgolf/SvGolf/TaskSeq.lean:889Open in code
combDepsTaskSeq.leanThe combinational dependencies of a design, by assignment: for each always_comb or continuous assign, every signal a write targets and every signal its value, its indices or an enclosing condition reads. A clocked process contributes none: its writes end a combinational path at the clock edge.
combDeps
/-- Every combinational dependency of a design, by assignment. -/
def combDeps (d : Design2) : List DepEdge := d.processes.toList.flatMap processDeps
svgolf/SvGolf/TaskSeq.lean:886Open in code
ModelsPUTaskSeq.leanModelsPU d P: from every power-up state, under every schedule, on every known stimulus, every completed run of d satisfies P. It replaces txtask-v1's runs from Lean's own start state, where an unreset register is x: an unreset register is a 0 or 1 nobody knows, so the claims must hold for every value it can have.
ModelsPU
/-- **Rule 2's judgment**: from every power-up state, under every schedule, on every known
stimulus, every completed run satisfies `P` (v1's `⊨₂`, whose runs start at `initState2 d`, with
the start quantified over the power-up states). -/
def ModelsPU (d : Design2) (P : List SvState → List SvState → Prop) : Prop :=
  ∀ st0, PowerUp d st0 → ∀ (σ : ScheduleOracle) (stim tr : List SvState), KnownStim d stim →
    RunsAt d σ st0 stim tr → P stim tr
svgolf/SvGolf/TaskSeq.lean:779Open in code
PowerUpTaskSeq.leanPowerUp d st: st binds every declared signal of d, in declaration order, to a value of its declared width whose every bit is 0 or 1 (2-state declarations included, initializers ignored).
PowerUp
/-- **A power-up state** of `d`: every declaration, in declaration order, bound to a value of its
declared width whose every bit is `0` or `1`. 2-state declarations are included (ls-sv's
`initState2` starts them at `0`, the standard's 2-state initial value; a flip-flop powers up 0 or
1), and declaration initializers play no part (the clocked source gate refuses them). -/
def PowerUp (d : Design2) (st : SvState) : Prop :=
  st.map Prod.fst = d.decls.toList.map Decl.name ∧
    ∀ b ∈ st.zip d.decls.toList, b.1.2.width = b.2.width ∧ b.1.2.allKnown = true
svgolf/SvGolf/TaskSeq.lean:725Open in code
KnownStimTaskSeq.leanKnownStim d stim: every stimulus entry binds each input port it drives to a value of the port's width whose every bit is 0 or 1. An x on an input is a value the environment does not know; each of its resolutions is a known entry.
KnownStim
/-- Every entry of a stimulus is known. -/
def KnownStim (d : Design2) (stim : List SvState) : Prop := ∀ e ∈ stim, KnownEntry d e
svgolf/SvGolf/TaskSeq.lean:755Open in code
KnownEntryTaskSeq.leanKnownEntry d e: every input port the entry e binds holds a known value of its declared width.
KnownEntry
/-- **A known stimulus entry**: every input port it binds holds a value of the port's declared
width whose every bit is `0` or `1`. An `x` on an input is a value the environment does not
know, and each of its resolutions is a known entry, so quantifying over known entries is the
formal reading of an `x` input. An input the entry does not bind keeps its value
(`applyInputs2`). -/
def KnownEntry (d : Design2) (e : SvState) : Prop :=
  ∀ n ∈ d.inputNames.toList,
    ((SvState.lookup e n).all fun v => v.allKnown && sigWidth d n == some v.width) = true
svgolf/SvGolf/TaskSeq.lean:742Open in code
sigWidthTaskSeq.leanThe declared width of a signal (its first declaration's).
sigWidth
/-- The declared width of the signal `n` (its first declaration's; `Design2.declWidth` of ls-sv's
comb layer, restated here so that this file imports no proof layer). -/
def sigWidth (d : Design2) (n : String) : Option Nat :=
  (d.decls.toList.find? fun dc => dc.name == n).map Decl.width
svgolf/SvGolf/TaskSeq.lean:737Open in code
RunsAtTaskSeq.leanRunsAt d σ st0 stim tr: simulating d from the state st0 under the schedule σ on the stimulus stim completes, with the trace tr.
RunsAt
/-- Some fuel completes the run of `d` from `st0` under `σ` on `stim` with the trace `tr` (the
`Runs2` of `run2At`). -/
def RunsAt (d : Design2) (σ : ScheduleOracle) (st0 : SvState) (stim tr : List SvState) : Prop :=
  ∃ fuel, run2At d σ fuel st0 stim = .ok tr
svgolf/SvGolf/TaskSeq.lean:774Open in code
run2AtTaskSeq.leanLean's run of a design (ls-sv's run2: the same clock cycles and checks) started from a given state instead of its own start state.
run2At
/-- **`run2` from the state `st0`** in place of `initState2 d`: the same cycles (`runFrom2`), the
same qualified-case validation (`run2_eq_run2At`: `run2` is `run2At` from `initState2 d`). -/
def run2At (d : Design2) (σ : ScheduleOracle) (fuel : Nat) (st0 : SvState)
    (stim : List SvState) : Res (List SvState) := do
  let tr ← runFrom2 d σ fuel st0 0 stim
  if d.processes.toList.any Process2.hasQualifiedCase then
    validateTraceChecks2 fuel d tr
  return tr
svgolf/SvGolf/TaskSeq.lean:761Open in code
TerminatesPUTaskSeq.leanThe trusted termination conjunct of txtask-v2 that TERMINATES restates: from every power-up state, under every schedule, every known stimulus completes.
TerminatesPU
/-- **Non-vacuity of `ModelsPU`**: from every power-up state, under every schedule, every known
stimulus completes (v1's `Terminates2` from the power-up states: a design that settles from the
x start but oscillates from a concrete one fails it). -/
def TerminatesPU (d : Design2) : Prop :=
  ∀ st0, PowerUp d st0 → ∀ (σ : ScheduleOracle) (stim : List SvState), KnownStim d stim →
    ∃ tr, RunsAt d σ st0 stim tr
svgolf/SvGolf/TaskSeq.lean:786Open in code
XSafeTaskSeq.leanThe trusted rule 3 of txtask-v2 that NO_X_CREATING restates: every process passes the structural check xsafeB.
XSafe
/-- **Rule 3**: no construct of `d` can create an `x` or a `z` from known operands. -/
def XSafe (d : Design2) : Prop := xsafeB d = true
svgolf/SvGolf/TaskSeq.lean:1085Open in code
xsafeBTaskSeq.leanThe structural check of rule 3, a Boolean function of the design's text and declared widths: every expression of every process has a rule-3 width (xsWidth), and every case pattern is an admitted expression or a casez/casex literal.
xsafeB
/-- **Rule 3, decided**: no process of `d` has a construct that can create an `x` from known
operands. -/
def xsafeB (d : Design2) : Bool := d.processes.toList.all (xsProc d)
svgolf/SvGolf/TaskSeq.lean:1081Open in code
xsWidthTaskSeq.leanThe width of an expression's value when no construct in it can create an x from known operands, and none otherwise: literals without x/z digits, declared signals, slices in range, run-time indices whose every value is in range, equal widths for bitwise and equality operators and for the two arms of ?:, and the operator rules of binW.
xsWidth
/-- **Rule 3 for an expression**: `some w` when no construct in `e` can create an `x` from known
operands, `w` being the width of its value on a state that binds every signal at its declared
width; `none` otherwise. -/
def xsWidth (d : Design2) : Expr2 → Option Nat
  | .lit v => if v.allKnown then some v.width else none
  | .ident n => sigWidth d n
  | .unary .lnot a => (xsWidth d a).map fun _ => 1
  | .unary _ a => xsWidth d a
  | .resizeSigned w a => (xsWidth d a).map fun _ => w
  | .squash2 a => xsWidth d a
  | .binary op l r => binW op l r (xsWidth d l) (xsWidth d r)
  | .scmp op l r => if scmpOp op then (do let _ ← xsWidth d l; let _ ← xsWidth d r; pure 1) else none
  | .logical _ l r => do let _ ← xsWidth d l; let _ ← xsWidth d r; pure 1
  | .ternary c t f => do
      let _ ← xsWidth d c; let a ← xsWidth d t; let b ← xsWidth d f; if a = b then pure a else none
  | .concat parts => xsWidthList d parts.toList
  | .slice b lo w => do let a ← xsWidth d b; if lo + w ≤ a then pure w else none
  | .index b i ew => do
      let a ← xsWidth d b; let k ← xsWidth d i
      if unsignedIdx d i = true ∧ 2 ^ k * ew ≤ a then pure ew else none
  | .repl n a => (xsWidth d a).map (· * n)
  | .reduce _ a => (xsWidth d a).map fun _ => 1
  | .resize w a => (xsWidth d a).map fun _ => w
  | .unsupported _ _ => none
termination_by structural e => e
svgolf/SvGolf/TaskSeq.lean:987Open in code
binWTaskSeq.leanRule 3 at a binary operator: / and % only by a nonzero constant, ** with a signed exponent only on a nonzero constant base, &, |, ^, ==, !=, ==?, !=? only on equal widths; every other operator is known on known operands.
binW
/-- Rule 3 at a binary operator, from its operands `l`, `r` and their rule-3 widths `wl`, `wr`:
the width of the result, or `none` if the operator can create an `x` from known operands. -/
def binW (op : BinOp) (l r : Expr2) (wl wr : Option Nat) : Option Nat :=
  match op with
  | .add | .sub | .mul => do let a ← wl; let b ← wr; pure (max a b)
  | .div | .sdiv | .rem | .srem => do
      let a ← wl; let b ← wr; if constNZ r then pure (max a b) else none
  | .pow _ se => do let a ← wl; let _ ← wr; if !se || constNZ l then pure a else none
  | .shl _ | .shr _ | .ashl _ | .ashr _ => do let a ← wl; let _ ← wr; pure a
  | .and | .or | .xor => do let a ← wl; let b ← wr; if a = b then pure a else none
  | .eq | .ne => do let a ← wl; let b ← wr; if a = b then pure 1 else none
  | .wildEq | .wildNe => do let a ← wl; let b ← wr; if a = b then pure 1 else none
  | .caseEq | .caseNe | .casez | .casex => do let _ ← wl; let _ ← wr; pure 1
  | .land | .lor | .lt | .le | .gt | .ge | .slt | .sle | .sgt | .sge => do
      let _ ← wl; let _ ← wr; pure 1
svgolf/SvGolf/TaskSeq.lean:957Open in code

What does not count

Designs that try to score without meeting the statement (negatives), or that exploit a place where the proof's reading and the scored netlist could differ (attacks). The checker stops at the first stage that refuses; each design is listed with that stage.

Refused before any proof is tried

The checker's static stages read the text itself and refuse it: an operator the task bans, a construct that two tools read differently, an unknown (x or z) value that could arise, or a program the language forbids.

  • async_reset.sv (attack, stopped at source): The control process has an asynchronous reset: the reset is synchronous on this task, the statement refuses an asynchronous one, and the source check refuses the second event first.

    the design, with its comments left out 
    module matmul #(parameter int N = 4, parameter int W = 8, parameter int AccW = 32) (
  input  logic                 clk, rst,
  input  logic                 start,
  input  logic [N*N*W-1:0]     A, B,
  output logic                 done,
  output logic [N*N*AccW-1:0]  C
);
  logic [31:0]      k;
  logic             busy;
  logic [N*N*W-1:0] a_sh, b_sh;

  always_ff @(posedge clk or posedge rst)
    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'd1;
      a_sh <= a_sh >> W;
      b_sh <= b_sh >> (N*W);
      if (k == N - 1) 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]};
    end
  end
endmodule
Rejected at the proof

These pass every static check. The proof that comes with each one does not compile, or does not prove the statement: a design that is wrong somewhere in the task's range (or has other ports) has no proof at all, and a proof that leaves a goal unproved is never accepted.

  • acc_2w.sv (attack, stopped at solution): The accumulator is only 2W bits wide and sign-extended to AccW bits: wrong when AccW > 2W and a dot product leaves the 2W-bit range.

    the design, with its comments left out 
    module matmul #(parameter int N = 4, parameter int W = 8, parameter int AccW = 32) (
  input  logic                 clk, rst,
  input  logic                 start,
  input  logic [N*N*W-1:0]     A, B,
  output logic                 done,
  output logic [N*N*AccW-1:0]  C
);
  logic [31:0]      k;
  logic             busy;
  logic [N*N*W-1:0] a_sh, b_sh;
  logic [N*N*2*W-1:0] acc;

  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'd1;
      a_sh <= a_sh >> W;
      b_sh <= b_sh >> (N*W);
      if (k == N - 1) 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)
          acc[(i*N+j)*2*W +: 2*W] <= '0;
        else if (busy)
          acc[(i*N+j)*2*W +: 2*W] <= acc[(i*N+j)*2*W +: 2*W]
              + {{2*W{a_sh[i*N*W + W - 1]}}, a_sh[i*N*W +: W]}
              * {{2*W{b_sh[j*W + W - 1]}}, b_sh[j*W +: W]};
      assign C[(i*N+j)*AccW +: AccW] = {{AccW{acc[(i*N+j)*2*W + 2*W - 1]}}, acc[(i*N+j)*2*W +: 2*W]};
    end
  end
endmodule

  • done_early.sv (attack, stopped at solution): done rises one step early (k == N - 2), while C still lacks the last product.

    the design, with its comments left out 
    module matmul #(parameter int N = 4, parameter int W = 8, parameter int AccW = 32) (
  input  logic                 clk, rst,
  input  logic                 start,
  input  logic [N*N*W-1:0]     A, B,
  output logic                 done,
  output logic [N*N*AccW-1:0]  C
);
  logic [31:0]      k;
  logic             busy;
  logic [N*N*W-1:0] a_sh, b_sh;

  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'd1;
      a_sh <= a_sh >> W;
      b_sh <= b_sh >> (N*W);
      if (k == N - 2)
        done <= 1'b1;
      if (k == N - 1)
        busy <= 1'b0;
    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]};
    end
  end
endmodule

  • missing_sign_ext.sv (attack, stopped at solution): Each W × W product is sign-extended to 2W bits only, then zero-extended into the accumulator: wrong for a negative product when AccW > 2W.

    the design, with its comments left out 
    module matmul #(parameter int N = 4, parameter int W = 8, parameter int AccW = 32) (
  input  logic                 clk, rst,
  input  logic                 start,
  input  logic [N*N*W-1:0]     A, B,
  output logic                 done,
  output logic [N*N*AccW-1:0]  C
);
  logic [31:0]      k;
  logic             busy;
  logic [N*N*W-1:0] a_sh, b_sh;
  logic [N*N*2*W-1:0] p;

  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'd1;
      a_sh <= a_sh >> W;
      b_sh <= b_sh >> (N*W);
      if (k == N - 1) 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
      assign p[(i*N+j)*2*W +: 2*W] = {{W{a_sh[i*N*W + W - 1]}}, a_sh[i*N*W +: W]}
                                   * {{W{b_sh[j*W + W - 1]}}, b_sh[j*W +: W]};
      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] + p[(i*N+j)*2*W +: 2*W];
    end
  end
endmodule

  • no_clear_on_start.sv (attack, stopped at solution): The accumulators are cleared by the reset but not by start, so every transaction after the first adds onto the previous result.

    the design, with its comments left out 
    module matmul #(parameter int N = 4, parameter int W = 8, parameter int AccW = 32) (
  input  logic                 clk, rst,
  input  logic                 start,
  input  logic [N*N*W-1:0]     A, B,
  output logic                 done,
  output logic [N*N*AccW-1:0]  C
);
  logic [31:0]      k;
  logic             busy;
  logic [N*N*W-1:0] a_sh, b_sh;

  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'd1;
      a_sh <= a_sh >> W;
      b_sh <= b_sh >> (N*W);
      if (k == N - 1) 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 (rst)
          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]};
    end
  end
endmodule

  • off_by_one_k.sv (attack, stopped at solution): The step counter starts at 1, so the last product never reaches C and done rises a cycle early.

    the design, with its comments left out 
    module matmul #(parameter int N = 4, parameter int W = 8, parameter int AccW = 32) (
  input  logic                 clk, rst,
  input  logic                 start,
  input  logic [N*N*W-1:0]     A, B,
  output logic                 done,
  output logic [N*N*AccW-1:0]  C
);
  logic [31:0]      k;
  logic             busy;
  logic [N*N*W-1:0] a_sh, b_sh;

  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'd1;
      a_sh <= A;
      b_sh <= B;
    end else if (busy) begin
      k    <= k + 32'd1;
      a_sh <= a_sh >> W;
      b_sh <= b_sh >> (N*W);
      if (k == N - 1) 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]};
    end
  end
endmodule

  • unsigned_product.sv (attack, stopped at solution): The entries are multiplied as unsigned numbers (zero-extended part-selects): wrong for a negative entry when AccW > W ≥ 2.

    the design, with its comments left out 
    module matmul #(parameter int N = 4, parameter int W = 8, parameter int AccW = 32) (
  input  logic                 clk, rst,
  input  logic                 start,
  input  logic [N*N*W-1:0]     A, B,
  output logic                 done,
  output logic [N*N*AccW-1:0]  C
);
  logic [31:0]      k;
  logic             busy;
  logic [N*N*W-1:0] a_sh, b_sh;

  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'd1;
      a_sh <= a_sh >> W;
      b_sh <= b_sh >> (N*W);
      if (k == N - 1) 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]
              + a_sh[i*N*W +: W] * b_sh[j*W +: W];
    end
  end
endmodule
Spec.lean, verbatim (114 lines) 
import SvGolf.TaskSeq

/-!
# Task `matmul`: N×N signed matrix multiplication, wrapping at the accumulator width
# (TRUSTED text, final, decided 2026-11-08, amended 2026-11-09; written 2026-11-04; contract C6 of `design/sequential/CONTRACT.md`)

Module (port order as written; `N`, `W`, `AccW` are the module's parameters, in this order):

```systemverilog
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
);
```

**Layout.** Flat, row-major, least significant entry first: entry `(i, k)` of `A` is
`A[(i*N+k)*W +: W]`, likewise `B`; entry `(i, j)` of `C` is `C[(i*N+j)*AccW +: AccW]`.

**Arithmetic (ruled 11/03).** The entries of `A` and `B` are SIGNED (two's complement,
`W` bits), products sign-extended; `C[i][j] = Σ_k A[i][k]·B[k][j]`, computed exactly in the
integers and then reduced mod `2^AccW` (wrap, as GPUs accumulate; order-independent, so every
summation order is legal). `C`'s entries are two's complement `AccW`-bit values.

**Protocol** (`TxTask`, `SvGolf/TaskSeq.lean`; C1 to C5): synchronous active-high reset `rst`;
claims from the cycle after its release; `start` a one-cycle pulse raised only when the design is
idle; `A` and `B` held from `start` until `done` rises; `done` rises within the declared latency
`lat` (cycles after the edge that samples `start`), then stays 1 with `C` = the product until the
next `start`. `done` is known in every cycle after the release, and 0 up to the first start
(`done` = 1 claims a result, and there is none before a start); `C` only where `done` = 1.

The declared latency `lat` is the submission's; the checker pins its value at the scoring point
`(4, 8, 32)` and the score uses it (C3, C7). Run-time `/ % **` are banned, as in every task (`task.json`).

**Range.** `N, W, AccW ≥ 1`, and the port widths `N·N·W` and `N·N·AccW` below `2^31`: the parameters
are `int`, and every width and index expression of the interface (`N*N*W-1`, `(i*N+k)*W`) must stay in
the 32-bit range, where a real elaboration and ls-sv's unbounded constant tier agree
(`PDesign.int32Agrees`; Task v2 decision 1, the `clmul` precedent).

**txtask-v2 (2026-11-05; final, decided 2026-11-08, amended 2026-11-09).** `Statement` is the v2
statement `TxTask.StatementV2`: txtask-v1's interface, clock discipline and latency bound; its claims
and termination from EVERY power-up state on every known stimulus (rule 2: an unreset register is an
unknown 0/1 value, not ls-sv's `x` start); Moore outputs (`MooreOutDep`, rule 1, nothing exempt: no
combinational path from `rst`, `start`, `A` or `B` to `done` or `C`); and no construct that creates an `x`
from known operands (`XSafe`, rule 3). `SvGolf/TaskSeq.lean`, last section, and
`design/soundness/TXTASK-V2-REVIEW.md`.
-/

namespace SvGolf.Tasks.Matmul

open SvGolf

/-- The parameters `(N, W, AccW)`. -/
abbrev Params := Nat × Nat × Nat

/-- Entry `idx` of a flat vector of `W`-bit signed entries, as an integer. -/
def entry (W : Nat) {n : Nat} (x : BitVec n) (idx : Nat) : Int :=
  (x.extractLsb' (idx * W) W).toInt

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

/-- The product `C = A·B`, each entry reduced mod `2^AccW`, packed flat row-major. -/
def product (N W AccW : Nat) {n : Nat} (a b : BitVec n) : BitVec (N * N * AccW) :=
  BitVec.ofNat (N * N * AccW)
    ((List.range (N * N)).foldl
      (fun acc ij =>
        acc + (BitVec.ofInt AccW (dot N W a b (ij / N) (ij % N))).toNat * 2 ^ (ij * AccW))
      0)

/-- **The task** (C6). -/
def task : TxTask Params where
  inRange p := 1 ≤ p.1 ∧ 1 ≤ p.2.1 ∧ 1 ≤ p.2.2 ∧
    p.1 * p.1 * p.2.1 < 2 ^ 31 ∧ p.1 * p.1 * p.2.2 < 2 ^ 31
  clk := "clk"
  rst := "rst"
  start := "start"
  operands p := [("A", p.1 * p.1 * p.2.1), ("B", p.1 * p.1 * p.2.1)]
  done := "done"
  payload p := [("C", p.1 * p.1 * p.2.2)]
  result p := fun (a, b, ()) => (product p.1 p.2.1 p.2.2 a b, ())

/-- **The challenge statement**, for the three-parameter design family `sem N W AccW` and the
latency function `lat N W AccW`. The checker's goal is `Statement design.sem lat ∧ lat 4 8 32 = n`
with the latency `lat` the proof file defines and the declared number `n` (C3). -/
abbrev Statement (sem : Nat → Nat → Nat → LeanModels.Sv.Design2) (lat : Nat → Nat → Nat → Nat) :
    Prop :=
  task.StatementV2 (fun p => sem p.1 p.2.1 p.2.2) (fun p => lat p.1 p.2.1 p.2.2)

/-! ## Sanity checks on the statement's data (proved; they add nothing to the trusted base) -/

/-- A 2×2 product with a negative entry: `A = [[-1, 2], [3, 4]]`, `B = [[5, 6], [7, 0]]` (W = 4)
gives `C = [[9, -6], [43, 18]]` (AccW = 8; `-6` is `0xFA`). -/
example : product 2 4 8 (0x432F#16) (0x0765#16) = 0x122BFA09#32 := by decide

/-- Wrap: `[[-8]]·[[-8]] = 64`, which is `0x40` in 8 bits and `0` in 6 bits (W = 4). -/
example : product 1 4 8 (0x8#4) (0x8#4) = 0x40#8 ∧ product 1 4 6 (0x8#4) (0x8#4) = 0#6 := by
  decide

/-- The off-points the extractor probes and the scoring point are in range (C6). -/
example : task.inRange (1, 1, 1) ∧ task.inRange (2, 3, 5) ∧ task.inRange (3, 4, 8) ∧
    task.inRange (4, 8, 32) := by
  simp [task]

/-- The port names are distinct. -/
example (p : Params) :
    (["clk", "rst", "start"] ++ (task.operands p).map Prod.fst).Nodup ∧
      task.done ∉ (task.payload p).map Prod.fst := by
  simp [task]

end SvGolf.Tasks.Matmul

Its trusted text

The modules specific to this task. Like every task, it also rests on the shared trusted base (the ls-sv semantics of SystemVerilog and svGolf's statement helpers), and a proof may import any module of the ls-sv library. Nothing else is trusted: proof helpers are kernel-checked like any submission.

modulerolelinessha256
tasks.matmul.Specsvgolf/tasks/matmul/Spec.leantask statement1142e8ec32ea060

How to participate #

  1. Write a circuit with the task's exact interface.
  2. Prove in Lean 4 that it meets the trusted statement; Start a new design, below, gives the route, and the proving guide shows how.
  3. Check and record it (how to submit): the checker accepts the pair or says which stage refused it, as it does for each design under what does not count.
  4. Beat par: an accepted design whose score (area × time) is below that of the best proved reference. The leaderboard ranks by it.

How to submit

You hand in two files: solution.sv, a module with the exact header under Interface, and Solution.lean, a Lean 4 proof that it meets the trusted statement, at the latency you declare.

Step 0, once per machine. Install:

  • elan, which installs the Lean toolchain that lean-toolchain pins (leanprover/lean4:v4.33.0-rc1) on first use;
  • Yosys 0.53 with its yosys-abc (every pinned tool and file: Reproduce a score);
  • Verilator 5, a C++ compiler and make, for the post-synthesis check (it compiles Verilator's model of the netlist);
  • Python 3.12 with python3.12 -m pip install -r requirements.txt (pyslang==11.0.0, the extractor's SystemVerilog frontend).
step 0
git clone https://github.com/thomasnormal/svgolf
cd svgolf
python3.12 -m pip install -r requirements.txt
# the trusted Lean and the checker's evaluator
lake build
# the pinned sky130 liberty, checked by its hash
python3.12 score/ppa.py --fetch-liberty

lake build takes about 6 minutes and 1 GB of disk the first time, on a laptop that already had the Lean toolchain (README.md's Step 0 says what was measured where; elan's first download of the toolchain comes on top): Lake clones proglib (formerly lean-surfaces) and its packages from github.com, so it needs network access there, and builds the LeanModels.Sv modules svGolf uses; Mathlib is cloned, never built.

Start from the reference pair under Files, matmul_g1, a complete and accepted one: copy it, from the same directory:

shell
cp tasks/matmul/reference/matmul_g1.sv solution.sv
cp tasks/matmul/reference/matmul_g1.lean Solution.lean

Then, for each design, from the same directory: find it without Lean and check it once without a proof, at the latency you mean to claim (the golfing loop and step 1), write its proof (Start a new design, below, gives the route), then check the pair and record it (steps 2 and 3):

shell
# the golfing loop, no Lean: area and period
python3.12 score/ppa.py solution.sv --task tasks/matmul \
    --seq --path
# 1. no proof needed; never accepts; exits 0 when every
#    stage passed, ending with area x time and par;
#    --latency: the cycles you mean to claim (4: par's)
python3.12 check.py tasks/matmul solution.sv --unproved \
    --latency 4 --stage-dir stage
# 2. the real check: prints "accepted": true; its
#    post-synthesis check is LIGHT by default (a subset of
#    the vectors, for local feedback), so stderr also says
#    "accepted, but the check was INCOMPLETE ... rerun with
#    --postsynth full": expected, since step 3 runs the
#    full one itself
python3.12 check.py tasks/matmul solution.sv Solution.lean
# 3. record it: the whole check again, full and sandboxed
python3.12 leaderboard/leaderboard.py add --task matmul \
    --player YOUR_HANDLE --assisted-by "TOOL OR MODEL" \
    --sv solution.sv --lean Solution.lean \
    --notes "YOUR DESIGN IN ONE LINE"

Done: step 3 prints added matmul/HASH: YOUR_HANDLE, … once the pair has passed the whole check, full and sandboxed, and its record is written (what it writes, and where: below); otherwise it prints REFUSED with the reasons and records nothing. Step 2's "accepted": true, with its INCOMPLETE line, is feedback for you, not a record.

The golfing loop and step 1, the first two commands above. The first command weighs the design through the clocked flow (--seq): the area and the register-to-register period, with the critical path (--path). The second runs every stage that needs no proof: the clocked source rules, the check that no construct can create an x (clocked_rules), the never-loaded register check, the score, and the clocked post-synthesis check, which drives the scored netlist through oracle.py's transactions from random power-up states and holds every C to the oracle's product and every done to the latency. A wrong design is named there, with the transaction, before any proof. It leaves the design staged in stage/ for probe files (PROVING.md, section 0). Rule 1 (Moore outputs) has no early check in this kind: the proof is what refuses a combinational path from an input to an output.

score/ppa.py is the inner loop of golfing; its ranked numbers are area_um2_sky130 and delay_ps_sky130 in what it prints. It runs only the source gate and the pinned flow: it does not check the banlist, the 4-state rules, whether ls-sv can read the design, the post-synthesis simulation or the task's function. Step 1 does, still without a proof.

The Lean file. The checker extracts your .sv itself and writes the trusted module Submission.Design; Goal lat unfolds to SvGolf.Tasks.Matmul.Statement Submission.design.sem lat ∧ lat 4 8 32 = n: the task's statement of your design at your latency lat (cycles, a function of the parameters), and its value at the scoring point (N = 4, W = 8, AccW = 32), the n of your header line -- svgolf-latency: n, which the score takes as the cycles (the checker reads the latency from this file, never from the .sv):

Submission.Design (generated: you never write it)
import LeanModels.Sv.Ingest2
import tasks.matmul.Spec

namespace Submission
load_design_sv2 design from "<the envelope of your .sv>"
abbrev Goal (lat : …) : Prop :=
  SvGolf.Tasks.Matmul.Statement design.sem lat ∧ lat <scoring point> = <your latency>
end Submission

Your Solution.lean imports it and proves Goal lat, as the skeleton in Start a new design (The proof in detail) shows. File names and paths are free (here solution.sv and Solution.lean); the module name Submission, the import Submission.Design header, the definition lat (one Nat per parameter, in the task's order), the theorem solution : Goal lat (in namespace Submission, theorem Submission.solution : Submission.Goal Submission.lat) and exactly one line -- svgolf-latency: n (n a decimal number of cycles, at least 1) are fixed.

Step 3 writes your record's three files (.json, .sv and .lean, named by the record's hash) to leaderboard/data/matmul/, the directory a pull request adds. Then open a pull request against https://github.com/thomasnormal/svgolf that adds them; CI re-verifies it. There is no submission server: nothing is sent anywhere by these commands. For a private trial, add --data-dir DIR: the record then goes to DIR and the board stays as it is. Repeat --assisted-by for each tool or AI system that helped, or leave it out.

YOUR_HANDLE is your public name: the board and the record's page show it. It is 1 to 32 characters, letters, digits, ., _ or -, the first a letter or a digit ([A-Za-z0-9][A-Za-z0-9._-]{0,31}). --notes is optional: one line on the design (at most 2000 characters), shown on the record's page. In a private trial (--data-dir DIR), add --from-check RESULT.json records the JSON that a check.py … --postsynth full --ppa require run printed instead of checking again; the board's own leaderboard/data/ refuses a stored result.

the sandbox, and machines without one

leaderboard.py add runs the check with --sandbox require: the proof's Lean, the extractor, Yosys and Verilator must run inside the operating system's sandbox (Seatbelt on macOS, bubblewrap on Linux). Where that sandbox is missing or fails its self-test, the check stops with an infrastructure error and nothing is recorded. On such a machine, --sandbox auto runs the check without it (and says so on stderr), and --sandbox off skips it: your proof file then runs with your own privileges, and the record is for your own use, since an official record is made with the sandbox or not at all. add also weighs the ranked sky130 numbers, which need the pinned liberty (Step 0). On a shared machine whose Lean calls go through a wrapper, set SVGOLF_LEAN_WRAP; check.py and leaderboard.py both read it, and SVGOLF_LEAN_WRAP_ONCE=1 takes the wrapper once for a whole run.

What moves the score

What players have seen move the ranked sky130 numbers: observations, not promises (the pinned flow is the judge, and score/ppa.py measures a variant in seconds).

  • Registering each product (a register between every unit's multiplier and its adder, one more cycle of latency) about halved the clock period at about the same area: area × time about a third under par.
  • The golfing loop's --path names the critical path with each net's arrival time: read it before you guess.

Leaderboard

by score · ASAP7
  1. 1
    fanout-ferret
    2026-11-10
    2 276 474241 921 µm² × 1 × 9.41 ns
  2. 2
    vacuity-check
    2026-11-10
    2 377 06385 261 µm² × 5 × 5.58 ns
  3. 3
    fanout-ferret
    2026-11-10
    2 511 471137 104 µm² × 2 × 9.16 ns
  4. 4
    vacuity-check
    2026-11-10
    3 407 66179 700 µm² × 4 × 10.7 ns
  5. ⚑
    matmul_g1
    par proved reference
    3 729 63687 174 µm² × 4 × 10.7 ns
every column: area, time, proof lines, assisted by, files
#playerdatescore (µm²·ns)area (µm²)time (ps)area (GE)depthproof linesassisted byrecordfiles
1fanout-ferret2026-11-102 276 474241920.8941057547.77273855Claude Sonnet 5.51ffe71156e90.sv .lean
2vacuity-check2026-11-102 377 06385260.52788020686.19751786Claude Sonnet 5.5263ce18b31ab.sv .lean
3fanout-ferret2026-11-102 511 471137104.01831832652.08172805Claude Sonnet 5.5abdd0afdf025.sv .lean
4vacuity-check2026-11-103 407 66179700.24275619022.82859722Claude Sonnet 5.59fdf50f9ae02.sv .lean
  1. 1
    fanout-ferret
    2026-11-10
    59353661.548 µm² × 1 × 1.62 ns
  2. 2
    vacuity-check
    2026-11-10
    64531315.583 µm² × 5 × 0.981 ns
  3. 3
    fanout-ferret
    2026-11-10
    65202085.873 µm² × 2 × 1.56 ns
  4. 4
    vacuity-check
    2026-11-10
    72911216.745 µm² × 4 × 1.50 ns
  5. ⚑
    matmul_g1
    par proved reference
    82171334.726 µm² × 4 × 1.54 ns
every column: area, time, proof lines, assisted by, files
#playerdatescore (µm²·ns)area (µm²)time (ps)area (GE)depthproof linesassisted byrecordfiles
1fanout-ferret2026-11-1059353661.548162157547.77273855Claude Sonnet 5.51ffe71156e90.sv .lean
2vacuity-check2026-11-1064531315.583490520686.19751786Claude Sonnet 5.5263ce18b31ab.sv .lean
3fanout-ferret2026-11-1065202085.873312632652.08172805Claude Sonnet 5.5abdd0afdf025.sv .lean
4vacuity-check2026-11-1072911216.745599219022.82859722Claude Sonnet 5.59fdf50f9ae02.sv .lean
score: area × time, µm²·nspar

At a glance

top module
matmul
parameters
N in range 1 <= N, N*N*W < 2^31, N*N*AccW < 2^31, W in range 1 <= W, N*N*W < 2^31, AccW in range 1 <= AccW, N*N*AccW < 2^31
scoring point
N = 4, W = 8, AccW = 32
depth budget
none
banned run-time operators
/ % **

No task-specific ban, * included: the task is the schedule (how many multipliers, how many cycles, how short a cycle), and the score prices it. Run-time / % ** are banned here as in every task: a zero divisor or a negative exponent makes an unknown value from known operands.

allowed axioms
propext, Classical.choice, Quot.sound
proof time limit
300 s of CPU time (a wall-clock backstop of 1500 s stops a proof that waits)

Start a new design

The route: a phase model, TxTask.satisfiedAtV2_of_phases (PROVING.md, section 19; reference/matmul_g1.lean is a complete proof). The reduction in SvGolf/SeqV2.lean turns the statement at one point into facts about ONE clock cycle:

  1. Interface: the ports in order and distinct declaration names (rfl, and decide on the names);
  2. Disciplined: ClockedBy clk none (no asynchronous reset), a simp over the processes;
  3. TerminatesPU, by TerminatesPU.of_invariant from the clock step;
  4. 1 ≤ lat;
  5. a TxTask.PhaseModel: the clock step in closed form (its CycleModel: a Shape and the one-cycle Step), the phases Ready (after a reset, before the first start, done = 0), Busy x m (working on the operands x, done within m + 1 more cycles) and Fin x (done = 1, C the product), and the one-cycle obligations reset, start, busy, hold_ready and hold_fin;
  6. the shape at every power-up state (powerUp_cons once per declaration);
  7. rule 1, MooreOutDep: for a design whose every process is an always_ff, MooreOutDep.of_noComb with combDeps_of_ffOnly;
  8. rule 3, XSafe: a simp over xsafeB and its helpers (xsProc, xsStmt, xsWidth, ...).

reference/matmul_g1.lean, named above, is 653 code lines long.

The proof in detailLay the design out so the proof stays short · The skeleton · Library lemmas that exist today

Lay the design out so the proof stays short:

  • register every output: with only always_ff processes, rule 1 is one line (combDeps_of_ffOnly);
  • keep every process an always_ff whose body writes with nonblocking assignments only: the library's clock step in closed form (cycleStep2_ffOnly; the reference uses it through cycleStep2_profile) is for such designs only. A continuous assign or an always_comb block anywhere, an output driven by one included, means proving the combinational settle yourself, as the arbiter's proof does (PROVING.md, section 20);
  • reset every register whose value matters (busy, done, the step counter): the claims hold from every power-up value, the first reset edge included (a design whose done timing within the latency depends on an unreset register can still be correct: the post-synthesis check holds each power-up's run to the claims); the operand and accumulator registers may stay unreset when start loads them, as in the reference;
  • nest generate loops: the loader gives each generate loop a fixed budget of (N + W + AccW + 2)² + 64 iterations at a point (the sum of the parameter values plus 2, squared, plus 64), and a nested loop gets the whole budget again. A loop over N or N² iterations always fits, and so does one loop per index, nested as in the reference. One flat loop over the bits of a port (N·N·W or N·N·AccW lanes) or over (i, j, k) triples (N³) exceeds the budget at points in the range (at (30, 10, 1): 9000 lanes against 1913), and there the loader gives up: the design reads as an empty one, so the statement is unprovable, however correct the circuit is;
  • for XSafe, operands of one width (sign-extend explicitly, as the reference does) and run-time indices whose every value is in range; shifting the operand registers keeps every select static;
  • no $signed(...) widened into a wider sum: ls-sv refuses its width conversion (ConversionExpression:width, at the design stage), although score/ppa.py weighs the design. Sign-extend a W-bit entry x by hand, as the reference does: {{AccW{x[W-1]}}, x}.

The skeleton (reference/matmul_g1.lean is it, filled in for the reference):

-- svgolf-latency: 4
import Submission.Design
import SvGolf.SeqV2

namespace Submission
open LeanModels.Sv SvGolf

def lat (N _W _AccW : Nat) : Nat := N   -- yours: your design's latency

-- 1. agreement: `design.sem N W AccW = myD N W AccW`, a hand-built Design2
-- 2. one cycle in closed form; 3. the invariant; 4. the phase model `model N W AccW`

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 (my_interface N W AccW hN hW hA)
    (my_disciplined N W AccW hN hW hA) (my_terminatesPU N W AccW hN hW hA) hN
    (model N W AccW hN hW hA hNW) (my_powerUp N W AccW hN hW hA) (my_moore N W AccW hN hW hA)
    (my_xsafe N W AccW hN hW hA)

end Submission

#print axioms solution must show propext, Classical.choice and Quot.sound only.

Library lemmas that exist today:

  • SvGolf.SeqV2: TxTask.satisfiedAtV2_of_phases (the reduction), MooreOutDep.of_noComb, combDeps_of_ffOnly, MooreOutDep.of_check (rule 1 by evaluation, for a design with combinational logic), TerminatesPU.of_invariant, powerUp_cons, powerUp_nil;
  • SvGolf.Seq: TxTask.PhaseModel and the v1 reduction it feeds (TxTask.guar_of_phases);
  • LeanModels.Sv.SeqProfile, LeanModels.Sv.SeqFamily, LeanModels.Sv.NbaCommit: G0's clock step for a flip-flop-only design and the packed-family commit lemmas; LeanModels.Sv.Lib.BitVecArith and LeanModels.Sv.CombViewArith for the sign extensions and the wrapped sums.

Compare the designs

ASAP7 · any two numbers · lower is better

N = 4, W = 8, AccW = 32, the scored point: the ranked numbers. The same designs are also measured at N = 2, W = 8, AccW = 32: measured, not ranked, the same proved designs through the same pinned flow at other parameters (the tables below, and how the designs scale).

matmul: area against time5 designs by Time (ps) (x) and Area (µm²) (y); lower is better on both. The table under the chart lists the same numbers.100k150k200k250k10k20k30k40kTime (ps)Area (µm²) · lower is betterthe Pareto front of the proved designsmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 3 729 636 µm²·ns · Time: 42 784 ps · Area: 87 173.6 µm²vacuity-check · submission · 2026-11-10 · Score: 3 407 661 µm²·ns · Time: 42 756 ps · Area: 79 700.2 µm²vacuity-check · submission · 2026-11-10 · Score: 2 377 063 µm²·ns · Time: 27 880 ps · Area: 85 260.5 µm²fanout-ferret · submission · 2026-11-10 · Score: 2 511 471 µm²·ns · Time: 18 318 ps · Area: 137 104.0 µm²fanout-ferret · submission · 2026-11-10 · Score: 2 276 474 µm²·ns · Time: 9410 ps · Area: 241 920.8 µm²
matmul: area against time5 designs by Time (ps) (x) and Area (µm²) (y); lower is better on both. The table under the chart lists the same numbers.100k150k200k250k10k20k30k40kTime (ps)Area (µm²) · lower is betterthe Pareto front of the proved designsmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 3 729 636 µm²·ns · Time: 42 784 ps · Area: 87 173.6 µm²vacuity-check · submission · 2026-11-10 · Score: 3 407 661 µm²·ns · Time: 42 756 ps · Area: 79 700.2 µm²vacuity-check · submission · 2026-11-10 · Score: 2 377 063 µm²·ns · Time: 27 880 ps · Area: 85 260.5 µm²fanout-ferret · submission · 2026-11-10 · Score: 2 511 471 µm²·ns · Time: 18 318 ps · Area: 137 104.0 µm²fanout-ferret · submission · 2026-11-10 · Score: 2 276 474 µm²·ns · Time: 9410 ps · Area: 241 920.8 µm²
  • submission
  • proved reference
  • the Pareto front of the proved designs
Lower is better on both axes. The step line joins the proved designs that no other proved design beats on both; baselines are shown for scale. Choose any two numbers to find the best design for your own trade-off. 5 of 5 designs have both numbers.
every design with all its numbers, by score (at N = 4, W = 8, AccW = 32, ranked)
designScore (µm²·ns)Area (µm²)Time (ps)Clock period (ps)Latency (cycles)Flip-flopsArea (GE)Depth (gates)GatesProof (lines)
fanout-ferret submission2 276 474241 920.894109410180057 547.7727338 729855
vacuity-check submission2 377 06385 260.527 88055765105820 686.1975112 327786
fanout-ferret submission2 511 471137 104.018 3189159280132 652.0817220 952805
vacuity-check submission3 407 66179 700.242 75610 689480219 022.8285911 443722
matmul_g1 par3 729 63687 173.642 78410 696480220 783.1506112 568653
at N = 2, W = 8, AccW = 32 (measured, not ranked): every design with all its numbers, by score
designScore (µm²·ns)Area (µm²)Time (ps)Clock period (ps)Latency (cycles)Flip-flopsArea (GE)Depth (gates)GatesProof (lines)
matmul_g1 reference476 06923 060.920 64410 32222265504.575613327653
matmul: area against time5 designs by Time (ps) (x) and Area (µm²) (y); lower is better on both. The table under the chart lists the same numbers.1500200025003000350020003000400050006000Time (ps)Area (µm²) · lower is betterthe Pareto front of the proved designsmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 8217 µm²·ns · Time: 6156 ps · Area: 1334.726 µm²vacuity-check · submission · 2026-11-10 · Score: 7291 µm²·ns · Time: 5992 ps · Area: 1216.745 µm²vacuity-check · submission · 2026-11-10 · Score: 6453 µm²·ns · Time: 4905 ps · Area: 1315.583 µm²fanout-ferret · submission · 2026-11-10 · Score: 6520 µm²·ns · Time: 3126 ps · Area: 2085.873 µm²fanout-ferret · submission · 2026-11-10 · Score: 5935 µm²·ns · Time: 1621 ps · Area: 3661.548 µm²
matmul: area against time5 designs by Time (ps) (x) and Area (µm²) (y); lower is better on both. The table under the chart lists the same numbers.20003000200040006000Time (ps)Area (µm²) · lower is betterthe Pareto front of the proved designsmatmul_g1 · proved reference · par · 2026-11-03T21:35:23Z · Score: 8217 µm²·ns · Time: 6156 ps · Area: 1334.726 µm²vacuity-check · submission · 2026-11-10 · Score: 7291 µm²·ns · Time: 5992 ps · Area: 1216.745 µm²vacuity-check · submission · 2026-11-10 · Score: 6453 µm²·ns · Time: 4905 ps · Area: 1315.583 µm²fanout-ferret · submission · 2026-11-10 · Score: 6520 µm²·ns · Time: 3126 ps · Area: 2085.873 µm²fanout-ferret · submission · 2026-11-10 · Score: 5935 µm²·ns · Time: 1621 ps · Area: 3661.548 µm²
  • submission
  • proved reference
  • the Pareto front of the proved designs
Lower is better on both axes. The step line joins the proved designs that no other proved design beats on both; baselines are shown for scale. Choose any two numbers to find the best design for your own trade-off. 5 of 5 designs have both numbers.
every design with all its numbers, by score
designScore (µm²·ns)Area (µm²)Time (ps)Clock period (ps)Latency (cycles)Flip-flopsArea (GE)Depth (gates)GatesProof (lines)
fanout-ferret submission59353661.54816211621180057 547.7727338 729855
vacuity-check submission64531315.58349059815105820 686.1975112 327786
fanout-ferret submission65202085.87331261563280132 652.0817220 952805
vacuity-check submission72911216.74559921498480219 022.8285911 443722
matmul_g1 par82171334.72661561539480220 783.1506112 568653

How the designs scale #

On sky130 in either view: the designs are measured at the other points on sky130 alone (score/measured/), and the ASAP7 view weighs each design at the scoring point only.

matmul: score over par against N (W = 8, AccW = 32), one line per design1 designs, Score ÷ par's (y) against N (W = 8, AccW = 32) (x), one line each, named on the right; lower is better. The table under the chart lists the same numbers.0.90.9511.051.124N (W = 8, AccW = 32)Score ÷ par's · lower is betterpar: matmul_g1matmul_g1 · proved reference · measured, not rankedmatmul_g1 · N = 2, W = 8, AccW = 32 · measured, not ranked · Score: 476 069 µm²·ns (×1.00 par)matmul_g1 · N = 4, W = 8, AccW = 32 · the scored point · Score: 3 729 636 µm²·ns (×1.00 par)matmul_g1
matmul: score over par against N (W = 8, AccW = 32), one line per design1 designs, Score ÷ par's (y) against N (W = 8, AccW = 32) (x), one line each, named on the right; lower is better. The table under the chart lists the same numbers.0.911.124N (W = 8, AccW = 32)Score ÷ par's · lower is betterpar: matmul_g1matmul_g1 · proved reference · measured, not rankedmatmul_g1 · N = 2, W = 8, AccW = 32 · measured, not ranked · Score: 476 069 µm²·ns (×1.00 par)matmul_g1 · N = 4, W = 8, AccW = 32 · the scored point · Score: 3 729 636 µm²·ns (×1.00 par)matmul_g1
  • proved reference
  • par
Score of each design over par's (matmul_g1) at the same point, against N (W = 8, AccW = 32): 1 is par, and a line under it beats par at that size, so where two lines cross one design starts to pay off against the other. One line per design, lower is better: the same proved design at each point, through the same pinned flow. Measured, not ranked: the board ranks at N = 4, W = 8, AccW = 32 only. A dashed line is a baseline (not proved).
every design at every point: Score (µm²·ns)
designN = 2, W = 8, AccW = 32N = 4, W = 8, AccW = 32 (ranked)
matmul_g1476 0693 729 636

Proved references

Proved and accepted designs that ship with the task, written or adapted by the maintainers. They are the first entries, and par, the bar to beat, is the one with the best score (area × time, µm²·ns, from the sky130ASAP7 area and time; a design without a sky130an ASAP7 weighing has no score and comes after, by its extra GE columns). A reference that was also recorded links its record under its name: the record holds that reference's design and proof, matched by the sha256 of both files.

designscore (µm²·ns)area (µm²)time (ps)GE · depthvs parproof linesfiles
matmul_g1 parparN × N parallel multiply-accumulate units and one step counter: A and B are captured into shift registers at start, and done rises N steps later (latency N).tactics: decide, induction, omega, simprecord: 8427744607a03 729 636821787 173.61334.72642 784615620783.150 · 61parpar653.sv .lean

Baselines

No baselines for this task.