Hardware Synthesis — SC-NeuroCore

19Verilog Modules

72Formal Properties

7SymbiYosys Modules

3673LUTs (7-series)

9Chip Emulators

5FPGA Targets

Verilog RTL Modules

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)

FPGA Targets

Xilinx 7-series Intel FPGAs Lattice iCE40 Lattice ECP5 Gowin

Open-source: Yosys + nextpnr. Commercial: Vivado, Quartus.

sc-neurocore deploy model.nir --target ice40

RTL Code — sc_lif_neuron.v

Q8.8 fixed-point LIF neuron with configurable leak, gain, threshold, refractory period, and noise input. Bit-true match with Python simulation.

// SC-NeuroCore — Fixed-point Leaky Integrate-and-Fire neuron
// Signed two's complement, Q(FRACTION) fixed-point

module sc_lif_neuron #(
  parameter integer DATA_WIDTH = 16,
  parameter integer FRACTION = 8,
  parameter signed [DATA_WIDTH-1:0] V_REST = 0,
  parameter signed [DATA_WIDTH-1:0] V_THRESHOLD = (1 << FRACTION),
  parameter integer REFRACTORY_PERIOD = 0
)(
  input wire clk, rst_n,
  input wire signed [DATA_WIDTH-1:0] leak_k, gain_k, I_t, noise_in,
  output reg spike_out,
  output reg signed [DATA_WIDTH-1:0] v_out
);

// Fixed-point multiply: (V_REST - v) * leak_k
wire signed [2*DATA_WIDTH-1:0] leak_mul = (V_REST - v_reg) * leak_k;
wire signed [DATA_WIDTH-1:0] dv_leak = leak_mul >>> FRACTION;

// Input current scaling
wire signed [2*DATA_WIDTH-1:0] in_mul = I_t * gain_k;
wire signed [DATA_WIDTH-1:0] dv_in = in_mul >>> FRACTION;

// Membrane update with noise
wire signed [DATA_WIDTH-1:0] v_next = v_reg + dv_leak + dv_in + noise_in;

always @(posedge clk) begin
  if (v_next >= V_THRESHOLD) begin
    spike_out <= 1'b1;
    v_reg <= V_RESET;
  end else begin
    spike_out <= 1'b0;
    v_reg <= v_next;
  end
end
endmodule

Simplified excerpt. Full module includes refractory period, saturation, reset logic, and debug output. 72 properties formally verified by SymbiYosys.

Formal Verification

SymbiYosys + SMT

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.

Event-Driven Architecture

15–39x fewer register toggles vs clock-driven

Activity rate: 0.01–10%. AER encoder packs spike events. Event neuron gates computation on activity. Router delivers spikes to target populations.