延續第三課，失敗映像仍不能取得取指許可。這次驗證器改送四個位元。接收端必須決定，十六種組合中哪一種代表放行。編碼器與接收端的判讀方式，都會影響結果。
先看接收端怎麼判讀
學校實驗室用四格通行卡，1001 表示不得進入，0110 才是准入。門口若逐格確認整張 0110，只會認一種值；若只問『看起來不同於 1001 嗎』，缺一格的 1000 也能過。這對應 strict 與 loose 解碼。同樣的卡需要不同判讀規則，十四種非法值也沒有憑空變成十四種合法資格；此處借卡講邏輯，沒有量測實體卡片防偽。
影片時序勘誤（英文 03:54–04:00）：影片說 accepting edge changes；這裡應讀成「edge 1 的接受結果改變，請求時程維持不變」。模型仍在 edge 1 提出同一次請求：strict 拒絕，loose 接受。換解碼政策沒有移動取樣緣。原影片與字幕保留，這段是明示勘誤，沒有宣稱已重製影片。
多位元控制把一個判斷表示成碼字。本課使用 FAIL＝1001、PASS＝0110。兩者有四個位置不同。Hamming distance 就是不同位元的數量。它描述碼字距離，沒有量測實體攻擊難度。
接收端可以完整比對 PASS。嚴格解碼只讓 0110 放行。另一種接法是「只要不是 FAIL 就放行」。寬鬆解碼會接受十五種值，包含十四種非法碼。同樣四條線，判讀方式卻讓保護範圍不同。
用 mask＝0001 翻轉 FAIL 的最低位，接收端會看到 1000。嚴格解碼拒絕，寬鬆解碼則放行。非法碼偵測器可以發出 alert，但脆弱版本刻意沒有把偵測結果接入放行路徑。看到 alert，仍可能已經越權。
OpenTitan 原始碼分開定義嚴格與寬鬆 MuBi 判讀，四位元常數為 6 與 9。本課借用公開值說明選擇，沒有測試 OpenTitan，也沒有宣稱寬鬆判讀在所有情境都錯。拒絕條件可能需要不同語意。MuBi 原始碼
同一個非法值，兩個接收答案
把拒絕卡的最低格改掉，1001 XOR 0001 得到 1000。卡片稽核員會報 bad=1；門口若只用 loose，卻照樣開門。『有人發現卡壞了』與『進門前已阻擋』要分開看。mask=1 是指定那一格的二進位遮罩，不是第一號學生或一次事件；報錯訊號沒有接到閘，就沒有提供這次阻擋。
PASS=0110、FAIL=1001。XOR mask 的 1 表示要翻轉的位元，0 表示保留。實驗輸入十進位 mask=1，對應二進位 0001；它不是「翻第一個事件」的編號。
1001 XOR 0001 = 1000。1000 既不是 PASS，也不是 FAIL，所以 bad=1。Strict 比對「等於 0110」得到 0；loose 比對「不等於 1001」得到 1。若 loose 接收端沒有把 bad 接進 grant，即使畫面報錯，它仍會接受失敗映像。
| seen | bad | strict：seen==PASS | loose：seen!=FAIL |
|---|---|---|---|
| 1001 | 0 | 0 | 0 |
| 1000 | 1 | 0 | 1 |
| 0110 | 0 | 1 | 1 |
先在 code target、未授權映像、mask=1 下切換 strict／loose，核對同一列的 seen、bad、commit。再以授權映像、mask=0 做正向控制。Strict 應允許合法工作，而不只是讓所有請求都失敗。
先寫預算，再談碼字距離
假設一份申請只准在保存後改一次卡，且至多改三格。從 1001 到 0110 四格都不同，這個預算內到不了准入卡；改四格的1111遮罩則做得到。保存後到門口之間對應 edge 0 後與 edge 1。『一次動手』若能改整張卡，就已超出三格前提；卡片的四格也沒有描述晶片上一次擾動會影響幾位。
儲存實驗從已保存的 FAIL 開始。一次事件在 edge 0 後，以 XOR 改動一個四位元暫存器。錯誤保留到 edge 1 的請求。程式枚舉全部十六種 mask，零值另作控制。該拍的 valid 與 ready 都成立。
「至多翻三位」的主張排除了 mask＝1111。預算內的非零 mask，會把 FAIL 改成嚴格解碼拒絕的非法值。1111 則直接得到合法 PASS。若一次實體事件能反相整個碼字，就不能沿用三位元預算。
儲存實驗先信任映像與獨立 reference。完成旗標、編碼與解碼也不受擾，時脈、重置及接受握手同樣可信。Reference 保存映像原本失敗的結果，不複製受擾碼字。否則錯誤 PASS 也會改掉測試判準。
合法碼字也能保存錯誤判斷
如果製卡前的核準判斷已被換成真，製卡員就會印出完整0110；嚴格門口仍會放行。原申請紀錄卻沒有核準，對應 source 故障與獨立reference不一致。另一次只改最後開門許可，是 grant target，卡本身不變。兩種反例各有一份實驗，不能算進『只改保存卡』的主表；四條線也沒有帶來四份來源證據。
接著把目標移到上游。在保存前翻轉一位元授權輸入。編碼器收到 true，便保存合法 PASS。嚴格比對會通過，因為碼字格式完全正確。錯誤發生在編碼之前。
這是單一來源目標的獨立實驗，沒有同時翻儲存位元。另一個擴大範圍實驗，只在 edge 1 反相最終 grant。兩者仍信任接受介面。它們指出碼字距離無法自行保護的兩個邊界。
設計者可以讓編碼判斷沿更多路徑傳遞，檢查來源，或在接收端使用另外產生的證據。每種做法都需要可信條件。把同一個受擾 bool 展開成四位，不會產生四個獨立判斷。
重跑兩種解碼政策
在實驗臺固定未授權申請與1000卡，只換門口規則。Strict拒絕，loose接受；匯出的seen與bad相同，commit不同，便能追到解碼政策。再用授權0110、不改卡，檢查正常能進入。這個對照沒有把故障機率加入模型；卡住所有學生的門也不能當成完整產品。
打開實驗，維持授權為 false。選 code 目標、strict 政策與 mask＝1。先看 raw、seen、bad 與 commit。只把政策改為 loose，接受結果就會改變。來源與故障都相同。匯出兩份軌跡，指出差異來自哪個閘。
Node 枚舉十六種 mask，嚴格解碼有一種越權，寬鬆解碼有十五種。數字包含四位元反例，只表示枚舉結果，不能當攻擊機率。無故障的授權 PASS 能被接受；無故障 FAIL 會被拒絕。
改選 source，再選 grant；非零 mask 在這兩組只作注入開關，不代表來源位元數。每組目標都是一個 bool。這些軌跡不能混入儲存 mask 表。最後設 authorized＝true、mask＝0，確認嚴格閘在正常情況能打開。
待驗證 RTL／SVA
把門口規則寫成程式，仍要留下另一份申請稽核簿。程式查『完整准入卡且已完成』，稽核簿查『這次申請真的核準』；兩者都在交付緣看。這分別對應 grant 與 reference assertion。寫下規則還不等於已經編譯或測過門禁；此節的SVA需要harness與正向控制。
讀懂本課的性質：編碼判斷與授權判準
稽核員若整天看到沒人進門，『凡進門者都有資格』這句會一直成立，卻沒測到准入路徑。拿授權0110、不改卡去門口，才能檢查合法交付至少可達；這對應cover與正向控制。稽核員的原申請簿不能從受改卡片抄回來，cover也只是一條可達路，沒有證明每位合法學生都能準時進門。
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 [3:0] Pass = 4'h6, Fail = 4'h9;
assign invalid = (code_q != Pass) && (code_q != Fail);
assign local_bad = invalid; // strict model: no independent detector added
assign grant = complete_q && (code_q == Pass) && !local_bad;
assign accepted_commit = req_valid && req_ready && grant;
// reference_pass is a trusted harness signal, not code_q.
assert property (@(posedge clk) disable iff (!rst_n)
accepted_commit |-> reference_complete && reference_pass);
cover property (@(posedge clk) disable iff (!rst_n)
reference_complete && reference_pass && accepted_commit);這段 RTL／SVA 尚未編譯。四態 X 傳播、相等比較的綜合結果、編碼 AND／OR 語意，以及解碼後故障，都需要另外處理。綜合後也要重新追來源到接收端。第五課會檢查冗餘來源是否真的獨立失效。
故障實驗台
操作時把raw當成原保存卡，seen當成門口看到的卡，bad當成格式檢查，commit當成這次真的放行。先逐一比較code、source、grant三種目標，再重設回未改的授權卡。這些欄位是教學模型的可檢查紀錄；reference是測試稽核簿，沒有在實驗室門口實作另一套驗證硬體。
已執行有限、兩態教學模型。RTL 模擬、合成、形式證明與晶片驗證均尚未執行。Reference 欄位是可信測試平台的觀察，不是晶片多出來的防禦。
檢查你的推理
做測驗前，請替門口預測三張卡：1001不放、1000在loose下放、0110正常放。再問0110是否可能來自錯的製卡判斷，或最終開門許可是否另被改。這對應解碼、來源與grant三個層次；只答出卡片外形，還沒有回答本次學生的資格。
1. Mask＝1 為何繞過寬鬆解碼？
它產生 1000，已不同於 FAIL。
2. FAIL 變成 PASS 要翻幾位？
四位，mask 為 1111。
3. 嚴格解碼能保護來源 bool 嗎？
不能，錯誤來源能產生合法 PASS。
4. 哪個正向控制能抓出永久關閉的閘？
授權 PASS 配 mask＝0，必須能 commit。
5. 允許反相最終 grant，改了哪個假設？
原本可信的解碼到接收端邊界，新增了故障目標。
MY ACADEMY · LESSON FILM
教學影片
影片依序說明本課的資料路徑。看完一段，可以回到下面的互動練習，改變輸入或故障條件。動畫呈現教學模型；它沒有替代 RTL 模擬。
旁白使用合成聲音。互動教學與動畫均有模型邊界；請以本課的來源與驗證範圍解讀結果。
本課故障互動實驗
此實驗執行有限、兩態教學模型。RTL／SVA 為待驗證範例，未執行 RTL 模擬、合成、形式證明、時序收斂或晶片驗證。枚舉數量不是實體攻擊機率。
Wrap-up｜把這一課帶回設計審查
把這次門口交付放回整張申請流程圖：哪格被改、當時採哪種判讀、原申請是否核準，都要留下。下面收尾仍用同一張四格卡整理模型與反例，沒有新增一次注入或新的硬體防護。
- 威脅模型與成立條件
一次改三格拒絕卡，仍到不了0110；改整張卡則需另放寬位元預算。這是儲存target的條件，不含來源與最後門口。
一次四位元儲存 XOR 在 edge 0 後作用，edge 1 接受。拒絕主張限定至多三位；四位、來源及 grant 另報。Reference 與非目標電路可信。
- 失效原因
1000卡在loose門口被接收，bad卻為1。錯誤來自接收規則，不能把報錯當成已經擋下進門。
寬鬆解碼接受非法值。嚴格解碼仍會接受上游產生的合法錯碼，或四位元替換後的 PASS。
- 防護方法
完整查0110能拒絕1000，但還須另查是誰核準這張卡。strict保護格式的一段，沒有順便保護制卡來源。
在權限接收端完整比對 PASS，另做來源綁定。當下局部錯誤也要參與接受閘。
- 驗證方式與待做檢查
把十六種卡依序送同一門口，另跑正常准入卡；這對應mask枚舉與正向控制，沒有實際執行RTL。
Node 已跑十六種 mask、來源／grant 反例及無故障正負控制。RTL／SVA 與實體實作尚未驗證。
- 防護界線與未驗證項目
一張紙卡看得到四格，仍不知道晶片一次擾動能改幾位。兩態枚舉不能提供glitch或實體範圍證據。
主表為兩態碼字替換，排除拍內 glitch、實體獨立性與解碼器實作故障。
換個情境再想一次
若一次能改整張卡，1001變0110就能過strict。寫清四位效果，再重算原先三位結論；不要只沿用一次事件限制。
允許一次事件反相整條 bus。說明為何只限制事件數，無法支持三位元主張。
以上整理對照本課的教學案例、參考資料與實驗範圍；未列為已完成的驗證，都是後續工作。