控制器正在檢查未授權映像。六位元狀態從 CHECK 變成 RELEASE，授權卻沒有完成。新碼字合法，狀態解碼器認得它，也因此開閘。本課先算哪些替換能造成這個結果。
先寫完整狀態表
器材室用六格流程牌表示等候、檢查、可交付與錯誤，分別是WAIT、CHECK、RELEASE、ERROR。牌上只准四種圖樣，其餘是非法值。任兩張指定牌都差四格，所以改一至三格會落到非法圖樣；改四格可能變另一張完整牌。流程牌的距離只講保存狀態，不會證明器材真的經過檢查或這位學生有資格。
影片時序勘誤（英文 01:17–01:24）：影片把 default 分支說成在接受緣之後才執行，容易把計算與保存混在一起。組合邏輯可以在緣前先算出下一態 ERROR；狀態暫存器則在本緣取樣後才更新。當下輸出仍須另外拒絕不安全交付。觀看該段請以這個區分為準。原影片與字幕保留，這段是明示勘誤，沒有宣稱已重製影片。
有限狀態機稱為 FSM，用暫存器保存目前階段。稀疏編碼在大位元空間中，只指定少數合法值。其他值能協助辨認錯誤，前提是實作真的識別它們，並拒絕不安全輸出。
本課六位元表為 WAIT＝000000、CHECK＝001111、RELEASE＝110011、ERROR＝111100。六組不同狀態配對都相差四位。只查 CHECK 到 RELEASE，可能漏掉其他較近配對；最小距離要遍歷整張表。
這張表中，一、二或三位儲存翻轉無法變成另一個命名狀態，只會得到非法值。四位則可能變成另一個合法態。因此，碼距支持的是有預算的替換主張，且仍須信任合法性檢查與輸出閘。
碼距擋住哪些翻轉？
CHECK牌是001111，四格遮罩111100把它變成110011，也就是RELEASE。遮罩碰巧與ERROR牌111100相同，卻只是『哪些格要改』，不是最終牌名。先做XOR再查狀態表，才不會以為發生了CHECK→ERROR。這對應mask=60；它超出三格預算，也沒有證明正常流程真的走到RELEASE。
| 名稱 | 六位元保存值 | 十六進位 |
|---|---|---|
| WAIT | 000000 | 00 |
| CHECK | 001111 | 0f |
| RELEASE | 110011 | 33 |
| ERROR | 111100 | 3c |
先算 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 走得過所有路徑。
當拍拒絕不安全輸出
門口看到一張不在表上的流程牌，必須在這次交器材前拒絕。值班員說『下一次鐘響換ERROR牌』，只能改變下一態，不能收回這次已交的器材。這對應當拍完整RELEASE解碼與next-state default。完整相等本來就拒絕非法牌，不要把旁邊的bad標簽算成第二套獨立防護；故事也不保證綜合後仍使用這四種圖樣。
Default 分支把下一態送進 ERROR，影響的是目前接受緣之後。若輸出解碼器已讓非法目前態放行，下一拍復原就太晚。RELEASE 要完整比對，當下非法態也要擋住同一接受緣。
小模型只在 state＝RELEASE 時放行。非法態另以 bad 回報。Sticky 能保存歷史供後續復原，不能代替當拍阻擋。此解碼的完整相等已拒絕非法態，不要把另一個閘說成額外獨立覆蓋。
RTL 常數不保證綜合後編碼相同。須檢查產出的 netlist 是否重編碼、暫存器寬度及輸出邏輯。OpenTitan 提供稀疏 FSM 儲存用的 flop wrapper，但 wrapper 與 assertion 本身不能證明整個控制器安全。稀疏 FSM 原始碼
分清狀態替換與正常轉移
這次演練從已保存CHECK牌開始，改一次後在edge1看交付。改四格變成完整RELEASE，牌子稽核不報非法，原資格卻仍拒絕。加binding要另外看獨立許可，對應bind政策；這份許可來自harness。演練只換一張牌，沒有實際走完WAIT→CHECK→RELEASE，也沒有把測試許可變成現成產品電路。
主實驗從已保存 CHECK 開始。在 edge 1 接受前，一次事件 XOR 六個保存位元，遍歷六十四種 mask。Reference 映像未授權。狀態解碼、來源、時脈與重置，以及最終接受端保持可信。
Mask＝111100，也就是十六進位 3c，把 001111 改成 110011。解碼器看到合法 RELEASE，bad 維持 false，請求便 commit。它影響四位，超出三位主張，但落在擴大後的四位預算內。
Bind 政策另要求獨立授權。因目前映像未獲許可，它能擋住合法態反例。模型從可信 harness 提供這個值。練習指出欠缺條件；真正設計仍須建立來源與完整性。
找出最近的合法放行碼
先改CHECK一格，看門口拒絕，再改四格到RELEASE，看未綁資格的門口放行。其他四格改動還可能得到WAIT或ERROR，沒有交器材也不一定報非法。這對應六十四種mask裡的合法落點。授權RELEASE不改牌的控制，只證明解碼可放行；流程是否走得通要看下一課的交易。
選 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
把四張流程牌寫成RTL常數，門口完整比對RELEASE，再檢查另有依據的auth_bound_i。交付簿每有一次接受，稽核就核對完成與真實許可，對應reference_complete與reference_pass。紙上流程牌只是編碼示例；尚未編譯的SVA不能證明制造後的牌子、scan或輸出路徑安全。
讀懂本課的性質：狀態碼與交易授權
稽核員看『牌子合法嗎』和『這次器材能交嗎』，是兩個問題。四格改出RELEASE會過第一關，未綁定而發生交付時，獨立未授權簿讓授權 assertion 失敗。Cover用授權RELEASE檢查一個可交付情況；如果一直掛WAIT牌，拒絕性質可能永遠成立，但沒有服務。此處仍沒有檢驗轉移條件的真假。
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 條件選到合法下一態。下一課會處理這個問題。
故障實驗台
在實驗臺把raw、seen與state讀成原牌、改後圖樣與查表牌名；bad只報非法圖樣，commit表示交付。重設後保持同一拒絕資格，切換binding，看完整RELEASE為何仍應拒絕。這個實驗沒有增加一條真實轉移歷史，也沒有量測器材室門的反應速度。
已執行有限、兩態教學模型。RTL 模擬、合成、形式證明與晶片驗證均尚未執行。Reference 欄位是可信測試平台的觀察，不是晶片多出來的防禦。
檢查你的推理
給同學四張流程牌，請他先算六組距離，再說明哪張改後的牌能交器材。最後問『下一拍換ERROR』是否來得及阻止本拍。這些題對應完整碼表、輸出解碼與接受緣；算出最小距離4仍沒有回答錯誤條件能否選到合法下一態。
1. 四狀態表要查幾組不同配對？
六組。
2. 三位元故障能到另一命名狀態嗎？
這張表內不能。
3. 哪個 mask 把 CHECK 改成 RELEASE？
0x3c，十進位 60。
4. Default：ERROR 保證當拍阻擋嗎？
不保證，輸出閘當拍就必須安全。
5. 綜合後要查什麼？
實際狀態碼、保存寬度及輸出邏輯是否保留。
MY ACADEMY · LESSON FILM
教學影片
影片依序說明本課的資料路徑。看完一段，可以回到下面的互動練習，改變輸入或故障條件。動畫呈現教學模型；它沒有替代 RTL 模擬。
旁白使用合成聲音。互動教學與動畫均有模型邊界；請以本課的來源與驗證範圍解讀結果。
本課故障互動實驗
此實驗執行有限、兩態教學模型。RTL／SVA 為待驗證範例，未執行 RTL 模擬、合成、形式證明、時序收斂或晶片驗證。枚舉數量不是實體攻擊機率。
Wrap-up｜把這一課帶回設計審查
交接時把CHECK牌、四格遮罩與未授權交付紀錄放在一起，別只留『合法RELEASE』截圖。下面同一器材室例子逐項說清保存預算與授權缺口；正常流程與實體檢查仍另外列，沒有從一張流程牌推論整個控制器。
- 威脅模型與成立條件
從CHECK牌一次改六格中的mask，edge1觀察交付。至多三格的主張先信任查牌與門口，沒有涵蓋四格替換。
Edge 1 前一次六位元狀態 XOR，從 CHECK 枚舉六十四種 mask；碼距主張限定低於四位。其他邏輯與 reference 可信。
- 失效原因
四格把CHECK改成完整RELEASE，牌沒有非法，學生仍沒有許可。問題是合法牌與真授權不同。
四位翻轉得到合法 RELEASE。合法性解碼不報錯，授權卻仍為 false。
- 防護方法
門口完整查RELEASE並核對獨立資格；制造後還查編碼是否保留。多一張流程牌本身沒有建立資格來源。
完整狀態與輸出解碼，加上另有可信依據的授權；還須驗證綜合保留表示法。
- 驗證方式與待做檢查
把六組牌距和六十四種CHECK改動都算完，再試授權RELEASE。後者只是解碼控制，正常排隊流程另外測。
Node 已查全部配對距離、六十四種 CHECK mask 及授權 RELEASE 解碼。正常流程另在第八課測。
- 防護界線與未驗證項目
用遮罩換牌沒有經歷檢查階段。不得把這條流跡說成轉移、scan或實物驗證；正常路線交給下一課。
解碼枚舉不能支持轉移、netlist、scan、實體或形式驗證結果。
換個情境再想一次
若把一張合法牌改近CHECK，先重算六組距離，再找新增的一格或兩格替換。只查CHECK到RELEASE會漏掉新的最小距離。
把一個狀態碼改近。重算最小距離，找出新增的低位元替換。
以上整理對照本課的教學案例、參考資料與實驗範圍；未列為已完成的驗證，都是後續工作。