Rules

Rules #

Universal task correctness (decided 2026-11-05). A candidate implementation is valid if, for every admissible initial state, external input sequence, and nondeterministic choice permitted by its execution semantics, the resulting observable behaviour satisfies the task specification.

• The specification may permit several outputs or execution traces, including approximate results.
• Nondeterministic choices need not produce identical outcomes; each must only produce a permitted one.
• The proof must account for every admissible choice (an unknown value's 0/1 resolution, the order of simultaneous events, how independent clocks interleave, how a synchronizer's metastable bit resolves) and preserve the correlations and timing constraints the semantics fixes (one power-up value per register, inputs stable around their own clock edge).
• A failed or incomplete proof does not establish validity: a timeout, a refusal or an unsupported construct is a rejection, never a pass.

So whatever value or order the synthesizer, the silicon or the environment picks is one of the cases already proved, and the real behaviour refines the proof.

• Proofs are symbolic and parametric. When a task is n-bit, the statement covers every N in the task's range, and so must the proof: induction on bit indices, BitVec algebra, the ls-sv proof layers. bv_decide is NOT supported for now: it runs an external SAT solver, which the checker declines to sandbox (decided 2026-11-01; "bv_decide" below). Use decide +kernel, omega, simp or a symbolic argument. native_decide is banned. sorry and admit never pass (the axiom check rejects sorryAx).

• Proof time limit. 300 s of CPU time of the Lean process for every task (decided 2026-11-06), with a wall-clock backstop of 5 times it, 1500 s. It is 300 because CPU seconds count every elaboration thread: the limit was 120 wall-clock seconds, and an honest proof uses about 2.3 CPU seconds per wall-clock second ("Proof effort").

• Axioms. Only the task's allowed_axioms (normally propext, Classical.choice, Quot.sound). No new axioms, no extern or implemented_by: an axiom of your own, the axioms native_decide and bv_decide generate, and Lean.ofReduceBool are all rejected.

• Banned operators, per task. A task bans the run-time operator that IS the task, and anything Yosys turns into the same cell: the adder and multiplier tasks ban + - * / % ** (Yosys's alumacc merges + chains into the same $macc cell as *); the divider bans / %. Every task bans run-time / % ** (since 2026-11-06, under the 2026-11-05 ruling below that svGolf disallows a construct where Yosys departs from the standard): a zero divisor, or 0 ** -1, makes an x from KNOWN operands, which ls-sv carries into a decision (the else branch of if (x)) while Yosys builds a defined value there, and with a 2-state destination IEEE itself defines the value (0) and Yosys builds another (tests/clmul/attacks/div_zero_x.sv: the right product everywhere in ls-sv, p[0] flipped in the netlist on one input pair in 2^32, which the post-synthesis vectors miss); score/banlist.py adds them to every task's list (ALWAYS_BANNED) and says why in its message. A task that bans + or - also bans run-time ordering comparisons < <= > >= (decided 2026-11-05): Yosys builds each as its own adder, an $alu, so the banlist rejects every $alu that alumacc builds; equality and comparisons over parameters stay allowed. Constant arithmetic stays allowed: parameter expressions, genvar loops (the step may be i++, i--, i = i + 1, i += 1, i = 1 + i, i = i - 1 or i -= 1; any other step such as i += 2 or i = i + K is refused at the design stage; i = i + 1 reaches the sv_comb tactics as i++, measured: PROVING.md, section 4), index arithmetic over parameters and genvars (a[i+1]), procedural for counters (k++), constant functions, and the size queries $bits(q) and $size(q) of a signal, which do not read it (since 2026-11-07: $bits(q) / $bits(q) is constant).

• One program for both tools (the source gate). The proof is about the design the extractor reads (through slang); the score is about the design Yosys reads. The checker makes them ONE text: it refuses preprocessor directives other than `timescale and `default_nettype none|wire (Yosys predefines SYNTHESIS and YOSYS, slang does not, so `ifdef SYNTHESIS would prove one circuit and score another), attributes (* ... *) (Yosys gives full_case, parallel_case, nosync, ... a synthesis meaning; slang none), comments that Yosys reads as pragmas (// synopsys translate_off, // synopsys full_case, ...), and the unique / unique0 / priority qualifiers (Yosys reads them as full_case/parallel_case, a synthesis don't-care, while ls-sv runs the first matching arm: a unique case that never matches scores 0 GE). It then strips every comment, and the extractor, the banlist and Yosys all read that canonical text (score/srcgate.py).

• No host access (also the source gate). The checker runs untrusted text on the organizer's machine, and the tools it runs read more than the text: Yosys's read_verilog opens the file of a $readmemh / $readmemb itself while it reads the design (measured with the pinned Yosys 0.53: the file's contents become the memory's initial value, so one submitted text scores 9.331 GE with one host file and 0 GE with another, and a file that does not exist is an error). A submission could pull a host file (a hidden salt, an oracle) into the netlist and leak bits of it through its score, and the proof never sees the file. The gate therefore refuses every construct that reaches the host: the memory-file tasks ($readmemh, $readmemb, $writememh, $writememb), the file I/O family ($fopen ... $ferror), process and environment access ($system, $test$plusargs, $value$plusargs, $getenv), the wave and dump writers ($dumpfile, $dumpvars, $dumpports*, the $fsdb* / $shm_* families), the coverage-database, SDF and Annex D file tasks ($coverage_save, $sdf_annotate, $input, $log, $save, ...), and DPI (import "DPI-C", export "DPI-C": native code). It reads slang's syntax tree, not the characters: a comment or a string literal that only NAMES one of them is fine, while a use in a function that is never called, in a generate branch the scoring point does not take, in a module the top does not instantiate or in a parameter initializer is refused all the same. An escaped identifier that begins with $ is refused whatever it spells: Yosys's lexer gives \$readmemh the very name of the system task (and runs it), where slang reads an ordinary identifier (the same trick lets a user function \$clog2 shadow the builtin for one tool and not the other). The console and simulation-control tasks ($display, $write, $finish, ...) and the pure system functions ($clog2, $bits, $signed, ...) stay. The table is HOST_FAMILIES in score/srcgate.py, one row per family. This rule covers the SystemVerilog text. The Lean file is not scanned for #eval, IO, run_cmd, elab or initialize (the shipped references use a local elab and macros, and Lean metaprograms reach IO under many names); it is CONTAINED instead: every process that runs submitted text runs in an operating-system sandbox (see "Sandbox" under "Checking"), and the same sandbox is the second layer under Yosys and Verilator for the constructs the gate would miss. Only the reading of files was ruled on (decided 2026-10-31); the rest of the family (writes, programs, the environment, dumps, DPI) is the register authors' extension of that ruling, awaiting confirmation.

• No x or z value may arise (the 4-state rules). ls-sv, like IEEE 1800 simulation, computes with unknown values: if (x) takes the else branch, a case item or == operand with a z bit never matches a known input. Yosys reads an x/z as a synthesis don't-care: it drops x/z bits from comparisons and resolves an unknown value however it likes. So wherever an x reaches a decision, the proved and the scored circuits can differ, and the player picks where (measured: the complementary items 2'b0z and 2'b1z on {a[0], cin} match no input in ls-sv and EVERY input in Yosys, so the default arm ls-sv runs is dead logic in the netlist, and the scored arms can differ from it on one input pair in 2^32). Every SOURCE of an x or z the checker knows is therefore refused statically, at the parameter points it probes (the scoring point and the task's probe and backstop points; what that leaves open is in "Checker v0 limits", "The x rules are decided at the probed points"):

  • the source gate refuses every x, z or ? digit in a literal (1'bz, 4'b10x0, 'x, 'z), except the wildcard digits of a casez item (z, ?) and of a casex item (x, z, ?), where both tools agree they match anything. No 'x don't-care assignments either;
  • the fourstate stage (score/fourstate.py, at every point the checker probes: the scoring point, then the task's probe and backstop points, since 2026-11-06; before, at the scoring point only, while the statement covers every N in range: the audit's tests/_example/attacks/ undriven_offpoint.sv is undriven only away from N = 16) refuses a parameter or constant expression with unknown bits (1 / 0 is not banned as constant arithmetic, but it is x), a constant index or range outside the declared range, a run-time index whose type lets it leave the declared range (an out-of-range read is x: declare a power-of-two array or narrow the index), and, by Yosys's check, a net that is used but undriven, has conflicting drivers, or sits on a logic loop;
  • a program slang's driver rejects is rejected, analysis errors included (decided 2026-11-01): the banlist front check and the fourstate stage read the errors of slang's ANALYSIS pass, which getAllDiagnostics() omits (score/slangdriver.py, per parameter point): two writers of one variable when one is always_comb/always_ff (an initial block counts), continuous and procedural assignments to one variable, writing an input port, an always without timing control. The verdict uses the slang driver's own severities and cannot be downgraded by a pragma (tests/add/attacks/slang_*.sv). Three x sources have no rule here because nothing can reach them today: run-time /, % and ** (x on a zero divisor or a negative exponent) are banned by every task, through the banlist, since 2026-11-06 (before, clmul, aes_sbox, matmul and sorter admitted them, and no rule refused the x a zero divisor makes: the universal-correctness audit); a function-local variable or return value read before it is assigned needs user function calls, which ls-sv does not have (such a design loads with an Unsupported node and is rejected at the design stage: tests/_example/attacks/fn_uninit.sv); and a latch that is never loaded (always_latch, or always @* assigning a variable on some paths only: x in IEEE, 0 in Yosys) is refused by rule (e) of score/fourstate.py (proc inferred a latch; latch_never.sv, latch_star.sv, rejected at the fourstate stage). A task that admits the first, or an ls-sv PR that adds a latch construct, needs its own rule first.

• A reactive task (kind react-family: the arbiter) is clocked, and these rules come with it (the statement ReactTask, SvGolf/TaskReact.lean; the task's README gives the reasons):

  • one clock, the task's clock, on its rising edge, and a synchronous reset, the task's reset port. The source gate refuses an asynchronous reset, a negedge clock and an iff guard; past it, the pinned loader refuses the last two itself and keeps an asynchronous reset (as alwaysFFR), which the statement's clock discipline (ClockedBy clk none) refuses (a comment in SvGolf/TaskReact.lean still says the loader drops the three; it is out of date, and the next round that edits the trusted text corrects it);
  • Moore outputs (MooreOut): no combinational path from an input port, the reset included, to an output port, so register every output. What a snapshot shows is on the wire for the whole next clock period;
  • every power-up state: the claims hold from every 0/1 power-up value of every register and variable, 2-state ones included, the first reset edge included, so a register that is never reset may only hold a value that does not matter. A register that is never loaded (u <= u), which the pinned flow removes while reads of it remain, is refused at the score stage;
  • no construct that can create an x from known operands (XSafe): the clocked_rules stage checks it before the proof (check/clocked_rules.py);
  • no latency: one decision per cycle, and a -- svgolf-latency: line is refused. The time is the register-to-register period of the clocked flow (score/svgolf_seq.ys, score/ppa.py --seq), the area includes the flip-flops ("Scoring");
  • the post-synthesis check is reactive: at each of the task's post-synthesis points the scored netlist runs from power-up states through the task oracle's segments, each a reset entry and then entries with rst = 0, the last one 70000 entries long without a reset. It rejects unless the netlist equals ls-sv from the all-zeros start, every grant meets the guarantee on the netlist at every seed, and the outputs sampled before each rising edge equal the previous snapshot (the Moore sample).

• A clocked task with a latency (kind tx-family: matmul; stream-family: the sorter) has the reactive task's clock rules and these (the statements TxTask.StatementV2 and StreamTask.StatementV2, txtask-v2, in SvGolf/TaskSeq.lean, final since 2026-11-08 and amended 2026-11-09 before any record of these tasks was published; the tasks' READMEs give the handshakes; some comments of the trusted text predate the amendment and are out of date: SvGolf/TaskSeq.lean twice calls everything before its v2 section txtask-v1, unchanged but for the distinct names, and it and both tasks' Spec.lean call the v2 clock discipline v1's, which is now ClockedBy clk none; the next round that edits the trusted text corrects them):

  • the latency line: Solution.lean declares its latency in exactly one header line -- svgolf-latency: n (a decimal number of cycles, 1 to 999999999) and defines Submission.lat, one Nat per parameter; the goal is the task's Statement design.sem lat ∧ lat p0 = n at the scoring point p0. At other points lat need only be a bound the proof establishes, but at each point of the post-synthesis check the kernel must reduce it to a number (1 to 999999999), which the check uses there (decided 2026-11-08; check.py and the tests call this rule F8; without a proof, check.py --unproved --latency n --latency-at POINT:m);
  • the time is n x the register-to-register period of the clocked flow (score/svgolf_seq.ys, score/ppa.py --seq), the area includes the flip-flops, and the ranked number is area x (cycles x period) ("Scoring"); one submission declares one latency;
  • one clock on its rising edge and a synchronous reset rst; no asynchronous process (the source gate refuses an asynchronous reset, a negedge clock, an iff guard, initial, initializers on state and always_latch; the statement itself refuses an asynchronous reset, ClockedBy clk none, as for the reactive kind, decided 2026-11-09);
  • Moore outputs (rule 1, MooreOutDep): no combinational path from an input port, rst included, to an output port, so register every output (decided 2026-11-09: no input is exempt). This kind has no early Moore check; the proof refuses a Mealy output;
  • every power-up state (rule 2) and no x-creating construct (rule 3, XSafe, checked before the proof by the clocked_rules stage), as for the reactive kind; a never-loaded register is refused at the score stage;
  • the post-synthesis check runs transactions: at each of the task's post-synthesis points, per seed, the scored netlist starts from a random power-up state, takes one reset cycle and then the task oracle's transactions, and it rejects unless every transaction finishes within that point's latency, the task's oracle (good) accepts every payload, and, where the netlist and ls-sv start from the same state (seed 0, all zeros), the netlist equals ls-sv on the flag (done, out_valid) at every cycle and on the payload where it is claimed; from different power-up states ls-sv's own run must meet the statement's claims (L5 of the two tasks' REVIEW.md, fixed 2026-11-08), so a correct design whose flag timing within the latency depends on an unreset register is not refused;
  • the loader expands one generate loop to at most (s + 2)² + 64 iterations at a point, s the sum of the parameter values (PDesign.surfaceFuel): nest one loop per index rather than one flat loop over a product of the parameters, or design.sem is the error design at the points beyond it.

• No other restrictions. Any SystemVerilog that passes these rules and that ls-sv and Yosys accept is fair game. Where ls-sv and Yosys disagree on what the same text means, that is a bug report we want, not an exploit.

• IEEE 1800 is the final arbiter for defined values (decided 2026-11-05). ls-sv follows the standard, never a tool. Where the pinned flow (Yosys and ABC) reads a construct differently from the standard, ls-sv does not change: svGolf disallows that construct in submissions instead (the source gate, the banlist or the fourstate rules, as with the latch and x/z cases above). An unknown is not a third value: an x stands for a bit whose 0/1 value is not known (IEEE 1800 §6.3.1), so a proof must hold for every resolution of it, as formal tools treat x; a simulator's resolution (the else branch of if (x)) is not the semantics. That is the rule; the trusted statement does not state it yet. It is stated over ls-sv's run2, which resolves an x the way a simulator does (if (x) takes the else branch, an x case subject matches nothing), so a design in which an x reaches a decision can satisfy the statement (tests/_example/attacks/undriven_mux.sv and oob_rare.sv do). Until ls-sv's every-resolution semantics lands (planned, not built), validity therefore rests also on the Python x-source rules (the source gate, the banlist and the fourstate stage), which are part of the trusted base, not only defence in depth.

• The post-synthesis check backs this up (the checker's postsynth stage, check/postsynth.py). The proof is about ls-sv's reading of the design, the score about the netlist Yosys built from the same text. After scoring, the checker simulates both at the scoring point on a vector set (the task's whole budget in full mode, a deterministic subset of it in the light mode that is check.py's default for local feedback: see "Checking", "Post-synthesis modes") and rejects the submission unless they agree on every vector:

  • ls-sv's side is design.sem itself, the term the proof is about, run by run2 under both schedules (check/SvEval.lean, compiled as svgolf-eval); the netlist's side is the very gate netlist the score counted (re-read and re-counted to be sure), simulated by Verilator (a C++ model of the netlist and Yosys's gate-cell models, built once per run while ls-sv evaluates, all vectors through one harness run);
  • the vectors are all-0, all-1, walking ones and zeros on every input, the task's corner values, inputs built from every constant the design compares against (so a difference hidden behind a == 16'hBEEF is found), and seeded random vectors; all deterministic, the seed recorded;
  • it fails closed: an ls-sv run that does not complete, an x or z in ls-sv's outputs, an unknown-valued constant in the netlist, a netlist Verilator will not lint, build or run cleanly, a harness that prints the wrong number of rows, the two schedules disagreeing, or different ports all reject;
  • Verilator is a 2-state simulator (decision 10/29: svGolf simulates with Verilator, not Icarus), so the netlist side has no x or z, and this stage cannot see an unknown the netlist computes. It does not need to: Yosys's gate cells (simcells.v) are total Boolean functions, so an unknown can only come from an unknown-valued constant in the netlist (1'hx; scanned for, and such a netlist is rejected on every vector, the report showing what a 2-state model reads) or from an undriven or unconnected net or pin (Verilator's lint runs with -Wall and every warning fatal except DECLFILENAME and UNUSEDSIGNAL: UNDRIVEN, PINMISSING, PINCONNECTEMPTY, MULTIDRIVEN, UNOPTFLAT and the WIDTH family reject). The x/z defences stay where they are: the source gate, the fourstate stage, and ls-sv's own 4-state outputs on the other side of the comparison. What is lost against the 4-state Icarus run it replaced is only a witness for an unknown that the netlist invents from known inputs and driven nets, and Yosys gate cells have none to find;
  • a rejection is written as a bug report: per failing vector the inputs, ls-sv's outputs, the netlist's, and Verilator's reading of the source (also 2-state) as a third opinion, with who agrees with whom. File it: either ls-sv or Yosys is wrong about your design;
  • light and full (WP-C2). The default light mode is a safety net for local feedback: it runs a deterministic SUBSET of the full vectors (a light rejection is always a full rejection) in seconds instead of minutes. Competition and verification runs, leaderboard.py add / verify and tests/run.py use full, which is the whole budget described here. Official artifacts are never light.

  It is sampling, not proof: a difference confined to a rare input region that no constant comparison selects slips through (see "Checker v0 limits"). That is why the known disagreements are refused statically before any proof is tried (the source gate's unique/priority and x/z-literal refusals, which are lexical and hold at every N; the banlist's run-time / % **; the 4-state rules, at the points the checker probes); the post-synthesis check is the backstop for the ones nobody has found yet (a Yosys or ls-sv bug). Measured on tests/<task>/attacks/ with the static rules bypassed (postsynth_alone in tests/expected.json): it rejects a 1'bz/1'bx case item (every vector), complementary z items, x/z constants in == operands, an undriven net and an out-of-range read, whose differences cover most of the inputs (x/z localparams and a constant 1 / 0 it rejects only because ls-sv does not support them and it fails closed); it rejects a z item confined to 2^-28 of the inputs only through the harvested comparison constant (its 0/1 bits; its x/z bits stay free); it PASSES add's zpair_add_rare.sv and _example's oob_rare.sv, whose difference is one input pair in 2^32 selected by a reduction-AND rather than a comparison constant. Before the x/z-literal rule, the 1'bz and 1'bx case items passed every other stage with ls-sv computing the right function (only a proof, which nobody wrote, stood between them and a 0 GE entry). For competition runs, set a secret SVGOLF_POSTSYNTH_SALT so that a player cannot predict the random vectors (the seed is recorded either way, so a run stays reproducible afterwards). A clocked task's check (F5, decided 2026-11-07) runs 8 seeds per point and derives EVERYTHING random in a seed's run from the salt and records it: the stimulus or transaction source, Verilator's randSeed (the netlist's random power-up) and ls-sv's power-up seed:<k>.

• Scoring is score/score.py with the pinned two-stage flow (score/canon.ys, then score/svgolf.ys in a fresh Yosys process) and the pinned table score/ge.json, at the task's scoring point (e.g. N = 16), and score/ppa.py weighs that netlist for the ranked numbers ("Scoring"). The score is a deterministic function of the file as submitted: names, comments, blank lines, whitespace and the file name never change it (stage 1 erases them), while the order of an operator's operands, how a chain of gates is grouped, gate forms and the order of independent statements do, always the same way (measured 2026-11-05: reordering the 113 assigns of aes_sbox's reference moved its delay by up to 17.7%, and moving one generate block of a proved multiplier ahead of another moved its area 12.6% and its delay 41%), because ABC's choices follow the order of the gates it reads. None of these changes what the circuit computes, which IEEE 1800 decides (above); they change only the netlist the pinned flow builds. Trying them is golf (decided 2026-10-31 and 2026-11-05): a golfer searches gate forms and statement orders with the pinned flow before submitting. Not every structural choice survives synthesis, though: ABC re-derives the logic, and some RTL carry-structure choices (a final adder that steps two bits at a time instead of one, in the dry run) score identically to the milli-GE. Score a block standalone with score/score.py before building a proof around it. See "Scoring".

The checker's stages #

check.py runs the stages in this order and stops at the first that refuses; the stage is what a rejection names. The table is the refusal register's text, which calls proglib by its former name, lean-surfaces.

Scoring #

The ranked score is sky130 A0' (decided 11/03): the scored netlist of the pinned flow below, each gate one sky130 cell, repaired by buffering only and weighed with the pinned sky130_fd_sc_hd liberty (score/ppa.py). Its two numbers are the cell area in um^2 (area_um2_sky130, exact as area_e4um2_sky130 in 1e-4 um^2) and the time in ps: the critical-path delay (delay_ps_sky130) of a combinational design, cycles x the register-to-register period of a clocked one (check.py's clocked time_ps; a reactive task makes one decision per cycle, so cycles = 1 and its time is the period). The one ranked number is their product, area x time in um2*ns (decided 11/05; leaderboard/combined.py defines it, exactly, in 1e-4 um^2 x ps), lower is better: par, the record and "under par" use it, and the site's leaderboard orders by it. The Pareto frontier of the two ("Leaderboard"), area in NAND2 gate equivalents (area_mge), depth (ltp -noff) and flow A1' are EXTRA columns for exploring: shown beside the score, ranked by nothing. "Reproduce a score" (the end of this section, and score/PPA.md's section of that name) gives every ranked number again, bit for bit. sky130 is the default; a reader may see the same golf scores on ASAP7 instead ("The ASAP7 view", at the end of this section).

The build ratings use (decided 2026-11-05). Every ranked number, on the boards and on the site, is made, or reproduced bit for bit, by one build of the tools, and it is not a slower portable one:

• Yosys 0.53 (git sha1 53c22ab7c0ced80861c7536c5dae682c30fb5834), the Homebrew build for macOS arm64, compiled by clang++ 17 with -O3 (version line Yosys 0.53 (git sha1 53c22ab7c0ced80861c7536c5dae682c30fb5834, clang++ 17.0.0 -fPIC -O3); the yosys binary's sha256 011e094340da48932dd0af17da0846519af24cee7de9ae84c11cc78753ab7732);
• its yosys-abc, ABC 1.01 of 6 May 2025 (UC Berkeley, ABC 1.01 (compiled May 6 2025 05:45:16); sha256 769348bb154a26d5d97cd877d086893b3c6a1c8242343a505025bad62c7fa653);
• the liberty sky130_fd_sc_hd__tt_025C_1v80.lib (sha256 ef34f999d582044cad9c1f4d5422504ae99702ad42baa432d75215476e5d23d5), score/ppa.py (sha256 1ef1b1c1904853711cbed9b3b5e275f333aade8f60361f8bbc61305c98c480ab) and score/ppa_pins.json (sky130_a0_v3, sha256 d66a6086a37a97f5985266057051979fb6a8a3c557d3ef9c42acc1b5e41502d8), with the scripts score/canon.ys (bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b) and score/svgolf.ys (ea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445).

Records made before this score/ppa.py (every record on the board on 2026-11-11) name the earlier file, sha256 912031912c3e3f6790725161753e95415df34846bd8c27dde3eb707747ddbcbe, in their checker files and as ppa_script_sha256. The change between the two adds the ASAP7 view (--pdk asap7, "The ASAP7 view", below) and leaves the sky130 output identical: rescoring all 23 records with this file on 2026-11-11 reproduced every stored sky130 field but that hash. So the records were not made again; leaderboard.py verify prints a note for the changed file, and a note never changes a record's status. The ASAP7 view's numbers come from the same build and the same score/ppa.py, with score/ppa_pins_asap7.json and its five pinned liberty files in place of the sky130 pins and liberty.

The flow is deterministic on that build: the same design text gives the same area, time and netlist on every run (measured 2026-11-05 on 52 designs, 826 runs). Another build of the same Yosys version can break ABC's ties differently (ABC's mapper sorts with the C library's qsort, which is not stable): measured, under YoWASP's WebAssembly Yosys 0.53 (the same git sha1) three fdivp designs moved, by up to 2.9% in delay and 0.3% in area, and the other 49 were identical. So a number you make on another platform may differ slightly from the board's; the same build gives it bit for bit, and you can get as close to it as you like. The binaries and these measurements are data (score/reference_build.json), which the site's rules page and every task's score card read; tests/site/test_rating_build.py checks that this paragraph states them.

python3.12 score/ppa.py SOLUTION.sv --task tasks/<name>        # the ranked score (sky130 um^2, ps) and the GE columns
python3.12 score/score.py SOLUTION.sv --task tasks/<name>      # the GE columns alone, at the task's scoring point
python3.12 score/score.py SOLUTION.sv --top T --param N=16     # anywhere
python3.12 score/score.py --pareto results/*.json              # the (GE area, depth) frontier: an extra view

The sources go through the source gate first and Yosys reads the canonical text (--no-gate skips this for experiments; the result then says "gated": false, and it is not an svGolf score). The pinned flow runs in TWO Yosys processes. Stage 1, score/canon.ys, canonicalizes:

read_verilog -sv <sources>
hierarchy -check -top <top> -chparam N <n>
proc
flatten -noscopeinfo
hierarchy -top <top>
setattr -unset src; setattr -mod -unset src            # source locations
setattr -unset hdlname; setattr -mod -unset hdlname    # original hierarchical names
rename -hide                                           # every non-port name private,
rename -enumerate                                      # then numbered
write_rtlil canon.il

and stage 2, score/svgolf.ys, in a FRESH process, synthesizes and measures:

read_rtlil canon.il
synth -flatten -top <top>
abc -g AND,NAND,OR,NOR,XOR,XNOR,ANDNOT,ORNOT,MUX
opt_clean
stat -json                      # gate counts by type
ltp -noff                       # longest topological path
write_verilog -noattr -noexpr   # the scored netlist, for the postsynth stage

The extra GE columns: area is the gate count weighted by score/ge.json (NAND2 gate equivalents: NOT 0.667, NAND/NOR 1, AND/OR/ANDNOT/ORNOT 1.333, XOR/XNOR 2, MUX 2.333), kept exactly as integer milli-GE (area_mge). Depth is the ltp -noff length, the number of gates on the longest path. Any other cell type (a latch, a flip-flop) makes the score fail. Every result records the Yosys version and the sha256 of both scripts (canon_script_sha256, script_sha256), of the GE table, of the sources and of the canonical RTLIL (rtlil_sha256), so two scores are comparable exactly when the flow's hashes agree. Scoring is deterministic: --repeat 2 synthesizes twice and fails unless the results are identical. --netlist OUT and --rtlil OUT keep the scored netlist and the canonical RTLIL.

Canonical layout: names, comments and layout never reach the score. With one Yosys process, the same circuit scored differently under a different layout: the former 16-bit divider's goalpost gave 2079.747 GE / depth 297 as committed and 2095.076 / 295 with its comments deleted (Yosys's results depend on process-global state, its table of interned names, which the frontend fills with names like $and$design.sv:42$17; stripping the names in the same process does not help, re-reading the design in a fresh one does). Under the two-stage flow, measured over 8 designs (the four tasks' references, the Sklansky, Kogge-Stone and comparison-carry adders), the canon step of tests/run.py checks:

• LAYOUT (leading blank lines, every line joined into one, one token per line, indentation removed, doubled or tabs, a line break after every comma) and RENAMING (every internal signal renamed four ways, generate labels and genvars renamed) leave the canonical RTLIL byte-identical, so the score cannot change. So does renaming a submodule (flattening in stage 1 removes module names);
• ORDER (declarations hoisted, the other module items reversed or shuffled) changes the numbering inside the canonical RTLIL, and with it the order of the gates ABC reads, so it can move the score: not the GE columns of the designs in tests/expected.json's canonical_layout (the canon step checks them), but a flat netlist's and a proved multiplier's, by up to 17.7% and 41% in sky130 delay (measured 2026-11-05; tasks/aes_sbox/README.md, Findings). Like commutation below, it is deterministic and the golfer's;
• COMMUTATION is scored: swapping the operands of every & | ^ ^~ == != && || is the same function but a different expression tree, and ABC starts from the tree it is given (mul_n 1962.576 → 2087.118 GE, the former 16-bit divider's goalpost 2089.081 / 298 → 2046.093 / 300, Sklansky 127.658 / 28 → 124.992 / 30). The score is a function of the design's expression structure: how you write a & b versus b & a is yours to golf. Decision (10/29): accepted as golfable, not normalized. Measured on mul_n at N = 16: one swapped operand moves the score by at most 0.03%; swapping every commutative operand adds 6.3% area at the same depth. Yosys hands ABC the same network in both cases (identical cell-type counts before ABC); ABC's mapping then picks different gate polarities (672 NAND / 269 AND / 0 ORNOT against 298 / 449 / 181), because its tie-breaking follows the order in which it receives the nodes. It is a property of heuristic logic synthesis, not of the pinned flow.

sky130 area and delay, two flows (A0' ranked since 11/03, repaired since 11/04: below). Beside the extra GE columns (area_ge_v1, depth_v1), every check (unless --ppa off) records ppa, the scored netlist weighed with the real sky130_fd_sc_hd liberty (score/ppa.py, score/PPA.md): area_um2_sky130 (um^2, exact: area_e4um2_sky130 is the integer in 1e-4 um^2; the sum of the cell areas of the repaired netlist), delay_ps_sky130 (integer ps: the latest primary-output arrival of a graph-based NLDM static timing analysis, every input driven by the task's input drive (default sky130_fd_sc_hd__buf_8) fed by a 50 ps ramp, every output bit 10 fF, no wires), unit_depth (the GE columns' depth), cells_sky130 and cell_hist_sky130, with the hashes of the liberty, ppa_pins.json, ppa.py and the weighed netlist, setup (the timing setup, its input_drive included), and ppa_version (sky130_a0_v3 since 11/04, below). This is flow A0': the pinned abc -g netlist re-expressed gate for gate as sky130 cells, then repaired by buffering only (no cell resized); no new synthesis and no mapping, so it is a function of the scored netlist (the one the GE columns count) and exact run to run. Beside it, as the sub-object ppa.mapped, flow A1': the canonical RTLIL of the same run mapped by a real abc -liberty run (the pinned Yosys script score/ppa_mapped.ys: Yosys 0.53's default ABC script, every ordinary sky130 cell and drive strength allowed, compound cells, no sizing pass), checked against the scored netlist on a sample of input vectors and weighed by the very same STA: area_um2_sky130_mapped_v1, mapped_delay_sky130_v1 (integer ps), mapped_cells_sky130_v1, mapped_cell_hist_sky130_v1, mapped_levels_sky130_v1, with its own version (ppa_mapped_version sky130_a1_v1) and hashes. A1' is closer to a fabricated chip and more sensitive to the mapper than A0': over the 18 reference and baseline designs of score/tests/ppa/designs.json it is a median 0.93x the repaired A0' in area and 1.04x in delay, and on the four proved multipliers it puts the array multiplier last in area where GE and A0' put it first. A0' is the ranked score (decided 11/03); A1' is an unranked research column; their fields are never swapped silently; the measured tables are in score/PPA.md. The liberty is fetched, not vendored: python3.12 score/ppa.py --fetch-liberty. What they do NOT claim: a fabricated chip's picoseconds (one library, one corner, no wires, a repair rather than timing closure, a 130 nm process; the board ranks the exact integers of this model). The numbers are not noisy. The pinned flow is a deterministic function of the design's text: the same file gives the same area, time and netlist on every run (measured 2026-11-05 on all 52 references, baselines, records and study designs of the ranked tasks, 14 to 16 runs each: serial and six at once, a dozen hash seeds, other temporary and working directories, two checkouts, two locales, other file names, two install paths; every number and every netlist byte equal), so anyone who runs the pinned tools gets the board's number, and there is no tie band and no best-of-k. The pinned tools include the Yosys and ABC BUILD ("The build ratings use", above): another build of Yosys 0.53 can give other numbers on some designs (measured 2026-11-05: three fdivp designs, up to 2.9% in delay), because ABC's mapper breaks ties in the order the C library's sort leaves them. What moves a score is how the circuit is written, and that is the golf: names, comments, blank lines, whitespace and the file name never change it (stage 1 erases them), while the order of an operator's operands, how a chain of XORs or ANDs is grouped and the order of independent statements do, always the same way (commuting operands moved A0' area by up to 11% and delay by up to 32%; moving one generate block of a proved multiplier moved its area 12.6% and its delay 41%), because ABC's choices follow the order of the gates it reads. None of it changes what the circuit computes (IEEE 1800 decides that: "Rules"). Trying gate forms and orders against the pinned flow is legitimate golf. A1' is ONE ABC script, so "mapped" is not "the" mapped result (between ABC scripts the same design's area moves a median 12% and delay 49%; commuting operands moves A1' area up to 15.5% and delay up to 20%). A clocked task's design is weighed through the clocked flow (--seq: its register-to-register period); every combinational idiom tried weighs once it reaches the stage, including run-time selects and shifts, case muxes and constant tables, dividers (score/tests/ppa/idioms.json). Some designs do not reach it: the postsynth stage refuses a netlist whose dead public-named wires are partly undriven or carry an x literal (a known gap of that stage, not of the columns: score/PPA.md, "Known gap"). leaderboard.py pareto lists the frontier of the A0' area and time (an exploration view: the ranked number is their product); pareto --axes area_mge,depth (or area_um2_sky130_mapped_v1,mapped_delay_sky130_v1) prints the Pareto frontier over other columns (opt-in; see "Leaderboard").

sky130 A0' is repaired, and an illegal netlist is rejected (sky130_a0_v2; decided 11/03: sky130 A0' is the ranked score; 11/04: the repair step everywhere, buffering only, and designs that produce illegal netlists rejected). Before it is weighed, the A0' netlist is REPAIRED BY BUFFERING ONLY (ppa.py's own repair, buffer_trees_v1, the pins file's repair and constants sections): every input is driven by the task's input drive (inputs are not free; buf_1 in v2, below for v3), every output BIT is a 10 fF load, and every net over its driver's limits (a load over max_capacitance or past the timing tables, a transition over max_transition), inputs, flop Q nets and nets driving output bits included, gets a balanced tree of buf_1..buf_16 cells sized from the liberty so that it is legal by construction, repeated until nothing is over; the constant tie cell is replicated within its limit; no cell is resized. area_um2_sky130, delay_ps_sky130 (for a clocked task the register-to-register period) and the histogram are those of the REPAIRED netlist; unit_depth and the GE columns are unchanged. A netlist the repair cannot make legal is REJECTED at stage ppa with the net named in the design's words (an input by its port bit, what it drives as output bits); nothing is extrapolated, and no such netlist is known on sky130. The trees are built to the limits, not for speed: a heavy net is slow, and a golfer who wants it faster restructures it. A first version that let ABC buffer and size the netlist (upsize; dnsize) was dropped before it shipped: it never load-checked the tie cell, it rejected loads ABC cannot see (an input or a flop Q wired to many output bits) that a golfer could not fix, and its sizing moved areas +2.4% to +40% unevenly. Details: score/PPA.md, "The repair and the legality check". Measured on every reference and baseline at its scoring point (11/04): all legal, none rejected; three netlists need buffers (fdivp_newton 1, matmul G1 5, the matmul duplication probe 2), so every other area is v1's to the 1e-4 um^2; combinational delays +0.0% to +60.7% (median +5.3%, the driven inputs; sbox_table, whose inputs are heavily loaded, most); matmul's period 48,079 to 10,705 ps (its v1 tables were extrapolated). Every task keeps v1's area and delay orders and Pareto frontiers, except matmul, where the flop-duplication probe (4.4x faster than the reference in v1) is now slower and leaves the frontier; score/PPA.md, "Rankings under sky130_a0_v2".

The input drive is the task's (sky130_a0_v3; decided 11/04: each task chooses the drive that is more realistic or interesting for it). A task's task.json may name input_drive, the cell in front of every primary input: one of the liberty's buffers sky130_fd_sc_hd__buf_1 .. buf_16, its inverters inv_1 .. inv_16, or sky130_fd_sc_hd__dfxtp_1 (a register's Q), the allowlist of score/ppa_pins.json timing.input_drive; absent, the default sky130_fd_sc_hd__buf_8, which every task uses today (their inputs stand for an on-chip bus or a register). Any other name is a task-configuration error (tests/run.py's layout step, an infrastructure error in check.py before any stage runs), never a number. The drive is audited like any driver, and its budget (buf_8 973 fF, buf_1 130 fF) is the load the repair holds an input net to; the record's ppa.setup.input_drive names it, so it is in the record hash, and each task's README states it; a record weighed under another drive than its task's now is not comparable: leaderboard.py verify marks it stale and pareto --axes does not rank it (never a failure). Why buf_8 (MEASURED over the 36 ranked rows under five drives): no drive changes any task's orders or Pareto frontier, and buf_8 adds a small, nearly uniform 73 to 192 ps over an ideal input where buf_1 added 70 to 1,276 ps (sbox_table +61% for one legal 115 fF input load, which the golfer could not buffer away). Measured against v2: every area unchanged, combinational delays -1,084 ps (sbox_table) to +25 ps (median -66), matmul's period 10,705 ps unchanged, and 0 flipped pairs and 0 frontier changes on every task: no ranking moves. score/PPA.md, "The input drive" and "Rankings under sky130_a0_v3".

Loads per edge (sky130_a0_v3, before its release, 11/04). A load pin presents its rise_capacitance to a rising edge and its fall_capacitance to a falling one, as OpenSTA reads them; the STA had loaded every net with the pins' capacitance and was 0.5% to 2.8% off OpenSTA on the references. With the change it equals OpenSTA to 1 fs per arc (score/test_ppa_opensta.py records OpenSTA's numbers). MEASURED on every reference and baseline at its scoring point: every area unchanged, delays -0.30% to +1.32%, no delay order, area x time order or Pareto frontier changes; matmul's period 10,705 to 10,696 ps (one of its five trees is now 2 x buf_4, 6 buffers, the same area), the sorter's 2,510 to 2,523. score/PPA.md, "The per-edge loads".

Reproduce a score. The ranked numbers (A0' area and time) are a pure function of the design text, the pinned flow and tool build, the pins and the task's scoring point and input drive, and each is reproduced bit for bit by one command from the repository's root (Python 3.12 with pyslang, Yosys 0.53 (git sha1 53c22ab7c0ce…) and the yosys-abc beside it on PATH):

python3.12 score/ppa.py --fetch-liberty                     # once: the pinned liberty (sha256 ef34f999…5d23d5) into score/lib/
python3.12 score/ppa.py SOLUTION.sv --task tasks/<name> --no-mapped --json out.json --netlist scored.v --repaired-netlist repaired.v
python3.12 score/ppa.py SOLUTION.sv --task tasks/matmul --seq   # a clocked task
python3.12 score/ppa.py SOLUTION.sv --task tasks/arbiter --seq  # a clocked task, reactive (one decision per cycle)

That is the source gate (score/srcgate.py: the canonical text), Yosys process 1 (score/canon.ys: read, hierarchy -chparam at the task's scoring point, proc, flatten, names and src attributes stripped, write_rtlil), Yosys process 2 (score/svgolf.ys: synth -flatten, abc -g AND,NAND,OR,NOR,XOR,XNOR,ANDNOT,ORNOT,MUX with Yosys 0.53's default ABC script, write_verilog; clocked: score/svgolf_seq.ys), then ppa.py in Python alone: one _1 cell per gate, the buffering repair, the STA with the task's input drive behind a 50 ps ramp and 10 fF per output bit, the legality audit. out.json carries every input's hash (Yosys version, scripts, canonical RTLIL, liberty, pins, ppa.py, the scored and the repaired netlist) and setup. score/PPA.md, "Reproduce a score", lists the tool versions and file hashes, prints both Yosys scripts as filled in for the add reference, shows the ABC scripts, and runs the same steps by hand (srcgate.py, two yosys -s runs, ppa.py --netlist-in); it was tested by following it literally in a scratch copy on the add and aes_sbox references, bit for bit equal to the goldens.

The ASAP7 view #

sky130 is the default; a reader may see the golf scores on ASAP7 instead (decided 2026-11-09). The site's library selector, on the home page and in the header of every page, switches every golf score on the site between the two libraries: the boards and their order, par and the record, the ranks, the score and Pareto charts, each task's score card and each record's overview. The browser remembers the choice (where it allows it) and the address carries it: ?pdk=asap7, and ?pdk=sky130 once a reader has chosen a library, so a copied link shows its recipient what its sender saw; an address without ?pdk= shows each reader their own choice (sky130 until they choose one), and Back and Forward show the reader's latest choice. Without JavaScript the site shows sky130. Both rankings are computed when the site is built, by leaderboard.py's own functions (board --pdk asap7), under the same rules (area x time, par, ties); a score of one library is never compared with one of the other. The records keep their sky130 columns, and nothing else changes with the view: the netlist cards, the scaling view and the task texts stay sky130's, each labelled so in the ASAP7 view; the energy figures are measured on sky130 alone, so the ASAP7 view shows none; GE and depth do not depend on the library.

How ASAP7 is scored. The same scored netlist as sky130's score (the pinned flow does not depend on the library), weighed by score/ppa.py --pdk asap7 (flow A0', asap7_a0_v1): each gate its least-area ASAP7 build, repaired by buffering only, an illegal netlist rejected, no wires, timed by the same static analysis. The area is in um^2 (exact in 1e-5 um^2), the time in ps (the critical-path delay; on a clocked task cycles x the register-to-register period). The library is asap7sc7p5t rev 28 (RVT, typical corner, 0.70 V, 25 C): five liberty files of The OpenROAD Project's OpenROAD-flow-scripts (commit a1a6c3ff, each file with its BSD 3-Clause licence header), fetched at pinned hashes, never vendored (decided 2026-11-10).

What ASAP7 is, and its quirks. ASAP7 is a predictive 7 nm library made for research: it has never been fabricated, so no chip can confirm its numbers, where sky130 is a real 130 nm process. What it forces on the scorer, each choice pinned with its reason in score/ppa_pins_asap7.json:

• it has no MUX, A&!B or A|!B cell, so those gates cost two cells each (an inverter in front);
• its x1 flip-flop has only an inverted output, so every flop gets an inverter forming Q;
• its timing tables start above the smallest input loads, so a read below a table's grid is read at the grid's floor (counted, and a floored delay errs slow) where sky130 rejects the netlist; above a grid the rule is sky130's;
• its timing setup is scaled from sky130's by the same reasons: a 20 ps input ramp, 2.5 fF per output bit, every input driven by BUFx8;
• its tie cells declare no capacitance limit, so one is pinned.

The two libraries order the designs by area almost alike (a sky130 area is 63 to 72 times the ASAP7 one) and differ on time, because they price AND, OR, XOR and MUX against NAND differently; so area x time can reorder close designs, and does on the add and mul boards.

Where the numbers live. Not in the records, whose hash and address would change for a column that is a pure function of the netlist they already pin: in leaderboard/asap7/<task>.json, one entry per design file a task's pages show (every record, proved reference and baseline), bound to its record by the canonical text, the canonical RTLIL, the GE columns, the cycles and the scored netlist. leaderboard.py asap7 --write measures them (a new or re-seeded record needs it), leaderboard.py asap7 checks them, and asap7 --rescore and verify weigh them again and require the same numbers, bit for bit. A design the ASAP7 view would show without a bound entry is "not ranked" or "–" there, never a sky130 number, and the site build warns about it (fatal under --strict, so a published site has the whole view) (leaderboard/README.md, "The ASAP7 view"; score/PPA.md, "ASAP7: an alternative library", has every choice and measurement).

python3.12 score/ppa.py --pdk asap7 --fetch-liberty                                 # once: the five pinned files
python3.12 score/ppa.py SOLUTION.sv --task tasks/<name> --pdk asap7 --no-mapped     # a design's ASAP7 numbers
python3.12 leaderboard/leaderboard.py board --task <name> --pdk asap7               # the ASAP7 board

The build ratings use #

Every ranked number on the board and on this site (the sky130 A0′ area and time, and with them par, the record and under par) is made by ONE build of the tools (decided 2026-11-05). The flow is deterministic on that build: the same design text gives the same area, time and netlist on every run (measured 2026-11-05 on 52 designs, 826 runs: every reference, baseline and record of the ranked tasks and two study designs, 14 to 16 runs each: serial and six at once, a dozen hash seeds, other temporary and working directories, two checkouts, two locales, other file names, two install paths; every number and every netlist byte equal on the rating build). Another build of the same Yosys version can break ABC's ties differently (ABC's mapper sorts with the C library's qsort, which is not stable, and its comparisons leave ties: another C library breaks the ties in another order): under YoWASP's WebAssembly Yosys 0.53 (the same git sha1, its own ABC and C library), 3 of the 52 designs, all fdivp, moved by up to 2.9% in delay and 0.3% in area. So a number you make on another platform may differ slightly from the board's; the same build gives it bit for bit. The build is not pinned to a slower portable one: get as close to it as you like.

The banlist #

score/banlist.py runs two independent checks, both driven by the task's banlist.operators plus the run-time / % ** that every task bans (ALWAYS_BANNED, since 2026-11-06: "Rules"), on the source gate's canonical text:

• the front check (pyslang) elaborates the design at the defaults and at the task's probe and backstop points, walks every run-time root (continuous assigns, procedural blocks, net and variable initializers, port connections, and the bodies of functions called with run-time arguments or whose body reads a signal declared outside the function, including generate branches the scoring point does not take), and flags each banned operator, unary minus, ++/-- and compound assignment whose operands read a run-time value. Parameters, localparams, genvars, enum values and procedural loop counters are constant; a loop counter is recognised by symbol identity (a module signal that shares its name is still run-time), a pre-declared counter (for (k = 0; ...)) only inside its loop, and a counter the loop body writes never. A call is constant only when its arguments are AND its body reads nothing but its own arguments, locals and return variable: function automatic logic [15:0] g(input int k); g = a / 16; endfunction assign q = g(0); divides a at run time (and the backstop cannot see it: Yosys turns / 16 into a shift). The system functions Yosys builds from $add chains ($countones, $countbits, $onehot, $onehot0, $isunknown) are banned with + on a run-time argument, and the array reduction methods .sum() and .product() with + and * (.and(), .or(), .xor() are bitwise and allowed). It reports file:line:col.
• the backstop (Yosys) runs proc; opt at the backstop points and rejects every cell of the banned operators' types ($add $sub $neg $mul $div $divfloor $mod $modfloor $pow, plus $alu $macc $macc_v2 $lcu $fa when any of + - * is banned). Then, in a task that bans + or - (decided 2026-11-05), it runs alumacc on the same design and rejects every $alu $macc $macc_v2 $lcu $fa cell that alumacc built: a run-time ordering comparison ($lt $le $gt $ge) becomes Yosys's adder ($alu) in tasks that ban + and - (a > ~b IS the carry out of a + b; tests/add/baselines/cmp_carry.sv builds a whole adder that way). Equality ($eq $ne $eqx $nex: alumacc builds no $alu for it), comparisons Yosys folds as constants (over parameters and genvars) and a comparator built from & | ^ ~ stay allowed; a task that bans neither + nor - (the divider) keeps every comparison. It reports the cell's source location (a lowered comparison's own). The front check does not look at comparisons.

Note that run-time index arithmetic is arithmetic: a[j + 1] with a signal j, v[sel -: 4] and x[sel*W +: W] build $add/$sub/$mul cells and are rejected under an arithmetic banlist.

Leaderboard #

leaderboard/leaderboard.py (documented in full in leaderboard/README.md; Python 3, standard library only) turns an accepted submission into a record and ranks the records on the sky130 A0' score: the area in um^2 and the time in ps, whose product, area x time, is the one ranked number (decided 2026-11-05; "Scoring"). board and export list the records by it, lowest first (# is the rank, as on the site); the Pareto layer of the two factors is an exploration column beside the GE area and depth, and pareto lists their frontier, also for exploring.

# record it: runs check.py on the pair and writes the record only if it is ACCEPTED, into
# leaderboard/data/add/, the directory a pull request adds (--data-dir DIR: a private trial elsewhere)
python3.12 leaderboard/leaderboard.py add --task add --player YOUR_HANDLE --assisted-by "TOOL OR MODEL" \
    --sv solution.sv --lean Solution.lean
python3.12 leaderboard/leaderboard.py pareto --task add        # the (sky130 area, time) frontier (exploration)
python3.12 leaderboard/leaderboard.py pareto --task add --axes area_mge,depth      # opt-in: the frontier over other columns (here GE)
python3.12 leaderboard/leaderboard.py pareto --task add --axes area_um2_sky130_mapped_v1,mapped_delay_sky130_v1   # ... over flow A1''s columns
python3.12 leaderboard/leaderboard.py board  --task add       # the table by area x time (--format json too)
python3.12 leaderboard/leaderboard.py board  --task add --pdk asap7   # the same on ASAP7 (the site's ASAP7 view)
python3.12 leaderboard/leaderboard.py verify                  # re-verify every stored record
python3.12 leaderboard/leaderboard.py export --out LEADERBOARD.md   # all tasks, Markdown

• There is no submission server yet. add writes a record on your machine and nothing is sent anywhere. A record is self-verifying (verify --full re-runs the whole check), so a pull request carrying the record directory is a possible hand-off, but how records reach a public board is an open decision (PLAN.md, "Open questions for the maintainers"); until it is taken, the board is the maintainers' leaderboard/data, and running add without --data-dir writes into it: leaderboard/data/<task>/ is where the records of a pull request go, and --data-dir DIR keeps a private trial out of it. That directory takes only a record whose check the board ran itself (decided 2026-11-06, the universal-correctness audit): add refuses --from-check (a stored result, never re-run) and --sandbox off there, and a check that did not run in the OS sandbox (sandbox.active); both options stay for a --data-dir trial.
• A record is one JSON file per accepted submission, leaderboard/data/<task>/<record_hash>.json, with the submitted .sv and .lean copied next to it. It holds the player handle, assisted_by, the sha256 of both files and of the source gate's canonical text, the GE columns (score: area_mge in integer milli-GE, depth, gate counts, scoring point), the checker's identity (the svgolf and proglib revisions, svgolf_revision and lean_surfaces_revision, Lean toolchain, Yosys and Verilator versions, the sha256 of the two scripts, the GE table and the checker's files), the proof's facts (axioms, build seconds, code lines, imports, tactics), the optional ppa object (check.py's sky130 columns, flow A0', THE RANKED SCORE, and inside it the optional sub-object mapped, flow A1', see "Scoring"; a record made before them has no such key and stays valid but is not ranked until it is backfilled, and a leaderboard.py from before the ppa key treats a record that has one as corrupt: update every reader first; one from before mapped accepts it) and record_hash, the sha256 of the record's canonical JSON. A clocked task's record (since 2026-11-07; the arbiter's) names the clocked flow (checker.flow "seq": score/svgolf_seq.ys and score/ge_seq.json, whose GE table prices the flip-flop), and its postsynth holds every post-synthesis point with every seed's cycles, power-ups and draw (leaderboard/README.md). add refuses anything check.py does not accept at every stage, a result check.py marks INCOMPLETE (complete: false, with the reasons in incomplete: --no-score, a light post-synthesis check, --no-trusted-build, a --time-limit other than the task's), a result without stages.trusted (the run did not build the trusted modules, so its comparator checked the goal against whatever statement was on disk) and a solution stage that did not run under the task's own CPU limit, or was stopped at a limit. A failed, timed-out or incomplete check establishes nothing ("Rules").
• How a record is verified. verify --offline re-hashes the record and the stored files and rechecks the area arithmetic (milliseconds); plain verify also rescores the stored design with score.py (the source gate and the pinned Yosys flow: seconds, no Lean); verify --full runs check.py again on every stored pair (the cost of the original checks). Records are tamper-evident, not tamper-proof; see leaderboard/README.md for what each level catches.
• Official artifacts are full, and carry the PPA columns. add runs check.py --ppa require --postsynth full (the whole post-synthesis vector budget, and the sky130 columns: an absent pinned liberty is an infrastructure error and a live add writes nothing; add --from-check RESULT.json records a stored result as it is, so a result made by --ppa auto that found no liberty is refused and a result with no ppa key (--ppa off, an older checker) gives a record without the columns, which add says in a NOTE), verify --full rechecks the same way (a record made before the columns: with --ppa off, it needs no liberty; under another Yosys flow the record is stale and the columns are not compared) and compares the columns exactly (verify without --full re-weighs through score/ppa.py when the liberty is there and says so when it is not; --offline checks the columns against the record's own score), and seed-references records in full mode: check.py's own default, light, is for local feedback. A result whose post-synthesis check ran light is REFUSED by add unless add --postsynth light asks for a light record, which the record marks (postsynth.mode: "light", with vectors and full_vectors), add says in its output, and the boards show (light after the record hash, and a footnote). A record without postsynth.mode was made before the modes existed and reads as full. A light record never ranks (decided 2026-11-06): its check was incomplete, so the boards list it under "Not ranked" with that reason, whatever its score; it is a legitimate local record, and not on a separate board.
• assisted_by is the list of tools and AI systems that helped write the design or the proof, as free text (["Claude (Anthropic)", "a proof assistant"]); empty means unassisted. It is the submitter's word, shown next to every entry, and --unassisted ranks only the entries with an empty list. It does not change the ranking otherwise.
• The boards weigh the sky130 score (decided 11/03; its product, area x time, is the ranked number since 2026-11-05). board and export rank the records by the product of the A0' area (ppa.area_e4um2_sky130, exact in 1e-4 um^2) and time (ppa.delay_ps_sky130; a clocked record's score.time_ps, cycles x period) and show the Pareto layer of the two, the GE area and depth as extra columns; pareto lists the frontier of the two. A record is ranked only if it carries the columns and they are comparable: weighed under the current ppa_version, liberty and pins file, and under the task's input drive now. The others are listed as "Not ranked" with the reason; a record without sky130 columns (made before them, or with --ppa off) is not ranked until it is backfilled (checked again under --ppa require). pareto --axes (any of area_mge, depth, area_um2_sky130, time_ps, delay_ps_sky130, unit_depth, cells_sky130, and flow A1''s area_um2_sky130_mapped_v1, mapped_delay_sky130_v1, mapped_cells_sky130_v1, mapped_levels_sky130_v1) is the opt-in n-dimensional frontier over other columns (--axes area_um2_sky130,time_ps is pareto's; ties kept, areas compared as exact integers); records without them, or computed under another ppa_version/liberty/pins (or, for the mapped axes, another ppa_mapped_version/script/pins), are listed as "not shown" with the reason. The boards print no confidence band and need none: the ranked numbers are exact integers and deterministic (the same design text gives the same numbers on every run of the pinned flow), so equal products tie and every other difference ranks.
• Policy: area x time ranks; the Pareto frontier is for exploring; no budget by default. The ranked number is a record's area x time (decided 2026-11-05: par, the record, "under par" and the board's order use it). The board lists the records by it, lowest first; equal products share a rank (1, 1, 3) and are listed as the site lists them (the smaller GE area, then the smaller depth, then the earlier date, then the record hash), so the order is the same on every machine. Each row names its Pareto layer of the two factors, an exploration column (pareto prints layer 1): a record is on the frontier iff no other record is at least as good on both sky130 area and time and strictly better on one; ties are kept. A task author may add a depth budget (leaderboard.depth_budget in task.json, ranking only; or the checker's own scoring.depth_budget, which rejects; on the unit depth): the board then also ranks the best area x time under it and flags the entries over it. No task has one today. Scores are comparable exactly when the pinned flow, the scoring point, the sky130 pins and the task's input drive agree, so the board ranks only records checked under the current ones and lists the rest as "Not ranked" until they are submitted again.

Reference points that are not records, because check.py accepts nothing unproved or with a banned operator (at N = 16: the ranked sky130 A0' area and time from score/tests/ppa/expected_ppa.json, the extra GE area and depth from tests/expected.json):

The proved references are the first records (svgolf-reference, assisted_by ["Claude (Anthropic)"], notes reference solution; leaderboard.py seed-references records them again; the records of leaderboard/data were re-seeded under sky130_a0_v3 on 11/04, with the same design and proof files, so they carry the ranked columns, again on 2026-11-05 after the checker's own files changed, with the same files and numbers, and on 2026-11-06 after the statement change, from the proofs updated for the parameter range, with the same designs and numbers).