XChaCha20 encryption accelerator
Four FPGA cores generate encryption data in parallel. I co-designed the four-core version and led formal verification of its timing and control behavior.
- Role
- Undergraduate researcher, RTL design and verification
- Team
- 16 contributors, CRNCH, Georgia Tech
- When
- Fall 2025 to Spring 2026
- Board
- Avnet Ultra96-V2 (AMD Zynq UltraScale+ ZU3EG)
- Result
- 9.75 Gbps compute peak with 4 cores at 100 MHz
The design
tiny-xcc generates the keystream that software combines with a message to encrypt it. It supports ChaCha20 (RFC 8439) and XChaCha20 on an FPGA. Software writes inputs and reads results through memory-mapped registers on an AXI4-Lite interface; a mode bit selects the cipher.
Each core reuses four quarter-round units across 20 column and diagonal passes, one pass per clock. A 64-byte block is ready 21 cycles after initialization. Four cores compute separate blocks in parallel. While software reads a completed batch, the register wrapper starts the next one. If software advances the counter by the core count and that batch is already complete, the result is available immediately.
Every block takes the same number of cycles, regardless of its key, nonce, or data. That gives the host a fixed compute latency to work with.
My part
- Co-designed the four-core architecture with a teammate, who committed the implementation.
- Led formal verification and co-wrote the verification plan. Wrote SystemVerilog assertions for the ChaCha20 block core with a teammate, and for the add-rotate-xor cell and XChaCha20 controller. Set up their SymbiYosys checks.
- Profiled encryption in software on the board's ARM Cortex-A53 to establish a comparison baseline.
- Co-wrote the datasheet, design documentation, and integration guide.
How we verified it
The checks address whether software can trust the core's timing and control signals: when a result becomes ready, whether it stays stable, and what happens when a new request interrupts an old one. SymbiYosys explores these properties through bounded model checking:
- Block core, 25 cycles: reset clears the busy and output-ready flags; output becomes ready exactly 21 cycles after initialization; busy and ready never overlap; the completed output stays stable; inputs remain latched during a job; a new initialization preempts the old job and becomes the active request.
- XChaCha20 controller, 30 cycles with a deeper run to 50: initialization order, mutual exclusion between HChaCha20 and ChaCha20, and input updates. These checks use a single-core configuration.
- Add-rotate-xor cell, depth 1: checks the arithmetic step inside a quarter round at rotation value 0. The cell is combinational, so this check covers every input value for that rotation.
The block core has 11 documented properties and about 40 assertions; the controller and arithmetic cell add about 30. Separately, 25 Icarus Verilog testbenches compare cipher outputs with RFC 8439 and IETF draft test vectors. The project also has a Verilator branch-coverage report for the block-core tests.
Results
| Metric | Value | Conditions |
|---|---|---|
| Block latency | 21 cycles | From init to valid, per 64-byte block |
| Throughput, one core | ~2.44 Gbps | 64 bytes per 21 cycles at 100 MHz |
| Throughput, 4 cores | ~9.75 Gbps | Compute peak, before AXI read overhead |
| Back-to-back blocks | 22 cycles | A new init cannot land on the final-addition cycle, so sustained output is about 9.3 Gbps for 4 cores |
| Software baseline | 11 to 16 | Cycles per byte on the Cortex-A53 at 1.5 GHz (~0.75 to 1.09 Gbps) |
| Speedup | ~9 to 13x | 4-core peak against software. One core: ~2.2 to 3.3x |
| Fmax | 150 MHz | Vivado implementation, all builds. Throughput above is quoted at 100 MHz |
| Area | 23.8% LUT | 16,810 LUTs for the 4-core build (14.6% for one core), Vivado implementation, from the project datasheet. 0 BRAM, 0 DSP |
These speedups compare peak computation rates. Host transfers over AXI4-Lite reduce overall throughput; end-to-end host throughput was not measured.