The benchmark
sysr exists to make a model's hardware mistakes cheap to catch. The benchmark is how that is measured: hardware tasks with hidden testbenches, a scorer that trusts only Yosys and Icarus Verilog, deliberately buggy designs that the checker must reject, and a loop in which a model writes a design, is told what failed, and repairs it, under the same rules in sysr and in Verilog.
The tasks
Fourteen tasks came with feature 001, from a priority encoder to a UART receiver; feature 002 added six harder ones (marked hard): an RV32I execute stage, an AXI4-Lite slave, an interrupt controller, an instruction cache, an SPI master and a reconfiguration-slot controller; features 004 and 007 added a RAM that must become block RAM and a multiply-accumulate unit. Each line below is the first sentence of the task's prompt. Filter by tag; the last columns show the task's spec stub, if it has one, and its seeded bug.
| Task | Prompt, first sentence | Spec stub | Seeded bug (expected codes) |
|---|
task.json and tests/seeded/, copied into this page (data.js has only the task names; the page checks its list against them). The feature that added each task is in its first tag.What a task holds
| File | What it is |
|---|---|
task.json | the name, the prompt, the top module's name, whether it is sequential, how many cycles the testbench runs, tags, and for sync-ram the cells synthesis must infer (resources) |
iface.v | the module's header with an empty body, and a comment stating the requirements on its inputs: where a Verilog candidate starts |
stub.sysr | the same ports and the requirements as requires, with a hole (?out) driving each output: where a sysr candidate starts. Neither stub has ensures or invariants; writing them is the candidate's work |
spec-stub.sysr | for eight tasks: the stub plus spec functions stating what the design must compute and ensures against them, so an accepted design is proven against the task's specification |
tb.v | the hidden Icarus testbench: drives only inputs that meet the requirements, compares with a model after each edge, prints FAIL cycle N: … at the first mismatch, or PASS |
ref.v, ref.sysr | a reference solution in each language; both pass |
Both starting files state the same requirements, one as a comment and one as requires, so neither language gets more of the specification. The spec stubs are the exception, used only in their own condition and compared only with other sysr runs. tests/spec-stub-test.rkt checks that each spec stub has only holes as errors, and that each sysr reference, with the stub's spec functions and ensures added, is proven against them.
The scorer: bench/score.rkt
bin/bench score --lang verilog|sysr scores candidates (by default the references) against every task. sysr is used only through its command line, and PASS is decided by Yosys and Icarus Verilog, never by sysr itself, so a sysr design is held to exactly what a Verilog design is. A candidate goes through these stages, and the first that fails names the result:
tests/bench-test.rkt checks the scorer and the tasks: every Verilog and every sysr reference passes; a candidate that does not parse, has a latch, has a combinational loop (which would pass simulation), gives a wrong output, never ends, is missing or misses its block RAM gets the right failure; and every task's testbench rejects a mutant of its reference (tests/fixtures/mutants/), so no testbench is too weak to notice a bug.
Seeded bugs: caught before simulation
A seeded bug is a sysr reference with one deliberate mistake, in tests/seeded/, whose first line says which diagnostic codes the checker must give, such as ; expect: V002. bin/bench seeded (bench/seeded.rkt) runs sysr check --json on each and requires it to be rejected with exactly those error codes, before anything is simulated. There are 20, one for each task except mac and sync-ram; the table above lists them. Most are caught as a property that may not hold (V002, with a trace from reset) or one that is not inductive (V007); see Diagnostics for the codes. The checker can only catch what a design states: every seeded design states properties, and its bug breaks one of them.
The loop: write, check, repair
bin/bench loop (bench/loop.rkt) gives a model a task and lets it repair its design from the scorer's own words, up to an attempt budget. The rules are the same for both languages: attempt 1 shows the prompt and the starting file; after a failure the model sees the result and its detail (the checker's diagnostics, the Yosys or Icarus output, or the failing test line) and is asked for the whole corrected file; the task ends at the first PASS or when the budget is spent. The sysr condition's system prompt contains the whole language reference, docs/reference.md. Here is a real exchange from the first recorded run, step by step.
pwm in sysr, from bench/results/2026-10-11-subagent-sonnet-sysr-pwm/run.json. The message texts are built from loop.rkt's templates and the task's prompt; the replies and the checker's detail are the recorded ones.Models are sysp's (anthropic:MODEL_ID, needing an API key, or scripted:FILE, replies from a file, which the tests use offline). relay:DIR (bench/relay.rkt) is for a model reached some other way: each prompt is written to DIR/<task>-<n>.prompt.json and the loop waits for <task>-<n>.reply.txt; token counts are then approximate, four characters each. Every attempt is recorded raw in the run's run.json (reply, extracted code, result, detail, feedback) with a transcript per task, and bin/bench summary (bench/summary.rkt, which uses sysp's summary unchanged) reports counts, never percentages. tests/loop-test.rkt drives the loop with a scripted model: a sysr proof failure repaired from the diagnostics, a Verilog wrong output repaired from the failing line, the budget respected, and a relay round trip.
Results so far
Three recorded runs, all on 2026-10-11, all with Claude Sonnet 5.5 reached as context-free subagents through relay: (no API key was available), 4 attempts per task, one run per task and language. From bench/results/*.md:
| Run | Tasks | Solved | First attempt | Notes |
|---|---|---|---|---|
| first | the 14 of feature 001 | sysr 14/14, Verilog 14/14 | sysr 12/14, Verilog 14/14 | both sysr repairs were language rules (an ensures naming a register; a hole left in place); sysr took about 13 times the input tokens, nearly all of it the reference |
| hard | the 6 of feature 002 | sysr 6/6, Verilog 6/6 | sysr 5/6, Verilog 5/6 | only plic-lite needed repairs, in both languages, and its first failure was an ambiguous prompt (since reworded) |
| spec stubs | 8, sysr only | 8/8 | 8/8 | every accepted design proven against the task's specification, against 1/8 with plain stubs; where the spec was a function, the model often copied it into the design |
With the references: make bench-refs scores 22/22 in each language, and make seeded rejects 20/20 before simulation.
What this does and does not show. No difference between the languages yet: the tasks are too easy for this model, which solved nearly everything on the first attempt in both. Most sysr solutions stated few properties, so the verifier was asked to prove little beyond widths and indices; spec stubs fixed that, at the cost of writing the spec. And none of it is a clean measurement: one run per task, approximate token counts, the subagents of the same model family that designed sysr, and working where they could have read the references (they were told not to).