FSM 狀態編碼：碼距只保護指定的保存狀態

先寫完整狀態表

有限狀態機稱為 FSM，用暫存器保存目前階段。稀疏編碼在大位元空間中，只指定少數合法值。其他值能協助辨認錯誤，前提是實作真的識別它們，並拒絕不安全輸出。

本課六位元表為 WAIT＝000000、CHECK＝001111、RELEASE＝110011、ERROR＝111100。六組不同狀態配對都相差四位。只查 CHECK 到 RELEASE，可能漏掉其他較近配對；最小距離要遍歷整張表。

這張表中，一、二或三位儲存翻轉無法變成另一個命名狀態，只會得到非法值。四位則可能變成另一個合法態。因此，碼距支持的是有預算的替換主張，且仍須信任合法性檢查與輸出閘。

碼距擋住哪些翻轉？

先算 CHECK XOR RELEASE：001111 XOR 110011 = 111100，四個 1 代表距離 4。其他五對 WAIT/CHECK、WAIT/RELEASE、WAIT/ERROR、CHECK/ERROR、RELEASE/ERROR 的 XOR 也各有四個 1。所以一至三位翻轉不能把任何一個命名狀態變成另一個命名狀態；它仍可能變成非法值，需要當拍拒絕。

實驗 mask=60 是十進位，等於十六進位 3c、二進位 111100。CHECK XOR mask = 001111 XOR 111100 = 110011，得到 RELEASE。Mask 和 ERROR 的碼字碰巧相同，但 mask 是運算元，不是轉移後狀態。四位翻轉已超出一至三位的預算；不能拿這個反例否定那個受限結論，也不能拿受限結論保證四位故障安全。

在 RELEASE，完整解碼與 illegal 檢查都通過。是否應放行，還要問這次交易是否被授權。綁定授權可擋住這條未授權替換；此教學替換不證明正常 FSM 走得過所有路徑。

當拍拒絕不安全輸出

Default 分支把下一態送進 ERROR，影響的是目前接受緣之後。若輸出解碼器已讓非法目前態放行，下一拍復原就太晚。RELEASE 要完整比對，當下非法態也要擋住同一接受緣。

小模型只在 state＝RELEASE 時放行。非法態另以 bad 回報。Sticky 能保存歷史供後續復原，不能代替當拍阻擋。此解碼的完整相等已拒絕非法態，不要把另一個閘說成額外獨立覆蓋。

RTL 常數不保證綜合後編碼相同。須檢查產出的 netlist 是否重編碼、暫存器寬度及輸出邏輯。OpenTitan 提供稀疏 FSM 儲存用的 flop wrapper，但 wrapper 與 assertion 本身不能證明整個控制器安全。稀疏 FSM 原始碼

分清狀態替換與正常轉移

主實驗從已保存 CHECK 開始。在 edge 1 接受前，一次事件 XOR 六個保存位元，遍歷六十四種 mask。Reference 映像未授權。狀態解碼、來源、時脈與重置，以及最終接受端保持可信。

Mask＝111100，也就是十六進位 3c，把 001111 改成 110011。解碼器看到合法 RELEASE，bad 維持 false，請求便 commit。它影響四位，超出三位主張，但落在擴大後的四位預算內。

Bind 政策另要求獨立授權。因目前映像未獲許可，它能擋住合法態反例。模型從可信 harness 提供這個值。練習指出欠缺條件；真正設計仍須建立來源與完整性。

找出最近的合法放行碼

選 CHECK、mask＝1 並關閉 binding。結果非法，commit 為 false。再試兩位或三位 mask。接著輸入 60，即 0x3c 的十進位。顯示碼變成 RELEASE，請求也被接受。把軌跡與狀態表一起保存。

已執行枚舉遍歷 CHECK 的每個 mask，並查所有配對距離。六十四種 CHECK mask 中，只有一種到未授權 RELEASE。其他四位 mask 可能到合法 WAIT 或 ERROR。因此，沒有 commit 的軌跡不能一律標為已偵測。

解碼正向控制設 RELEASE、授權 true、binding true、mask＝0。第八課另跑正常 WAIT→CHECK→RELEASE 交易。單獨解碼控制不能證明完整控制器可達放行，也沒有證明轉移條件可信。

待驗證 RTL／SVA

讀懂本課的性質：狀態碼與交易授權

SVA 是 SystemVerilog Assertions；assertion 是檢查規則，不是放行電路。以下每個上升緣，reset 未生效時，若 accepted_commit（第九課用 csr_commit）為 1，|-> 要求右側判準在同一緣成立。沒有接受時，這條蘊涵不會報授權失敗；還需要正常工作的正向控制。disable iff (!rst_n) 排除 reset 有效期間；不能據此保證 reset 安全。

Cover 找一條符合條件的路徑，不證明所有交易正確。Reference 是 testbench（測試平台）獨立保存的期望值，harness 是提供輸入、注入預算與判準的測試外框，DUT 是被測設計。本課的兩態模型只計 0、1，不模擬 X 或拍內延遲；「兩態」不指 FSM 只有兩個狀態。語法與接線對照可回查第一課第 5 節。片段尚未編譯，不能把列出性質當成已證明。

localparam logic [5:0] Wait=6'h00, Check=6'h0f, Release=6'h33, Error=6'h3c;
assign illegal = !(state_q inside {Wait,Check,Release,Error});
assign grant = (state_q == Release) && !illegal && auth_bound_i;
assert property (@(posedge clk) disable iff (!rst_n)
  accepted_commit |-> reference_complete && reference_pass);
cover property (@(posedge clk) disable iff (!rst_n)
  state_q == Release && reference_pass && accepted_commit);

RTL／SVA 尚未編譯。ERROR 可達性、輸出解碼故障、scan 存取與綜合重編碼，都要另查。請回第四課，用獨立 grant 目標檢查解碼後輸出受擾；本課儲存枚舉沒有涵蓋它。最小距離四，也沒有涵蓋錯誤 CHECK 條件選到合法下一態。下一課會處理這個問題。

檢查你的推理