# svGolf

> A competition for SystemVerilog hardware: write a circuit (combinational, or clocked on a clocked task such as `arbiter`), prove in Lean 4 that it meets a task's trusted statement, and get scored by a pinned flow. The one ranked number is area x time on the sky130 cell library (flow A0'): the cell area in um^2 (flip-flops included) times the critical-path delay (on a clocked task, the register-to-register clock period, times the latency in cycles where the task has one), in um2*ns, lower is better. Par, Record and Under par use it; to beat par is to be accepted with a smaller area x time than the task's best proved reference. The Pareto front of area and time, area in NAND2 gate equivalents (GE), depth in gates and the other flows are exploration columns. [Reproduce a score](reproduce.html) says how to get the same numbers. sky130 is the default; the site can also show every golf score on ASAP7, a predictive 7 nm library (the same netlists weighed by score/ppa.py --pdk asap7; leaderboard.py board --pdk asap7; data/site.json `asap7`; [the rules](rules.html#the-asap7-view) say how).

All paths below are relative to this file. There is no submission server. Records are made locally with leaderboard/leaderboard.py (written to leaderboard/data/<task>/, the directory a pull request adds) and handed in by pull request to https://github.com/thomasnormal/svgolf. Par, the bar to beat, is a task's best proved reference; the records of svgolf-reference are the references, not entries. [llms-full.txt](llms-full.txt) is the whole proving guide in plain text.

## Step 0, once per machine

Install elan (it installs the Lean toolchain that lean-toolchain pins, leanprover/lean4:v4.33.0-rc1), Yosys 0.53 with yosys-abc, Verilator 5, a C++ compiler and make (the post-synthesis check compiles Verilator's model of the netlist) and Python 3.12. Then, from the root of a clone:

```bash
git clone https://github.com/thomasnormal/svgolf
cd svgolf
python3.12 -m pip install -r requirements.txt   # pyslang==11.0.0
lake build                                      # the trusted Lean and the checker's evaluator
python3.12 score/ppa.py --fetch-liberty         # the pinned sky130 liberty, checked by its hash
```

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

## The commands (task `add`; any task: tasks/<name>)

```bash
# the golfing inner loop: the ranked area and delay in about 2 s, no Lean (--path: the critical path)
python3.12 score/ppa.py solution.sv --task tasks/add --no-mapped --path
# a clocked task (arbiter) is weighed through the clocked flow, its time the period:
# python3.12 score/ppa.py solution.sv --task tasks/arbiter --seq --path
# 1. no proof needed: every stage but the proof; never accepts; exits 0 when every stage passed
python3.12 check.py tasks/add solution.sv --unproved
# on a task with a latency (matmul, sorter), --unproved needs --latency n, the cycles you mean to claim (the n of your `-- svgolf-latency: n` line; check.py refuses the run without it), e.g. par's on matmul:
# python3.12 check.py tasks/matmul solution.sv --unproved --latency 4
# 2. the real check: prints "accepted": true; its post-synthesis check is LIGHT by default (a subset of the vectors, for local feedback), so stderr also says "accepted, but the check was INCOMPLETE ... rerun with --postsynth full": expected, since step 3 runs the full one itself
python3.12 check.py tasks/add solution.sv Solution.lean
# 3. record it (the whole check again, full mode, OS sandbox); --data-dir DIR for a private trial
python3.12 leaderboard/leaderboard.py add --task add --player YOUR_HANDLE --assisted-by "TOOL OR MODEL" --sv solution.sv --lean Solution.lean
```

score/ppa.py runs the source gate and the pinned flow and prints ppa.area_um2_sky130 and ppa.delay_ps_sky130 (their product is the ranked number). It does not check the banlist, the 4-state rules, whether ls-sv can read the design, the post-synthesis simulation or the task's function, and needs no proof: step 1 must still pass before you prove. Every run of check.py that reaches its ppa stage ends its stderr with the ranked headline `ranked (sky130 A0'): <area> um^2 x <delay> ps = <axt> um2*ns; par <par axt> (<par ref>)`, or `ranked: liberty missing, run python3.12 score/ppa.py --fetch-liberty`.

## The Lean contract

A submission is two files, here solution.sv (the task's exact module header) and Solution.lean; names and paths are free. The checker extracts the .sv itself and generates the trusted module Submission.Design:

```lean
import LeanModels.Sv.Ingest2
import tasks.add.Spec

namespace Submission
load_design_sv2 design from "<the envelope of your .sv>"
abbrev Goal : Prop := SvGolf.Tasks.Add.Statement design.sem
end Submission
```

Solution.lean must `import Submission.Design` and, inside `namespace Submission`, prove `theorem solution : Goal` (that is `theorem Submission.solution : Submission.Goal`); Goal unfolds to the task's statement of the design, `SvGolf.Tasks.Add.Statement Submission.design.sem` for add. The module name, the import and the theorem are fixed. On a task with a latency (`matmul` and `sorter`), Goal takes the solution's latency: Solution.lean also defines `lat` (cycles, one Nat per parameter, in the task's order), proves `theorem solution : Goal lat`, which unfolds to the statement of `design.sem lat` and `lat <scoring point> = n`, and declares that n in exactly one line `-- svgolf-latency: n`; the score's time is n times the clock period. Allowed imports: Init, Std, Lean, LeanModels.Sv.*, SvGolf.*, tasks.*, and Mathlib with its packages; axioms: the task's allowed_axioms (normally propext, Classical.choice, Quot.sound); no sorry, native_decide or bv_decide. Every task ships a complete reference pair under tasks/<name>/reference/.

## Pages

- [Tasks and scorecard](index.html)
- [The tutorial: your first submission, step by step](tasks/_example/index.html#first-submission)
- [Rules, checker stages, scoring, leaderboard](rules.html)
- [Reproduce a score: the pinned tools, files and commands](reproduce.html)
- [How to prove a task](proving.html) ([plain text](llms-full.txt))
- [Everything the checker refuses](refusals.html)
- [Roadmap](roadmap.html)
- [About svGolf](about.html)

## Tasks

- [Bitwise AND](tasks/_example/index.html) (`_example`): A toy task that runs the whole pipeline: y = a & b on N bits. Scored at N = 16; par 28.03 um2*ns (band: 100.096 um^2, 280 ps), record 28.03 um2*ns; no submissions yet. Statement: `SvGolf.Tasks.Example.Statement`. Data: [data/tasks/_example.json](data/tasks/_example.json). The statement as named properties: [tasks/_example/properties.html](tasks/_example/properties.html).
- [N-bit adder](tasks/add/index.html) (`add`): Add two N-bit numbers and a carry in, with logic gates only. Scored at N = 16; par 1202 um2*ns (add_n: 460.4416 um^2, 2611 ps), record 1176 um2*ns; best submission 474.2048 um^2, 2479 ps. Statement: `SvGolf.Tasks.Add.Statement`. Data: [data/tasks/add.json](data/tasks/add.json). The statement as named properties: [tasks/add/properties.html](tasks/add/properties.html).
- [N-bit multiplier](tasks/mul/index.html) (`mul`): The full 2N-bit product of two unsigned N-bit numbers, with logic gates only. Scored at N = 16; par 51 311 um2*ns (mul_tree_h: 8563.2128 um^2, 5992 ps), record 42 530 um2*ns; best submission 7961.3856 um^2, 5342 ps. Statement: `SvGolf.Tasks.Mul.Statement`. Data: [data/tasks/mul.json](data/tasks/mul.json). The statement as named properties: [tasks/mul/properties.html](tasks/mul/properties.html).
- [Carry-less multiplier](tasks/clmul/index.html) (`clmul`): Multiply two polynomials over GF(2): ANDs and XORs, no carries. Scored at N = 16; par 3821 um2*ns (clmul_n: 3429.5392 um^2, 1114 ps), record 3821 um2*ns; no submissions yet. Statement: `SvGolf.Tasks.Clmul.Statement`. Data: [data/tasks/clmul.json](data/tasks/clmul.json). The statement as named properties: [tasks/clmul/properties.html](tasks/clmul/properties.html).
- [AES S-box](tasks/aes_sbox/index.html) (`aes_sbox`): The byte substitution of AES (FIPS 197): 8 bits in, 8 bits out. Scored at the one fixed size; par 3833 um2*ns (sbox_bp: 892.1056 um^2, 4297 ps), record 2858 um2*ns; best submission 890.8544 um^2, 3208 ps. Statement: `SvGolf.Tasks.AesSbox.Statement`. Data: [data/tasks/aes_sbox.json](data/tasks/aes_sbox.json). The statement as named properties: [tasks/aes_sbox/properties.html](tasks/aes_sbox/properties.html).
- [IEEE 754 division, every format](tasks/fdivp/index.html) (`fdivp`): One divider for every exponent width and precision, rounded to nearest even. Scored at W = 5, P = 11; par 340 950 um2*ns (fdivp_srt: 12356.8512 um^2, 27592 ps), record 340 950 um2*ns; no submissions yet. Statement: `SvGolf.Tasks.FdivP.Statement`. Data: [data/tasks/fdivp.json](data/tasks/fdivp.json). The statement as named properties: [tasks/fdivp/properties.html](tasks/fdivp/properties.html).
- [Fair N-client arbiter, clocked and reactive](tasks/arbiter/index.html) (`arbiter`): At most one grant per cycle, only to a requester, someone whenever anyone requests, and a requester that asks N cycles in a row granted within them. Clocked: weigh it with `score/ppa.py --seq`; its time is the register-to-register clock period, one decision per cycle. Scored at N = 8; par 2175 um2*ns (rr_mask: 769.488 um^2, 2826 ps), record 2175 um2*ns; no submissions yet. Statement: `SvGolf.Tasks.Arbiter.Statement`. Data: [data/tasks/arbiter.json](data/tasks/arbiter.json).
- [N × N matrix multiplication, clocked](tasks/matmul/index.html) (`matmul`): Multiply two signed N × N matrices, wrapping at AccW bits, behind a start/done handshake. Clocked: weigh it with `score/ppa.py --seq`; its time is the register-to-register clock period, times its latency in cycles (the solution's `-- svgolf-latency: n` line); `check.py --unproved` needs `--latency n` on it (par's n: 4). Scored at N = 4, W = 8, AccW = 32; par 3 729 636 um2*ns (matmul_g1: 87173.6064 um^2, 42784 ps), record 2 276 474 um2*ns; best submission 241920.7712 um^2, 9410 ps. Statement: `SvGolf.Tasks.Matmul.Statement`. Data: [data/tasks/matmul.json](data/tasks/matmul.json). The statement as named properties: [tasks/matmul/properties.html](tasks/matmul/properties.html).
- [Streaming sorter, clocked](tasks/sorter/index.html) (`sorter`): N unsigned W-bit values in, one per cycle; the same values out in ascending order, one per cycle. Clocked: weigh it with `score/ppa.py --seq`; its time is the register-to-register clock period, times its latency in cycles (the solution's `-- svgolf-latency: n` line); `check.py --unproved` needs `--latency n` on it (par's n: 16). Scored at N = 8, W = 8; par 222 540 um2*ns (sorter_ins: 5512.7872 um^2, 40368 ps), record 157 015 um2*ns; best submission 4754.5600 um^2, 33024 ps. Statement: `SvGolf.Tasks.Sorter.Statement`. Data: [data/tasks/sorter.json](data/tasks/sorter.json). The statement as named properties: [tasks/sorter/properties.html](tasks/sorter/properties.html).

## Data

- [data/site.json](data/site.json): every task's par, best submission and counts
- data/tasks/<task>.json: leaderboard.py's board of every record (`board`), the players' board (`submissions_board`), references, baselines, rejected designs, the statement's import closure and its properties (`properties`: each one's Lean declaration, file, line and plain-English text)