19 synthesisable Verilog RTL modules with 72 formally verified properties. Targets 5 FPGA families.
| Module | Purpose |
|---|---|
| sc_lif_neuron.v | Q8.8 fixed-point LIF neuron |
| sc_bitstream_encoder.v | LFSR stochastic bitstream generation |
| sc_bitstream_synapse.v | AND-gate synaptic multiplication |
| sc_mux_add.v | Multiplexer-based scaled addition |
| sc_cordiv.v | CORDIV stochastic division (Li et al. 2014) |
| sc_dense_layer_core.v | Dense layer computation pipeline |
| sc_dense_matrix_layer.v | Full matrix dense layer |
| sc_axil_cfg.v | AXI-Lite configuration interface |
| sc_axis_interface.v | AXI-Stream data interface |
| sc_dma_controller.v | DMA controller for data transfer |
| sc_aer_encoder.v | Address-Event Representation encoder |
| sc_event_neuron.v | Event-driven neuron (activity-gated) |
| sc_aer_router.v | Spike packet router |
| + 6 co-simulation testbenches (tb_sc_*.v) | |
Post-implementation resource, timing, and power from the v3.15.35 hardware benchmark report (Vivado flow, validated 2026-06-06).
| Design | Config | LUTs | DSPs | Fmax (MHz) | Power (mW) |
|---|---|---|---|---|---|
| LIF Neuron | Q8.8 | 156 | 0 | 312 | 12 |
| Dense Layer | 64×32 | 1,450 | 32 | 250 | 85 |
| AER Router | 16-port | 890 | 0 | 400 | 45 |
Bit-true parity between Python simulation and emitted RTL verified for all Q-formats.
Xilinx 7-series Intel FPGAs Lattice iCE40 Lattice ECP5 Gowin
Open-source: Yosys + nextpnr. Commercial: Vivado, Quartus.
Q8.8 fixed-point LIF neuron with configurable leak, gain, threshold, refractory period, and noise input. Bit-true match with Python simulation.
Simplified excerpt. Full module includes refractory period, saturation, reset logic, and debug output. 72 properties formally verified by SymbiYosys.
7 SymbiYosys modules with SMT solver backend verify 72 properties across all HDL modules. Properties cover: arithmetic overflow, state machine correctness, reset behaviour, timing constraints, bitstream integrity.
Activity rate: 0.01–10%. AER encoder packs spike events. Event neuron gates computation on activity. Router delivers spikes to target populations.