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.
Compute the bitwise AND of two N-bit inputs, y = a & b, combinationally, and prove it for every
N ≥ 1.
The optimum is obvious: one AND gate per bit, 100.1 µm² with a 0.28 ns critical path on sky130
for N = 16 (21.328 GE, depth 1). The task exists to run
the whole pipeline (statement, proof, checker, banlist, scoring) on a design small enough to read in one
sitting, and to be the template for real tasks. Its reference proofs are complete for every width:
band_tactics with the sv_comb tactics, the route of the real tasks and the proof the walk-through starts
from, and band by hand, walking the design's structure symbolically. The run-time operators + - * / % ** and the ordering
comparisons < <= > >= are banned only to exercise the banlist.
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 band #(parameter int N = 4) (
input logic [N-1:0] a,
input logic [N-1:0] b,
output logic [N-1:0] y
);| port | direction | width (bits) |
|---|---|---|
a | input | N |
b | input | N |
y | output | N |
The trusted statement #
A proof must establish the task's trusted statement, the constant SvGolf.Tasks.Example.Statement of Spec.lean (module tasks._example.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 exactly the output port y (N 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 = [("y", 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_ANDIn every completed run, every cycle whose stimulus drives a and b with known values ends with y holding their bitwise AND.
In every cycle in which the inputs a and b are driven with known 0/1 values, the output y settles to a & b, their bitwise AND. 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 `y` holding their bitwise AND. -/
def ComputesAnd (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 [("y", N)] (a &&& b, ())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.Example.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 `y = a &&& b`, for `1 ≤ N < 2^31`. -/
def task : CombTask where
inRange N := 1 ≤ N ∧ N < 2 ^ 31
inputs N := [("a", N), ("b", N)]
outputs N := [("y", N)]
fn _ := fun (a, b, ()) => (a &&& b, ())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: 27 designs (by stage:
source11,extract2,banlist4,fourstate9,design1) - Rejected at the proof: 1 design (by stage:
solution1)
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.
casex_item.sv(attack, stopped atsource): Acaseitem with anxdigit: ls-sv computesa & b, while Yosys treats the item as a match and drives an unknown value at 0 GE.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic s; assign s = 1'b0; always_comb case (s) 1'bx: y = '0; default: y = a & b; endcase endmodulepriority_nomatch.sv(attack, stopped atsource): Apriority casethat never matches, which lets Yosys drive anything (0 GE).the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb begin y = a & b; priority case (1'b1) (a[0] & ~a[0]): y = '0; endcase end endmoduleunique0_nomatch.sv(attack, stopped atsource): A harmlessunique0 casethat never matches, refused like everyunique,unique0andpriorityqualifier because they let synthesis read acasedifferently from simulation.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb begin y = a & b; unique0 case (1'b1) (a[0] & ~a[0]): y = '0; endcase end endmoduleunique_first_const.sv(attack, stopped atsource): A harmless-lookingunique case (1'b1)whose first item is the constant 1, so two items can match at once.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb begin y = '0; unique case (1'b1) 1'b1: y = a & b; a[0]: y = a | b; endcase end endmoduleunique_nomatch.sv(attack, stopped atsource): Aunique casethat never matches, which lets Yosys drive anything (0 GE).the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb begin y = a & b; unique case (1'b1) (a[0] & ~a[0]): y = '0; endcase end endmoduleunique_overlap.sv(attack, stopped atsource): Aunique casewith overlapping items, where Yosys ORs the arms of the items that both match.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb begin y = a & b; unique case (1'b1) a[1]: y = a & b; a[0]: y = a | b; endcase end endmoduleunique_rare.sv(attack, stopped atsource): The same overlap confined to one input pattern in 2^24.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb begin y = a & b; unique case (1'b1) (a[7:0] == 8'hEF): y = a & b; (b == 16'h1234): y = a | b; endcase end endmodulez_rare.sv(attack, stopped atsource): Acaseitem withzdigits that Yosys ignores, so the netlist differs on one input in 2^28.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb case ({a, b}) 32'hDEAD_BEEz: y = '0; default: y = a & b; endcase endmodulezconst_param.sv(attack, stopped atsource):xandzbits hidden in local parameters built by concatenation, used ascaseitems.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); localparam logic [1:0] K0 = {1'b0, 1'bz}; localparam logic [1:0] K1 = {1'b1, 1'bx}; always_comb case (a[1:0]) K0: y = a | b; K1: y = a | b; default: y = a & b; endcase endmodulezeq_pair_if.sv(attack, stopped atsource): Comparisons against constants withzdigits: unknown in ls-sv, always true in Yosys.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb if ((a[1:0] == 2'b0z) || (a[1:0] == 2'b1z)) y = a | b; else y = a & b; endmodulezpair_or.sv(attack, stopped atsource): Two complementarycaseitems withzdigits: neither matches in ls-sv, together they match every input in Yosys.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb case ({a[0], b[0]}) 2'b0z: y = a | b; 2'b1z: y = a | b; default: y = a & b; endcase endmoduleextra_in.sv(negative, stopped atextract): A hidden extra input port: the statement allows exactly the task's ports.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, input logic en, output logic [N-1:0] y ); assign y = en ? (a & b) : '0; endmodulewide_out.sv(negative, stopped atextract): The output is N + 1 bits wide instead of N.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N:0] y ); assign y = a & b; endmodulearray_sum.sv(attack, stopped atbanlist): Sums an unpacked array with the.sum()method: run-time addition in disguise.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic [N-1:0] arr [2]; assign arr[0] = a & b; assign arr[1] = '0; assign y = arr.sum(); endmodulefor_counter_skip.sv(attack, stopped atbanlist): Aforloop that skips an iteration by incrementing its own counter: simulation and synthesis disagree on the result.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb begin y = a & b; for (int k = 0; k < 2; k++) begin if (k == 1) y = '0; k = k + 1; end end endmodulefor_counter_write.sv(attack, stopped atbanlist): Aforloop whose body overwrites its own counter: Yosys ignores the write, while a simulator can loop forever.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); always_comb begin y = '0; for (int k = 0; k < 2; k++) begin k = int'(a[0]); y = y | (a & b); end end endmodulearith_and.sv(negative, stopped atbanlist): The right function, written with run-time+and-, which this task bans.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); assign y = (a + b) - (a | b); endmodulelatch_never.sv(attack, stopped atfourstate): Analways_latchthat is never enabled: unknown in simulation, while Yosys resolves the latch to a constant.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic r; logic t; assign t = a[0] & ~a[0]; always_latch begin if (t) r = 1'b1; end always_comb begin if (!r) y = a | b; else y = a & b; end endmodulelatch_star.sv(attack, stopped atfourstate): The same never-enabled latch, written withalways @*.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic r; always @* begin if (a[0] & ~a[0]) r = 1'b1; end always @* begin if (!r) y = a | b; else y = a & b; end endmoduleoob_rare.sv(attack, stopped atfourstate): An out-of-range read that changes the netlist's output on a single input pair, too rare for any sampling to find.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic [2*N-1:0] wa; logic [3*N-1:0] wb; logic [N-1:0] pa, pb; logic rare, t; logic [3:0] k; assign wa = {N{2'b10}}; assign wb = {N{3'b011}}; assign pa = wa[N-1:0]; assign pb = wb[N-1:0]; assign rare = (&(~(a ^ pa))) & (&(~(b ^ pb))); assign k = 4'b0001; assign t = k[{rare, 2'b00}]; always_comb if (t) y = (a & b) ^ {{(N-1){1'b0}}, rare}; else y = a & b; endmoduleoob_select.sv(attack, stopped atfourstate): An index that always reads past the end of a 4-bit vector: an unknown value that ls-sv and Yosys resolve differently.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic [3:0] k; logic t; assign k = 4'b0101; assign t = k[{1'b1, a[1:0]}] ? 1'b0 : 1'b1; always_comb if (t) y = a | b; else y = a & b; endmoduleparam_divzero.sv(attack, stopped atfourstate): A constant1 / 0used as acaseitem: an unknown value without anxliteral, matched by Yosys and never by ls-sv.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); localparam logic [1:0] K = 2'd1 / 2'd0; always_comb case (a[1:0]) K: y = a | b; default: y = a & b; endcase endmodulerare_mid.sv(attack, stopped atfourstate): An out-of-range read that changes the output on about one input in 512: sampling finds it only with the full vector set.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic [2*N-1:0] wa; logic [N-1:0] pa, ma; logic rare, t; logic [3:0] k; assign wa = {N{2'b10}}; assign pa = wa[N-1:0]; assign ma = ~({N{1'b1}} << 9); assign rare = &(~(a ^ pa) | ~ma); assign k = 4'b0001; assign t = k[{rare, 2'b00}]; always_comb if (t) y = (a & b) ^ {{(N-1){1'b0}}, rare}; else y = a & b; endmoduleundriven_mux.sv(attack, stopped atfourstate): A multiplexer steered by a signal that nothing drives: ls-sv and Yosys pick different branches.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic u, t; assign t = u ? 1'b0 : 1'b1; always_comb if (t) y = a | b; else y = a & b; endmoduleundriven_offpoint.sv(attack, stopped atfourstate): The same undriven multiplexer, driven at the scoring width N = 16 only: at every other width ls-sv and Yosys pick different branches.the design, with its comments left out
module band #(parameter int N = 16) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic u, t; generate if (N == 16) begin : g_drv assign u = 1'b1; end endgenerate assign t = u ? 1'b0 : 1'b1; always_comb if (t) y = a | b; else y = a & b; endmodulereads_x.sv(negative, stopped atfourstate): Reads a net that nothing drives, so its value is unknown (x).the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); logic [N-1:0] z; assign y = a & b & ~z; endmodulefn_uninit.sv(attack, stopped atdesign): A function reads a local variable before assigning it: unknown in SystemVerilog, a fixed value in Yosys, and a construct ls-sv cannot run.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); function automatic logic f(input logic s); logic r; if (s) r = 1'b1; f = r; endfunction always_comb if (f(a[0])) y = a | b; else y = 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.
or_gate.sv(negative, stopped atsolution): The wrong function: OR instead of AND.the design, with its comments left out
module band #(parameter int N = 4) ( input logic [N-1:0] a, input logic [N-1:0] b, output logic [N-1:0] y ); assign y = a | b; endmodule
Spec.lean, verbatim (58 lines)
import SvGolf.Task
/-!
# Task `_example`: N-bit bitwise AND (TRUSTED)
The toy task that exercises the svGolf pipeline end to end. It is not a real
challenge: the optimum (N two-input AND gates, depth 1) is obvious.
Module (port order as written; `N` is the module's only parameter):
```systemverilog
module band #(parameter int N = 4) (
input logic [N-1:0] a,
input logic [N-1:0] b,
output logic [N-1:0] y
);
```
Statement: for every `N` with `1 ≤ N < 2^31` (the values an `int` parameter
holds), the design has exactly the ports `a`, `b` (inputs, `N` bits) and `y`
(output, `N` 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 `y` is `a &&& b`.
-/
namespace SvGolf.Tasks.Example
open SvGolf
/-- The task: inputs `a b : BitVec N`, output `y = a &&& b`, for `1 ≤ N < 2^31`. -/
def task : CombTask where
inRange N := 1 ≤ N ∧ N < 2 ^ 31
inputs N := [("a", N), ("b", N)]
outputs N := [("y", N)]
fn _ := fun (a, b, ()) => (a &&& b, ())
/-- **The challenge statement.** A submission proves
`SvGolf.Tasks.Example.Statement Submission.design.sem`. -/
abbrev Statement : (Nat → LeanModels.Sv.Design2) → Prop := task.Statement
/-! Sanity checks on the statement's data (closed, by `decide`). -/
/-- 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]
/-- The function on a concrete value: `0b1100 &&& 0b1010 = 0b1000`. -/
example : (task.fn 4 (0b1100#4, 0b1010#4, ())).1 = 0b1000#4 := by decide
end SvGolf.Tasks.Example
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._example.Spec | task statement | 58 | 433e431a44d7 |
How to participate #
- Write a circuit with the task's exact interface.
- Prove in Lean 4 that it meets the trusted statement; 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.