Record `78eafaad6144`

reference: not an entryreference: not an entry scored at the one fixed size

Recorded by the maintainers from the proved reference sbox_table: its design and its proof sbox_table.lean (9 code lines). The 256-entry table of FIPS 197 as one case statement. The record shows that reference passing the whole checker. It is shown with parshown with par, not a player's entry, and it is not ranked among the submissions (proved references).

Area

3 445.80µm²

3 445.8048 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: +286.3% largersbox_bp · 892.11 µm²
on this page: 4th of 5 designs (tied with 1)

cells: 612
flops: 0
repair: 0 buffers, 0 tie cells
GE: 786.894 extra
A1′: 2 343.50 µm² research

Performance · time

2 288ps

the delay: the latest output arrival, y[0] falling

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par: −46.8% fastersbox_bp · 4 297 ps
on this page: 1st of 5 designs (tied with 1)

Fmax-eq.: 437.1 MHz derived
critical path: 9 cells
unit depth: 11 extra
A1′: 1 648 ps research

Score · area × time

7884µm²·ns

3 445.8048 µm² × 2 288 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: +105.7% worsesbox_bp · 3833 µm²·ns
on this page: 4th of 5 designs (tied with 1)
board: a proved reference, shown with par: never ranked
Pareto: on the front

On the board, of 1 other player: 0 beaten, 0 level, 1 trade off, 0 ahead.

how these numbers are measured and compared

Area: sky130 A0′, the repaired netlist. Time: NLDM, inputs driven by buf_8, 10 fF per output bit, no wires.

Area, time and score are ranked (the leaderboard orders by the score); a number tagged extra, derived or research is shown, never ranked. Fmax-equivalent = 10⁶ / time in ps, for comparison with sites that quote Fmax.

The field is the ranked records of aes_sbox's other players at this revision (1 player, 1 record), never the references, the baselines or a rejected design; each player counts once, at their best, and ties are exact at the recorded unit; advisory, recomputed at every build, never stored in a record and never used by the ranking.

On the board, another player is beaten when this design dominates every record of theirs, level when none of theirs is better and one is identical (the rest dominated), ahead when a record of theirs dominates this design, and a trade off otherwise (one of theirs better on one axis, worse on the other).

“On this page” and “Pareto” compare with the 5 designs of the area-time plot (2 references, 1 submission and 2 baselines): not a ranking.

Area

51.817µm²

51.81732 µm² exactly

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: +288.0% largersbox_bp · 13.355 µm²
on this page: 4th of 5 designs (tied with 1)

cells: 734
flops: 0
repair: 0 buffers, 0 tie cells
GE: 786.894 extra

Performance · time

373ps

the delay: the latest output arrival

Beats 100% · matches 0%

1 of 1 other player beaten, 0 equal.

vs par: −47.0% fastersbox_bp · 704 ps
on this page: 1st of 5 designs (tied with 1)

Fmax-eq.: 2681.0 MHz derived
unit depth: 11 extra

Score · area × time

19.33µm²·ns

51.81732 µm² × 373 ps

Beats 0% · matches 0%

0 of 1 other player beaten, 0 equal.

vs par: +105.6% worsesbox_bp · 9.402 µm²·ns
on this page: 4th of 5 designs (tied with 1)
board: a proved reference, shown with par: never ranked
Pareto: on the front

On the board, of 1 other player: 0 beaten, 0 level, 1 trade off, 0 ahead.

how these numbers are measured and compared

Area: ASAP7 A0′ (asap7_a0_v1), the same scored netlist, each gate its least-area ASAP7 build, repaired by buffering. Time: NLDM, inputs driven by BUFx8, 2.5 fF per output bit, no wires; a table read below its grid is read at its floor. ASAP7: a predictive 7 nm library, never fabricated; no wires, like sky130's score (how ASAP7 is scored, and its quirks).

Area, time and score order this view's board (by the score); the records' ranked score is sky130's, the default view; a number tagged extra, derived or research is shown, never ranked. Fmax-equivalent = 10⁶ / time in ps, for comparison with sites that quote Fmax.

“On this page” and “Pareto” compare with the 5 designs of the area-time plot (2 references, 1 submission and 2 baselines): not a ranking.

The sources

sbox_table.svdownload

// svGolf task `aes_sbox`, reference solution (WP-G S3a): the S-box as a 256-entry `case` table in one
// `always_comb`, proved with the sv_comb tactics (reference/sbox_table.lean). Entry x is the decimal 8'd<x>:
// y = 8'd<S(x)> (FIPS 197, Table 4); the default arm is unreachable but required (a latch without it).
module aes_sbox (input logic [7:0] x, output logic [7:0] y);
  always_comb begin
    case (x)
      8'd0: y = 8'd99;
      8'd1: y = 8'd124;
      8'd2: y = 8'd119;
      8'd3: y = 8'd123;
      8'd4: y = 8'd242;
      8'd5: y = 8'd107;
      8'd6: y = 8'd111;
      8'd7: y = 8'd197;
      8'd8: y = 8'd48;
      8'd9: y = 8'd1;
      8'd10: y = 8'd103;
      8'd11: y = 8'd43;
      8'd12: y = 8'd254;
      8'd13: y = 8'd215;
      8'd14: y = 8'd171;
      8'd15: y = 8'd118;
      8'd16: y = 8'd202;
      8'd17: y = 8'd130;
      8'd18: y = 8'd201;
      8'd19: y = 8'd125;
      8'd20: y = 8'd250;
      8'd21: y = 8'd89;
      8'd22: y = 8'd71;
      8'd23: y = 8'd240;
      8'd24: y = 8'd173;
      8'd25: y = 8'd212;
      8'd26: y = 8'd162;
      8'd27: y = 8'd175;
      8'd28: y = 8'd156;
      8'd29: y = 8'd164;
      8'd30: y = 8'd114;
      8'd31: y = 8'd192;
      8'd32: y = 8'd183;
      8'd33: y = 8'd253;
      8'd34: y = 8'd147;
      8'd35: y = 8'd38;
      8'd36: y = 8'd54;
      8'd37: y = 8'd63;
      8'd38: y = 8'd247;
      8'd39: y = 8'd204;
      8'd40: y = 8'd52;
      8'd41: y = 8'd165;
      8'd42: y = 8'd229;
      8'd43: y = 8'd241;
      8'd44: y = 8'd113;
      8'd45: y = 8'd216;
      8'd46: y = 8'd49;
      8'd47: y = 8'd21;
      8'd48: y = 8'd4;
      8'd49: y = 8'd199;
      8'd50: y = 8'd35;
      8'd51: y = 8'd195;
      8'd52: y = 8'd24;
      8'd53: y = 8'd150;
      8'd54: y = 8'd5;
      8'd55: y = 8'd154;
      8'd56: y = 8'd7;
      8'd57: y = 8'd18;
      8'd58: y = 8'd128;
      8'd59: y = 8'd226;
      8'd60: y = 8'd235;
      8'd61: y = 8'd39;
      8'd62: y = 8'd178;
      8'd63: y = 8'd117;
      8'd64: y = 8'd9;
      8'd65: y = 8'd131;
      8'd66: y = 8'd44;
      8'd67: y = 8'd26;
      8'd68: y = 8'd27;
      8'd69: y = 8'd110;
      8'd70: y = 8'd90;
      8'd71: y = 8'd160;
      8'd72: y = 8'd82;
      8'd73: y = 8'd59;
      8'd74: y = 8'd214;
      8'd75: y = 8'd179;
      8'd76: y = 8'd41;
      8'd77: y = 8'd227;
      8'd78: y = 8'd47;
      8'd79: y = 8'd132;
      8'd80: y = 8'd83;
      8'd81: y = 8'd209;
      8'd82: y = 8'd0;
      8'd83: y = 8'd237;
      8'd84: y = 8'd32;
      8'd85: y = 8'd252;
      8'd86: y = 8'd177;
      8'd87: y = 8'd91;
      8'd88: y = 8'd106;
      8'd89: y = 8'd203;
      8'd90: y = 8'd190;
      8'd91: y = 8'd57;
      8'd92: y = 8'd74;
      8'd93: y = 8'd76;
      8'd94: y = 8'd88;
      8'd95: y = 8'd207;
      8'd96: y = 8'd208;
      8'd97: y = 8'd239;
      8'd98: y = 8'd170;
      8'd99: y = 8'd251;
      8'd100: y = 8'd67;
      8'd101: y = 8'd77;
      8'd102: y = 8'd51;
      8'd103: y = 8'd133;
      8'd104: y = 8'd69;
      8'd105: y = 8'd249;
      8'd106: y = 8'd2;
      8'd107: y = 8'd127;
      8'd108: y = 8'd80;
      8'd109: y = 8'd60;
      8'd110: y = 8'd159;
      8'd111: y = 8'd168;
      8'd112: y = 8'd81;
      8'd113: y = 8'd163;
      8'd114: y = 8'd64;
      8'd115: y = 8'd143;
      8'd116: y = 8'd146;
      8'd117: y = 8'd157;
      8'd118: y = 8'd56;
      8'd119: y = 8'd245;
      8'd120: y = 8'd188;
      8'd121: y = 8'd182;
      8'd122: y = 8'd218;
      8'd123: y = 8'd33;
      8'd124: y = 8'd16;
      8'd125: y = 8'd255;
      8'd126: y = 8'd243;
      8'd127: y = 8'd210;
      8'd128: y = 8'd205;
      8'd129: y = 8'd12;
      8'd130: y = 8'd19;
      8'd131: y = 8'd236;
      8'd132: y = 8'd95;
      8'd133: y = 8'd151;
      8'd134: y = 8'd68;
      8'd135: y = 8'd23;
      8'd136: y = 8'd196;
      8'd137: y = 8'd167;
      8'd138: y = 8'd126;
      8'd139: y = 8'd61;
      8'd140: y = 8'd100;
      8'd141: y = 8'd93;
      8'd142: y = 8'd25;
      8'd143: y = 8'd115;
      8'd144: y = 8'd96;
      8'd145: y = 8'd129;
      8'd146: y = 8'd79;
      8'd147: y = 8'd220;
      8'd148: y = 8'd34;
      8'd149: y = 8'd42;
      8'd150: y = 8'd144;
      8'd151: y = 8'd136;
      8'd152: y = 8'd70;
      8'd153: y = 8'd238;
      8'd154: y = 8'd184;
      8'd155: y = 8'd20;
      8'd156: y = 8'd222;
      8'd157: y = 8'd94;
      8'd158: y = 8'd11;
      8'd159: y = 8'd219;
      8'd160: y = 8'd224;
      8'd161: y = 8'd50;
      8'd162: y = 8'd58;
      8'd163: y = 8'd10;
      8'd164: y = 8'd73;
      8'd165: y = 8'd6;
      8'd166: y = 8'd36;
      8'd167: y = 8'd92;
      8'd168: y = 8'd194;
      8'd169: y = 8'd211;
      8'd170: y = 8'd172;
      8'd171: y = 8'd98;
      8'd172: y = 8'd145;
      8'd173: y = 8'd149;
      8'd174: y = 8'd228;
      8'd175: y = 8'd121;
      8'd176: y = 8'd231;
      8'd177: y = 8'd200;
      8'd178: y = 8'd55;
      8'd179: y = 8'd109;
      8'd180: y = 8'd141;
      8'd181: y = 8'd213;
      8'd182: y = 8'd78;
      8'd183: y = 8'd169;
      8'd184: y = 8'd108;
      8'd185: y = 8'd86;
      8'd186: y = 8'd244;
      8'd187: y = 8'd234;
      8'd188: y = 8'd101;
      8'd189: y = 8'd122;
      8'd190: y = 8'd174;
      8'd191: y = 8'd8;
      8'd192: y = 8'd186;
      8'd193: y = 8'd120;
      8'd194: y = 8'd37;
      8'd195: y = 8'd46;
      8'd196: y = 8'd28;
      8'd197: y = 8'd166;
      8'd198: y = 8'd180;
      8'd199: y = 8'd198;
      8'd200: y = 8'd232;
      8'd201: y = 8'd221;
      8'd202: y = 8'd116;
      8'd203: y = 8'd31;
      8'd204: y = 8'd75;
      8'd205: y = 8'd189;
      8'd206: y = 8'd139;
      8'd207: y = 8'd138;
      8'd208: y = 8'd112;
      8'd209: y = 8'd62;
      8'd210: y = 8'd181;
      8'd211: y = 8'd102;
      8'd212: y = 8'd72;
      8'd213: y = 8'd3;
      8'd214: y = 8'd246;
      8'd215: y = 8'd14;
      8'd216: y = 8'd97;
      8'd217: y = 8'd53;
      8'd218: y = 8'd87;
      8'd219: y = 8'd185;
      8'd220: y = 8'd134;
      8'd221: y = 8'd193;
      8'd222: y = 8'd29;
      8'd223: y = 8'd158;
      8'd224: y = 8'd225;
      8'd225: y = 8'd248;
      8'd226: y = 8'd152;
      8'd227: y = 8'd17;
      8'd228: y = 8'd105;
      8'd229: y = 8'd217;
      8'd230: y = 8'd142;
      8'd231: y = 8'd148;
      8'd232: y = 8'd155;
      8'd233: y = 8'd30;
      8'd234: y = 8'd135;
      8'd235: y = 8'd233;
      8'd236: y = 8'd206;
      8'd237: y = 8'd85;
      8'd238: y = 8'd40;
      8'd239: y = 8'd223;
      8'd240: y = 8'd140;
      8'd241: y = 8'd161;
      8'd242: y = 8'd137;
      8'd243: y = 8'd13;
      8'd244: y = 8'd191;
      8'd245: y = 8'd230;
      8'd246: y = 8'd66;
      8'd247: y = 8'd104;
      8'd248: y = 8'd65;
      8'd249: y = 8'd153;
      8'd250: y = 8'd45;
      8'd251: y = 8'd15;
      8'd252: y = 8'd176;
      8'd253: y = 8'd84;
      8'd254: y = 8'd187;
      8'd255: y = 8'd22;
      default: y = 8'd0;
    endcase
  end
endmodule

sbox_table.lean (9 code lines)

import Submission.Design
import SvGolf.Comb
import LeanModels.Sv.CombExhaustiveTactic

/-!
# Reference solution for task `aes_sbox`: the 256-entry `case` table (WP-G S3a)

This is a submission file like any player's `Solution.lean`: the checker generates `Submission.Design`
(`Submission.design`, `Submission.Goal`) and this file proves `theorem Submission.solution : Submission.Goal`
for the fixed-size S-box statement (`SvGolf.Tasks.AesSbox.Statement`, i.e. `y = sbox x` for every known `x`).
The design is `reference/sbox_table.sv`: one `always_comb` with a plain `case (x)` of 256 constant items
`8'dK: y = 8'dS;` and a `default`.

The proof is `sv_exhaustive` (`LeanModels/Sv/CombExhaustiveTactic.lean`): the design is read through its
lowering (`CombTask.satisfiedAt_of_lowered`, no qualified `case` by `NoQ.sem_noQ`), the `case` is compiled
once into a word-level table lookup (one bitmap per output bit), and `y` is decided against the task's `sbox`
on all 256 inputs by kernel evaluation. `PROVING.md`, section 15.
-/

namespace Submission

set_option maxHeartbeats 1000000 in
/-- **The reference solution**: the `aes_sbox` statement for the `case` table. -/
theorem solution : Goal := by sv_exhaustive

/--
info: 'Submission.solution' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms solution

end Submission

The netlist

The netlist card shows the sky130 weighing (its cells, its critical path): the ASAP7 view changes the overview above, not this card.

Schematic

The repaired A0′ netlist that the score weighs: 612 cells. aes_sbox has one fixed size, so there is no smaller instance to draw.

The drawing is its critical path (9 cells, ending at y[0] falling, 2 288 ps), every cell of it, and each net that enters or leaves the path drawn as a port named after the net: the whole netlist at this size is a tangle of wires. The path's own nets are in the accent colour. Drawn by netlistsvg with svGolf's sky130 skin (derived from netlistsvg's default skin, as the drawing is: MIT licence, Copyright (c) 2016 Neil Turley, the notice): one symbol per cell function, the cell above it, the instance on hover; nor2b and nand2b are drawn with the bubble on their inverted input. The cells of the path are listed under Critical path, each a link to the cell here.

The netlist at its one fixed size: 612 cells, 264 nand2_1, 129 and2_1, 70 or2_1, 63 mux2_1, 38 nand2b_1, 21 nor2b_1, 18 nor2_1, 5 xnor2_1, 3 inv_1, 1 xor2_1; 9 drawn. Open the drawing on its own (SVG, 8.7 KB) to pan and zoom it with the browser's own controls.

Critical path

at the one fixed size · scored

The path the ranked delay ends on, at the task's one size: 10 nets, 9 cells, to y[0] falling at 2 288 ps. Each row is a net of the repaired netlist with the arrival and the transition the STA computed there (NLDM tables, the larger transition carried; no wires). The first row is an input: its arrival is the input driver's own delay (buf_8 fed by a 50 ps ramp). From ppa.py --path (critical_path_timing); the instance names are the schematic's (the same netlist), each a link to its cell there.

#	net	edge	driven by	cell	arrival (ps)	transition (ps)	stage (ps)
0	`x[3]`	rise	input port	–	198.7	180.5
1	`_0069_`	fall	`_0604_`	`inv_1`	478.7	275.7	280.0
2	`_0547_`	fall	`_0648_`	`and2_1`	755.2	77.2	276.5
3	`_0558_`	rise	`_0649_`	`nor2b_1`	921.9	155.1	166.7
4	`_0038_`	fall	`_0725_`	`nor2b_1`	977.5	39.4	55.6
5	`_0039_`	fall	`_0726_`	`or2_1`	1 166.9	41.7	189.4
6	`_0043_`	fall	`_0730_`	`mux2_1`	1 430.3	49.3	263.4
7	`_0052_`	fall	`_0739_`	`mux2_1`	1 696.0	49.3	265.7
8	`_0053_`	fall	`_0740_`	`mux2_1`	1 961.7	49.3	265.7
9	`y[0]`	fall	`_0741_`	`mux2_1`	2 287.7	92.4	326.0

Cells

at the one fixed size · scored

The area of each cell type in the repaired A0′ netlist, at the scoring point: the count times the cell's area in the pinned liberty. Their sum is the ranked area.

cell	count	µm² each	µm² in all	share
`nand2_1`	264	3.7536	990.9504	28.8%
`and2_1`	129	6.2560	807.0240	23.4%
`mux2_1`	63	11.2608	709.4304	20.6%
`or2_1`	70	6.2560	437.9200	12.7%
`nand2b_1`	38	6.2560	237.7280	6.9%
`nor2b_1`	21	6.2560	131.3760	3.8%
`nor2_1`	18	3.7536	67.5648	2.0%
`xnor2_1`	5	8.7584	43.7920	1.3%
`inv_1`	3	3.7536	11.2608	0.3%
`xor2_1`	1	8.7584	8.7584	0.3%
total	612		3445.8048

Repair (buffer_trees_v1): 0 buffers on 0 nets, 0 tie cells, 1 weighing round; nothing is resized.

Legality: worst load 0.474 × max_capacitance, worst transition 0.47 × max_transition; 0 timing-table reads outside the characterized grid.

the gate mix of the extra GE column (the pinned GE table, score/ge.json)

Cells by type; area is the count weighted by the pinned GE table.

cell	count	GE each	GE total
`NAND`	264	1.000	264.000
`AND`	129	1.333	171.957
`OR`	70	1.333	93.310
`MUX`	63	2.333	146.979
`ORNOT`	38	1.333	50.654
`ANDNOT`	21	1.333	27.993
`NOR`	18	1.000	18.000
`XNOR`	5	2.000	10.000
`NOT`	3	0.667	2.001
`XOR`	1	2.000	2.000
total	612		786.894

The record

task: aes_sbox
player: svgolf-reference
assisted by: Claude (Anthropic)
submitted: 2026-11-07
notes: reference solution
scoring point: the one fixed size
design: sbox_table.sv sha256 32e0c39420f12a4758c3e618337a5be8957c7d8b7718c82e0a55eaf409402163
proof: sbox_table.lean sha256 ac6c99916423cd56b0ed71203eb0e474f7866f1fa09fa55590cc890dd29b7c4d: the proof of the reference sbox_table (sbox_table.lean, 9 code lines)
canonical text: sha256 570d69bd001f1bf79e555d3cf87fd63b18f202457a56f279adc04676c6631e32
record hash: 78eafaad6144a56d7f9bc189bea080f4b96d63f38d8cffcd27d4d72d69bb8cc3
downloads: 78eafaad6144.sv 78eafaad6144.lean 78eafaad6144.json

The proof

code lines: 9
build time: 35.43 s
axioms: Classical.choice, Quot.sound, propext
tactics seen: none
imports: Submission.Design, SvGolf.Comb, LeanModels.Sv.CombExhaustiveTactic

Checker and flow

Checked under the pinned flow of this site's boards.

Yosys: Yosys 0.53 (git sha1 53c22ab7c0ced80861c7536c5dae682c30fb5834, clang++ 17.0.0 -fPIC -O3)
Verilator: Verilator 5.042 2025-11-02 rev UNKNOWN.REV
Lean toolchain: leanprover/lean4:v4.33.0-rc1
svGolf revision: d1f3cae6f01a088007a57b31ff8baa6b839d6f74
lean-surfaces revision: d1f3cae6f01a088007a57b31ff8baa6b839d6f74
canonicalization script: bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b
scoring script: ea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445
GE table: 6a29196a3f4b58241f4c9af650c9141e4632b737214d563a11ba142a725c4bea
extractor: 4930696021c588c75dc890034c534c95560ad9a28a4955b87d1f8d68b5edbc0c
canonical RTLIL: 6c7b6677d1798bc8099cfccaed4d4c7e65d78a153d9180a6cfc4f64bc2754b4a

the checker's files (sha256)

file	sha256
`check.py`	`e708084f72f955b0ae1aaabe469dba3eacc5a91484a1ed81bcc073b60f3c0b6d`
`check/Comparator.lean`	`3145eb578ca71e452eff05a398e8ad04673e6c72ca5343b234cb22e2cefe65a6`
`check/SvEval.lean`	`fb51d72510b515460866c2798aad3c6f55295536e627b92854c3580af215bb91`
`check/clocked_rules.py`	`73856a45905724544247ad29042bdc2f1778271ec07b15cdb3a5f214685165c1`
`check/envelope.py`	`076db01a9791bcc25ee84e9b0033604a4b675f00b212eab0c864078e6a4748b7`
`check/postsynth.py`	`4e1ee2110c63f24e033dd689c929ea686ddf10f4db23b9057c6fb711394c7558`
`lakefile.toml`	`f35a88404367d22906effc14d644aac9a9cad47dfd3b704ea8fec88acfaf9c4d`
`lean-toolchain`	`62c2d9c0fc1ec4c67e151c11eff41ca004ef38e179cf9476c230406e6defedef`
`score/banlist.py`	`f18c14c23a14d55db63e202f42cc424dc84c1dd1c337f132ad60859dc9d5d33a`
`score/canon.ys`	`bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b`
`score/fourstate.py`	`95332451ae3754226fb87b46027385b46a91121e7eb9ae25b302bce756d90475`
`score/ge.json`	`6a29196a3f4b58241f4c9af650c9141e4632b737214d563a11ba142a725c4bea`
`score/ge_seq.json`	`54b93ca63888009d0671c8978e8ab7bf4fb8ce303bc78d3b4e1f83d946cc3201`
`score/ppa.py`	`912031912c3e3f6790725161753e95415df34846bd8c27dde3eb707747ddbcbe`
`score/ppa_mapped.ys`	`93547b343dbac135737e98516b1004a780e1cf2f579e1bd7fed82c908c6d4125`
`score/ppa_mapped_pins.json`	`4b8688ba3f4d67681658e5944afe878592adf588cd416a8b47597ebe06deb045`
`score/ppa_pins.json`	`d66a6086a37a97f5985266057051979fb6a8a3c557d3ef9c42acc1b5e41502d8`
`score/score.py`	`71d2e3b82f8813ec64a58f0a46909ca23dfab377db44eda6f294b713f45ae781`
`score/srcgate.py`	`11952f61058051c9e8de91a801b672d07e66a29308e978156c04ffd9f0dbef45`
`score/svgolf.ys`	`ea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445`
`score/svgolf_seq.ys`	`c3874dbfc85921a87df6eacdfc6b2c9a0e2b34edd5738951e0d8bdb51f4558b2`

Post-synthesis check

ls-sv's reading of the design and the scored netlist, simulated on the same vectors, agreed on every one. The vectors are a sample of the inputs: a guard against the two tools disagreeing, not a proof.

mode: full
vectors: 256
full set: 256
mismatches: 0
point: default
seed: 891e0c945d7ceee58218fe60c16e6d9d17e672a57bd3dc5a449a5850849b9af1
salted: no

Area against time

µm² × ps · lower left is better · ASAP7

submission
proved reference
baseline (not proved)
the Pareto front of the entries

this design
par's score: area × time = 3833 µm²·ns

sky130 area (x) against the ranked time (y); lower left is better on both. The step line is the Pareto front of the entries (the proved references and the players' ranked records); a design under par's score curve has a better score than par. Baselines are drawn for scale: scored, never proved. Every design is in view.

the designs as numbers, by score

design	kind	area (µm²)	time (ps)	score (µm²·ns)
tower-shuffle	submission	890.85	3 208	2858
`sbox_bp_d16`	baseline, not proved	952.16	3 670	3494
`sbox_bp`	proved reference · par	892.11	4 297	3833
`sbox_table` · this design	proved reference	3 445.80	2 288	7884
`sbox_table`	baseline, not proved	3 445.80	2 288	7884

submission
proved reference
baseline (not proved)
the Pareto front of the entries

this design
par's score: area × time = 9.402 µm²·ns

ASAP7 area (x) against the ASAP7 time (y); lower left is better on both. The step line is the Pareto front of the entries (the proved references and the players' ranked records); a design under par's score curve has a better score than par. Baselines are drawn for scale: scored, never proved. Every design is in view.

the designs as numbers, by score

design	kind	area (µm²)	time (ps)	score (µm²·ns)
tower-shuffle	submission	13.414	556	7.458
`sbox_bp_d16`	baseline, not proved	14.245	627	8.931
`sbox_bp`	proved reference · par	13.355	704	9.402
`sbox_table` · this design	proved reference	51.817	373	19.33
`sbox_table`	baseline, not proved	51.817	373	19.33

Reproduce and verify

From svgolf/, with the pinned tools (reproduce a score lists them):

shell

# the ranked numbers, at the scoring point (from svgolf/, with the pinned Yosys and liberty)
python3.12 score/ppa.py tasks/aes_sbox/reference/sbox_table.sv --task tasks/aes_sbox --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256: 6c7b6677d1798bc8099cfccaed4d4c7e65d78a153d9180a6cfc4f64bc2754b4a
ppa.netlist_sha256: 43edd658bdb80404c7a8fb8fe61ba9d84ea9d837972450c0120494b33d2bc016
ppa.repair.netlist_sha256: b4d04a31d73c656be20f7a61fdc88dc2d1dd3522aa24f815cff41c1b81168dc0
ppa.area_e4um2_sky130: 34458048
ppa.delay_ps_sky130: 2288

The schematic and the critical-path data are site/schematics/aes_sbox/32e0c39420f12a47.json and its .svg, written by site/gen_schematics.py (the display instance is ppa.py ... --repaired-netlist, drawn by netlistsvg 1.0.2; repaired netlist sha256 b4d04a31d73c656b…).

From svgolf/, with the pinned tools (reproduce a score lists them):

shell

# the ASAP7 view's numbers, at the scoring point (from svgolf/, with the pinned Yosys; once:
# python3.12 score/ppa.py --pdk asap7 --fetch-liberty, the five pinned ASAP7 files into score/lib/asap7/)
python3.12 score/ppa.py tasks/aes_sbox/reference/sbox_table.sv --task tasks/aes_sbox --pdk asap7 --no-mapped \
    --json out.json

Expect, in out.json:

ppa.netlist_sha256: 43edd658bdb80404c7a8fb8fe61ba9d84ea9d837972450c0120494b33d2bc016
ppa.repair.netlist_sha256: b339cc280a6d33865ab421e2879a83d99982cabd381c57f3469135805a2f7385
ppa.area_e5um2_asap7: 5181732
ppa.delay_ps_asap7: 373

leaderboard/asap7/aes_sbox.json keeps these numbers; python3.12 leaderboard/leaderboard.py asap7 --rescore --task aes_sbox weighs every design of the task again and compares, bit for bit.

Verify the record

Download the three files, then from svgolf/:

shell

# re-run the whole check on this record's files (the cost of the original check)
H=78eafaad6144a56d7f9bc189bea080f4b96d63f38d8cffcd27d4d72d69bb8cc3
mkdir -p rec/aes_sbox && cp "$H.json" "$H.sv" "$H.lean" rec/aes_sbox/
python3.12 leaderboard/leaderboard.py verify --data-dir rec --task aes_sbox --full

verify --offline checks only the hashes and the arithmetic; plain verify also rescores the design (no Lean; seconds for most designs, a minute or more for the largest), on sky130 and on ASAP7.