aes

AES crypto core for FPGA — AES-128/192/256, encrypt and decrypt, FIPS-197 bit-exact.

An AES crypto core for FPGA — AES-128/192/256, encrypt and decrypt, FIPS-197 bit-exact, with ECB/CTR/CBC/XTS/GCM modes, a full verification stack (golden-model KAT, formal proofs, on-board HIL), and a timing-closed Vivado flow for the Digilent Arty A7-100T (xc7a100tcsg324-1).

Philosophy: the SystemVerilog is the product. RTL in rtl/ is readable and self-contained; the Python layer never emits core datapath logic — only constant tables (S-box/Rcon), golden vectors, and test/formal orchestration.

Top features

Area	Detail
Cipher	AES-128 / 192 / 256, encrypt + decrypt, FIPS-197 / NIST CAVP bit-exact
Architectures	(a) round-rolled iterative (1 round/clk) and (b) fully-pipelined `aes_core_pipe` (1 block/clk, ~12.8 Gbit/s @100 MHz AES-128)
S-box	table · composite-field GF((2⁴)²) `aes_sbox_comp` (LUT-free) · first-order DOM-masked `aes_sbox_dom` (2 shares, fresh randomness, 5-stage pipeline) — all proven equal to the table for every input
Round transforms	SubBytes / ShiftRows / MixColumns + inverses, GF(2⁸) poly 0x11B, fully-unrolled constant-slice datapath (synthesis/formal clean)
Key schedule	Sequential on-load expansion (one word/clock), AES-128/192/256, key zeroization, straightforward inverse cipher
Modes	ECB · CTR · CBC · XTS (storage) · GCM/AEAD — verified against pycryptodome / OpenSSL. GCM handles any IV length (96-bit fast path + GHASH-derived J0) and arbitrary AAD/plaintext byte lengths (partial blocks, AAD-only/GMAC, empty); XTS (IEEE 1619 / SP 800-38E) for AES-128/256, block-aligned data units, cross-checked against the OpenSSL XTS reference; GHASH multiplier selectable: single-cycle parallel (default, closes 100 MHz) or bit-serial
Bus / IP	AXI4-Stream data plane + AXI4-Lite control (`aes_axi_top`), drop-in for a Vivado block design
Portability	plain behavioral SV — vendor specifics isolated in a technology abstraction layer (`rtl/tech/`: generic/Xilinx/Intel/Lattice, `TECH=` selectable); packaged as vendor-neutral IEEE 1685-2014 IP-XACT (`make ipxact`) and as a Vivado IP (`make ip`)
Verification	2500+ KAT vectors (FIPS-197 + AESAVS Variable-Key/Variable-Text) + NIST Monte Carlo Test + NIST SP 800-38A + 300-case ACVP + CTR/CBC/GCM/AXI/S-box TBs, SymbiYosys formal (control contract proven), post-implementation gate-level timing sim (SDF back-annotated), on-board continuous HIL
Board	Arty A7-100T HIL: power-on self-test LED beacon + UART KAT server. Two builds, both timing-closed at 100 MHz and board-verified — iterative (Fmax ≈ 103 MHz) and pipelined (`aes_core_pipe`, Fmax ≈ 105 MHz, 2000/2000 on-board)

Repository layout

rtl/        SystemVerilog source (the product), grouped by function
  common/   tables_pkg.sv (S-box/Rcon constants), pkg.sv (GF(2^8) + transforms),
            sbox_comp_pkg.sv (composite-field maps), gf4_pkg.sv
  core/     key_schedule.sv, core.sv (iterative enc/dec 128/192/256),
            core_pipe.sv (1 block/clock), block.sv (single-block API),
            sbox_comp.sv (composite GF((2^4)^2) S-box), transforms.sv
  modes/    ctr.sv cbc.sv xts.sv (storage), ctr_pipe.sv,
            ghash_mul.sv ghash_mul_par.sv gcm.sv gcm_pipe.sv (GCM/AEAD)
  masking/  dom_mul_gf4.sv, sbox_dom.sv (DOM S-box), core_masked.sv,
            core_masked_dec.sv, key_schedule_masked.sv, masked.sv
  bus/      axil_ctrl.sv, axi_stream.sv, axi_top.sv (AXI4-Lite + AXI4-Stream IP)
  io/       uart_tx.sv, uart_rx.sv (8N1 UART for the board)
  tech/     technology abstraction layer: aes_tech_sync per vendor
            (generic/ xilinx/ intel/ lattice/, one dir compiled per build)
ipxact/     vendor-neutral IEEE 1685-2014 IP-XACT package (generated, make ipxact)
model/      Python golden model + NIST/ACVP/XTS vector generation
tb/         Verilator self-checking testbenches (block KAT, modes, masking, TVLA)
formal/     SymbiYosys harnesses + .sby (control contract, datapath invertibility)
hw/         aes_hil_top.sv / aes_hil_pipe_top.sv, Arty A7-100T XDC, Vivado TCL
scripts/    gen_tables.py (constants), hil_test.py (host-side continuous HIL)

Module names keep the aes_ prefix (e.g. aes_core) for namespace safety when the IP is dropped into a host SoC; only the file names are unprefixed.

Byte ordering (important)

Big-endian throughout: for a 128-bit word, logical byte i occupies bits [8*(15-i) +: 8], byte 0 is the MSB. The AES state is column-major (state_byte[i] -> row = i%4, col = i/4). Keys and data on every interface are MSB-first, matching the FIPS-197 test-vector presentation.

Quick start

make sim            # regenerate tables+vectors, build & run the KAT (incl. AESAVS)
make sim-all        # every testbench: block/ctr/cbc/pipe/gcm/axi/sbox
make mct            # NIST Monte Carlo Test (100x1000 chained, ECB 128/192/256)
make lint           # Verilator lint of the full HIL hierarchy
make formal         # SymbiYosys: prove the ready/valid contract + FSM safety
make formal-xforms  # SymbiYosys: prove inverse transforms invert the forward ones
make synth          # Vivado synth+impl on Arty A7-100T, gated on timing closure
make prog           # program the board over USB (openFPGALoader)
make hil PORT=/dev/ttyUSB1   # continuous on-board KAT vs pycryptodome

Simulation (Verilator)

make sim runs tb/tb_aes_block.sv against tb/vectors.hex (generated by model/gen_vectors.py). The vector set includes the FIPS-197 appendix-C anchors (128/192/256), the AESAVS Variable-Key and Variable-Text known-answer tests, and randomized round-trips in both directions — 2500+ vectors, e.g.:

AES KAT: 2526/2526 passed (0 errors)
AES P 0000

make mct runs the NIST AESAVS Monte Carlo Test — 100 outer × 1000 inner chained ECB operations with key feedback, for encrypt and decrypt across all three key lengths — checked against pycryptodome (MCT P 0000). This chained test surfaces key-schedule/datapath bugs that independent vectors miss.

The mode engines are checked against the NIST SP 800-38A published known-answer vectors (CBC and CTR, 128/192/256) — exact published ciphertext, not just round-trip (tb_nist_kat, NIST38A P 0000).

make acvp generates ACVP-format vector sets (NIST ACVP JSON shape: AES ECB/CBC/CTR, AFT, encrypt+decrypt, all key lengths — build/acvp/*.json) and runs all 300 cases through the RTL, checking against the ACVP-expected responses (ACVP: ALL PASS). This is the structure a CAVP/ACVP submission uses.

CTR mode: tb/tb_aes_ctr.sv encrypts an 8-block message and decrypts it back, proving the stream cipher round-trips (CTR P 0000).

make coverage merges Verilator line coverage across the testbenches and reports it for rtl/ only: 97.6% (164/168), the remainder being unreachable FSM default branches (defensive code).

make tvla runs a simulated first-order TVLA (Hamming-weight leakage model, fixed-vs-random Welch t-test). On the DOM-masked S-box the masked design shows max |t| = 0.55 at 100k traces/group (no first-order leakage in the model) vs |t| = 42 for the +NOMASK negative control. make tvla-core runs the same assessment on the whole masked AES-128 core (round-state shares): max |t| = 1.97 at 50k traces vs |t| = 310 unmasked. The controls show the test is sensitive and the masking holds in the model — a model-based check, not a substitute for measured traces on silicon (which can leak through glitches and routing that a Hamming-weight model does not capture).

Formal (SymbiYosys)

The OSS formal path flattens the SV with sv2v then runs SymbiYosys/Yosys:

formal/aes_core.sby — proves the AXI-style ready/valid contract and FSM safety on aes_core: no overlap of accept/emit, no phantom output, payload held stable while stalled, and bounded progress (output within Nr+2 cycles). The control path is data-independent, so key/data are pinned to constants to keep the proof fast.
formal/aes_xforms.sby — proves the inverse linear layers exactly invert the forward ones for all 2¹²⁸ inputs: InvShiftRows∘ShiftRows and InvMixColumns∘MixColumns are each the identity (something simulation can't cover). The nonlinear S-box's invertibility is instead covered exhaustively in simulation (tb_aes_sbox_comp, 256/256) — its LUT does not bit-blast efficiently for SMT.

On-board (Arty A7-100T)

make synth runs the non-project Vivado flow (hw/tcl/build_arty.tcl): synth → place → phys_opt → route → reports, and fails the build if WNS or WHS is negative (timing-closure gate). Then make prog loads the bitstream.

On the board, aes_hil_top:

Power-on self test — encrypts the FIPS-197 C.1 vector in hardware and checks it. led[3] = pass, led[2] = fail (sticky). led[0] = heartbeat.
UART command server (115200 8N1) — the host streams 50-byte frames op | klen | key(32) | data(16) and the core replies with 16 result bytes.

make hil runs scripts/hil_test.py, which fires thousands of random vectors at the board and checks every reply against pycryptodome — the silicon equivalent of the simulation KAT, for continuous regression on real hardware.

There are two board builds. make synth && make prog is the iterative core; make synth-pipe && make prog-pipe is the pipelined core (aes_core_pipe), which closes at ~105 MHz and passed 2000/2000 AES-128-encrypt vectors on-board (scripts/hil_test.py --enc-only --klen 0). Both gate the build on timing closure — a negative worst-slack aborts before the bitstream is written.

Gate-level (post-implementation timing sim)

make gate-sdf runs aes_block through out-of-context synth + implementation, then launch_simulation -type timing: Vivado back-annotates the routed SDF (cell + interconnect delays, with setup/hold checks) onto the netlist and runs the KAT against the gates with real delays — a timing-accurate sign-off that the implemented logic is correct, not just the RTL. make gate is the faster functional check on the same post-route netlist (no annotation).

Performance & resources

Both HIL builds are timing-closed at 100 MHz on Arty A7-100T (xc7a100t-1) and verified on the board:

HIL build	WNS @100 MHz	Fmax	LUT / FF / BRAM	On-board KAT
Iterative (`aes_hil_top`)	+0.302 ns	≈ 103 MHz	4911 / 2881 / 0	continuous, all key lengths
Pipelined (`aes_hil_pipe_top`)	+0.493 ns	≈ 105 MHz	8694 / 3635 / 0	2000/2000 AES-128 encrypt

make maxf characterizes the ceiling with performance-directive synthesis (PerformanceOptimized + retiming) and Explore place/route + double phys-opt: the iterative core reaches Fmax ≈ 113 MHz (5142 LUT). The limit is the round's S-box→MixColumns feedback loop — retiming can't break it, so the gain is place/route quality, not register rebalancing.

The pipelined core takes a SUBPIPE parameter: with SUBPIPE=1 a second register after the S-box splits each round into two shorter stages, lifting the pipelined Fmax from ≈ 105 to ≈ 123 MHz (build_arty_pipe_maxf.tcl) at +1.5k FF, same 1 block/clock throughput (latency 2·NR+1). The composite S-box logic depth is then the floor (~8 ns/stage); pushing into the 150 MHz+ range needs a shorter-depth S-box or a register inside the S-box. (Running the board above 100 MHz needs an MMCM to synthesize the faster clock from the 100 MHz input.)

Throughput (block = 128 bits):

Core	Cycles / block	Datapath throughput @100 MHz
Iterative AES-128 (`aes_core`)	~12	≈ 1.07 Gbit/s
Iterative AES-192	~14	≈ 0.91 Gbit/s
Iterative AES-256	~16	≈ 0.80 Gbit/s
Pipelined AES-128 (`aes_core_pipe`)	1 (1 block/clk, +11 latency)	≈ 12.8 Gbit/s

The pipelined figure is the datapath rate when fed one block/clock at the closed 100 MHz (timing verified on the board above); sustaining it needs a matching data source — the pipelined CTR/GCM provide that, the UART HIL does not (it's single-frame, so it confirms correctness, not line rate).

Notes:

Iterative latency excludes the one-time key expansion (4·(Nr+1) clocks, amortised over all blocks under one key).
GCM: the iterative aes_gcm tracks the iterative cipher rate (single-cycle GHASH, so authentication is not the bottleneck). aes_gcm_pipe is the line-rate variant — pipelined CTR (1 block/clk) + a 1-block/clk serial GHASH around the single-cycle multiplier → ~12.8 Gbit/s AEAD at 100 MHz (96-bit IV, block-aligned; bulk runs at 1 block/clk, only setup/AAD-fill bubble).
DOM-masked S-box: 5-cycle latency, 2 shares, 20 fresh random bits/clock.
0 BRAM because the S-box is logic (composite field / table-as-LUTs), not a memory — which is also what makes the masked variant possible.

How to continue (roadmap)

Done: iterative + pipelined cores (both timing-closed and board-verified on the Arty A7-100T), ECB/CTR/CBC/XTS/GCM (any IV length, partial blocks), AXI IP, composite S-box, single-cycle GHASH, the full KAT stack (FIPS-197 + AESAVS + NIST Monte Carlo + NIST SP 800-38A + 300-case ACVP) at 97.6% coverage, SymbiYosys formal, post-route gate-level timing sim with SDF back-annotation, and a first-order DOM-masked S-box (simulated TVLA) plus a DOM-masked AES datapath core. Remaining build-out:

Complete the masked core — aes_masked.sv is a fully first-order masked AES-128 encrypt: both the key schedule (aes_key_schedule_masked, DOM SubWord) and the cipher datapath (aes_core_masked, AES-128/192/256) operate on shares, so no key/round-key/state is ever unmasked; verified to unmask to the reference and (datapath) to pass a first-order TVLA. Masked decrypt (aes_core_masked_dec, inverse DOM S-box) and the masked key schedule for 128/192/256 are also done, and aes_masked_block now wraps both directions under one masked key schedule (fully-masked encrypt + decrypt; checked unmasked against the reference and round-trip, both ways). Still open: a leakage assessment on real silicon traces (the TVLA here is a Hamming-weight model, not a substitute for lab measurement), and a masked AEAD top (a masked GHASH is the larger remaining piece).
Pipelined GCM throughput tuning — aes_gcm_pipe is feature-complete (any IV length, partial blocks, AAD-only) at ~12.8 Gbit/s. For a 96-bit IV the one-time setup now overlaps E_K(0) (=H) and E_K(J0): both are pushed through the pipeline back-to-back instead of serially, saving ~LAT (~11) cycles per message — most of the short-message setup bubble. Remaining: the AAD→ciphertext pipe-fill bubble and the non-96-IV path (where J0 depends on H).
Round-trip formal (layer-wise done) — all three round transforms are now proven invertible over all 2¹²⁸ states: ShiftRows and MixColumns (make formal-xforms) and the nonlinear S-box (make formal-sbox: InvSubBytes(SubBytes(x)) == x, ~2 min in boolector). With AddRoundKey trivially self-inverse, the full round inverts by composition. The composed round-trip / key-schedule equivalence in a single SMT call is intractable (the S-box datapath does not bit-blast — confirmed by a timed-out full-round proof), so the composed cipher is covered both directions by KAT + NIST MCT instead.
CDC sign-off (done) — the design is a single clock domain (no inter-clock CDC); the async inputs (button reset, UART RX) use ASYNC_REG 2-FF synchronizers, and make cdc (report_cdc) reports all paths safely timed.

Lint is -Wall-clean (make lint, and make lint-tech re-lints the full hierarchy against every rtl/tech/ vendor); CI (GitHub Actions) runs lint + the simulation suite + the formal proof on every push. Two IP packagings: make ipxact emits a vendor-neutral IEEE 1685-2014 IP-XACT package (ipxact/, consumable by Kactus2 and other 1685-2014-aware tools), and make ip packages aes_axi_top as a Vivado IP (interfaces auto-inferred). Both share one register-map source of truth (gen/regmap.py, documented in docs/registers.md). Vendor-specific synthesis attributes live only in the technology abstraction layer (rtl/tech/, TECH=generic|xilinx|intel|lattice). To drop the core into a design, see the integration guide.

Toolchain

Verilator 5.x · Icarus 12 · Yosys + SymbiYosys + sv2v · yices/boolector · Vivado 2025.2 · openFPGALoader · Python 3 + pycryptodome + pyserial.