This task
This text quotes sky130 numbers and compares the designs on sky130, the default library; the score, the boards and the charts of this page are on ASAP7, where the order of the designs can differ.
Multiply two unsigned N-bit numbers: p = a * b, all 2N bits of the product, for every N ≥ 1,
scored at N = 16.
Run-time + - * / % ** and the ordering comparisons < <= > >= are banned, so the multiplier is built from partial products and adders made of
gates. The proved array multiplier has 8290.5 µm² and a 10.9 ns critical path on sky130
(1962.576 GE, depth 88). The proved tree references are much faster for a little more area:
par is the tree mul_tree_h, 8563.2 µm² at 5.99 ns, 51 311 µm²·ns. An unproved
Dadda tree with a ripple final adder is both smaller and faster than par, 8230.4 µm² at
5.46 ns (44 946 µm²·ns): proving a tree like it is the open challenge.
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.
module mul_n #(parameter int N = 16) (
input logic [N-1:0] a, b,
output logic [2*N-1:0] p
);| port | direction | width (bits) |
|---|---|---|
a | input | N |
b | input | N |
p | output | 2*N |
The trusted statement #
A proof must establish the task's trusted statement, the constant SvGolf.Tasks.Mul.Statement of Spec.lean (module tasks.mul.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 meets the trusted statement exactly when, for every width N with 1 ≤ N < 2^30, it has all of the properties below. Lean checks that, together, they 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 widths the statement covers: every N with 1 ≤ N < 2^30 (so that the output width 2N, an int expression of the module, stays below 2^31, the values an int holds).
The statement covers every width N with 1 ≤ N < 2^30 at once (the module's port widths are int expressions of N, such as 2N, and an int holds no value of 2^31 or more): one proof works for all of them, not just for the width the design is scored at (N = 16). Every property below must hold at each width.
/-- The widths the statement covers: every `N` with `1 ≤ N < 2^30` (so that the output width `2N`,
an `int` expression of the module, stays below `2^31`, the values an `int` holds). -/
def ParamsInRange (N : Nat) : Prop :=
1 ≤ N ∧ N < 2 ^ 30INTERFACEExactly these ports, in this order, with these widths.
The module has exactly the input ports a and b (N bits each) and exactly the output port p (2N 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.
/-- Exactly these ports, in this order, with these widths. -/
def Interface (N : Nat) (d : Design2) : Prop :=
inputPorts d = [("a", N), ("b", N)] ∧ outputPorts d = [("p", 2 * N)]UNCLOCKEDNo process runs at a clock edge (no always_ff, no always @(posedge …)).
No process of the design runs at a clock edge: no always_ff, no always @(posedge …), no asynchronous-reset block; only continuous assignments and always_comb blocks. The task is combinational, so it never needs one. The rule closes a gap between Lean's model of SystemVerilog, which the proof is about, and real tools: the model runs every clocked block once per cycle whatever its clock does, so a design that registers correct outputs on a clock nothing drives would look right there, while a simulator sees a clock that never ticks and synthesis removes the registers.
/-- No process runs at a clock edge (no `always_ff`, no `always @(posedge …)`). -/
def Unclocked (d : Design2) : Prop :=
∀ p ∈ d.processes.toList, p.isEdgePhase = falseLOOP_FREENo combinational loop: the design lowers to continuous assigns (Design2.lowerComb) that are ranked (Acyclic): each reads only what lower-ranked ones write.
The design has no combinational loop: written as continuous assignments (each always_comb block becomes one), its processes can be ranked so that each reads only what lower-ranked ones write. A latch (an always_comb block that keeps a value on some path) is refused with it. Lean's model starts every signal at x and settles, so it would read a loop at one state, while a circuit powers up in any 0/1 state the loop can hold and keeps it; the rule removes that question instead of answering it. The ranking is of processes, not bits, so a process that reads a part of a signal it writes itself is refused too, even when no bit depends on itself: write such bits as separate assignments.
/-- No combinational loop: the design lowers to continuous assigns (`Design2.lowerComb`) that are
ranked (`Acyclic`): each reads only what lower-ranked ones write. -/
def LoopFree (d : Design2) : Prop :=
∃ d', d.lowerComb = some d' ∧ Acyclic d'TERMINATESUnder every schedule and every stimulus, the run completes.
Whatever order the simulator picks for processes that are ready at the same moment (the schedule), and whatever values the inputs take, simulating the design completes: every 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 next property its teeth: that one is about completed runs, and a design with no completed run would satisfy it without computing anything.
/-- Under every schedule and every stimulus, the run completes. -/
def Terminates (d : Design2) : Prop :=
∀ (σ : ScheduleOracle) (stim : List SvState), ∃ tr, Runs2 d σ stim trCOMPUTES_PRODUCTIn every completed run, every cycle whose stimulus drives a and b with known values ends with p holding their full product, on 2N bits.
In every cycle in which the inputs a and b are driven with known 0/1 values, the output p settles to a × b, the product of the two unsigned numbers. p has 2N bits, enough for the largest product, so nothing is truncated. The outputs must be fully known 0/1 values in every cycle of every run, whatever the earlier cycles were, so they cannot depend on history.
/-- In every completed run, every cycle whose stimulus drives `a` and `b` with known values ends
with `p` holding their full product, on `2N` bits. -/
def ComputesProduct (N : Nat) (d : Design2) : Prop :=
d ⊨₂ spec2 fun stim tr =>
∀ (c : Nat) (inputs st : SvState), stim[c]? = some inputs → tr[c]? = some st →
∀ (a b : BitVec N),
HoldAll inputs [("a", N), ("b", N)] (a, b, ()) →
HoldAll st [("p", 2 * N)] (BitVec.ofNat (2 * N) (a.toNat * b.toNat), ())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
StatementSpec.leanThe trusted challenge statement that these properties restate, part by part.
/-- **The challenge statement.** A submission proves
`SvGolf.Tasks.Mul.Statement Submission.design.sem`. -/
abbrev Statement : (Nat → LeanModels.Sv.Design2) → Prop := task.StatementtaskSpec.leanThe task as data: the parameter range, the ports at each parameter value, and the function the outputs must compute.
/-- The task: inputs `a b : BitVec N`, output `p = a * b` on `2N` bits, for
`1 ≤ N < 2^30`. -/
def task : CombTask where
inRange N := 1 ≤ N ∧ N < 2 ^ 30
inputs N := [("a", N), ("b", N)]
outputs N := [("p", 2 * N)]
fn N := fun (a, b, ()) => (BitVec.ofNat (2 * N) (a.toNat * b.toNat), ())The shared trusted base
CombTask.SatisfiedAtTask.leanThe trusted form of a combinational statement at one parameter value: the interface, then no clock and termination, then the function.
/-- The statement at one parameter value: interface; no clocked process, no
combinational loop and termination; function. Conjunct 2 is the triple
`Unclocked d ∧ LoopFree d ∧ Terminates2 d`. -/
def SatisfiedAt (N : Nat) (d : Design2) : Prop :=
t.Interface N d ∧ (Unclocked d ∧ LoopFree d ∧ Terminates2 d) ∧ t.Computes N dinputPortsTask.leanThe design's input ports, each with its declared width, in declaration order.
/-- 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 noneoutputPortsTask.leanThe design's output ports, each with its declared width, in declaration order.
/-- 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 noneHoldAllTask.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 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⊨₂Spec2.leand ⊨₂ P: in every completed run of the design d, under every schedule and every stimulus, the stimulus and the trace satisfy P.
/-- `d ⊨₂ P` — for **every** legal schedule, every stimulus, and every
completed run (`Runs2`), the trace satisfies `P`. Introduce from a raw
∀-fuel fact with `Models2.of_run`; eliminate against a concrete run with
`Models2.run` / `Models2.runs`. Says nothing about whether runs complete —
pair it with `Terminates2`. -/
def Models2 (d : Design2) (P : TraceProp2) : Prop :=
∀ (σ : ScheduleOracle) (stim tr : List SvState), Runs2 d σ stim tr → P d stim tr
@[inherit_doc] scoped infix:50 " ⊨₂ " => Models2spec2Spec2.leanTurns a property of a stimulus (one input entry per cycle) and a trace (one snapshot of every signal per cycle) into the form ⊨₂ takes.
/-- Lift a design-agnostic stimulus/trace predicate into `⊨₂`
(`d ⊨₂ spec2 fun stim tr => …`). -/
def spec2 (P : List SvState → List SvState → Prop) : TraceProp2 := fun _ stim tr => P stim trRuns2Spec2.leanRuns2 d σ stim tr: simulating d under the schedule σ on the stimulus stim completes, with the trace tr.
/-- The fuel-abstracted Design2 run judgment: *some* fuel completes the run
of `d` under schedule `σ` and stimulus `stim` with trace `tr`. The only place
fuel appears in a Design2 spec. -/
def Runs2 (d : Design2) (σ : ScheduleOracle) (stim tr : List SvState) : Prop :=
∃ fuel, run2 d σ fuel stim = .ok trScheduleOracleSemantics.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.
/-- 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 readyProcess2.isEdgePhaseSem2.leanTrue for the processes that run at the clock edge: always_ff, always @(posedge …) and asynchronous-reset blocks.
/-- 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
| _ => falseWhat 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: 2 designs (by stage:
extract1,banlist1) - Rejected at the proof: 3 designs (by stage:
solution3)
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.
narrow_out.sv(negative, stopped atextract): The productpis 2N - 1 bits wide instead of 2N.the design, with its comments left out
module mul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-2:0] p ); logic [2*N-1:0] full; assign p = full[2*N-2:0]; logic [N-1:0][N-1:0] pp; logic [N-1:0][N:0] s; logic [N-1:0][N:0] c; logic [N-1:0][N-1:0] t; genvar i, j; generate for (i = 0; i < N; i++) begin : g_pp for (j = 0; j < N; j++) begin : g_pp_j assign pp[i][j] = a[j] & b[i]; end end endgenerate assign s[0] = {1'b0, pp[0]}; assign c[0] = '0; assign t[0] = '0; generate for (i = 1; i < N; i++) begin : g_row assign c[i][0] = 1'b0; for (j = 0; j < N; j++) begin : g_bit assign t[i][j] = s[i-1][j+1] ^ pp[i][j]; assign s[i][j] = t[i][j] ^ c[i][j]; assign c[i][j+1] = (s[i-1][j+1] & pp[i][j]) | (c[i][j] & t[i][j]); end assign s[i][N] = c[i][N]; end endgenerate generate for (i = 0; i < N; i++) begin : g_out assign full[i] = s[i][0]; end endgenerate assign full[2*N-1:N] = s[N-1][N:1]; endmodulemul_star.sv(negative, stopped atbanlist): The right function through the banned run-time*.the design, with its comments left out
module mul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-1:0] p ); assign p = a * b; 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.
drop_carry.sv(negative, stopped atsolution): Every adder row drops its carry out.the design, with its comments left out
module mul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-1:0] p ); logic [N-1:0][N-1:0] pp; logic [N-1:0][N:0] s; logic [N-1:0][N:0] c; logic [N-1:0][N-1:0] t; genvar i, j; generate for (i = 0; i < N; i++) begin : g_pp for (j = 0; j < N; j++) begin : g_pp_j assign pp[i][j] = a[j] & b[i]; end end endgenerate assign s[0] = {1'b0, pp[0]}; assign c[0] = '0; assign t[0] = '0; generate for (i = 1; i < N; i++) begin : g_row assign c[i][0] = 1'b0; for (j = 0; j < N; j++) begin : g_bit assign t[i][j] = s[i-1][j+1] ^ pp[i][j]; assign s[i][j] = t[i][j] ^ c[i][j]; assign c[i][j+1] = (s[i-1][j+1] & pp[i][j]) | (c[i][j] & t[i][j]); end assign s[i][N] = 1'b0; end endgenerate generate for (i = 0; i < N; i++) begin : g_out assign p[i] = s[i][0]; end endgenerate assign p[2*N-1:N] = s[N-1][N:1]; endmoduleonly_n16.sv(negative, stopped atsolution): Correct only at the scoring width N = 16, zero elsewhere.the design, with its comments left out
module mul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-1:0] p ); logic [N-1:0][N-1:0] pp; logic [N-1:0][N:0] s; logic [N-1:0][N:0] c; logic [N-1:0][N-1:0] t; genvar i, j; generate if (N == 16) begin : g_scored for (i = 0; i < N; i++) begin : g_pp for (j = 0; j < N; j++) begin : g_pp_j assign pp[i][j] = a[j] & b[i]; end end assign s[0] = {1'b0, pp[0]}; assign c[0] = '0; assign t[0] = '0; for (i = 1; i < N; i++) begin : g_row assign c[i][0] = 1'b0; for (j = 0; j < N; j++) begin : g_bit assign t[i][j] = s[i-1][j+1] ^ pp[i][j]; assign s[i][j] = t[i][j] ^ c[i][j]; assign c[i][j+1] = (s[i-1][j+1] & pp[i][j]) | (c[i][j] & t[i][j]); end assign s[i][N] = c[i][N]; end for (i = 0; i < N; i++) begin : g_out assign p[i] = s[i][0]; end assign p[2*N-1:N] = s[N-1][N:1]; end else begin : g_other assign p = '0; end endgenerate endmoduletop_shift.sv(negative, stopped atsolution): The top half of the product is read from the wrong bits.the design, with its comments left out
module mul_n #(parameter int N = 16) ( input logic [N-1:0] a, b, output logic [2*N-1:0] p ); logic [N-1:0][N-1:0] pp; logic [N-1:0][N:0] s; logic [N-1:0][N:0] c; logic [N-1:0][N-1:0] t; genvar i, j; generate for (i = 0; i < N; i++) begin : g_pp for (j = 0; j < N; j++) begin : g_pp_j assign pp[i][j] = a[j] & b[i]; end end endgenerate assign s[0] = {1'b0, pp[0]}; assign c[0] = '0; assign t[0] = '0; generate for (i = 1; i < N; i++) begin : g_row assign c[i][0] = 1'b0; for (j = 0; j < N; j++) begin : g_bit assign t[i][j] = s[i-1][j+1] ^ pp[i][j]; assign s[i][j] = t[i][j] ^ c[i][j]; assign c[i][j+1] = (s[i-1][j+1] & pp[i][j]) | (c[i][j] & t[i][j]); end assign s[i][N] = c[i][N]; end endgenerate generate for (i = 0; i < N; i++) begin : g_out assign p[i] = s[i][0]; end endgenerate assign p[2*N-1:N] = s[N-1][N-1:0]; endmodule
Spec.lean, verbatim (89 lines)
import SvGolf.Task
/-!
# Task `mul`: N-bit unsigned multiplier (TRUSTED)
The main svGolf challenge. Module (port order as written; `N` is the
module's only parameter):
```systemverilog
module mul_n #(parameter int N = 16) (
input logic [N-1:0] a, b,
output logic [2*N-1:0] p
);
```
Statement: for every `N` with `1 ≤ N < 2^30` (so that the output width `2N`, an
`int` expression of the module, stays below `2^31`, the values an `int` holds),
the design has exactly the ports `a`, `b` (inputs, `N` bits) and `p`
(output, `2N` bits), no process is clocked, there is no combinational loop,
every run terminates, and in every cycle whose stimulus drives `a` and `b` with
known values the snapshot's `p` is the FULL product `a * b`: the
natural-number product of the two unsigned inputs, as a `2N`-bit vector.
Nothing is truncated: the product of two `N`-bit numbers is below `2^(2N)`
(`fn_toNat` below), so `p` carries it exactly.
Run-time `+ - * / % **` are banned (`task.json`), so the circuit has to be
built from bitwise logic; constant arithmetic (parameter expressions, genvar
indices such as `s[i-1][j+1]`) is fine.
-/
namespace SvGolf.Tasks.Mul
open SvGolf
/-- The task: inputs `a b : BitVec N`, output `p = a * b` on `2N` bits, for
`1 ≤ N < 2^30`. -/
def task : CombTask where
inRange N := 1 ≤ N ∧ N < 2 ^ 30
inputs N := [("a", N), ("b", N)]
outputs N := [("p", 2 * N)]
fn N := fun (a, b, ()) => (BitVec.ofNat (2 * N) (a.toNat * b.toNat), ())
/-- **The challenge statement.** A submission proves
`SvGolf.Tasks.Mul.Statement Submission.design.sem`. -/
abbrev Statement : (Nat → LeanModels.Sv.Design2) → Prop := task.Statement
/-! Sanity checks on the statement's data. -/
/-- The scoring point `N = 16` (and the reported points 8 and 32) are in range. -/
example : task.inRange 16 ∧ task.inRange 8 ∧ task.inRange 32 := by simp [task]
/-- The range ends below `2^30`: the output width `2N` (the port's `[2*N-1:0]`, evaluated as an
`int`) stays below `2^31`, the values an `int` holds. -/
example : task.inRange (2 ^ 30 - 1) ∧ ¬ task.inRange (2 ^ 30) := by simp [task]
/-- At the top of the range the output width is still an `int`. -/
example : 2 * (2 ^ 30 - 1) + 1 < 2 ^ 31 := by decide
/-- The input names are distinct (the non-vacuity theorem
`CombTask.SatisfiedAt.exists_run` needs it), at every `N`. -/
example (N : Nat) : ((task.inputs N).map Prod.fst).Nodup := by
simp [task]
/-- **No truncation**: the output is exactly the natural-number product. -/
theorem fn_toNat (N : Nat) (a b : BitVec N) :
(task.fn N (a, b, ())).1.toNat = a.toNat * b.toNat := by
show (BitVec.ofNat (2 * N) (a.toNat * b.toNat)).toNat = a.toNat * b.toNat
rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
rw [Nat.two_mul, Nat.pow_add]
exact Nat.mul_lt_mul_of_lt_of_lt a.isLt b.isLt
/-- The same function, read as `BitVec` multiplication at double width. -/
theorem fn_eq_mul (N : Nat) (a b : BitVec N) :
(task.fn N (a, b, ())).1 = a.setWidth (2 * N) * b.setWidth (2 * N) := by
apply BitVec.eq_of_toNat_eq
have hlt : ∀ x : BitVec N, x.toNat < 2 ^ (2 * N) := fun x =>
Nat.lt_of_lt_of_le x.isLt (Nat.pow_le_pow_right (by decide) (by omega))
rw [fn_toNat, BitVec.toNat_mul, BitVec.toNat_setWidth, BitVec.toNat_setWidth,
Nat.mod_eq_of_lt (hlt a), Nat.mod_eq_of_lt (hlt b), Nat.mod_eq_of_lt]
rw [Nat.two_mul, Nat.pow_add]
exact Nat.mul_lt_mul_of_lt_of_lt a.isLt b.isLt
/-- Concrete values: `15 * 15 = 225` at `N = 4`, `255 * 255 = 65025` at
`N = 8`, `3 * 3 = 9` at `N = 2` (the top bit is used). -/
example : (task.fn 4 (15#4, 15#4, ())).1 = 225#8 := by decide
example : (task.fn 8 (255#8, 255#8, ())).1 = 65025#16 := by decide
example : (task.fn 2 (3#2, 3#2, ())).1 = 9#4 := by decide
end SvGolf.Tasks.Mul
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.
| module | role | lines | sha256 |
|---|---|---|---|
tasks.mul.Spec | task statement | 89 | 8791b67eebf4 |
How to participate #
- Write a circuit with the task's exact interface.
- Prove in Lean 4 that it meets the trusted statement; Start a new design, below, gives the route, and the proving guide shows how.
- 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.
- Beat par: an accepted design whose score (area × time) is below that of the best proved reference. The leaderboard ranks by it.