18 / 37 · Verifica

Verifica del progetto: larghezza, priorità e ritorno

Valutare confini e controlli simultanei dalla specifica delle transizioni.

Contratto di un contatore modulo 10

Per count unsigned^{Unsigned Interpretazione dei bit come intero non negativo. Il campo a n bit è 0–2^n−1 e può differire dalla lettura signed degli stessi bit. Approfondisci} a quattro bit, la priorità è reset, enable, hold. reset=1 porta a 0; altrimenti enable=1 riporta a 0 da count≥9 e incrementa gli altri stati.

N=\lceil\log_2 10\rceil=4

Quattro bit significano 16 stati memorizzabili, non l'implementazione automatica dei dieci desiderati. In particolare, count=9 con enable=0 non deve tornare a 0.

Ogni colonna registra un fronte di salita^{Fronte di salita Passaggio del clock da 0 a 1, distinto dall’intero intervallo di livello CLK=1. Approfondisci}. Gli ingressi sono quelli immediatamente precedenti; gli stati con „after“ quelli subito dopo l’aggiornamento. Le colonne indicano l’ordine dei campioni, non il ritardo fisico di propagazione^{Ritardo di propagazione Tempo dalla variazione d’ingresso all’assestamento corretto dell’uscita. Equivalenza logica e proprietà temporali sono distinte. Approfondisci}. Inizialmente count=9. Senza reset, la prima colonna con enable=0 mantiene 9; solo la successiva con enable=1 torna a 0.

Anche al valore limite deve essere rispettato hold

Mostra i dati della forma d’onda

Dati della forma d’onda: ogni carattere è un intervallo; il punto mantiene lo stato precedente; p è un ciclo di clock.
Segnale	Forma d’onda	Valori del bus
edge	`2345`	E0 → E1 → E2 → E3
reset	`0.10`
enable	`01..`
count after	`23.4`	9 → 0 → 1

Altri problemi di progetto

Calcolate il prossimo valore con count=9, reset=0, enable=0.
Spiegate il recupero da count=15 con enable=1.
Con count=9, reset=1, enable=1 deve uscire un impulso terminale? Definite la risposta assumendo l'uscita a 0 durante reset^{Reset Controllo che riporta allo stato iniziale specificato. Occorre definirne sincronicità e priorità rispetto agli altri controlli. Approfondisci}.

Prova tu

Quante transizioni singole coprono count 0–15 e tutte le combinazioni reset/enable? Provano automaticamente tutti i requisiti di sequenze lunghe?

Leggi la spiegazione

$16\times2\times2=64$ . Se count rappresenta tutto lo stato e stato successivo e uscite sono specificati correttamente, la verifica a un passo è forte evidenza. Non dimostra requisiti omessi come inizializzazione, ipotesi d’ingresso, stato separato dell’impulso o timing reale.

Con count=9 si campionano insieme reset=1 ed enable=1. Quali count successivo e impulso terminale rispettano la priorità del reset?

Scegli una rispostacount=0, impulso=1: normale ritorno.count=10, impulso=0: prevale enable.count=0, impulso=0: reset inizializza stato e impulso.