LeNet-5 ASIC Convolution Accelerator

A verified, technology-independent RTL implementation of the LeNet-5 inference datapath, built as a semi-custom ASIC starting point. Every testbench checks the SystemVerilog against a bit-exact Python oracle — none of them assert hand-written expected values.

• the canonical 1998 LeNet-5 architecture, including sparse C3 connectivity;
• a NumPy floating-point model of C1/S2/C3/S4/C5/F6/RBF;
• a bit-exact signed-int8 convolution golden model;
• synthesizable SystemVerilog for a 5-lane row-stationary convolution PE;
• a configurable, memory-backed 5x5 convolution reference engine;
• a full lenet5_top that sequences C1→S2→C3→S4→C5→F6→classifier;
• self-checking RTL tests with generated golden vectors and backpressure;
• real area/timing/power against the sky130hd PDK for every storage-free arithmetic block, plus semi-custom implementation guidance for the rest.

The RTL was written technology-independent, but it is no longer PPA-blind: docs/PPA.md has real gate-level area, static-timing slack, and power against sky130hd for conv5x5_pe and its four sibling leaf blocks — pre-layout (synthesis + STA, no place-and-route yet; see that doc for exactly what is and is not covered).

Pipeline

flowchart LR
    IMG["image<br/>1x32x32 int8"] --> C1["C1<br/>conv2d_engine<br/>6x28x28"]
    C1 --> S2["S2<br/>avg_pool2x2<br/>6x14x14"]
    S2 --> C3["C3<br/>conv2d_engine<br/>sparse, 16x10x10"]
    C3 --> S4["S4<br/>avg_pool2x2<br/>16x5x5"]
    S4 --> C5["C5<br/>conv2d_engine<br/>120x1x1"]
    C5 --> F6["F6<br/>dense_engine<br/>84"]
    F6 --> CLS["classifier_argmax<br/>10"]
    CLS --> OUT["class_o"]

Loading

One conv2d_engine instance is resource-shared across C1, C3, and C5; one avg_pool2x2_stream across S2 and S4. The reusable physical-design block is conv5x5_pe — five signed multipliers evaluating one kernel row per accepted cycle, with a stationary int32 accumulator. See docs/ARCHITECTURE.md for dataflow rationale and the fixed-point contract.

Verification status

All nineteen regression stages below pass under Icarus Verilog 12.0 and Siemens ModelSim; generic synthesis passes under Yosys. Separately from simulation, make equiv proves by SAT that each synthesized netlist computes the same function as its RTL — 1,592 equivalence points across the three synthesizable leaf blocks, none unproven. make equiv-mapped carries that proof onto the sky130hd-mapped netlist behind docs/PPA.md for the two blocks where unbounded SAT converges, and make gls re-runs the existing testbenches against those mapped netlists for the blocks where it does not — see docs/VERIFICATION_PLAN.md for which is which and why.

The two multiply-accumulate blocks are the ones neither SAT tier can reach, so they now carry their own block-level testbenches — every lane swept across the full int8 range on both operands, weights rotated to pin lane pairing, and rows that cancel to exactly zero. Driven that way, gate-level mutation testing catches 5/5 on each; driven through their wrappers, the same netlists and the same mutations score 4/5 and 2/5. That comparison is the tier's real result and is written up in results/mac_stimulus_20260815.log.

The PE's control logic around those MACs got the same treatment, taking its netlist from 3/4 to 4/4 and the tier as a whole to 23 of 24 (results/pe_stimulus_20260816.log). The one mutation that survives every testbench turned out not to be a coverage gap at all: it changes the output register only on cycles where out_valid_o is low, and scripts/prove_pe_output_hold.sh proves by SAT that no valid/ready consumer can observe it — with a cover check and a negative control, because a bounded proof that cannot fail proves nothing.

The engines are also checked at the shapes the real network actually uses. tb_lenet5_top drives C1/C3/C5/F6/classifier already, but only checks the final predicted class, which tolerates a great deal of intermediate error. tb_layer_shapes drives the same five shapes through standalone conv2d_engine and dense_engine instances and checks every beat against deploy_forward_int8 — reconfiguring each engine between shapes with no reset, which no engine-level testbench had exercised before. Corrupting one entry of the sparse C3 table fails it immediately with the offending connection count; the same corruption leaves tb_lenet5_top's predicted class correct and trips only its cycle-count check, 400 cycles off, with no indication of what moved.

Everything above checks the RTL against a golden model driven by untrained weights. That is the right stimulus for arithmetic — uniformly random weights push accumulators through ranges a trained network never visits — but it cannot answer whether the accelerator recognises a digit, because the model it is compared against does not either. tb_trained_mnist closes that. A LeNet-5 with this design's exact topology, including the 60/96 sparse C3 table as a training constraint, reaches 99.13% on the MNIST test set in float and 99.11% after quantization to the power-of-two fixed-point scheme requantize.sv implements — a 0.02-point drop, with per-layer shifts calibrated to 9/8/9/9 rather than the flat 7 every other tier uses. The RTL then classifies the first ten MNIST test digits, in dataset order and unmodified, 10 of 10 correctly, matching the golden model exactly on each. It is also the only tier that instantiates lenet5_top at non-default SHIFT_* parameters, and the only one that streams different images back to back with the weight ROMs resident — which is what makes its third assertion possible: every inference must cost an identical number of cycles, so inference time cannot depend on image data.

Check	What it proves
golden.test_golden	quantization corner cases + the full floating LeNet-5 shape chain
lint	SystemVerilog elaboration of the complete RTL list, three top modules
tb_conv5x5_pe	PE accumulation, bias injection, requantization, output backpressure
tb_requantize	5,504-case differential sweep vs the oracle: half-way rounding, both saturation boundaries, shift=0 bypass, int32 extremes, plus randomized coverage
tb_conv5x5_row_mac	6,592-case sweep of the 5-tap MAC: every lane across the full int8 range on both operands, the largest-magnitude product in every lane, weight rotation to pin lane pairing, and sums that cancel to exactly zero
tb_dense_row_mac	the same for the 8-lane dense MAC, 9,540 cases
tb_conv5x5_pe_stream	848 pixels of 1–8 rows through the PE's control logic: every shift 0–31 with ReLU off and on, both saturation rails, bias to ±2²⁸, single-beat pixels, pixels started while the previous one is still requantizing, and randomized backpressure on both streams
tb_lenet5_c3_connectivity	the exact 60 canonical C3 input-map connections
tb_conv2d_engine	48 engine outputs vs the Python int8 oracle
tb_avg_pool2x2_stream	12 pooling outputs vs the oracle
tb_dense_engine	5 F6 outputs vs the oracle
tb_classifier_argmax	predicted class vs the oracle
tb_classifier_argmax_tie	tied max score resolves to the lowest index
tb_config_guard	all 22 config-validation reject conditions across the four engines, each proven inert, plus recovery on a legal config
tb_robustness	the three streaming engines reproduce their unstalled output beat for beat under pseudorandom backpressure and after a mid-stream reset; a continuous protocol checker catches withdrawn valid and payload movement while stalled
tb_extremes	-128 and +127 at every operand position, at the largest layer the engines accept (400 MACs) and the smallest legal one; a second pass with weights cancelling to zero at shift 0 resolves a single wrong product; dense_engine's raw out_acc_o checked against the golden model
tb_layer_shapes	conv2d_engine and dense_engine driven standalone through the real network's own five shapes — C1 1x32x32→6x28x28, C3 6x14x14→16x10x10 with the live 60-connection sparse table, C5 16x5x5→120x1x1, F6 120→84, classifier 84→10 — each engine reconfigured between shapes on one instance with no reset, every beat checked against deploy_forward_int8 rather than only the final class
tb_lenet5_top	full 32x32 image end-to-end vs deploy_forward_int8, twice back-to-back with no reset, plus 20/20 state and 33/33 transition coverage of the control FSM
tb_trained_mnist	a trained network (99.11% INT8 on the MNIST test set) classifying ten real MNIST digits in dataset order, 10/10 correct and all ten matching the golden model; the only tier at non-default SHIFT_* parameters (9/8/9/9), and the only one streaming different images with weights resident — which lets it assert that every inference costs identical cycles regardless of image data

Nominal cost

Metric	Value
Canonical trainable parameters	60,000
C3 input-map connections	60 (not 96)
MACs across C1/C3/C5	315,600
PE row cycles across C1/C3/C5	63,120
End-to-end measured cycles (lenet5_top, ModelSim)	209,290
Steady-state cycles per inference (ROMs already resident)	146,544

The 209,290 figure is the cold path: the host writing all 62,730 ROM words plus one inference. 146,544 is the per-image cost once the weights are resident, measured start_i to done_o; tb_lenet5_top runs two inferences back to back with no reset and fails if either count moves.

The end-to-end figure includes every per-layer weight/bias ROM load and is a non-overlapped, resource-shared sequencing baseline — not a throughput target. Overlapping ROM loads with the previous stage's compute is the obvious first optimization.

Quick start

Requirements:

• Python 3.10+ and NumPy
• Icarus Verilog 11+ (iverilog, vvp) or Siemens ModelSim/Questa
• optional Yosys for generic synthesis

sudo apt-get install -y iverilog yosys python3-numpy

Run the complete open-source regression:

make regression

Run generic synthesis of the arithmetic leaf blocks:

make synth

Prove each generic netlist computes the same function as the RTL it came from — by SAT and induction over all inputs, not by replaying vectors (~8 minutes, equiv_status -assert fails the target on a single unproven point):

make equiv

Carry the same proof onto the sky130hd-mapped netlist, for the two blocks where unbounded SAT converges (needs the sky130hd liberty from an ORFS install; set ORFS_ROOT if it is not at /root/OpenROAD-flow-scripts):

make equiv-mapped

Re-run the existing testbenches against the sky130hd-mapped netlists instead of the RTL — same golden vectors, gates underneath — which is how the mapped MAC blocks get checked at all. Each netlist is built once and driven by every testbench that reaches it, since mapping is the only expensive step:

make gls

Run real sky130hd area/timing/power (needs yosys and openroad on PATH; see docs/PPA.md for what it produces):

make ppa

Check that docs/PPA.md still matches those results (Python only, no PDK needed — CI runs it on every push):

make check-ppa

Run in ModelSim/Questa:

python golden/generate_vectors.py
vsim -do scripts/modelsim.do

On Windows PowerShell, from the project folder:

.\scripts\run_modelsim.ps1

Waveforms are written to results/conv2d_engine.vcd by Icarus and to results/conv2d_engine.wlf by ModelSim.

Repository map

Path	Purpose
rtl/conv5x5_pe.sv	Primary semi-custom arithmetic block
rtl/conv2d_engine.sv	Memory-backed reference scheduler and engine
rtl/lenet5_c3_connectivity.sv	Exact canonical C3 sparse table
rtl/lenet5_top.sv	Full pipeline, resource-shared across layers
golden/lenet5.py	Full canonical floating-point network
golden/quantized_conv.py	Bit-exact int8 RTL oracle
golden/deploy.py	End-to-end int8 deployment model the RTL implements
tb/	Self-checking SystemVerilog tests
docs/ARCHITECTURE.md	Dataflow, performance, and LeNet mapping
docs/INTERFACES.md	Cycle-level and tensor-layout contracts
docs/SEMICUSTOM_FLOW.md	RTL-to-GDS plan and sign-off checklist
docs/VERIFICATION_PLAN.md	Verification scope and remaining work
docs/PPA.md	Real sky130hd area/timing/power, pre-layout
synth/	Generic synthesis scripts and 100 MHz sample SDC
asic/openroad/	OpenROAD Flow Scripts configuration, run script, toolchain patches
asic/sta/	Real sky130hd synthesis + OpenSTA sweep (make ppa), and the raw CSV/logs docs/PPA.md is checked against

Important project boundary

Wherever the vectors carry weights, they are deterministic random values chosen to verify arithmetic, not trained MNIST weights, and no accuracy claim rests on them — a predicted class from those tiers is an arithmetic result, not a recognition result. tb_trained_mnist is the sole exception and the only source of an accuracy figure in this repository: it runs a genuinely trained, calibrated, quantized network at 99.11% INT8, measured once on the MNIST test set with the per-layer shifts fitted to training images only. Do not generalize that figure to the other tiers, and do not generalize their random weights to it. A classifier tapeout still additionally requires SRAM integration, DFT, physical implementation, and PVT sign-off, none of which exist here.

Key references

• Y. LeCun, L. Bottou, Y. Bengio, and P. Haffner, “Gradient-Based Learning Applied to Document Recognition”, Proceedings of the IEEE, 1998.
• Y.-H. Chen et al., Eyeriss project and publications, for the principle that reducing data movement and exploiting reuse are central to energy-efficient CNN hardware.
• OpenROAD Flow Scripts tutorial, for an open RTL-to-GDS implementation path.

Contributing

See CONTRIBUTING.md. The short version: golden model first — update the Python oracle, regenerate vectors, then make the RTL match. CI fails if the committed vectors drift from what golden/ generates.

License

MIT — see LICENSE.