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.
Add two N-bit numbers and a carry in: s is the low N bits of a + b + cin and cout the carry
out of the top bit. The proof covers every width N ≥ 1; the score is taken at N = 16.
The circuit must be built from bitwise logic, multiplexers, selects and concatenations: run-time
+ - * / % ** and the ordering comparisons < <= > >= are banned, because addition is the task (== and !=
stay allowed, and so does constant arithmetic on parameters and genvars). The proved ripple-carry reference has 460.4 µm² and a 2.61 ns critical path on
sky130 (112 GE, depth 33), 1202 µm²·ns: par. Parallel-prefix adders trade area for
delay (Sklansky 541.8 µm² at 2.45 ns, Kogge-Stone 641.9 µm² at
2.06 ns, both simulated but not yet proved); on sky130's area × time neither is ahead of the ripple
yet (1328 µm²·ns and 1325 µm²·ns).
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 add_n #(parameter int N = 16) (
input logic [N-1:0] a, b,
input logic cin,
output logic [N-1:0] s,
output logic cout
);| port | direction | width (bits) |
|---|---|---|
a | input | N |
b | input | N |
cin | input | 1 |
s | output | N |
cout | output | 1 |
The trusted statement #
A proof must establish the task's trusted statement, the constant SvGolf.Tasks.Add.Statement of Spec.lean (module tasks.add.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^31, 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^31 (the values an int parameter holds).
The statement covers every width N with 1 ≤ N < 2^31 at once (the module's parameter is an int, which holds no larger value): 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^31` (the values an `int` parameter
holds). -/
def ParamsInRange (N : Nat) : Prop :=
1 ≤ N ∧ N < 2 ^ 31INTERFACEExactly these ports, in this order, with these widths.
The module has exactly the input ports a and b (N bits each) and cin (1 bit) and exactly the output ports s (N bits) and cout (1 bit), 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), ("cin", 1)] ∧ outputPorts d = [("s", N), ("cout", 1)]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_SUMIn every completed run, every cycle whose stimulus drives a, b, cin with known values ends with s and cout holding the low N bits and the carry of a + b + cin.
In every cycle in which the inputs a, b and cin are driven with known 0/1 values, the outputs settle to the sum: with t = a + b + cin taken as whole numbers, s = t mod 2^N (the low N bits) and cout = t div 2^N (the carry out, 0 or 1). So {cout, s} is the full (N+1)-bit sum and nothing is lost. 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`, `b`, `cin` with known values
ends with `s` and `cout` holding the low `N` bits and the carry of `a + b + cin`. -/
def ComputesSum (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) (cin : BitVec 1),
HoldAll inputs [("a", N), ("b", N), ("cin", 1)] (a, b, cin, ()) →
HoldAll st [("s", N), ("cout", 1)]
(BitVec.ofNat N (a.toNat + b.toNat + cin.toNat),
BitVec.ofNat 1 ((a.toNat + b.toNat + cin.toNat) / 2 ^ N), ())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.Add.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`, `cin : BitVec 1`; outputs
`s = (a + b + cin) mod 2^N` and `cout = (a + b + cin) / 2^N`, the sum taken
in `Nat`; for `1 ≤ N < 2^31`. -/
def task : CombTask where
inRange N := 1 ≤ N ∧ N < 2 ^ 31
inputs N := [("a", N), ("b", N), ("cin", 1)]
outputs N := [("s", N), ("cout", 1)]
fn N := fun (a, b, cin, ()) =>
let t := a.toNat + b.toNat + cin.toNat
(BitVec.ofNat N t, BitVec.ofNat 1 (t / 2 ^ N), ())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: 14 designs (by stage:
source3,extract2,banlist6,fourstate2,design1) - Rejected at the proof: 5 designs (by stage:
solution5)
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.
eqx_x.sv(attack, stopped atsource):(cin === 1'bx) ? '0 : sum: a 4-state simulator computes the sum, while Yosys folds the test and outputs 0 at 0 GE.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N-1:0] sr; logic cr; logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign sr[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate assign cr = c[N]; assign s = (cin === 1'bx) ? '0 : sr; assign cout = (cin === 1'bx) ? 1'b0 : cr; endmodulez_case_item.sv(attack, stopped atsource): A correct sum behind acaseitem with azdigit, which Yosys reads as a match, turning the output into an unknown value at 0 GE.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N-1:0] sr; logic cr; logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign sr[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate assign cr = c[N]; always_comb case (cin) 1'bz: begin s = '0; cout = 1'b0; end default: begin s = sr; cout = cr; end endcase endmodulezpair_add_rare.sv(attack, stopped atsource): Complementaryzitems that make the netlist wrong on a single input pair, too rare for sampling to find.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N-1:0] sr; logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign sr[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate logic rare; logic [N-1:0] ka, kb, pa, pb; logic [2*N-1:0] wa; logic [3*N-1:0] wb; assign wa = {N{2'b10}}; assign wb = {N{3'b011}}; assign pa = wa[N-1:0]; assign pb = wb[N-1:0]; assign ka = ~(a ^ pa); assign kb = ~(b ^ pb); assign rare = (&ka) & (&kb); always_comb case ({a[0], cin}) 2'b0z: begin s = {sr[N-1:1], sr[0] ^ rare}; cout = c[N]; end 2'b1z: begin s = {sr[N-1:1], sr[0] ^ rare}; cout = c[N]; end default: begin s = sr; cout = c[N]; end endcase endmodulecin_name.sv(negative, stopped atextract): The carry-in port is namedciinstead ofcin.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic ci, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = ci; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate assign cout = c[N]; endmodulewide_s.sv(negative, stopped atextract): One (N + 1)-bit output{cout, s}instead of the two portssandcout.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N:0] s ); logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate assign s[N] = c[N]; endmoduleslang_always_notime.sv(attack, stopped atbanlist): A plainalwaysblock that never advances time, which the language forbids (it deadlocks a simulator) but Yosys reads as a wire.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate always cout = c[N]; endmoduleslang_initial_comb.sv(attack, stopped atbanlist): Aninitialblock and analways_combboth writingcout, which the language forbids but Yosys accepts.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate initial cout = 1'b0; always_comb cout = c[N]; endmoduleslang_input_assign.sv(attack, stopped atbanlist): Assigns to the input portcin, which the language forbids.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate assign cin = a[0]; assign cout = c[N]; endmoduleslang_mixed_assign.sv(attack, stopped atbanlist): Drivescoutfrom both a continuous assignment and analways_comb, which the language forbids.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate assign cout = c[N]; always_comb cout = c[N]; endmoduleslang_two_always.sv(attack, stopped atbanlist): Twoalways_combblocks writingcout, which the language forbids.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate always_comb cout = c[N]; always_comb cout = c[N]; endmoduleplus.sv(negative, stopped atbanlist): The right function through the banned run-time+.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); assign {cout, s} = a + b + cin; endmoduleeqx_undriven.sv(attack, stopped atfourstate): Compares an undriven signal with===, which Yosys folds to a constant.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N-1:0] sr; logic cr; logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign sr[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate assign cr = c[N]; logic u; assign s = (u === cin) ? '0 : sr; assign cout = (u === cin) ? 1'b0 : cr; endmoduledead_clock.sv(negative, stopped atfourstate): A correct sum stored in flip-flops on a clock that nothing drives: every simulator seesx, and it would score 0 GE.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic clk; logic [N-1:0] sc; logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign sc[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate always_ff @(posedge clk) begin s <= sc; cout <= c[N]; end endmoduledead_clock_tied.sv(negative, stopped atdesign): The same with the clock tied to1'b0: a clock must be an input port.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic clk; logic [N-1:0] sc; logic [N:0] c; assign clk = 1'b0; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign sc[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate always_ff @(posedge clk) begin s <= sc; cout <= c[N]; 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.
add_proc_case.sv(negative, stopped atsolution): A correct adder whose carry cell is acasearm wrapped inbegin … end, a shape the proof's tactics do not handle, so its proof leaves a goal unproved.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; logic [N-1:0] p; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign p[i] = a[i] ^ b[i]; always_comb begin case (p[i]) 1'b1: begin c[i+1] = c[i]; end default: c[i+1] = a[i]; endcase end assign s[i] = p[i] ^ c[i]; end endgenerate assign cout = c[N]; endmodulecarry_bug.sv(negative, stopped atsolution): A wrong carry gate,(a & b) | (c & a).the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & a[i]); end endgenerate assign cout = c[N]; endmodulecout_off.sv(negative, stopped atsolution): The carry out is taken one bit too early (c[N-1]).the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = cin; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate assign cout = c[N-1]; endmoduleno_cin.sv(negative, stopped atsolution): The carry in is ignored.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = 1'b0; genvar i; generate for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end endgenerate assign cout = c[N]; endmoduleonly_n16.sv(negative, stopped atsolution): A ripple adder at the scoring width N = 16 only, wrong at every other width.the design, with its comments left out
module add_n #(parameter int N = 16) ( input logic [N-1:0] a, b, input logic cin, output logic [N-1:0] s, output logic cout ); logic [N:0] c; assign c[0] = cin; genvar i; generate if (N == 16) begin : g_ripple for (i = 0; i < N; i++) begin : g_bit assign s[i] = a[i] ^ b[i] ^ c[i]; assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i])); end assign cout = c[N]; end else begin : g_cheap assign s = a ^ b; assign cout = 1'b0; end endgenerate endmodule
Spec.lean, verbatim (94 lines)
import SvGolf.Task
/-!
# Task `add`: N-bit adder with carry in and carry out (TRUSTED)
The warm-up challenge. Module (port order as written; `N` is the module's
only parameter):
```systemverilog
module add_n #(parameter int N = 16) (
input logic [N-1:0] a, b,
input logic cin,
output logic [N-1:0] s,
output logic cout
);
```
Statement: for every `N` with `1 ≤ N < 2^31` (the values an `int` parameter
holds), the design has exactly the input ports `a`,
`b` (`N` bits) and `cin` (1 bit), in that order, and exactly the output
ports `s` (`N` bits) and `cout` (1 bit), in that order; no process is
clocked; there is no combinational loop; every run terminates; and in every
cycle whose stimulus drives `a`, `b`, `cin` with known values, the snapshot holds `{cout, s} = a + b + cin`: with
`t = a + b + cin` computed in the natural numbers, `s = t mod 2^N` and
`cout = t / 2^N` (which is 0 or 1).
The banned run-time operators (`+ - * / % **`) are listed in `task.json`
and enforced by the checker's banlist stage, not here.
-/
namespace SvGolf.Tasks.Add
open SvGolf
/-- The task: inputs `a b : BitVec N`, `cin : BitVec 1`; outputs
`s = (a + b + cin) mod 2^N` and `cout = (a + b + cin) / 2^N`, the sum taken
in `Nat`; for `1 ≤ N < 2^31`. -/
def task : CombTask where
inRange N := 1 ≤ N ∧ N < 2 ^ 31
inputs N := [("a", N), ("b", N), ("cin", 1)]
outputs N := [("s", N), ("cout", 1)]
fn N := fun (a, b, cin, ()) =>
let t := a.toNat + b.toNat + cin.toNat
(BitVec.ofNat N t, BitVec.ofNat 1 (t / 2 ^ N), ())
/-- **The challenge statement.** A submission proves
`SvGolf.Tasks.Add.Statement Submission.design.sem`. -/
abbrev Statement : (Nat → LeanModels.Sv.Design2) → Prop := task.Statement
/-! ## Sanity checks on the statement's data
They are proved, so they add nothing to the trusted base; they are here so
that a reader can see the statement means what the prose says. -/
/-- The scoring point `N = 16` is in range. -/
example : task.inRange 16 := by simp [task]
/-- The range ends below `2^31`, the values an `int` parameter holds. -/
example : task.inRange (2 ^ 31 - 1) ∧ ¬ task.inRange (2 ^ 31) := by simp [task]
/-- 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]
/-- `0xFFFF + 0x0001 + 0 = 0x1_0000`: `s = 0`, `cout = 1`. -/
example : (task.fn 16 (0xFFFF#16, 0x0001#16, 0#1, ())).1 = 0#16 ∧
(task.fn 16 (0xFFFF#16, 0x0001#16, 0#1, ())).2.1 = 1#1 := by decide
/-- `0xFFFF + 0xFFFF + 1 = 0x1_FFFF`: `s = 0xFFFF`, `cout = 1`. -/
example : (task.fn 16 (0xFFFF#16, 0xFFFF#16, 1#1, ())).1 = 0xFFFF#16 ∧
(task.fn 16 (0xFFFF#16, 0xFFFF#16, 1#1, ())).2.1 = 1#1 := by decide
/-- `3 + 4 + 1 = 8` at `N = 4`: no carry out. -/
example : (task.fn 4 (3#4, 4#4, 1#1, ())).1 = 8#4 ∧
(task.fn 4 (3#4, 4#4, 1#1, ())).2.1 = 0#1 := by decide
/-- **The arithmetic reading of `fn`**, at every `N`: `cout · 2^N + s` is
exactly `a + b + cin` in the natural numbers (so `{cout, s}` is the
`(N+1)`-bit sum, and nothing is lost to the 1-bit width of `cout`). -/
theorem fn_arith (N : Nat) (a b : BitVec N) (cin : BitVec 1) :
(task.fn N (a, b, cin, ())).2.1.toNat * 2 ^ N + (task.fn N (a, b, cin, ())).1.toNat =
a.toNat + b.toNat + cin.toNat := by
have ha := a.isLt
have hb := b.isLt
have hc : cin.toNat < 2 := cin.isLt
have hp := Nat.two_pow_pos N
have hq : (a.toNat + b.toNat + cin.toNat) / 2 ^ N < 2 := by
rw [Nat.div_lt_iff_lt_mul hp]
omega
simp only [task, BitVec.toNat_ofNat, Nat.pow_one, Nat.mod_eq_of_lt hq]
exact Nat.div_add_mod' _ _
end SvGolf.Tasks.Add
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.add.Spec | task statement | 94 | 08be62a5c0b2 |
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.