Stochastic & Neuromorphic Computing  /  Learn  /  Neuromorphic hardware

Neuromorphic hardware
from equation to proven silicon

The reason to compute with spikes and probability is that both map directly onto logic gates. This page follows a single neuron the whole way down: from an ordinary differential equation, to generated RTL, to a bit-true co-simulation that proves the Python and the Verilog agree cycle-for-cycle, to open Yosys synthesis on a real FPGA, and finally to a formal proof that the hardware cannot misbehave.

The lowering — one command, five stages

A trained network is not "run" on an FPGA; it is lowered onto one. Each stage is a well-defined, checkable transform, and SC-NeuroCore keeps every stage bit-true so the model you trained is provably the circuit you ship.

Neuron ODE
dv/dt = f(v,I)
→
Quantise
Q8.8 / Q4.12 / Q16.16
→
Generate RTL
SystemVerilog
→
Co-simulate
iverilog, bit-true
→
Synthesise
Yosys + nextpnr
and, in parallel — formal proof of each generated module with SystemVerilog Assertions + SymbiYosys
# the whole path, driven from one CLI
sc-neurocore compile "dv/dt = -(v-E_L)/tau + I/C" \
  --threshold "v > -50" --reset "v = -65" \
  --params "E_L=-65,tau_m=10,C=1" --init "v=-65" \
  --target ice40 --testbench --synthesize
The five stages, explained
01RTL — the generated hardware

RTL (register-transfer level) is the description of a circuit as registers and the combinational logic between them — it is the input a synthesis tool turns into gates. SC-NeuroCore emits human-readable SystemVerilog: a fixed-point datapath for the neuron's state update, an event neuron that only recomputes when a spike arrives, and an address-event (AER) router that carries spikes as compact addresses instead of dense vectors. Because idle neurons do no work, the event RTL toggles 15–39× fewer registers than a clocked datapath.

Deeper: fixed-point state and the module set
The neuron state is carried in signed fixed-point — Q8.8 by default (8 integer, 8 fractional bits), so a register value $r$ represents the real number $r/2^{8}$. The update is an integer add/shift/compare with no floating-point unit, which is what makes a neuron a few dozen LUTs rather than a DSP block. SC-NeuroCore ships over 40 synthesizable HDL modules — the neuron datapath (LIF, event-driven and voltage-scaled neurons), the AER encoder, router and priority queue, the stochastic-computing arithmetic (CORDIV, MUX-adder, decorrelator), dense-layer cores (folded Q8.8, int8-sparse, mixed-precision, block-floating), axonal delays, DMA and AXI interfaces, plasticity synapses (STDP, R-STDP), softmax attention and safety blocks (a triple-modular-redundancy voter, precision guards). The same modules feed both co-simulation and synthesis so there is a single source of truth. See the hardware page for the full module list and Verilog exports.
40+ Verilog modules →What a spike is →
02Co-simulation (COSIM) — proving Python = Verilog

A generated circuit is only trustworthy if it does exactly what the model did. Co-simulation runs the Python neuron and the generated Verilog side by side on the same input and checks they agree. SC-NeuroCore auto-generates a Verilog testbench that drives a constant current for N clock cycles, compiles and runs it with the open Icarus Verilog simulator (iverilog + vvp), and compares the two spike trains. The match is bit-true — cycle-exact, not "close".

# generate the RTL + a self-checking testbench, then co-simulate
sc-neurocore compile model.nir --target sim --testbench
pytest tests/hardware/test_cosimulation.py # skips cleanly if iverilog absent
Deeper: precision tiers and verified parity
Co-simulation is run at three fixed-point precisions — Q8.8 (16-bit) as the baseline, Q4.12 (16-bit, more fractional bits) and Q16.16 (32-bit) — so a designer can trade area for accuracy with evidence. Six deterministic Q8.8 baseline models are verified this way; five reach exact spike-count parity, and Izhikevich carries a declared one-spike Q8.8 quantisation boundary (exact at Q16.16). The testbench is self-checking and the tests skip gracefully when Icarus Verilog is not installed, so the suite stays green on machines without an HDL toolchain while still gating real hardware on the machines that have one.
Bit-true, from first principles →Benchmarks →
03Synthesis — Yosys onto a real FPGA

Synthesis turns RTL into the actual look-up-tables and flip-flops of an FPGA. SC-NeuroCore targets a fully open-source flow: Yosys maps the SystemVerilog to a gate netlist, nextpnr places and routes it, and a packer writes the bitstream — no vendor licence required. It runs on inexpensive Lattice boards (an iCE40 UP5K iCEBreaker is about €70, an ECP5 board €80–150), with a Xilinx Vivado path for Artix-7/Zynq parts when you need them.

# open flow: Yosys + nextpnr + packer, one command
sc-neurocore deploy model.nir --target ice40 # runs yosys, nextpnr, icepack

# or the Xilinx path for Artix-7
python tools/fpga_deploy.py --synth vivado --part xc7a35t
Deeper: targets and resource evidence
Open targets are Lattice iCE40 (Yosys + nextpnr + icepack) and ECP5 (Yosys + nextpnr-ecp5); Gowin GW2A can be driven through Yosys or the free Gowin IDE; Xilinx Artix-7/Zynq/UltraScale go through Vivado ML Standard (free for the smaller parts). Because a fixed-point neuron is small, several fit on a sub-€100 board. Reported LUT/flip-flop utilisation and Fmax per module are tracked as synthesis evidence rather than asserted here — see the toolchain guide and the benchmarks.
FPGA targets & toolchain →Resource & timing →
04Formal verification — proof, not just testing

Tests show a circuit works on the inputs you tried; a formal proof shows it cannot fail on any input. SC-NeuroCore attaches SystemVerilog Assertions (e.g. "the accumulator never overflows") to each generated module and discharges them with SymbiYosys using bounded model checking. Over a hundred formal properties across the module tree are proved — the generated hardware modules carry proofs, not just tests.

$$\phi_{\text{BMC}}(k) \;=\; I(s_0)\;\wedge\;\bigwedge_{i=0}^{k-1} T(s_i,s_{i+1})\;\wedge\;\neg P(s_k)$$

If $\phi_{\text{BMC}}(k)$ is unsatisfiable, no run of length $k$ from reset can violate the property $P$ — the module is safe up to depth $k$.

Deeper: from bounded checks to unbounded proof (k-induction)
Bounded model checking unrolls the state-transition relation $T$ for $k$ cycles from the reset state $I(s_0)$ and asks a SAT solver whether the property $P$ can be broken; UNSAT means it cannot, within $k$ steps. To lift this to all time, SymbiYosys uses k-induction: a base case (BMC shows no violation reachable in $k$ cycles) plus an inductive step (assume $P$ holds for $k$ consecutive states, prove it holds for the next). When both pass, the property is proved for unbounded execution. Typical neuron properties are absence of arithmetic overflow, membrane-bound invariants, and reset correctness.
The pipeline →
05NIR — the universal on-ramp

You should not have to marry one framework to reach hardware. NIR (Neuromorphic Intermediate Representation) is a shared exchange format — a directed graph of 18 primitives that every major spiking-network framework can export. SC-NeuroCore reads NIR, so a model trained in anyone's tool can enter the pipeline above and come out as proven RTL.

Deeper: how a NIR graph becomes an ODE becomes a circuit
The compiler maps the five NIR neuron primitives to canonical ODE strings, quantises the parameters to fixed-point, discretises the dynamics with an explicit Euler step $v[n{+}1] = v[n] + \Delta t\, f(v[n], I[n])$, and honours the NIR affine interconnect ($y = W x + b$) exactly, so the graph semantics are preserved end to end. Both the eager Python runtime and the generated RTL follow the same discretisation, which is precisely what the co-simulation stage checks.
Encoding & primitives →NIR notebooks →
In one sentence

A neuron equation is quantised to fixed-point, emitted as SystemVerilog, checked bit-true against the Python model with Icarus Verilog, synthesised to a real FPGA with the open Yosys flow, and formally proved correct with SymbiYosys — so what you trained is what you ship, and it is provably what it claims to be.

Hardware synthesis in depth ← Back to the field Run it in a notebook