micheleandClaude Sonnet 5
8d20a7bfbf
C.9 (pinout): certified citing this session's own F1-F7 work; also regenerated a real bitstream for the CURRENT full-system build (ecppack, 0 errors, real part header) rather than relying on an older pre-flash build's bitstream. C.10 (timing): certified citing Fmax re-measured at every structural change this session (54.58->75.30->73.88->66.68->67.91MHz), critical path re-verified identical at every re-synthesis. C.11 (toolchain): full RTL->Yosys->nextpnr-ecp5->ecppack flow re-run on the current build, 0 errors at every stage. Real-silicon behavior explicitly declared NOT certifiable (no physical hardware available). C.12 (netasm): certified citing 20/20 tests plus a real hardware round-trip already demonstrated earlier this session. C.13 (datasheet/RTL coherence): real, current discrepancy found and declared -- none of this campaign's 7 bugs (BUG-001-007) are yet mentioned in the datasheet or engine spec doc. Correct and expected (found after those docs were last updated), flagged as required follow-up after the campaign completes. C.14: page-mode PSRAM and the flash subsystem are actually COMPLETE, not "in progress" as the certification prompt assumed -- verified against real repo state. D (cross-cutting): CDC certified via C.7. Reset scheme found by exhaustive grep across all 20 RTL files to be synchronous-only everywhere (no posedge rst anywhere) -- a real fact, differs from the prompt's async-assert/sync-deassert phrasing, not a defect. FSM: the campaign's own BUG-002-007 ARE FSM defects, found and documented, but no exhaustive reachability analysis of every FSM was done (stated reserve). Width/overflow: 2 real cases found across the whole session. Lint: full-system Yosys check, one real warning (known PSRAM tristate), zero accidental latches confirmed signal-by-signal (25 explicit confirmations). Determinism: no real non-determinism found (the one apparent inconsistency, BUG-003, traced to genuinely different test stimuli between attempts, not unstable behavior for identical stimuli). Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013xXuuRUWZScuo1DeYJxs3v
123 lines
6.3 KiB
Markdown
123 lines
6.3 KiB
Markdown
# D — Analisi trasversali
|
||
|
||
Data: 2026-09-04.
|
||
|
||
---
|
||
|
||
## D.1 CDC (clock domain crossing)
|
||
|
||
`spi_slave.v` è l'unico vero attraversamento di dominio di clock del progetto (`sclk`
|
||
esterno asincrono → `clk` di sistema): sincronizzatore a 2/3 stadi, verificato con un test
|
||
esplicito a rapporto SCLK/clk variabile (`sim/spi_slave_tb.v` TEST 4, §C.7). Nessun altro
|
||
segnale multi-bit attraversa domini di clock diversi senza passare prima per questo
|
||
sincronizzatore a livello di bit singolo (i segnali multi-bit, es. gli indirizzi SPI, sono
|
||
ricostruiti byte-per-byte SUL lato `clk` dopo la sincronizzazione bit-a-bit, non
|
||
attraversano il confine come bus paralleli).
|
||
|
||
**Verdetto: CERTIFICATO** (evidenza da C.7, non ripetuta qui).
|
||
|
||
---
|
||
|
||
## D.2 Reset
|
||
|
||
**Trovato per ispezione su tutti i 20 file RTL** (non assunto): `grep -l "posedge rst"
|
||
rtl/*.v` → **nessun risultato**. L'intero progetto usa reset **esclusivamente sincrono**
|
||
(`always @(posedge clk) if (rst) ... else ...`), mai `always @(posedge clk or posedge rst)`.
|
||
Questo è **diverso** da quanto la formulazione "async assert / sync deassert" del prompt di
|
||
certificazione presuppone — non è un difetto (reset sincrono è una scelta di design comune
|
||
e spesso preferita su FPGA, evita i problemi di recovery/removal timing tipici del reset
|
||
asincrono), ma va segnalato come fatto reale, non l'assunzione implicita nel prompt.
|
||
|
||
Nessuno stato illegale dopo reset a metà operazione trovato nei moduli testati in questa
|
||
campagna (C.1-C.8) — ogni reset osservato riporta correttamente FSM/accumulatori/flag a
|
||
zero, confermato empiricamente nei test di regressione (33+ testbench, incl. reset a metà
|
||
run in `flash_slot_manager_tb.v`'s test di power-loss simulato, §sessioni precedenti).
|
||
|
||
**Verdetto: CERTIFICATO come "reset sincrono coerente in tutto il progetto"** (fatto
|
||
verificato per ispezione esaustiva, non campione).
|
||
|
||
---
|
||
|
||
## D.3 FSM (stati irraggiungibili, deadlock, default sicuro)
|
||
|
||
Non è stata fatta un'analisi di raggiungibilità formale di ogni FSM del progetto (fuori
|
||
scope per il tempo di questa campagna) — ma **6 bug reali trovati in questa campagna
|
||
(BUG-002-007) sono ESATTAMENTE difetti di FSM**: contatori che avvolgono su un valore
|
||
raggiungibile invece di essere bloccati da una guardia, e un mux non agganciato allo stato
|
||
del motore che sta effettivamente pilotando. Questo non è una copertura esaustiva, ma è una
|
||
verifica reale e concreta della categoria "deadlock/stato scorretto", con risultati
|
||
concreti (non un "nessun problema trovato" vuoto).
|
||
|
||
Ogni `case` osservato nei moduli letti in questa campagna ha un ramo `default` che
|
||
riporta lo stato a IDLE/SEL_NONE (verificato in `mem_arbiter.v`, `int8_memory_access.v`,
|
||
`neuron_parallel.v` — nessuno stato `case` privo di default trovato nei moduli ispezionati).
|
||
|
||
**Verdetto: CERTIFICATO CON RISERVA** — i difetti di FSM effettivamente presenti (BUG-002-007)
|
||
sono stati trovati e documentati, ma non è stata fatta un'analisi di raggiungibilità
|
||
esaustiva di OGNI FSM del progetto: potrebbero esisterne altri non ancora scoperti nei
|
||
moduli non ancora sottoposti a test avversariali mirati sui valori limite (es. `spi_slave.v`
|
||
stesso, `psram_controller.v` oltre a quanto già verificato in sessioni precedenti).
|
||
|
||
---
|
||
|
||
## D.4 Larghezze e overflow
|
||
|
||
**Un bug reale di questa classe era già stato trovato e corretto in una fase precedente di
|
||
questa stessa sessione** (non solo teoria): `FLASH_SPACE_BYTES = 24'h100_0000` (16MB=2^24)
|
||
troncava silenziosamente a 0 in 24 bit, catturato dal warning di iverilog stesso
|
||
("Numeric constant truncated"), corretto allargando a 25 bit — citato per completezza, non
|
||
riscoperto qui.
|
||
|
||
**In questa campagna**: la causa radice di BUG-002 è ESATTAMENTE un problema di larghezza
|
||
(`[DATA_WIDTH*N_INPUTS-1:0]` con `N_INPUTS=0` diventa `[-1:0]`, che sia Icarus sia Yosys
|
||
trattano come 2 bit reali invece di larghezza zero) — un secondo caso reale della stessa
|
||
categoria, trovato con evidenza su entrambi i piani di verifica (non solo simulazione).
|
||
|
||
**Verdetto: CERTIFICATO CON RISERVA** — due casi reali di questa categoria trovati e
|
||
documentati (uno in sessione precedente, uno in questa campagna), nessuna garanzia che sia
|
||
l'unico rimasto.
|
||
|
||
---
|
||
|
||
## D.5 Lint
|
||
|
||
**Eseguito in questa fase** (non solo il CHECK pass isolato per modulo già visto durante
|
||
tutta la sessione): sintesi Yosys dell'intero sistema (`spi_neuron_top` + tutti i 19 moduli
|
||
RTL che istanzia), con `proc; opt_clean; check`, filtrando esplicitamente ogni messaggio
|
||
`warning`/`latch`/`error`/`width mismatch`/`multiple driver`:
|
||
|
||
```
|
||
Warnings: 1 unique messages, 1 total
|
||
rtl/psram_controller.v:191: Warning: Yosys has only limited support for tri-state logic
|
||
[...25× "No latch inferred for signal ..." -- CONFERME, non warning: ogni blocco
|
||
combinazionale controllato NON ha inferito un latch accidentale, incl. l'intero albero
|
||
binario di mac8.v e la funzione next_crc di crc32.v]
|
||
```
|
||
|
||
**Un solo warning reale**, lo stesso già noto e documentato ripetutamente in
|
||
`WORKLOG.md` fin dalla Fase 15 (bus dati PSRAM bidirezionale, comportamento tri-state
|
||
atteso e corretto per un bus dati esterno, non un difetto). **Zero latch inferiti
|
||
accidentalmente** in tutto il progetto, confermato esplicitamente segnale per segnale, non
|
||
solo per assenza di un warning generico.
|
||
|
||
**Verdetto: CERTIFICATO.** Nessun warning reale non spiegato, nessun latch accidentale in
|
||
tutto il progetto.
|
||
|
||
---
|
||
|
||
## D.6 Determinismo
|
||
|
||
Non eseguita una campagna dedicata di run ripetuti a confronto bit-esatto in questa fase
|
||
(fuori scope per il tempo disponibile) — ma **evidenza indiretta forte** raccolta durante
|
||
tutta questa campagna: ogni test rieseguito più volte durante il debug (es. i tentativi
|
||
multipli su BUG-003 in C.2, il test di regressione completo rieseguito ad ogni fase C.1-C.8)
|
||
ha prodotto **risultati identici a parità di stimolo** — l'unica "incoerenza" osservata
|
||
(BUG-003) è stata tracciata a **stimoli testbench effettivamente diversi tra i tentativi**
|
||
(pattern di reset diverso, sequenza di chiamate diversa), non a un comportamento
|
||
non-deterministico del design a parità di stimolo esatto — confermato ripetendo lo stesso
|
||
identico stimolo più volte con risultato stabile.
|
||
|
||
**Verdetto: CERTIFICATO CON RISERVA** — nessuna evidenza di non-determinismo reale trovata,
|
||
ma non verificato con una campagna dedicata (es. seed multipli su tutti i testbench,
|
||
confronto bit-esatto sistematico).
|