This task
Give the grant to at most one of N requesters per cycle, only to one that asks, to someone whenever
anyone asks, and never let a requester ask N cycles in a row without being granted. This is svGolf's
first reactive task: a controller that runs for ever, specified by a safety property on every cycle and a
bounded response over the whole input trace, with no assumption about the requesters. The proof covers
every N with 1 ≤ N and N·N < 2^31; the score is taken at N = 8.
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. The grant is registered, a Moore output: a clock edge samples req,
and the grant it decides is on gnt
for the whole next clock period, so a grant follows its request by one cycle. No output may depend
combinationally on an input. The claims hold from every power-up value of every register, the first reset
included, so a register that is never reset may only hold a value that does not matter; no construct may
create an unknown value, and a register that is never loaded is refused. Run-time / % ** are banned. Any
fair policy is allowed (round-robin pointer or mask, rotating priority, a tree, a matrix), so the task is the
policy and its state, which the score prices. The bound N is tight: no design can serve every persistent requester
within N - 1 cycles.
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 arbiter #(parameter int N = 8) (
input logic clk, rst,
input logic [N-1:0] req,
output logic [N-1:0] gnt
);| port | direction | width (bits) |
|---|---|---|
clk | input | 1 |
rst | input | 1 |
req | input | N |
gnt | output | N |
The trusted statement #
A proof must establish the task's trusted statement, the constant SvGolf.Tasks.Arbiter.Statement of Spec.lean (module tasks.arbiter.Spec). The proved references meet it. The last tab, what does not count, lists the designs the checker rejects.
Properties
STATEMENT
/-- **The challenge statement**: the task at every `N` in range with the response bound `N - 1`
(G4: `N` consecutive requests are granted at least once). -/
abbrev Statement (sem : Nat → LeanModels.Sv.Design2) : Prop :=
task.Statement sem (fun N => N - 1)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: 3 designs (by stage:
source1,extract2) - Rejected at the proof: 2 designs (by stage:
solution2) - Rejected after scoring: 16 designs (by stage:
score1,postsynth15)
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.
a13_async.sv(attack, stopped atsource): A round-robin with an asynchronous reset: the reset is synchronous on this task, and the source check refuses the second event.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] mask, mreq, pick; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end always_ff @(posedge clk or posedge rst) begin if (rst) begin gnt <= '0; mask <= '1; end else begin gnt <= pick; if (pick != '0) mask <= ~((pick << 1) - 1'b1); end end endmodulem004_wide_req.sv(attack, stopped atextract): The reference with its request port one bit wider than the task's: right grants on the wrong interface, so no proof can exist; refused when the checker compares the ports, before any other stage.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-0:0] req, output logic [N-1:0] gnt ); logic [N-1:0] mask, mreq, pick; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end always_ff @(posedge clk) begin if (rst) begin gnt <= '0; mask <= '1; end else begin gnt <= pick; if (pick != '0) mask <= ~((pick << 1) - 1'b1); end end endmodulem007_wide_gnt.sv(attack, stopped atextract): The reference with its grant port one bit wider than the task's, the extra bit never set: refused when the checker compares the ports.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-0:0] gnt ); logic [N-1:0] mask, mreq, pick; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end always_ff @(posedge clk) begin if (rst) begin gnt <= '0; mask <= '1; end else begin gnt <= pick; if (pick != '0) mask <= ~((pick << 1) - 1'b1); 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.
bit_ring.sv(negative, stopped atsolution): A correct round-robin behind a test of a 2-state ring that is never reset: fair from the power-up value 0, where a simulator starts it, and fixed priority for ever from all ones.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); bit [31:0] u; logic [N-1:0] mask, mreq, pick, fix; always_ff @(posedge clk) u <= {u[30:0], u[31]}; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); fix = req & (~req + 1'b1); end always_ff @(posedge clk) begin if (rst) begin gnt <= '0; mask <= '1; end else begin if (&u) gnt <= fix; else gnt <= pick; if (pick != '0) mask <= ~((pick << 1) - 1'b1); end end endmodulereset_edge.sv(negative, stopped atsolution): A correct round-robin behind a flag that the reset sets from a register's power-up value: from all ones the first segment after the reset is fixed priority.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [31:0] u; logic bad; logic [N-1:0] mask, mreq, pick, fix; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); fix = req & (~req + 1'b1); end always_ff @(posedge clk) begin if (rst) begin u <= '0; if (&u) bad <= 1'b1; else bad <= 1'b0; gnt <= '0; mask <= '1; end else begin u <= {u[30:0], ~(u[31] ^ u[21] ^ u[1] ^ u[0])}; if (bad) gnt <= fix; else gnt <= pick; if (pick != '0) mask <= ~((pick << 1) - 1'b1); end end endmodule
Rejected after scoring
These get through the proof stages and are rejected by scoring or by the post-synthesis check.
a16_xopt.sv(attack, stopped atscore): A correct round-robin behind a test of a register that only holds itself: synthesis removes the register and builds fixed priority, a simulator stays fair, and from the power-up value 0 the design is fixed priority too. The checker refuses a register that is never loaded.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic u; logic [N-1:0] mask, mreq, pick, fix; always_ff @(posedge clk) u <= u; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); fix = req & (~req + 1'b1); end always_ff @(posedge clk) begin if (rst) begin gnt <= '0; mask <= '1; end else begin if (!u) gnt <= fix; else gnt <= pick; if (pick != '0) mask <= ~((pick << 1) - 1'b1); end end endmodulea01_never.sv(attack, stopped atpostsynth): Never grant: nobody is served when someone requests.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); always_ff @(posedge clk) gnt <= '0; endmodulea02_everyone.sv(attack, stopped atpostsynth): Grant every requester: two clients hold the grant at once.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); always_ff @(posedge clk) gnt <= rst ? '0 : req; endmodulea03_zero.sv(attack, stopped atpostsynth): Always grant client 0: a grant to a client that does not ask, and the others starve.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); always_ff @(posedge clk) gnt <= rst ? '0 : 1; endmodulea04_fixed.sv(attack, stopped atpostsynth): Fixed priority, the lowest requester wins: every cycle is legal, but a persistent high requester starves.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); always_ff @(posedge clk) gnt <= rst ? '0 : (req & (~req + 1'b1)); endmodulea05_ring.sv(attack, stopped atpostsynth): A free-running token ring that ignores the requests: it grants clients that do not ask.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] tok; always_ff @(posedge clk) begin if (rst) begin tok <= 1; gnt <= '0; end else begin tok <= (tok << 1) | (tok >> (N - 1)); gnt <= tok; end end endmodulea06_tdma.sv(attack, stopped atpostsynth): Time division: a token ring gated by the requests is fair but idles while someone waits.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] tok; always_ff @(posedge clk) begin if (rst) begin tok <= 1; gnt <= '0; end else begin tok <= (tok << 1) | (tok >> (N - 1)); gnt <= tok & req; end end endmodulea07_late.sv(attack, stopped atpostsynth): A correct round-robin decision delivered one cycle late: it answers the previous cycle's requests.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] mask, mreq, pick; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end logic [N-1:0] q; always_ff @(posedge clk) begin if (rst) begin gnt <= '0; q <= '0; mask <= '1; end else begin q <= pick; gnt <= q; if (pick != '0) mask <= ~((pick << 1) - 1'b1); end end endmodulea08_sticky.sv(attack, stopped atpostsynth): A sticky round-robin: the priority stays with the granted client, so a persistent requester keeps it.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] mask, mreq, pick; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end always_ff @(posedge clk) begin if (rst) begin gnt <= '0; mask <= '1; end else begin gnt <= pick; if (pick != '0) mask <= ~(pick - 1'b1); end end endmodulea09_rotate_pow2.sv(attack, stopped atpostsynth): Rotating priority whose counter wraps at the next power of two: right at N = 8, wrong at N = 3 and 5.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); localparam int PW = (N > 1) ? $clog2(N) : 1; logic [PW-1:0] p; logic [2**PW-1:0] reqp, pickp; logic [PW:0] s; logic [PW-1:0] idx; logic [N-1:0] pick; logic found; always_comb begin reqp = '0; reqp[N-1:0] = req; pickp = '0; found = 1'b0; s = '0; idx = '0; for (int k = 0; k < N; k++) begin s = p + k; idx = (s >= N) ? s - N : s; if (!found && reqp[idx]) begin pickp[idx] = 1'b1; found = 1'b1; end end pick = pickp[N-1:0]; end always_ff @(posedge clk) begin if (rst) begin gnt <= '0; p <= '0; end else begin gnt <= pick; p <= p + 1'b1; end end endmodulea10_mealy_last.sv(attack, stopped atpostsynth): A correct registered grant behind a combinational output that copies the requests whenever they change: every snapshot is right, the wire is not.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] mask, mreq, pick; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end logic [N-1:0] g, last; always_ff @(posedge clk) begin last <= req; if (rst) begin g <= '0; mask <= '1; end else begin g <= pick; if (pick != '0) mask <= ~((pick << 1) - 1'b1); end end assign gnt = (req == last) ? g : req; endmodulea11_noreset.sv(attack, stopped atpostsynth): A round-robin whose grant register has no reset: out of reset it still shows its power-up value or its last grant.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] mask, mreq, pick; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end always_ff @(posedge clk) begin gnt <= pick; if (rst) mask <= '1; else if (pick != '0) mask <= ~((pick << 1) - 1'b1); end endmodulea12_stale_mask.sv(attack, stopped atpostsynth): A mask round-robin that forgets to update the mask on the wrap-around grant: a requester starves.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] mask, mreq, pick; logic wrap; always_comb begin mreq = req & mask; wrap = (mreq == '0); pick = !wrap ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end always_ff @(posedge clk) begin if (rst) begin gnt <= '0; mask <= '1; end else begin gnt <= pick; if (pick != '0 && !wrap) mask <= ~((pick << 1) - 1'b1); end end endmodulea14_mealy_rr.sv(attack, stopped atpostsynth): A combinational round-robin with the mask registered, no output register: the grant moves with the requests within a cycle.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] mask, mreq; always_comb begin mreq = req & mask; gnt = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end always_ff @(posedge clk) begin if (rst) mask <= '1; else if (gnt != '0) mask <= ~((gnt << 1) - 1'b1); end endmodulea15_half_rate.sv(attack, stopped atpostsynth): A round-robin that arbitrates every other cycle: requesters wait while nobody is granted.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [N-1:0] mask, mreq, pick; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); end logic t; always_ff @(posedge clk) begin if (rst) begin gnt <= '0; mask <= '1; t <= 1'b0; end else begin t <= !t; gnt <= t ? pick : '0; if (t && pick != '0) mask <= ~((pick << 1) - 1'b1); end end endmodulea17_timebomb.sv(attack, stopped atpostsynth): A correct round-robin for 4095 cycles after a reset and fixed priority after that: only a long run without a reset shows it.the design, with its comments left out
module arbiter #(parameter int N = 8) ( input logic clk, rst, input logic [N-1:0] req, output logic [N-1:0] gnt ); logic [11:0] age; logic [N-1:0] mask, mreq, pick, fix; always_comb begin mreq = req & mask; pick = (mreq != '0) ? (mreq & (~mreq + 1'b1)) : (req & (~req + 1'b1)); fix = req & (~req + 1'b1); end always_ff @(posedge clk) begin if (rst) begin gnt <= '0; mask <= '1; age <= '0; end else begin if (age != '1) age <= age + 1'b1; if (age == '1) gnt <= fix; else gnt <= pick; if (pick != '0) mask <= ~((pick << 1) - 1'b1); end end endmodule
Spec.lean, verbatim (171 lines)
import SvGolf.TaskReact
/-!
# Task `arbiter`: a fair N-client arbiter
# (TRUSTED text, final, decided 2026-11-07; written 2026-11-05, txtask-v2's rules 2026-11-06; the reactive kind `ReactTask`, `SvGolf/TaskReact.lean`)
Module (port order as written; `N` is the module's parameter):
```systemverilog
module arbiter #(parameter int N = 8) (
input logic clk, rst,
input logic [N-1:0] req,
output logic [N-1:0] gnt
);
```
## What the statement says (`Statement sem`)
For every `N` with `1 ≤ N` and `N·N < 2^31`, the design `sem N`:
1. has exactly the ports above, and no two declarations of one name (`Interface`);
2. is clocked by `clk` alone with no asynchronous reset, never reads `clk` as data (`ClockedBy clk
none`), has no combinational path from an input port to an output port (`MooreOut`), and
terminates from every power-up state under every schedule and known stimulus (`TerminatesPU`);
3. has no construct that can create an `x` from known operands (`XSafe`, txtask-v2's rule 3);
4. from EVERY power-up state (every register and variable, 2-state ones included, starts at some
0/1 value, one value per signal), under every schedule, on every known stimulus, in every
completed run, at every RESET RELEASE `c1` (the entry `c1 - 1` asserts `rst`) and for every list
`x0 :: xs` of request vectors that the entries `c1 - 1, c1, c1 + 1, …` drive (the reset entry,
then the entries with `rst` = 0), the snapshots `c1 - 1, c1, c1 + 1, …` show known grant vectors
`y0, ys[0], ys[1], …` with
* **G0, reset**: `y0 = 0` (no grant comes out of reset);
* **G1, mutual exclusion**: every `ys[j]` has at most one bit set;
* **G2, no spurious grant**: a bit of `ys[j]` is set only if the same bit of `xs[j]` is;
* **G3, work conservation**: `xs[j] ≠ 0` implies `ys[j] ≠ 0`;
* **G4, bounded fairness** with `K = N - 1`: if requester `i` requests at all `N` entries
`j, …, j + N - 1` of the segment, then `ys[j + k]` grants `i` for some `k ≤ N - 1`.
The grant in snapshot `c` answers the request of entry `c` (the one the edge of cycle `c`
samples); by `MooreOut` it is what the requesters see on `gnt` for the whole next clock period,
while they drive entry `c + 1`. So a requester learns of its grant one period after it asserts its
request: a REGISTERED (Moore) arbiter, like verilog-axis `arbiter.v` (`grant_reg`), or a Mealy one
(OpenTitan `prim_arbiter_tree`) behind one output register.
## Decided 2026-11-05 (the study's defaults; reasons in `README.md`)
* Moore observation (`MooreOut`), from the kind.
* Safety (G1 to G3, per cycle: the ghost state is `Unit`) and bounded response (G4) with the bound
`K = N - 1` fixed here, not declared by the golfer: no design can beat it (`bound_tight`, among the
task's kernel-checked refutations, `tests/arbiter/negative/`), so a declared `K` would be a dead column.
* No environment assumption beyond reset and known inputs.
* "Any fair" policy: the statement pins fairness, not a grant order.
* Scored at `N = 8` (`task.json`).
## Why it cannot be satisfied vacuously or gamed (the kind's list, `SvGolf/TaskReact.lean`, plus)
* **Request-ignoring designs.** The free-running token ring that is SYNTCOMP-minimal for the
simple and round-robin arbiter families grants without requests (G2), the time-sliced ring
gated by the requests wastes slots (G3), grant-everyone breaks G1, never-grant breaks G3 and G4,
fixed priority starves (G4). The task's refutations (`tests/arbiter/negative/`) refute four of them
by kernel-evaluated runs.
* **The Mealy phantom.** Register `last <= req` and drive `gnt = (req == last) ? g : req` from a
correct registered grant `g`: every snapshot shows `g`, while in silicon `gnt = req` whenever
`req` changes, which breaks mutual exclusion. `MooreOut` rejects it (`mealy_refuted`).
* **Unknown and unreset values** (rules 2 and 3). The claims hold from every power-up state, so a
design may keep an unreset register only where its value does not matter. A correct round-robin
behind `if (~u)` on a never-reset, self-holding `u` fails G4 from the power-up `u = 0`
(`xopt_refuted`); behind `if (&u)` on a never-reset 2-state rotating ring `u`, from `u` all ones
(`ring_refuted`; ls-sv's `x` start would have made `u` 0 for ever); and with a flag set at the
first reset edge from the pre-reset `&u`, from `u` all ones (`reset_edge_refuted`). These runs
are ls-sv's: that the scored netlist agrees with them on defined values (obligation C) is
SAMPLED by the post-synthesis check, not proved. Yosys keeps such a register as a flop that
powers up to some value, and the checker refuses a never-loaded one (`u <= u`) where the pinned
flow removes its flip-flop while reads of it remain (it resolves each read separately).
* **Never-reset grant flops.** G0 requires a KNOWN zero at every reset snapshot, from every
power-up.
## What it does NOT pin, on purpose
* which requester wins (any policy meeting G4 is legal: round-robin pointer, mask, rotating
priority, matrix/LRU), and the state encoding (one-hot mask, binary pointer, matrix);
* the grant of a requester that drops its request before `N` consecutive requests: the reference
round-robin itself starves a requester that asks at every other entry (measured, `README.md`),
so a stronger form would reject every round-robin;
* anything while `rst` = 1 except the reset snapshot, and anything before the first reset.
-/
namespace SvGolf
open LeanModels.Sv
namespace Tasks.Arbiter
/-- At most one bit of `g` is set (one-hot or zero). -/
def AtMostOne {N : Nat} (g : BitVec N) : Prop :=
∀ i j, g.getLsbD i = true → g.getLsbD j = true → i = j
/-- **One cycle of arbitration**: `gnt` grants at most one requester (G1), only a requester of
`req` (G2), and someone whenever anyone requests (G3). Together: `gnt = 0` if `req = 0`, else `gnt`
is one bit of `req`. -/
def Grants {N : Nat} (req gnt : BitVec N) : Prop :=
AtMostOne gnt ∧ (∀ i, gnt.getLsbD i = true → req.getLsbD i = true) ∧ (req ≠ 0#N → gnt ≠ 0#N)
/-- **The task.** The ghost state is trivial (the safety property is per cycle); the obligations
are the requesters `i < N`: requesting triggers, being granted responds. -/
def task : ReactTask Nat where
inRange N := 1 ≤ N ∧ N * N < 2 ^ 31
clk := "clk"
rst := "rst"
inputs N := [("req", N)]
outputs N := [("gnt", N)]
atReset N := fun (g, ()) => g = 0#N
Ghost _ := Unit
ginit _ := ()
gnext _ _ _ _ := ()
safe _ _ := fun (r, ()) (g, ()) => Grants r g
Obl N := Fin N
trig _ i := fun (r, ()) => r.getLsbD i.val = true
resp _ i := fun (g, ()) => g.getLsbD i.val = true
/-- **The challenge statement**: the task at every `N` in range with the response bound `N - 1`
(G4: `N` consecutive requests are granted at least once). -/
abbrev Statement (sem : Nat → LeanModels.Sv.Design2) : Prop :=
task.Statement sem (fun N => N - 1)
/-! ## Sanity checks on the statement's data (proved; they add nothing to the trusted base) -/
/-- The scoring point `N = 8` and the probe points are in range; `N = 0` is not, nor any `N` with
`N·N ≥ 2^31` (a matrix arbiter declares `N·N` bits). -/
example : task.inRange 1 ∧ task.inRange 2 ∧ task.inRange 3 ∧ task.inRange 8 ∧
¬ task.inRange 0 ∧ ¬ task.inRange 46341 := by
simp [task]
/-- The port names are distinct. -/
example : ["clk", "rst", "req"].Nodup ∧ "gnt" ∉ ["clk", "rst", "req"] := by decide
/-- `Grants` with the bit indices bounded by `N` (bits at `i ≥ N` read `false`): decidable on
concrete vectors. -/
theorem grants_iff {N : Nat} {r g : BitVec N} : Grants r g ↔
(∀ i, i < N → ∀ j, j < N → g.getLsbD i = true → g.getLsbD j = true → i = j) ∧
(∀ i, i < N → g.getLsbD i = true → r.getLsbD i = true) ∧ (r ≠ 0#N → g ≠ 0#N) := by
constructor
· rintro ⟨h1, h2, h3⟩
exact ⟨fun i _ j _ hi hj => h1 i j hi hj, fun i _ hi => h2 i hi, h3⟩
· rintro ⟨h1, h2, h3⟩
exact ⟨fun i j hi hj => h1 i (BitVec.lt_of_getLsbD hi) j (BitVec.lt_of_getLsbD hj) hi hj,
fun i hi => h2 i (BitVec.lt_of_getLsbD hi) hi, h3⟩
/-- A one-hot grant of a requester is a legal arbitration; so is no grant without requests. -/
example : Grants (0b1011#4) (0b0010#4) ∧ Grants (0#4) (0#4) :=
⟨grants_iff.2 (by decide), grants_iff.2 (by decide)⟩
/-- The trivial answers are not legal arbitrations: grant everyone (G1), grant client 0 always
(G2), never grant (G3). -/
example : ¬ Grants (0b11#2) (0b11#2) ∧ ¬ Grants (0b00#2) (0b01#2) ∧ ¬ Grants (0b01#2) (0b00#2) :=
⟨fun h => absurd (grants_iff.1 h) (by decide), fun h => absurd (grants_iff.1 h) (by decide),
fun h => absurd (grants_iff.1 h) (by decide)⟩
/-- **Fixed priority starves** (G4 at `N = 2`, `K = 1`): both clients request twice in a row and
client 0 is granted both times, so the segment's guarantee fails for client 1. -/
example : ¬ task.Guar 2 1 [(0b11#2, ()), (0b11#2, ())] (0#2, ()) [(0b01#2, ()), (0b01#2, ())] := by
rintro ⟨-, -, hr⟩
obtain ⟨i, y, hi, hy, hg⟩ := hr (⟨1, by decide⟩ : Fin 2) 0 (by decide) (fun i x hi hx => by
have : i = 0 ∨ i = 1 := by omega
rcases this with rfl | rfl <;> (have hx' := Option.some.inj hx; subst hx'; exact rfl))
have : i = 0 ∨ i = 1 := by omega
rcases this with rfl | rfl <;> (have hy' := Option.some.inj hy; subst hy'; exact Bool.false_ne_true hg)
end Tasks.Arbiter
end SvGolf
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.arbiter.Spec | task statement | 171 | 21c83d684dee |
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.