Tasks / aes_sbox / record

Record `d2880a7160dd`

on the Pareto frontieron the Pareto frontier scored at the one fixed size

Area

890.85µm²

890.8544 µm² exactly

vs par: −0.1% smallersbox_bp · 892.11 µm²
on this page: smallest of 5 designs

cells: 122
flops: 0
repair: 0 buffers, 0 tie cells
GE: 204.659 extra
A1′: 1 078.53 µm² research

Performance · time

3 208ps

the delay: the latest output arrival, y[3] rising

vs par: −25.3% fastersbox_bp · 4 297 ps
on this page: 3rd of 5 designs

Fmax-eq.: 311.7 MHz derived
critical path: 15 cells
unit depth: 16 extra
A1′: 3 522 ps research

Score · area × time

2858µm²·ns

890.8544 µm² × 3 208 ps

vs par: −25.4% bettersbox_bp · 3833 µm²·ns
on this page: best of 5 designs
board: layer 1, rank 1 of 1 by score
Pareto: on the front

No other player has a ranked record on aes_sbox yet: the beats and matches lines come with the first one.

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 (0 players, 0 records), never the references, the baselines or a rejected design; advisory, recomputed at every build, never stored in a record and never used by the ranking.

“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

13.414µm²

13.41360 µm² exactly

vs par: +0.4% largersbox_bp · 13.355 µm²
on this page: 2nd of 5 designs

cells: 133
flops: 0
repair: 0 buffers, 0 tie cells
GE: 204.659 extra

Performance · time

556ps

the delay: the latest output arrival

vs par: −21.0% fastersbox_bp · 704 ps
on this page: 3rd of 5 designs

Fmax-eq.: 1798.6 MHz derived
unit depth: 16 extra

Score · area × time

7.458µm²·ns

13.41360 µm² × 556 ps

vs par: −20.7% bettersbox_bp · 9.402 µm²·ns
on this page: best of 5 designs
board: layer 1, rank 1 of 1 by score
Pareto: on the front

No other player has a ranked record on aes_sbox yet: the beats and matches lines come with the first one.

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

solution.svdownload

// k0_934.6464_3348.sv re-optimized: strash;&get -n;&deepsyn -T 10 -S 483;&put;dch -f;map
module aes_sbox (input logic [7:0] x, output logic [7:0] y);
  logic g73, g109, g46, g9, g4, g67, g50, g86, g15, g37, g69, g59, g10, g48, g83, g43;
  logic g72, g32, g124, g58, g75, g35, g95, g2, g97, g49, g16, g14, g11, g88, g29, g54;
  logic g89, g45, g61, g6, g38, g39, g22, g53, g64, g111, g25, g70, g30, g23, g3, g68;
  logic g118, g66, g120, g76, g44, g7, g103, g51, g100, g18, g81, g8, g12, g19, g31, g102;
  logic g1, g17, g20, g79, g52, g34, g105, g91, g77, g0;
  assign y[5] = ((g105 ^ g95) ^ g76);
  assign g2 = ~(x[6] ^ x[1]);
  assign g30 = g29 ^ g15;
  assign g20 = g19 ^ g17;
  assign g29 = ((g23 & ~(g25 & ~g2)) ^ x[0]) ^ (g20 | ~g16);
  assign g75 = (g8 & ~g73) ^ g68;
  assign g22 = ~x[7];
  assign g111 = ~((~(g109 | g39)) ^ g83);
  assign g12 = g11 ^ x[4];
  assign g10 = ~(x[2] ^ x[0]);
  assign g19 = g18 ^ g2;
  assign y[3] = ((g124 ^ g120) ^ g86);
  assign g52 = g51 ^ g6;
  assign g45 = g44 | g30;
  assign g23 = g18 | g22;
  assign g51 = g2 ^ g22;
  assign g39 = g34 ^ g10;
  assign g88 = g69 & ~(g49 & ~g79);
  assign g3 = g2 ^ g1;
  assign g61 = ~((g50 & ~g59) ^ g45);
  assign g32 = g17 ^ g8;
  assign g105 = ~((g102 & ~g103) | g53);
  assign y[0] = (((g19 & ~g89) ^ g105) ^ g86);
  assign g31 = ~(x[5] ^ x[0]);
  assign g48 = (g18 & ~g46) ^ g35;
  assign g53 = x[3] & ~g52;
  assign g120 = g34 & ~g109;
  assign g34 = g0 ^ g9;
  assign g6 = ~x[4];
  assign g66 = (g49 | ~g44) & ~(g64 & g45);
  assign y[6] = ((g120 ^ (~(g118 ^ g103))) ^ ((g38 & ~g72) ^ g75));
  assign g124 = (~(g81 | g32)) ^ g102;
  assign g95 = (((~(g11 ^ x[5])) | g72) ^ g91) ^ (g51 & ~g89);
  assign g73 = g72 ^ g66;
  assign g49 = g48 ^ g15;
  assign g100 = ((g4 & ~g61) ^ g91) ^ g77;
  assign g64 = g58 ^ g43;
  assign g38 = g17 ^ g9;
  assign g44 = g43 ^ g37;
  assign g16 = g3 ^ g6;
  assign g0 = ~(x[7] ^ x[5]);
  assign g4 = g3 ^ x[5];
  assign g37 = (~(g35 ^ x[6])) ^ (g32 | g31);
  assign g50 = g44 | ~g49;
  assign y[4] = (g95 ^ g86);
  assign g17 = ~(x[3] ^ x[2]);
  assign y[1] = ((~(g105 ^ g100)) ^ g111);
  assign g76 = g75 ^ (g61 | g0);
  assign g54 = g25 & g23;
  assign g77 = g67 | g16;
  assign g102 = g88 | g1;
  assign g7 = ~(x[6] ^ x[7]);
  assign g69 = g64 | ~g30;
  assign g89 = ~(g88 ^ g61);
  assign g83 = ~((~(g32 ^ g31)) | g81);
  assign g91 = g12 & ~g73;
  assign g15 = g14 ^ (~(g4 | g0));
  assign g11 = g10 ^ g9;
  assign y[7] = (((g97 ^ g68) ^ (g124 ^ g118)) ^ g111);
  assign g14 = (g8 & ~g12) ^ x[3];
  assign g86 = ((g83 ^ (g66 & ~g18)) ^ g77) ^ g76;
  assign g18 = ~(x[4] ^ x[5]);
  assign g43 = ~(((g22 & ~g38) | (g38 & ~g39)) ^ g14);
  assign g72 = g50 & ~(g69 & ~g70);
  assign y[2] = (~(g100 ^ g97));
  assign g81 = ~((g50 & g30) | g79);
  assign g103 = ~(g88 | g52);
  assign g1 = ~x[3];
  assign g9 = ~x[1];
  assign g8 = g7 ^ g6;
  assign g109 = ~(g81 ^ g67);
  assign g68 = g67 | g20;
  assign g79 = g59 & ~g70;
  assign g97 = g54 & ~g89;
  assign g35 = g10 | ~g34;
  assign g59 = g58 ^ g37;
  assign g118 = ~(g66 & g46);
  assign g25 = (x[4] ^ x[5]) | x[7];
  assign g70 = ~(g48 ^ g29);
  assign g58 = ((g54 & ~x[1]) | (g7 & ~g54)) ^ g53;
  assign g46 = g38 ^ g8;
  assign g67 = g66 ^ g61;
endmodule

Solution.lean (7 code lines)

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

/-!
# aes_sbox: a tower-field (composite-field GF(((2^2)^2)^2)) netlist, proved by exhaustive kernel evaluation

`sv_exhaustive` (LeanModels/Sv/CombExhaustiveTactic.lean) compiles the flat netlist once into a packed gate
program, checks the compilation, and decides `y = sbox x` on all 256 inputs by kernel evaluation.
-/

namespace Submission

set_option maxHeartbeats 0 in
theorem solution : Goal := by sv_exhaustive

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: 122 cells. aes_sbox has one fixed size, so there is no smaller instance to draw.

The drawing is its critical path (15 cells, ending at y[3] rising, 3 208 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: 122 cells, 53 xnor2_1, 22 nand2_1, 20 xor2_1, 7 and2_1, 5 nand2b_1, 5 or2_1, 4 nor2_1, 4 nor2b_1, 2 mux2_1; 15 drawn. Open the drawing on its own (SVG, 14.9 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: 16 nets, 15 cells, to y[3] rising at 3 208 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[2]`	fall	input port	–	116.6	24.0
1	`_240_`	rise	`_322_`	`xor2_1`	356.6	260.9	240.0
2	`_241_`	rise	`_323_`	`xnor2_1`	557.9	247.8	201.3
3	`_242_`	rise	`_324_`	`xnor2_1`	716.7	142.7	158.8
4	`_243_`	fall	`_325_`	`nor2_1`	782.5	83.5	65.8
5	`_244_`	rise	`_326_`	`xnor2_1`	1 022.7	251.2	240.2
6	`_245_`	rise	`_327_`	`xnor2_1`	1 222.5	248.2	199.8
7	`_246_`	fall	`_328_`	`xnor2_1`	1 344.5	84.3	122.0
8	`_275_`	fall	`_357_`	`nand2b_1`	1 521.0	76.4	176.5
9	`_278_`	rise	`_360_`	`xnor2_1`	1 847.1	346.4	326.1
10	`_284_`	fall	`_366_`	`xnor2_1`	2 005.0	104.8	157.9
11	`_190_`	fall	`_387_`	`and2_1`	2 210.6	61.6	205.6
12	`_200_`	rise	`_399_`	`xnor2_1`	2 460.3	250.9	249.7
13	`_201_`	fall	`_400_`	`xnor2_1`	2 601.9	95.4	141.6
14	`_205_`	rise	`_404_`	`xnor2_1`	2 933.6	343.5	331.7
15	`_161_`	rise	`_421_`	`xor2_1`	3 208.4	247.4	274.8

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
`xnor2_1`	53	8.7584	464.1952	52.1%
`xor2_1`	20	8.7584	175.1680	19.7%
`nand2_1`	22	3.7536	82.5792	9.3%
`and2_1`	7	6.2560	43.7920	4.9%
`nand2b_1`	5	6.2560	31.2800	3.5%
`or2_1`	5	6.2560	31.2800	3.5%
`nor2b_1`	4	6.2560	25.0240	2.8%
`mux2_1`	2	11.2608	22.5216	2.5%
`nor2_1`	4	3.7536	15.0144	1.7%
total	122		890.8544

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

Legality: worst load 0.222 × max_capacitance, worst transition 0.252 × 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
`XNOR`	53	2.000	106.000
`NAND`	22	1.000	22.000
`XOR`	20	2.000	40.000
`AND`	7	1.333	9.331
`OR`	5	1.333	6.665
`ORNOT`	5	1.333	6.665
`ANDNOT`	4	1.333	5.332
`NOR`	4	1.000	4.000
`MUX`	2	2.333	4.666
total	122		204.659

The record

task: aes_sbox
player: tower-shuffle
assisted by: Claude Opus 5.5 (Anthropic)
submitted: 2026-11-05
notes: Made by an AI agent (Claude Opus, Anthropic) in the maintainers' newcomer study on 2026-11-05, as a new design rather than a variation of a shipped one; the agent chose the player name. The design is a flat netlist of 82 continuous assigns over & | ^ ~ for a tower-field (composite-field GF(((2^2)^2)^2)) AES S-box. It was generated by the agent's own program (polynomial bases, the composite-field inverse formula of Satoh et al. and Canright, greedy common-subexpression XOR layers; all 128 basis choices checked against the S-box on the 256 inputs), then re-optimized with the pinned Yosys and ABC (&deepsyn with searched seeds, then dch, written back as & | ^ ~ assigns), its single-use nets inlined to cut the number of assigns, and its statement order searched; every step was scored with score/ppa.py. The proof is one line, `theorem solution : Goal := by sv_exhaustive`: the library tactic compiles the netlist to a gate program and decides the output on all 256 inputs by kernel evaluation. The comments in both files are the agent's; the first line of the .sv names an intermediate netlist of the search and the ABC commands of one step. Re-recorded by the maintainers for the 2026-11-07 statement-fingerprint change; design and proof unchanged.
scoring point: the one fixed size
design: solution.sv sha256 cb336371552e63d0cd9de9439e2faf7bc8fbee407cb19868f1ebb5e5c7fcd06d
proof: Solution.lean sha256 18a23b398e3187d950fc400fe381e0972e61809df6c7baebd33689a39782c353
canonical text: sha256 9c2fb349e833dbdf9fd2ef3638d31d9066b8729e9bccdec6609258358687e926
record hash: d2880a7160dd09519db7626bdd17a0bff9cc65b9f87de0a6b66857c9dfc1ecc6
downloads: d2880a7160dd.sv d2880a7160dd.lean d2880a7160dd.json
previous frontier: none: this is the task's first submission

The proof

code lines: 7
build time: 59.11 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: 000130d1b08c3462e30e22fefe48567ac1f0a8d5
lean-surfaces revision: 000130d1b08c3462e30e22fefe48567ac1f0a8d5
canonicalization script: bbd11227d45dc1365f27597fd45c565fe721ba2648450588fc4fd983d00b367b
scoring script: ea58219d8ef14c3bad265218ee266ccdb709ac9d4dc5258edc34d51ee83a0445
GE table: 6a29196a3f4b58241f4c9af650c9141e4632b737214d563a11ba142a725c4bea
extractor: 4930696021c588c75dc890034c534c95560ad9a28a4955b87d1f8d68b5edbc0c
canonical RTLIL: 9354e2ca48e233fd026217297eeae9160a330503adcc9f747cbc29bee4423cd0

the checker's files (sha256)

file	sha256
`check.py`	`ceceeb055076dc2c59350f7778f09c600c8dfd96ff07485b9d6ba8d722ed69be`
`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: 70d819c8f54fc93940d18d46d85cc02601d570a555a3a7c93f3a2d6371acfd3c
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 · this design	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`	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 · this design	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`	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 d2880a7160dd09519db7626bdd17a0bff9cc65b9f87de0a6b66857c9dfc1ecc6.sv --task tasks/aes_sbox --path \
    --json out.json --netlist scored.v --repaired-netlist repaired.v

Expect, in out.json:

score.rtlil_sha256: 9354e2ca48e233fd026217297eeae9160a330503adcc9f747cbc29bee4423cd0
ppa.netlist_sha256: 17dab15a1dbbf2d016ae90e5bf85fc33136a09384a9ee9e1f560fd159f6b7511
ppa.repair.netlist_sha256: 44c5b4c32e8f30fd21fb1e931e045d76a692a2b8113e73fb044c6c1ab61d7354
ppa.area_e4um2_sky130: 8908544
ppa.delay_ps_sky130: 3208

The schematic and the critical-path data are site/schematics/aes_sbox/cb336371552e63d0.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 44c5b4c32e8f30fd…).

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 d2880a7160dd09519db7626bdd17a0bff9cc65b9f87de0a6b66857c9dfc1ecc6.sv --task tasks/aes_sbox --pdk asap7 --no-mapped \
    --json out.json

Expect, in out.json:

ppa.netlist_sha256: 17dab15a1dbbf2d016ae90e5bf85fc33136a09384a9ee9e1f560fd159f6b7511
ppa.repair.netlist_sha256: 5f16602fa6382d8361e34c1d4c8a8a1a34fd14b61da01a9eeee56d98c1393adf
ppa.area_e5um2_asap7: 1341360
ppa.delay_ps_asap7: 556

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=d2880a7160dd09519db7626bdd17a0bff9cc65b9f87de0a6b66857c9dfc1ecc6
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.