18 / 37 · 理解測驗

設計確認：寬度、優先權與回捲邊界

依給定狀態轉移規格判斷邊界值與同時控制輸入。

Modulo-10 計數器契約

4 位元 unsigned^{無符號（unsigned）將位元序列解讀為非負整數。n 位元範圍為 0 至 2^n−1；相同位元序列的帶符號解讀可能得到不同數值。詳細內容} count 的優先權為 reset、enable、hold。reset=1 時歸零；enable=1 時，9 以上返回 0，其他狀態加 1。

N=\lceil\log_2 10\rceil=4

4 位元代表能儲存 16 個狀態，不會自動實作只使用 10 個狀態的規格。尤其 count=9、enable=0 時，不應回到 0。

每欄是一次上升緣^{上升緣是時脈由 0 變成 1 的瞬間。它與表示整段 CLK=1 期間的高準位不同。詳細內容}的觀察紀錄。輸入為邊緣前值，名稱含「後」的狀態為更新後值。欄位對齊表示取樣順序，並未繪出實體傳播延遲^{傳播延遲是輸入改變後，輸出穩定至正確值所需的時間。邏輯式是否等價與時間特性是兩個不同問題。詳細內容}。
初始 count=9。第一欄沒有 reset、enable=0，應保持 9；下一欄 enable=1 時才回到 0。

邊界值也必須維持保持行為

查看波形資料

波形資料：每個字元表示一個區間；句點保持先前狀態；p 表示一個時脈週期。
訊號	波形	匯流排值
邊緣	`2345`	E0 → E1 → E2 → E3
reset	`0.10`
enable	`01..`
count 後	`23.4`	9 → 0 → 1

進一步設計問題

求 count=9、reset=0、enable=0 時的下一值。
說明 count=15、enable=1 時的復原策略。
定義 count=9、reset=1、enable=1 時是否應輸出結束脈衝。假設規格已將重設^{重設將狀態回復至規格指定的初始值。必須一併定義它是同步或非同步，以及是否優先於其他控制訊號。詳細內容}期間的輸出定為 0。

自己試試看

要窮舉 count=0～15 與 reset、enable 的所有組合，需要幾個單步轉移案例？這是否自動證明長狀態序列的全部要求？

查看解說

$16\times2\times2=64$ 個。若如本設計，count 表示完整狀態且下一狀態、輸出規格精確，單步檢查是有力證據。但它無法證明被遺漏的要求，例如初始化、輸入假設、結束脈衝的獨立狀態與實際時序。

目前 count=9，同時取樣 reset=1 與 enable=1。依重設優先規格，下一個 count 與結束脈衝為何？

選擇答案count=0、結束脈衝=1：視為正常回捲。count=10、結束脈衝=0：enable 優先。count=0、結束脈衝=0：重設初始化狀態與脈衝。