svGolf

Golf scores on ASAP7, a predictive 7 nm library: never fabricated, and like sky130's score it counts no wires. sky130, a real 130 nm process, is the default. How ASAP7 is scored, and its quirks.

Prove a circuit correct, then golf its gates.

Each task fixes what a circuit must do in a trusted Lean statement: a function, or on a clocked task a property of every cycle. You write the circuit in SystemVerilog, prove in Lean that it meets the statement for every width the task allows, and the checker scores the circuit by area × time (on a clocked task, the time is the clock period, times the latency in cycles where the task has one). Lower is better.

Start with the tutorial Read the rulesThe proving guideThe repository

The course

Tasks

sky130: SkyWater's open 130 nm process, the default.ASAP7: a predictive 7 nm library, never fabricated. How it is scored

Par is the best proved reference that ships with the task: a design the maintainers wrote or adapted and proved, the bar to beat, never an entry. Record is the best accepted design so far; with no submissions it is par. Both are the one ranked number, area × time on the sky130 cell library (µm²·ns), lower is better; “–” marks a task whose designs are not weighed on sky130 yet. Under par is how far the record is below par, as a share of par's score (0% while par is the record).Par is the best proved reference that ships with the task: a design the maintainers wrote or adapted and proved, the bar to beat, never an entry. Record is the best accepted design so far; with no submissions it is par. In this view both are area × time, the number it orders by, on the ASAP7 cell library (µm²·ns), lower is better; “–” marks a task whose designs are not weighed on ASAP7 yet. Under par is how far the record is below par, as a share of par's score (0% while par is the record). ASAP7: a predictive 7 nm library, never fabricated; no wires, like sky130's score (how ASAP7 is scored, and its quirks).

How it works, on the adder #

  1. Write solution.sv, with the task's module header. The adder bans the arithmetic operators, so the sum is built from gates. The adder's ripple-carry reference, tasks/add/reference/add_n.sv:

    module add_n #(parameter int N = 16) (
  input  logic [N-1:0] a, b,
  input  logic         cin,
  output logic [N-1:0] s,
  output logic         cout
);
  logic [N:0] c;
  assign c[0] = cin;
  genvar i;
  generate
    for (i = 0; i < N; i++) begin : g_bit
      assign s[i]   = a[i] ^ b[i] ^ c[i];
      assign c[i+1] = (a[i] & b[i]) | (c[i] & (a[i] ^ b[i]));
    end
  endgenerate
  assign cout = c[N];
endmodule

  2. Prove Solution.lean: one theorem. The checker turns your .sv into the Lean constant design, the circuit as ls-sv, the formal semantics of SystemVerilog in Lean, runs it. Goal is the task's trusted statement about it (trusted: you read it, and Lean's kernel checks your proof against it): for every N with 1 ≤ N < 2^31, whenever the inputs are known, {cout, s} = a + b + cin.

    import Submission.Design   -- written by the checker: `design`, `Goal`
namespace Submission
theorem solution : Goal := by
  -- your proof (add_n.lean: a complete one)
end Submission

  3. Check both files with one command. It accepts the pair or names the stage that refused it. Its last line is the score: the pinned Yosys and ABC synthesize your circuit, each gate becomes a sky130 cell, and the area in µm² times the critical-path delay in ns is the one ranked number. Par is the best proved reference; beat it.

    $ python3.12 check.py tasks/add solution.sv Solution.lean
...
  "accepted": true,
...
ranked (sky130 A0'): 460.4416 um^2 x 2611 ps = 1202.21 um2*ns; par 1202.21 (add_n)

You submit two files, solution.sv and Solution.lean (any names). Checking and recording them run on your own machine and upload nothing. Golf without Lean: python3.12 score/ppa.py solution.sv --task tasks/add --no-mapped prints the same area and delay in a second or two, and the same file always scores the same (reproduce a score). Install once: Step 0.

How a design becomes Lean #

You never write the Lean model of your circuit. The checker reads your .sv through a source gate that makes one canonical text for every tool, and the pinned extractor of proglib (formerly lean-surfaces), built on the slang SystemVerilog frontend, turns that text into an envelope: the elaborated design, cross-checked at several parameter values. The checker then writes the trusted module Submission.Design, whose load_design_sv2 design from "<envelope>" makes the Lean constant design: design.sem N is your circuit at parameter N as ls-sv runs it, and Goal is the task's statement of design.sem. Your Solution.lean imports that module and proves theorem solution : Goal in namespace Submission. The proving guide shows the loop: stage the design, print its equations, prove. Each task page's "Start a new design" says which tactics prove a new circuit of that task, how to lay the circuit out so that they take it, and which library lemmas exist.

The proof and the score #

The proof is about the design as ls-sv reads it, the score about the netlist Yosys builds from the same text. Before it accepts, the checker simulates the scored netlist against the proved design on a sample of input vectors and rejects any disagreement: fixed patterns and the task's corner values, inputs built from the constants the design compares against, and seeded random vectors, salted in competition runs so that nobody can predict them (every input where the input space is small, as for the AES S-box's 256). On a clocked task both run long seeded input traces from several power-up states, and the checker also holds the netlist's outputs to the task's property on every cycle. That is sampling, not a proof: a guard against the two tools disagreeing, behind the static rules that refuse every known disagreement before any proof is tried. Read the rules and the proving guide, or start with the tutorial task.