michele/FPGA-Neural
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
Files
8890b0abc234505639cf686321f27ecae8921b8a
FPGA-Neural/docs/validation/CERTIFICATION.md
T
micheleandClaude Sonnet 5 07a48e401f fix: close 7 zero-value/mid-run guard gaps found in re-certification campaign 
Fixes all 7 bugs found in the FPGA-Neural re-certification campaign
(docs/validation/bugs.md, CERTIFICATION.md), per campaign policy that
fixes land as a commit separate from the analysis work (commits
313a199..77e74db):

- BUG-005 (CRITICAL): layer_sequencer.v -- RUN_NETWORK(num_layers=0)
  ran through 256 fabricated layers reading arbitrary PSRAM data as
  descriptors. Now an immediate no-op.
- BUG-007 (CRITICAL): spi_engine.v -- SET_NET_TYPE received mid-run
  remapped the arbiter mux and hung the in-progress engine. Now
  rejected while graph_busy/seq_busy, verified not to partially apply.
- BUG-002 (MEDIA): neuron_parallel.v -- N_INPUTS=0 bypassed the
  elaboration-time guard, leaving x_bus/w_bus undriven. Guard extended
  to reject N_INPUTS==0.
- BUG-003 (MEDIA): neuron_parallel.v -- n_inputs_real=0 at runtime had
  inconsistent behavior across repeated runs. Now an explicit early-out
  via the existing "finishing" completion path.
- BUG-004 (BASSA): neuron_memory.v -- n_neurons_real=0 silently ignored
  the limit. Fixed at all three entry points into the vulnerable
  termination checks (STATE_READ_X, STATE_READ_W, and the X->W
  dispatch).
- BUG-006 (BASSA): graph_engine.v -- num_neurons_graph=0 relied on an
  incidental guard rather than a real one. Now an explicit no-op.
- BUG-001 (INFO): removed sim/top.v, confirmed dead code from the
  pre-INT8 Q8.8 era.

Every bug-reproduction testbench is rewritten from observe-only to
hard-assert the fixed behavior (sim/*_bug00[2-7]*_tb.v), verified
individually and via a full regression (44 testbenches, 43 PASS, 0
FAIL/ERROR, 1 benchmark by design). Re-verified on the real toolchain
(Yosys synth_ecp5 + nextpnr-ecp5): 0 constraint errors, Fmax 68.65 MHz
(was 67.91 MHz, within known placement noise), critical path
structurally unchanged (neuron_parallel/mac8 accumulator carry chain).

Updates docs/validation/bugs.md and CERTIFICATION.md to reflect the
resolved state, and docs/FPGA-NeuralNetwork-Engine.md + the LaTeX
datasheet (IT/EN) with inline notes on each fixed edge case, closing
the datasheet/RTL gap flagged in C.13 of the original certification.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013xXuuRUWZScuo1DeYJxs3v
2026-09-04 20:29:05 +02:00

144 lines
9.7 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
# CERTIFICATO FPGA-Neural — Campagna di ri-certificazione 2026-09-04 (aggiornato post-fix)
Metodo per ogni aspetto: analisi statica del codice reale (non di descrizioni), test con
oracolo indipendente (Python, calcolo a mano, o citazione datasheet), verifica su entrambi
i piani (simulazione Icarus + sintesi reale Yosys/nextpnr-ecp5 dove applicabile). Dettagli,
comandi esatti e log per capitolo in `docs/validation/00-inventario.md` e
`docs/validation/01-datapath.md` … `D-trasversali.md`. Dettagli dei fix e delle relative
verifiche in `docs/validation/bugs.md`.
Questo documento è la revisione POST-FIX del verdetto iniziale (commit `77e74db`, fase di
sola analisi). Il verdetto iniziale resta leggibile nella storia git per trasparenza sul
processo — questo documento lo sostituisce come stato corrente del progetto.
---
## Verdetto complessivo
**Il datapath aritmetico di base è solido e certificato esaustivamente dove possibile**
(`mac_unit.v`: 65536/65536 combinazioni INT8 esaustive, 0 mismatch). **Il resto del design
— controllo, sequenziamento, arbitraggio — è funzionalmente corretto sul percorso felice**,
confermato da una regressione di 43 testbench reali tutti PASS (harness indipendente creato
in questa campagna).
**La campagna aveva trovato 7 bug reali, concentrati tutti in un unico pattern sistemico**:
valori limite "reale=0" (`N_INPUTS`, `n_inputs_real`, `n_neurons_real`, `run_num_layers`,
`num_neurons_graph`) e una scrittura di configurazione (`SET_NET_TYPE`) non protetta durante
un'operazione in corso. Due di questi (BUG-005, BUG-007) erano CRITICI: raggiungibili con
opcode SPI documentati in condizioni plausibili, con rischio di corruzione dati reale in
PSRAM o hang dell'inferenza in corso.
**Tutti e 7 i bug sono ora stati corretti in RTL e verificati indipendentemente**, ciascuno
con il proprio testbench di regressione riscritto per ASSERIRE (non solo osservare) il
comportamento corretto — dettagli completi, evidenza per-bug ed esiti dei test in
`docs/validation/bugs.md`. Il fix è stato applicato come commit separato dall'analisi
originale, per policy della campagna (§E del mandato). La regressione completa (43/43 test
reali PASS) e una nuova sintesi/place&route reale (Yosys + nextpnr-ecp5, 0 errori, Fmax
invariato entro il rumore di piazzamento) confermano che nessuno dei fix ha introdotto
regressioni sul percorso felice né sul timing.
**Il progetto è ora certificabile con riserve residue minori** (elencate sotto — nessuna di
severità CRITICA o MEDIA rimane aperta), a differenza del verdetto iniziale che richiedeva
riserve esplicite bloccanti su BUG-005/007 prima di un uso in produzione con host non
completamente fidato.
---
## Tabella per aspetto (aggiornata post-fix)
| Aspetto | Verdetto | Capitolo |
|---|---|---|
| Fase 0 — Inventario | CERTIFICATO (fotografia reale, non presunta) | `00-inventario.md` |
| C.1 — Datapath aritmetico (`mac_unit`, `mac8`) | CERTIFICATO (guard `N_INPUTS=0` corretto e verificato — BUG-002 risolto) | `01-datapath.md`, `bugs.md` |
| C.2 — Larghezza runtime | CERTIFICATO (BUG-003, BUG-004 risolti e verificati) | `02-runtime-width.md`, `bugs.md` |
| C.3 — Sottosistema memoria | CERTIFICATO | `03-memoria.md` |
| C.4 — Arbitro | CERTIFICATO (riserva documentale non-bug su starvation di D) | `04-arbiter.md` |
| C.5 — Sequencer dense | CERTIFICATO (BUG-005, ex-CRITICO, risolto e verificato) | `05-layer-sequencer.md`, `bugs.md` |
| C.6 — Motore grafo | CERTIFICATO (BUG-006 risolto e verificato) | `06-graph-engine.md`, `bugs.md` |
| C.7 — SPI slave + engine | CERTIFICATO | `07-spi.md` |
| C.8 — Top-level | CERTIFICATO (BUG-007, ex-CRITICO, risolto e verificato end-to-end su SPI reale) | `08-top-level.md`, `bugs.md` |
| C.9 — Pinout / `.lpf` | CERTIFICATO | `09-pinout.md` |
| C.10 — Timing | CERTIFICATO (Fmax post-fix 68.65 MHz, invariato entro rumore di piazzamento rispetto a 67.91 MHz pre-fix) | `10-timing.md`, `bugs.md` |
| C.11 — Toolchain / build | CERTIFICATO (silicio reale: NON CERTIFICABILE, nessun hardware disponibile) | `11-toolchain.md` |
| C.12 — `netasm` | CERTIFICATO | `12-netasm.md` |
| C.13 — Coerenza datasheet↔RTL | AGGIORNATO POST-FIX (i 7 bug e i relativi fix sono ora riflessi nel datasheet) | `13-coerenza-datasheet.md` |
| C.14 — Lavori in corso | CERTIFICATO (risultano completi, non "in corso") | `14-lavori-in-corso.md` |
| D.1 — CDC | CERTIFICATO | `D-trasversali.md` §D.1 |
| D.2 — Reset | CERTIFICATO (fatto: sincrono ovunque, non async) | `D-trasversali.md` §D.2 |
| D.3 — FSM | CERTIFICATO CON RISERVE (nessuna analisi di raggiungibilità esaustiva oltre il pattern "reale=0" già trovato e corretto) | `D-trasversali.md` §D.3 |
| D.4 — Larghezze/overflow | CERTIFICATO CON RISERVE | `D-trasversali.md` §D.4 |
| D.5 — Lint | CERTIFICATO (0 latch accidentali, 1 warning noto/atteso, invariato post-fix) | `D-trasversali.md` §D.5 |
| D.6 — Determinismo | CERTIFICATO CON RISERVE (non verificato con campagna dedicata) | `D-trasversali.md` §D.6 |
---
## Registro bug — riepilogo (dettagli completi in `bugs.md`)
| ID | Severità | Sintomo | Raggiungibilità | Stato |
|---|---|---|---|---|
| BUG-001 | INFO | `sim/top.v` non compilava (dead code, residuo pre-INT8) | N/A (non nella regressione) | **RISOLTO** — file rimosso |
| BUG-002 | MEDIA | `N_INPUTS=0` bypassava il guard compile-time, `start` ignorato | Richiede una nuova sintesi | **RISOLTO** — guard esteso, verificato (fallimento di compilazione atteso) |
| BUG-003 | MEDIA | `n_inputs_real=0` a runtime, comportamento incoerente tra ripetizioni (hang o limite ignorato) | Runtime, via SPI (`SET_BASE` sel 7) | **RISOLTO** — early-out esplicito, verificato (1 ciclo, y=0) |
| BUG-004 | BASSA | `n_neurons_real=0`, limite ignorato silenziosamente, conteggio cicli incoerente tra build | Runtime, via SPI (`SET_BASE` sel 8) | **RISOLTO** — guard su 3 punti d'ingresso, verificato (32 vs 155 cicli) |
| BUG-005 | **CRITICA** | `RUN_NETWORK(0)` eseguiva 256 layer fasulli, scriveva PSRAM a indirizzi arbitrari | Un solo opcode SPI documentato | **RISOLTO** — no-op immediato, verificato (1 ciclo, layer_idx=0) |
| BUG-006 | BASSA | Stessa causa di BUG-005 in `graph_engine`, mitigata incidentalmente da un guard esistente | Un solo opcode SPI, rischio pratico basso osservato | **RISOLTO** — no-op immediato, verificato (13 cicli, no err) |
| BUG-007 | **CRITICA** | `SET_NET_TYPE` durante un run bloccava il motore in corso | Due opcode SPI documentati in sequenza ravvicinata | **RISOLTO** — scrittura rifiutata mentre busy, verificato end-to-end su SPI reale |
Tutti i fix e le rispettive verifiche sono in un commit separato dall'analisi originale
(policy §E). Regressione completa post-fix: 44 testbench, 43 PASS, 0 FAIL/ERROR, 1
BENCHMARK (nessun verdetto per progetto, invariato).
---
## Riserve aperte residue (onestà sui limiti, §A.5)
Nessuna riserva CRITICA o MEDIA rimane aperta. Riserve residue, tutte già dichiarate nel
verdetto iniziale e non toccate dalla campagna di fix (fuori scope, o limiti strutturali
della metodologia):
1. **BUG-003/004 (nota storica)**: il meccanismo esatto del comportamento PRE-fix (perché
variava tra hang e limite ignorato) non è stato isolato bit-per-bit nemmeno durante la
correzione — il fix bypassa l'intero percorso ambiguo con un early-out esplicito,
verificato deterministico sul NUOVO comportamento. Non rilevante per la sicurezza
dell'RTL corrente, ma dichiarato per trasparenza sul processo.
2. **C.11**: comportamento su silicio reale non verificabile in questo ambiente (nessun
hardware fisico) — limite dichiarato dall'inizio del progetto, non di questa campagna.
3. **D.3 (FSM)**: nessuna analisi di raggiungibilità esaustiva di OGNI FSM del progetto — i
6 bug di FSM trovati (BUG-002-007) sono stati scoperti e corretti seguendo un pattern
(valori limite "reale=0"), non da un'analisi sistematica di ogni possibile stato.
**Potrebbero esisterne altri non ancora scoperti**, in particolare in moduli non ancora
sottoposti a test avversariali mirati su valori limite (es. `psram_controller.v`,
`spi_slave.v`).
4. **D.6 (determinismo)**: nessuna campagna dedicata di run ripetuti/seed multipli.
5. **Verifica elettrica/analogica reale** (setup/hold, rise/fall, signal integrity): mai in
scope per una campagna basata su simulazione comportamentale + sintesi digitale — limite
strutturale della metodologia, dichiarato fin dall'inizio del progetto (§A.5).
---
## Verifica dei fix (dual-plane, §A.4)
- **Simulazione**: ciascuno dei 6 bug RTL (BUG-002 – BUG-007) ha un testbench di
regressione dedicato, riscritto dopo il fix per ASSERIRE il comportamento corretto
(non solo osservarlo, come durante la fase di scoperta) — vedi `docs/validation/bugs.md`
per il dettaglio di ogni asserzione e il relativo esito.
- **Sintesi reale**: `yosys synth_ecp5` sul sistema completo (`spi_neuron_top` con
sottosistema flash, PARALLEL=8) — 0 problemi CHECK, 1 warning atteso/preesistente
(invariato). `nextpnr-ecp5` reale — 0 errori di vincolo, 0 pin non vincolati, Fmax 68.65
MHz (invariato entro il rumore di piazzamento rispetto ai 67.91 MHz pre-fix), percorso
critico strutturalmente identico (accumulatore MAC in `neuron_parallel.v`/`mac8.v`, non
toccato dai fix). Log: `synth/ecp5/post_fix_verify/`.
- **Regressione**: `python3 tools/run_regression.py` — 44 testbench, 43 PASS, 0
FAIL/ERROR, 1 BENCHMARK (per progetto, invariato).
---
## Stato lavori residui
1. ~~BUG-005 e BUG-007 (CRITICI)~~ — **RISOLTI**.
2. ~~BUG-002/003/004 (MEDIA/BASSA)~~ — **RISOLTI**.
3. ~~BUG-006~~ — **RISOLTO**.
4. ~~BUG-001~~ — **RISOLTO** (file rimosso).
5. ~~Aggiornamento datasheet/documentazione (C.13)~~ — completato in questo stesso ciclo di
lavoro (markdown + LaTeX IT/EN).
Reference in New Issue View Git Blame Copy Permalink