A test shows a circuit behaves on the inputs you happened to try. A formal proof shows it cannot misbehave on any input. For neuromorphic hardware headed toward safety-adjacent use, you need both — and a traceable chain from each requirement to the test and the proof that discharge it. SC-NeuroCore proves properties of its generated RTL with SymbiYosys, and keeps that chain explicit.
The core method unrolls a module's state-transition relation to a depth $k$ and asks a solver whether any reachable state in those $k$ steps violates a property. If the formula is unsatisfiable, no violation exists within the bound — a proof, not a sample.
For properties that must hold forever, SymbiYosys uses k-induction: prove the property in a base case of $k$ steps, then prove that if it holds for $k$ consecutive states it holds for the next — lifting a bounded check to an unbounded guarantee. These are attached to the generated modules as SystemVerilog assertions (for example, "the accumulator never overflows") and discharged automatically.
Every requirement is tied to the test that exercises it and, where one exists, the SymbiYosys proof that discharges it. This is the matrix that makes a safety case reviewable — and it is honest about which requirements are proved versus tested. Filter it below.
| Requirement | What it guarantees | Test | Proof |
|---|
5 of 17 requirements shown carry a SymbiYosys formal proof; the rest are covered by tests (including property-based tests). "Tested" is a real guarantee — it is simply a weaker one than "proved", and the matrix does not blur the two.
An FMEA walks the compiler pipeline — IR to SystemVerilog to FPGA — and classifies each failure mode by whether it is silent (a wrong output that looks valid) or detectable (a checker catches it). The design goal is to turn the first kind into the second: make faults loud.
overflow_vector, a same-cycle trap_event_vector, and a sticky per-lane trap_vector latched until the host clears it — so a saturation raises an immediate, latching trap rather than washing out silently. Counter under/overflows (an off-by-one in a refractory counter) are similarly caught by property-based tests and an in-RTL non-negativity assertion. Fail-closed, not fail-silent.Safety standards do not accept "it passed our tests" — they want structured evidence: requirements, traceability, verification results, failure analysis. SC-NeuroCore extracts that evidence toward the relevant standards for hardware and functional safety (DO-254 for airborne electronics, IEC 61508 for functional safety, with ISO 26262 in the automotive lineage), packaged from the same artefacts shown above.
This produces certification evidence, not a certificate. A proved property is a genuine mathematical guarantee within its bound and assumptions; a traceability matrix and an FMEA are the artefacts an assessor needs — but sign-off requires an independent safety assessment, target-specific timing and hardware validation, and domain-authority acceptance, none of which a compiler can grant itself. What the toolkit offers is that the evidence is generated during design, kept honest about proved-versus-tested, and ready for that external process rather than reconstructed after it.