michele/FPGA-Neural
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
Files
main
FPGA-Neural/hardware/v1/docs/validation/CERTIFICATION.md
T
micheleandClaude Sonnet 5 dc0b331d3e feat(v2): scaffold hardware/v1 frozen baseline + M1 Neural Processor 
Begins the V2 Neural Multiprocessor / Dataflow architecture per
docs/v2-description.md, per explicit user request to freeze V1 and
start V2 development, copying from V1 what's needed.

Scaffold:
- hardware/v1/: byte-exact, read-only copy of the current V1 codebase
  (rtl, testbenches, tools, constraints, a representative subset of
  synthesis results, and reference docs) -- verified identical via
  diff/cmp against the live top-level tree before being made
  filesystem-read-only. The live top-level tree is untouched and
  remains the project's "production" V1 (see hardware/v1/README.md
  and hardware/v2/logs/decisions.log DEC-0001 for why copy-not-move).
- hardware/v2/: mandatory structure (rtl/sim/constraints/synthesis/
  reports/scripts/logs/docs) plus the full logging system required by
  the spec (development/architecture/simulation/synthesis/timing/
  benchmark/decisions/experiments/errors.log).

M1 -- Neural Processor (hardware/v2/rtl/neural_processor.v):
- 8-stage pipelined perceptron unit (P_IN=8): input align, 8
  multipliers, 3-level adder tree, accumulator, bias+activation, INT8
  saturation. Genuine 1-tile/cycle throughput, not just a wider
  combinational datapath.
- 7-state FSM (NP_IDLE..NP_ERROR per docs/v2-description.md §6, with
  4 baseline states merged into NP_WAIT_OPERANDS -- see
  decisions.log DEC-0002); valid/ready/data/last stream interfaces
  per §7.
- Bit-exact vs the frozen hardware/v1/rtl/neuron_parallel.v + mac8.v
  + mac_unit.v: 7/7 tests pass (hardware/v2/sim/tb_neural_processor.v),
  covering regular/mixed-sign/extreme-INT8 vectors, both activations,
  a zero-idle-gap back-to-back-tiles throughput check, and an 8-tile
  job -- verified with Verilator (see below for why).
- Real synthesis + place&route (Yosys + nextpnr-ecp5): 0 CHECK
  problems, Fmax 183.12 MHz at ACC_WIDTH=32 (PASS at 80MHz, ~3x V1's
  isolated PARALLEL=8 Fmax of 61.71 MHz) and 176.21 MHz at ACC_WIDTH=24
  (a user-requested comparison experiment, also bit-exact-verified;
  see experiments.log EXP-0001/EXP-0002 and benchmark.log).

Three real bugs found and resolved during M1 development (full
diagnostic record in errors.log):
- Two independent, reproducible Icarus Verilog v13.0 scheduling
  defects (ERR-0001, ERR-0002) that silently produced wrong simulation
  results for standard sequential Verilog -- confirmed via Verilator
  5.050 giving correct results on the same minimal repros. Verilator
  is now the trusted simulator for hardware/v2/ (decisions.log
  DEC-0004); Icarus's affected protocol-violation check was removed
  from the RTL and deferred architecturally to the Neural Director
  (DEC-0003) rather than chased further.
- One real RTL bug (ERR-0003): last0 wasn't gated like valid0,
  letting a "last tile" tag leak into the pipeline ahead of its
  actual valid tile on back-to-back jobs. Fixed and verified.

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

144 lines
9.7 KiB
Markdown
Raw Permalink 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