Roadmap

Done 8

• Six combinational tasks, each with a proved reference
  _example, add, mul, clmul, aes_sbox and fdivp. The parametric ones are proved for every width; fdivp is IEEE 754 division proved for every binary format, with three proved references (restoring, Newton-Raphson and radix-4 SRT).
• The checker
  One canonical text for the proof and the score (the source gate), the banlist, the 4-state rules, the kernel check and replay of the proof, the pinned scoring flow, the post-synthesis check against the scored netlist, and an operating-system sandbox around every process that runs submitted text. See the rules.
• Self-verifying records and the Pareto board
  A record carries the hashes of both files, the score, the checker's identity and the proof's facts; leaderboard.py verify re-checks it at three levels, up to re-running the whole check.
• The sky130 score ranks
  Each check weighs the scored netlist with a real standard-cell library, the open SkyWater sky130 cells: the cell area in µm² and the critical-path delay in ps (a clocked task: the cycles times the clock period), every input driven by the task's input drive. The leaderboard ranks those two; area in gate equivalents and depth are extra columns. Reproduce a score lists the pinned tools and files and the commands that give a recorded number again.
• Comparisons in the arithmetic tasks
  Decided 2026-11-05: in a task that bans + or - (add, mul, clmul, the toy _example), a run-time ordering comparison < <= > >= is banned too, at the Yosys level. Yosys builds it as its own adder (an $alu, the carry logic of +), so the banlist rejects every $alu that Yosys's alumacc builds. Equality, comparisons over parameters, and a comparator built from gates stay allowed.
• A first clocked task: the arbiter
  arbiter, a fair N-client arbiter: a statement that holds on every cycle of every input trace and from every power-up state (one grant at most, only to a requester, someone whenever anyone asks, and a requester that asks N cycles in a row granted within them), a checker for clocked designs (one clock, a synchronous reset, registered outputs, no construct that can create an unknown value, and a post-synthesis check that runs the netlist from random power-up states), the clocked scoring flow (the area with the flip-flops, times the register-to-register clock period), and a reference proved for every N.
• Clocked tasks with a latency: matmul and the sorter
  matmul, matrix multiplication behind a start/done handshake, and sorter, a streaming sorter: each transaction is answered within a latency the submission declares as a function of the parameters, from every power-up state and under every environment that follows the protocol. The post-synthesis check drives seeded transactions through the scored netlist and ls-sv's reading of the design, and the score is the area times the latency in cycles times the register-to-register clock period. Each has a reference proved for every parameter value in range.
• Records for every task
  Every task's par design has a record, so the bar to beat is re-checked like any entry (leaderboard.py verify --full).

In progress 1

• This website
  Generated from the repository by site/build.py and published from its main branch by the pages workflow. Every record and every proved reference of a ranked task has a page: the area, time and score cards, the design among the task's designs, the schematic of a small display instance, the critical path, the cells, the sources and the proof. Next: the placed and routed layout on those pages.

Planned 3

• A public hand-off for records
  There is no submission server. The plan is a pull request carrying the record's files, re-verified by CI.
• More tasks
  Candidates are well-known primitives with published comparison points, such as hash rounds and CRC steps, written so that a table and a gate network are judged against the same mathematics.
• Lifting refusals
  Many refusals are marked later: each names what has to exist first (for example a 4-state rule, or more of the language in ls-sv). See the refusals.

Open questions 1

• One score across tasks
  Points that sum over tasks need a definition that respects two axes first; until then every task has its own frontier of sky130 area and time.