Python ↔ Verilog Co-Simulation Guide¶

This guide documents the SC-NeuroCore co-simulation framework for validating that Verilog RTL generated by the equation compiler agrees with the Python reference under the metric appropriate to the model class. Deterministic non-chaotic models usually compare spike counts; discrete or sensitive maps use bounded state trajectories and event vectors.

Overview¶

The co-simulation framework:

Compiles a model schema to Verilog via the equation compiler
Generates a testbench that drives constant current for N clock cycles
Compiles and runs the simulation via Icarus Verilog (iverilog + vvp)
Captures the declared observable (spikes or a bounded state trace)
Compares against the Python UniversalNeuron.step() reference

flowchart LR
    A["Schema<br/>(TOML)"] --> B["UniversalNeuron<br/>.from_schema()"]
    B --> C["Python<br/>simulation"]
    B --> D["to_verilog()"]
    D --> E["generate_testbench()"]
    E --> F["iverilog<br/>+ vvp"]
    C --> G{"Compare class<br/>observable"}
    F --> G
    G -->|match| H["✓ Verified"]
    G -->|mismatch| I["✗ Investigate"]

    style H fill:#e8f5e9
    style I fill:#ffcdd2

Prerequisites¶

Python 3.10+ with the sc_neurocore package installed
Icarus Verilog (iverilog, vvp) — install via apt install iverilog
Tests skip gracefully if iverilog is not available

Running Co-Simulation Tests¶

Bash

# Run all co-simulation tests
python -m pytest tests/test_cosimulation.py -v -s

# Run just the accuracy tests
python -m pytest tests/test_cosimulation.py -k "accuracy" -v -s

# Run Q4.12 precision tests
python -m pytest tests/test_cosimulation.py -k "Q412" -v -s

# Run Q16.16 precision tests
python -m pytest tests/test_cosimulation.py -k "Q1616" -v -s

Test Structure¶

The co-simulation suite is organized into four test classes:

TestCoSimulation — Q8.8 Baseline¶

Test	Description	Assertion
`test_both_produce_spikes`	Both Python and Verilog spike (6 models)	`spikes > 0`
`test_spike_count_accuracy`	Spike counts match within 1% (6 models)	`gap < 1%`
`test_no_current_no_spikes`	Zero current → zero spikes (5 models)	`spikes == 0`
`test_python_sim_is_deterministic`	Python gives same result twice	`a == b`
`test_verilog_sim_is_deterministic`	Verilog gives same result twice	`a == b`

TestQ412Precision — Q4.12 (16-bit, 12 fractional)¶

Test	Description
`test_lif_q412_spikes`	Q4.12 LIF produces spikes
`test_lif_q412_near_python`	Q4.12 within 5% of Python
`test_q412_vs_q88_comparison`	Both Q4.12 and Q8.8 within 5%
`test_q412_zero_current_lif_is_range_classified`	LIF zero-current is excluded from Q4.12 parity by range diagnostics

Q4.12 is a narrow-range, high-resolution mode. It can track driven LIF spike counts in the existing test window, but it is not an mV-range LIF mode: v_rest=-65.0, initial v=-65.0, and tau_m=10.0 exceed the [-8, +7.9998] Q4.12 range. Use python -m sc_neurocore.neurons precision lif before treating any Q4.12 LIF run as a parity claim.

TestQ1616Precision — Q16.16 (32-bit, 16 fractional)¶

Test	Description
`test_lif_q1616_spikes`	Q16.16 LIF produces spikes
`test_lif_q1616_near_python`	Q16.16 within 1% of Python
`test_q1616_zero_current_silence`	Zero current → silence ✓

Verified Models¶

Six deterministic Q8.8 baseline models are verified. Five have exact spike-count parity; Izhikevich has a declared one-spike Q8.8 quantisation boundary and exact Q16.16 parity at the same operating point:

Model	State Variables	Complexity	Spikes (I=50, 200 steps)
LIF	v	Linear	200
SC Lapicque LIF compatibility	v	Linear hard-reset recurrence	200
Quadratic IF	v	Quadratic	50
Izhikevich	v, u	Quadratic (2-var)	25 float64 / 24 Q8.8; 25 Q16.16
Resonate-and-Fire	v, w	Linear (2-var)	200
Perfect Integrator	v	Linear ramp	200

FitzHugh-Rinzel Q16.16 enrolment¶

The three-state fitzhugh_rinzel schema is validated separately from the Q8.8 baseline set because its slow variable and cubic RK4 datapath need Q16.16 range and resolution. The schema mirrors the hand model's coupled v, w, and y equations, rising-edge v >= 1 decision, and no-reset flow. Over 3000 steps, hand model, schema runner, and emitted RTL agree exactly on spike counts throughout the enrolled current band: seven crossings at I=0.4, eight at I=0.5, and eight at I=0.6. The marginal crossing at I=0.7 is outside the declared parity band because fixed-point rounding changes its count.

Hindmarsh-Rose Q16.16 enrolment¶

The three-state hindmarsh_rose schema now mirrors the maintained 1984 model: simultaneous classical RK4 over the cubic fast membrane, recovery, and slow adaptation equations; rising-edge x >= x_threshold observation; and no reset. The previous explicit-Euler schema carried an identity reset, which made the runtime treat detection="crossing" as a level decision and count every above-threshold timestep. The paired TOML/JSON schemas remove that semantic caricature.

Over 2,000 steps, the hand model, both schema formats, and emitted Q16.16 RTL agree exactly at five enrolled operating points: 0/0/26/40/52 crossings at I=0/2/3/4/5. This is a bounded behavioural contract, not indefinite chaotic trajectory identity. Over 5,000 steps at I=2/3/4/5, float64 reports 9/48/85/114 crossings while Q16.16 reports 10/49/86/115; dedicated tests preserve that one-crossing boundary explicitly.

The S5/H1 promotion emits a Q8.8 formal-catalogue core and port-only harness. Its depth-4 SymbiYosys/Z3 job proves reset-spike safety only; the Q16.16 operating points remain the behavioural parity evidence.

Pernarowski Q16.16 enrolment¶

The three-state pernarowski schema mirrors the maintained autonomous beta-cell burster: simultaneous classical RK4 over a cubic fast coordinate and two separated slow variables, rising-edge v >= 0.5 detection, and no reset. Its slow-wave rhythm is intrinsic, so input current shifts the trajectory rather than gating a silent/single/train response. Over 5000 steps, the hand model, schema runner, and emitted Q16.16 RTL agree exactly at all four enrolled operating points: 17 crossings at each of I=-0.1, 0.0, 0.1, and 0.2. The corresponding S5/H1 promotion also emits a Q8.8 formal-catalogue core and port-only harness. Its depth-4 SymbiYosys/Z3 job proves the bounded reset-spike safety property; the Q16.16 harness remains the behavioural parity evidence.

Terman-Wang Q16.16 enrolment¶

The two-state terman_wang schema mirrors the maintained LEGION relaxation oscillator: simultaneous classical RK4 over the cubic fast nullcline and tanh-gated recovery, rising-edge v >= 1.5 detection, and no reset. Because the recovery equation is transcendental, raw state bit identity is not portable across math libraries or fixed-point look-up tables. The enrolled observable is therefore the robust crossing count. Over 8,000 steps the hand model, schema runner, and Q16.16 RTL agree exactly on the full silent/single/train set: zero crossings at I=-1.0, one at I=0.0, and three at I=0.5.

The S5/H2 promotion also emits a Q8.8 formal-catalogue core and port-only harness. Its depth-4 SymbiYosys/Z3 job proves bounded reset/output safety only; the three Q16.16 operating points remain the behavioural parity evidence.

Rulkov map Q16.16 trajectory enrolment¶

The rulkov_map schema mirrors the maintained Rulkov 2002 hand model as a simultaneous discrete recurrence: rational subthreshold branch, spike plateau, hard reset, slow y drift, and rising x >= 0 crossing detection. It is not an ODE and receives no timestep scaling or integrator smoothing.

The class-correct evidence is a bounded trajectory rather than a long-window spike count. At I=1.5 over 30 iterations, the rational, plateau, and reset branches execute ten times each. The hand model and paired TOML/JSON schemas agree exactly on every state and event. The Q16.16 RTL reproduces the complete ten-event vector, with both committed state coordinates within 0.001 absolute error of float64. This validates fixed-point lowering without claiming that a sensitive map must retain float64 trajectory identity indefinitely.

The S5/H2 descriptor additionally points to the raw Yosys 0.33 synth_xilinx report for the generated Q16.16 core. Its formal-catalogue entry uses generated Q8.8 RTL, a port-only harness, and a depth-4 SymbiYosys/Z3 reset-spike safety job; behavioural evidence remains the Q16.16 short-window trajectory.

Cazelles map Q16.16 trajectory enrolment¶

The cazelles_map schema mirrors equation (1) and the Figure-1 parameters of Cazelles, Courbage, and Rabinovich (2001): one scalar state, four piecewise-linear branches, and the optional alpha*x^m term. I is a maintained additive perturbation; zero input recovers the source map. Because the paper leaves exact breakpoints open, the implementation discloses a right-continuous convention. A crossing into x < x1 marks the slow-regime minimum used as a burst-cycle observation.

The hand model and paired TOML/JSON schemas agree exactly for the complete 600-step source orbit and visit every branch. Q16.16 RTL is event-exact through the first 55 iterations, with maximum scalar-state error at most 0.0062. That bounded window reaches the approach to the first discontinuous return.

The 600-step fixed-point orbit is an explicit exclusion: binary64 emits seven slow-regime entries while Q16.16 emits two. Chaotic amplification of quantisation is expected, and the test pins the measured divergence so the bounded co-simulation result cannot be read as long-window identity.

The S5/H2 descriptor also carries a Q8.8 Yosys coarse-synthesis report. Its depth-4 SymbiYosys/Z3 port-only harness proves reset-spike safety; neither artefact claims timing, PPA, board, device, or physical-silicon evidence. The former clipped-logistic fast/slow recurrence remains independently enrolled as the count-neutral SCClippedLogisticBurstingMapNeuron identity.

Chialvo map Q16.16 event-class enrolment¶

The chialvo_map schema reproduces Chialvo (1995), DOI 10.1016/0960-0779(93)E0056-H: simultaneous x*x*exp(y-x) + k + I and a*y - b*x + c commits with method="map". The paper permits k to be constant or a time-dependent additive perturbation, so I carries the time-dependent part. The upward x_threshold=1.0 crossing is a maintained observation convention and is not attributed to the paper.

At I=-0.05/0/0.01/0.1/1.0 over 100 iterations, the hand model and paired TOML/JSON schemas agree exactly on every state and event. Q16.16 RTL preserves the event counts 0/2/3/0/1. At the stable I=-0.05/0.1/1.0 points, maximum absolute errors stay below 0.055 for x and 0.093 for y.

The exponential LUT phase-shifts four event positions at I=0 and six at I=0.01, although the total counts remain exact. Event timing and complete oscillatory trajectory identity are therefore explicit exclusions rather than hidden inside a loose tolerance.

The S5/H2 closure adds a tracked Q8.8 formal-catalogue core and a 117-cell coarse-synthesis receipt. Its depth-4 SymbiYosys/Z3 job proves exact reset state and the maintained upward-crossing relation on public ports; the Q16.16 operating set remains the behavioural evidence. Timing, PPA, device, physical silicon, and universal float64 equivalence remain outside the claim.

Aihara map Q8.24 bounded chaotic shadowing¶

The aihara_map schemas encode Aihara's reduced one-state Eqs. 10–11 and the Eq. 12 level waveform shaper. They do not retain the former unrelated two-state fast/recovery recurrence or reinterpret the level output as an upward crossing. The Figure 4 chaotic defaults are k=0.7, alpha=1, bias=0.3968, and epsilon=0.01, with y0=0.1.

Hand, TOML, and JSON trajectories agree exactly. The committed Q8.24 core preserves all 12 autonomous event decisions in the enrolled short horizon and keeps the internal-state error below 0.01. The short horizon is a scientific boundary: sigmoid LUT quantisation and binary64 exp differences amplify on a chaotic orbit, so long-window pointwise identity is not claimed.

The depth-6 SymbiYosys/Z3 job proves reset hygiene and the public Eq. 12 relation between the state sign and event output. A regression test also pins the explicit signed casts required at the generated sigmoid-LUT boundary.

Medvedev first-return Q16.16 enrolment¶

The medvedev_map schema is the scalar slow-calcium first-return reduction in Medvedev (2005), DOI 10.1016/j.physd.2005.01.021; it is not the superseded tent-map recurrence. Its three regions follow equations 4.4/4.7, 4.8 with 4.13, and 4.15. The paper does not tabulate one unique global pair of return functions, so the decay, affine-return, average, exponent, and scale constants are disclosed as SC-NeuroCore's reproducible calibration. I=0 is the sourced map; non-zero I is a maintained perturbation of active returns. An event is the maintained pre-step observation u <= u_HC, not a paper-defined spike.

The hand model and paired TOML/JSON schemas agree exactly on every state and event. At I=2 over 100 iterations they traverse the exact four-state cycle and emit the same 75-event vector. Q16.16 RTL preserves that complete vector with maximum state error below 0.007813. Q8.8 is not a valid target because the calibrated d=2271.1927977404063 log scale exceeds its signed range.

The emitted log datapath uses the shared 256-entry positive-domain LUT over [1/256, 8 + 1/256) at step 1/32. The S5/H1 promotion therefore emits a Q16.16 catalogue core and port-only harness; its depth-4 SymbiYosys/Z3 job proves bounded reset/event safety, while the 100-iteration co-simulation is the behavioural evidence.

Ibarz-Tanaka four-branch Q16.16 enrolment¶

The ibarz_tanaka_map schema implements the Shilnikov-Rulkov (2004) map in the profile restated by Ibarz et al. (2007), Eqs. 2–3: constant, parabolic, plateau, and fixed -1 reset branches for v, plus the simultaneous u - mu*(v + 1 - sigma) slow update. I is the paper's I_v. The reset event is the branch-ordered pre-state decision v > 0 and v >= 1 + I + u; the first term prevents a low upper guard from overriding the earlier v <= 0 branch. There is no separate threshold or reset parameter; I carries the source beta/analysis I_v input.

Hand Python and paired TOML/JSON schema traces are identical in both enrolled protocols. I=-0.5 over four iterations visits one parabolic and three constant branches; I=0.2 over 30 iterations visits 23 parabolic, four plateau, and three reset branches. Together they cover all four branches. Generated Q16.16 RTL preserves both complete event vectors with maximum errors below 0.003 for v and 0.0001 for u.

Q8.8 is invalid because mu=0.001 quantises to zero. The S5/H2 catalogue job therefore uses Q16.16; its depth-4 SymbiYosys/Z3 proof establishes exact event equivalence to the ordered fourth-branch guard and event => v_next=-1. The tracked Yosys coarse-synthesis report contains 33 cells and no residual processes; timing and higher silicon claims remain open.

Courbage-Nekorkin map fixed-point trajectory enrolment¶

The courage_nekorkin_map schema reproduces Courbage, Nekorkin, and Vdovin (2007), equations 3–5: both coordinates commit simultaneously, the fast map uses its three published piecewise-linear branches, and the x >= d Heaviside term applies on the upper side of the discontinuity. I is the maintained API extension; I=0 is the published autonomous recurrence. The software event is an upward x >= x_threshold crossing and does not reset either coordinate.

At I=-0.3/0/0.3, the hand model and paired TOML/JSON schemas agree exactly on every state and event. Q16.16 RTL is event-exact over bounded 30/20/30-iteration windows. The points exercise all three fast-map branches and both sides of the Heaviside discontinuity; maximum coordinate errors remain below 0.014 for x and 0.00031 for y.

Q32.32 extends each input to 30 iterations and preserves the complete event vectors of one, four, and one events. Across that set, the maximum errors are 2.604e-5 for x and 8.379e-7 for y.

The autonomous 30-iteration Q16.16 trace is an explicit exclusion: float64 emits four events, RTL emits six, and six positions differ. Q32.32 resolves that same window at four events on both paths. The exclusion prevents bounded fixed-point evidence from being read as long-window identity for a sensitive discontinuous map.

The S5/H1 promotion adds a Q8.8 formal-catalogue core and port-only harness. Its depth-4 SymbiYosys/Z3 job proves reset-spike safety only; Q16.16/Q32.32 trajectories remain the behavioural evidence.

Ermentrout-Kopell theta-Euler Q16.16 enrolment¶

The ermentrout_kopell_map_neuron schema mirrors the maintained hand class, not the older catalogue theta schema. The sourced object is the continuous Ermentrout-Kopell (1986) theta equation. The hand implementation adds dt=0.1, input gain, forward Euler, an upward theta=pi event, and modulo 2*pi; the schema states those as maintained choices and commits the complete recurrence with method="map".

The event predicate uses theta_prev and the unwrapped candidate. This matters at negative current: the first candidate can fall below zero and commit near 2*pi, but that backward wrap is not an upward event. Positive-literal modulo is lowered with the same floored-remainder correction in Verilog and the generated integer C/Rust kernels.

The hand model and paired TOML/JSON schemas agree exactly on every float64 state and event under the varied-drive test. Over 2,000 steps, Q16.16 RTL preserves the class-correct spike counts at all enrolled points: zero at I=-0.5, 45 at I=0.5, and 64 at I=1.0. Maximum circular phase errors are respectively below 0.081, 0.089, and 0.025 rad. The cosine LUT shifts some event positions, so full fixed-point event vectors and trajectories are not claimed exact.

The integer C and Rust generators match Verilog state and event words cycle-for-cycle over 240 steps at both current signs. The S5/H1 promotion also emits a Q8.8 catalogue core and port-only harness; its depth-4 SymbiYosys/Z3 job proves the bounded reset/spike safety property only.

GLIF Q16.16 enrolment¶

The glif schema mirrors the maintained Allen Institute GLIF5 model: simultaneous classical RK4 over membrane voltage, adaptive threshold, and two after-spike currents, followed by candidate-level v >= theta detection and a candidate-first adaptive reset. A varied 4,000-step drive produces 181 resets; the hand model and both schema formats agree exactly on every event and all four post-step states.

Over 1,000 constant-current steps, hand model and schema runner report 0/0/23/54/86/95 spikes at I=0/15/22/30/45/50; emitted Q16.16 RTL reports the same six counts exactly. The compiler evaluates state-dependent resets from the integrated candidate and exposes post-reset output state, matching the schema runner's integrate-detect-reset order. This removes the former one-spike drift that had masked a pre-step-reset semantic mismatch. The enrolled hardware contract spans the whole operating set rather than one selected exact current.

The S5/H1 promotion retains the existing formal-catalogue enrolment with regenerated Q8.8 RTL, a port-only harness, and a depth-6 SymbiYosys/Z3 safety job. The Q16.16 six-point set remains the behavioural parity evidence.

Source Mihalas-Niebur Q32.32 enrolment¶

The mihalas_niebur schema implements equations 2.1--2.2 from Mihalaş and Niebur (2009): simultaneous classical RK4 over membrane voltage, adaptive threshold, and two spike-induced currents, followed by sampled v >= theta detection and the published event map. The event sets v to V_r, floors the threshold at Theta_r, and applies I_j <- R_j I_j + A_j; it does not scale the candidate membrane voltage.

The committed Q32.32 RTL exercises the paper's Table 1 common constants and panel-M parameters for 2,000 intervals at I=0.002. Python, the TOML schema, and the complete RTL event vector all report 14 events. All four post-step state trajectories remain within 1.3e-6 of the binary64 source trajectory. The H2 descriptor additionally binds a Xilinx 7-series Yosys synthesis report and a depth-2 SymbiYosys/Z3 public-port safety job; no timing, board, or silicon claim is made.

Retained SC scaled-reset Q16.16 enrolment¶

The separate count-neutral sc_scaled_reset_adaptive_if identity preserves the former project recurrence without attributing its candidate-proportional reset to the Mihalas-Niebur paper. Its Python class, paired schemas, and Q16.16 RTL produce the same complete 31-event vector over 250 steps at I=3; all four RTL state trajectories remain within 0.001 of binary64. Its H2 descriptor binds a generic coarse Yosys synthesis report and a depth-2 SymbiYosys/Z3 public-port safety job. The retained recurrence does not alter the literature-model count.

Wilson-HR Q16.16 enrolment¶

The two-state wilson_hr schema mirrors the maintained polynomial cortical model: source capacitance C=0.8, simultaneous classical RK4 over membrane v and recovery r, continuous state, and sampled upward v=0 crossings without a reset. Over 5,000 constant-current steps the hand model, schema runner, and Q16.16 RTL agree exactly at the robust operating points: 0, 44, 46, 49, and 52 crossings at I=0, 0.08, 0.1, 0.14, and 0.2. The nearby I=0.07 and I=0.075 points are explicit quantisation boundaries where binary64/schema counts of 42/43 become 43/44 in Q16.16.

The S5/H1 promotion also emits a Q8.8 formal-catalogue core and port-only harness. Its depth-4 SymbiYosys/Z3 job proves bounded reset-spike safety only; the Q16.16 operating points remain the behavioural parity evidence.

Retained SC resetting Wilson-HR enrolment¶

The separately named sc_resetting_wilson_hr schema preserves the former project recurrence: unit capacitance, r=0.1, level v>=0.4 detection, and a hard v=-0.7 reset that preserves the simultaneous RK4 recovery candidate. It does not attribute those specialisations to Wilson's source model. Hand, TOML/JSON schema, and generated Q16.16 RTL agree on 0, 1, and 4 events at I=0, I=2, and I=10 over 5,000 steps. The committed Q8.8 core passes Yosys synthesis and a depth-4 public-port safety job; this retained SC identity does not increment the literature-model count.

Adding a New Model to Co-Simulation¶

Ensure paired TOML/JSON schemas exist in src/sc_neurocore/neurons/model_schemas/.
Create dedicated files named tests/test_cosim_<model>.py and tests/test_reference_<model>.py; do not add new enrolments to the legacy aggregate buckets.
Run those model-specific tests — if they fail:
Check whether a transcendental LUT changes the class-correct observable
Check if parameters overflow the chosen precision mode
Use python -m sc_neurocore.neurons precision <model> for diagnostics

Bash

python -m pytest -q \
    tests/test_cosim_your_new_model.py \
    tests/test_reference_your_new_model.py

Schema-Gap Reporting¶

Use the schema-gap report before selecting the next schema co-simulation target:

Bash

python tools/schema_gap_report.py --format markdown --output docs/internal/schema_gap_report_latest.md

The tool scans live source modules and schema files without importing optional backends. It reports the net schema gap, source modules still lacking a same-name or alias schema, schema-only names, source-evidence classifications, and a ranked enrolment table. The current checkout has 154 model source modules, 32 unique schema models, a net schema gap of 122, and 124 source-module rows still needing same-name or alias schema coverage because izhikevich and lif are schema-only names.

Testbench Architecture¶

The generated testbench follows this structure:

Verilog

module tb_sc_lif;
    reg clk;
    reg rst_n;
    wire spike_out;
    wire signed [15:0] v_out;

    sc_lif uut (
        .clk(clk), .rst_n(rst_n),
        .I_t(16'sd12800),    // Q8.8 encoded input current
        .spike_out(spike_out),
        .v_out(v_out)
    );

    // 100 MHz clock
    initial clk = 0;
    always #5 clk = ~clk;

    integer spike_count;

    initial begin
        $dumpfile("tb_sc_lif.vcd");
        $dumpvars(0, tb_sc_lif);
        spike_count = 0;

        // Reset phase
        rst_n = 0;
        #20;
        rst_n = 1;
        @(posedge clk);        // 1 settling cycle

        // Measurement phase
        repeat (200) begin
            @(posedge clk);
            #1;                 // combinational settling
            if (spike_out)
                spike_count = spike_count + 1;
        end

        $display("Simulation complete: %0d spikes in 200 cycles",
                 spike_count);
        $finish;
    end
endmodule

Key timing details:

Phase	Purpose	Duration
Reset (`rst_n = 0`)	Initialise all registers	20ns (2 clock periods)
Settling (`@(posedge clk)`)	Allow reset to propagate	1 clock cycle
`#1` after posedge	Let combinational outputs settle	1ps (minimal)

Historical note: The settling cycle and #1 delay were added in 2026-05-01 to eliminate a 0.5% residual gap caused by sampling spike_out before combinational logic had propagated after reset de-assertion.

Compiler Correctness: Six Critical Fixes¶

The following fixes were applied to achieve 0.0% co-simulation accuracy:

#	Fix	Impact
1	Intermediate wire for bit-select	iverilog compilation
2	Persistent wire counters	Multi-variable models
3	Portable negative literals	Cross-tool compatibility
4	Q-format division	99% → 50% gap
5	Look-ahead threshold	50% → 0.5% gap
6	Testbench timing	0.5% → 0.0% gap

Fix #4: Q-Format Division¶

Bug: Division by parameters used bare Verilog integer division (a / b), which divides by the Q-encoded raw value (e.g., 2560 for tau_m=10 in Q8.8).

Fix: Proper Q-format: (a << fraction) / b, with explicit sign extension:

Verilog

wire signed [15:0] _dop0 = numerator;                       // named operand
wire signed [31:0] _dnum0 = $signed({...}) <<< 8;           // shift up
wire signed [31:0] _div0 = _dnum0 / $signed({...});         // divide
wire signed [15:0] _dres0 = _div0[15:0];                    // extract Q result

Fix #5: Look-Ahead Threshold¶

Bug: Threshold compared v_reg (current cycle) instead of v_next (computed new voltage), creating a 1-cycle detection delay.

Fix: Threshold expression uses v_next wires:

Verilog

// Before: if ((v_reg > threshold))     ← 1 cycle late
// After:  if ((v_next > threshold))    ← matches Python semantics

Troubleshooting¶

Model produces spikes in Python but not in Verilog¶

Check dt encoding: python -m sc_neurocore.neurons precision <model>
If dt underflows (Q-value = 0), the Euler update is zero
Solution: increase dt or use wider precision mode
Check parameter range: Look for ⚠ Overflow or ⚠ Underflow warnings
Solution: use Q16.16 for wide-range parameters
Check division: Parameters used as divisors should be > 0.004 (Q8.8 minimum representable value)

Verilog produces more spikes than Python¶

Check for Q-format overflow: Large v² products may wrap in 16-bit
Solution: use Q16.16 for nonlinear models
Example: Izhikevich at zero current — 0.04*v² overflows Q8.8

Compilation fails with iverilog¶

Ensure -g2012 flag is passed (SystemVerilog 2012 features required)
Check for bit-select on complex expressions (should be caught by the compiler)

Python ↔ Verilog Co-Simulation Guide¶

Overview¶

Prerequisites¶

Running Co-Simulation Tests¶

Test Structure¶

TestCoSimulation — Q8.8 Baseline¶

TestQ412Precision — Q4.12 (16-bit, 12 fractional)¶

TestQ1616Precision — Q16.16 (32-bit, 16 fractional)¶

Verified Models¶

FitzHugh-Rinzel Q16.16 enrolment¶

Hindmarsh-Rose Q16.16 enrolment¶

Pernarowski Q16.16 enrolment¶

Terman-Wang Q16.16 enrolment¶

Rulkov map Q16.16 trajectory enrolment¶

Cazelles map Q16.16 trajectory enrolment¶

Chialvo map Q16.16 event-class enrolment¶

Aihara map Q8.24 bounded chaotic shadowing¶

Medvedev first-return Q16.16 enrolment¶

Ibarz-Tanaka four-branch Q16.16 enrolment¶

Courbage-Nekorkin map fixed-point trajectory enrolment¶

Ermentrout-Kopell theta-Euler Q16.16 enrolment¶

GLIF Q16.16 enrolment¶

Source Mihalas-Niebur Q32.32 enrolment¶

Retained SC scaled-reset Q16.16 enrolment¶

Wilson-HR Q16.16 enrolment¶

Retained SC resetting Wilson-HR enrolment¶

Adding a New Model to Co-Simulation¶

Schema-Gap Reporting¶

Testbench Architecture¶

Compiler Correctness: Six Critical Fixes¶

Fix #4: Q-Format Division¶

Fix #5: Look-Ahead Threshold¶

Troubleshooting¶

Model produces spikes in Python but not in Verilog¶

Verilog produces more spikes than Python¶

Compilation fails with iverilog¶

Further Reading¶