控制器必須完成四筆傳輸，才交出結果。正數計數器已到四，倒數計數器也到零，兩者相加仍是四。但真正只完成三筆。共用 enable 讓兩份計數一起提早前進。
關係檢查有自己的範圍
一位學生要交四份作業。桌上兩個計數欄，『已交』從0開始，『還欠』從4開始；每次真正收件便一加一減，總和仍是4。它們對應up與down。若一起錯加、錯減，總和也能正確，卻沒有真的多收到一份。關係檢查只核對兩數相加，不會自己翻出抽屜裡有哪些作業。
交叉計數器以相反方向保存進度。本課三位元暫存器從 up＝0、down＝4 開始。每次計數，up 加一、down 減一。非模數相加必須維持四。比較時須加寬，避免截斷溢位而掩蓋錯誤。
單獨改 up，通常會破壞總和。偵測器可以當拍擋完成，並記住錯誤。但總和仍成立時，檢查器不知道數值怎麼到達這裡。協同錯誤更新能躲過這種關係檢查。
OpenTitan 提供交叉計數器。SYNFI 也討論共用 increment 與 clear 的保護邊界。以下小排程說明這個機制；本課沒有執行 SYNFI，也沒有重現論文的 netlist 實驗。計數器原始碼、SYNFI 第 4.4.1 節
計算完成的工作
學生拿出作業，老師也準備收，才算一次真正交件，對應valid AND ready的handshake。只拿出但老師忙，或老師等著但沒有作業，都不增加獨立收件簿ref。固定在第1、3、4拍真正交件，第2拍空等；故障卻讓桌上兩欄在第2拍後多走一步。這是同一份行程的計數錯誤，沒有憑時間過去就認定作業完成。
真正一步是傳輸已被接受：valid 與 ready 在約定上升緣同時成立。停等一拍沒有完成工作。獨立 reference 只在真正握手時加一，並排除於故障範圍外。
負向排程在 edge 1、3、4 有真正握手，edge 2 閒置。一次錯誤共用 enable 在 edge 2 後仍更新兩份計數。Edge 4 後，DUT 成為 4／0，reference 進度卻只有三。
結果請求在 edge 5 到達。只檢查總和的版本會放行。授權 reference 要求四次真正傳輸，因此判為越權。總和檢查正確地回報沒有錯誤；它漏看未完成工作，並非算術計算壞掉。
一個錯誤 enable 如何增加不存在的工作
到第4拍後，桌上寫『已交4、還欠0』，獨立收件簿卻只有3份。第5拍學生要領取完成證明，sum政策會發，progress政策則看出up與ref不同。第2拍後那次多算是抽象狀態更新，下次鐘響前才看見；沒有讓學生倒回第2拍真的交一份，也沒有模擬enable的電氣取樣。三位元6+6被截成4，則是另一個算術寬度反例。
Handshake 是工作真的交付的取樣事件。本例只有 edge 1、3、4 的 handshake=1；edge 2 是閒置。表中先列緣前的 up、down、ref，再說明緣後更新。Ref 只計真實 handshake。
| edge | 緣前 (up,down,ref) | 緣後發生什麼 |
|---|---|---|
| 1 | (0,4,0) | 真實工作：變 (1,3,1) |
| 2 | (1,3,1) | 沒有工作；錯誤 enable 只把 DUT 改成 (2,2)，ref 仍是 1 |
| 3 | (2,2,1) | 真實工作：變 (3,1,2) |
| 4 | (3,1,2) | 真實工作：變 (4,0,3) |
| 5 | (4,0,3) | 收到結果請求；sum=4，但真實工作僅三次 |
每列 up+down 都是 4，所以 sum checker 沒有說謊；它回答的是兩個數值的關係。它沒有計算工作來源。Progress 政策在 edge 3 已看到 up=2、ref=1，並保存差異；edge 5 不放行。這裡可信 ref 是 testbench 判準，產品必須另設能成立的工作證據，不能把測試判準當成現成硬體防護。
寬度也屬於關係定義。三位元的 6+6 是四位元 1100；若只保留低三位，會變成 100（4），讓錯誤配對看似符合 sum=4。這是說明截斷風險的算術反例，不是上表 enable 實驗的值。因此程式先把運算元擴成四位，再比較完整和。
本教學模型把 enable 故障定義為 edge 2 取樣與正常更新之後，額外套用一次 up+1、down−1 的狀態操作；它沒有模擬 enable 訊號的 setup/hold。這次操作不改 edge 2 已取樣的值，最早在 edge 3 緣前看見。若 RTL 用緣前 enable pulse 實現同一效果，必須另外驗證其取樣與更新順序。
每個目標都要有明確效果
改『已交』欄一格、把兩欄整組換成另一組，和讓共同收件開關多動一次，是三種不同效果。配對替換先在正常更新後算 proposed_up = up XOR mask。只有 proposed_up 在0～4時，才寫成(proposed_up, 4−proposed_up)；算出5就不作用。這對應pair的受限範圍。這讓你區分『交了一個注入參數』與『真的改到狀態』。故事中的獨立收件簿是harness判準，不是桌上自動新增的產品防護。
主要反例只在共用 enable 發生一次事件，沒有暫存器 XOR。窗口固定為 edge 0～5。兩份計數到端點即停。時脈、重置與工作負載可信；握手觀察器、reference、總和檢查與接收端也不受擾。
實驗另提供三位元 up 暫存器 XOR，也能替換配對，使 down＝4−up。配對替換只接受 up 在 0～4 內的提案，超出範圍便不作用。這是受限的相關替換，不能叫兩次獨立 bit flip。提交參數與實際生效要分開記錄。
進度版本另比較 up 與獨立進度輸入，並記住差異。可執行模型借可信 reference 示範所需條件。產品必須另建立可信的工作完成觀察。把 testbench 判準接到 grant，不等於完成硬體防護。
先看閒置拍，再看結果請求
先在空等的第2拍加一次計數，再到第5拍查完成證明。改sum為progress時，真實三次交件不變，所以可以追到檢查條件的差別。另做四次真實交件的正向控制，證明正常能領證明。96組提案有零mask與不生效配對，沒有一次接受也可能只是未完成四份；不能全寫成老師偵測了96次搞鬼。
選 enable、fault edge＝2 與 sum 政策，逐拍看表。Edge 3 的配對已包含錯誤一步，ref 沒有增加。Edge 5 的 commit 為 true，reference 為 false。改 progress 政策，工作負載不變，這條反例會被擋住。
三次交握排程的 96 組 up／pair 測試，在 progress 政策下都不提交。這本身不能證明故障被偵測，因為 reference 根本沒有到四。另有斷言檢查共用 enable 的進度不一致、up XOR 打破總和，以及配對替換繞過總和檢查。無故障四次交握控制會在 edge 5 接受。
試著在 edge 5 後注入。這個窗口沒有後續請求，因此沒有越權只說明觀察已結束。若要判定錯誤進度無害，先把請求移晚。也要記錄注入是否真的改動配對。
96 組參數是兩種 target（up／pair）×六個 faultEdge（0～5）×八個 mask（0～7）。mask=0 是無改動控制；不合法的 pair 提案也不作用。提交 96 組，不表示 96 次有效注入。
待驗證 RTL／SVA
程式裡的完整總和就像把『已交、還欠』兩欄相加時，保留十位而不只看個位。Progress再對獨立收件簿，確認每一步有收件依據，最後在領取證明時檢查reference_handshakes==4。這裡的參照來自可信測試外框；真正產品須自行建立並保護完成事件，不能把課堂的收件簿當成已做好的硬體。
讀懂本課的性質：完成計數與真實工作
稽核規則在發完成證明的同一拍，問『真正收過四份嗎』。把學生提出請求當成『應該加一』會失去判準，因為提出未必被收下。這是accepted_commit與reference_handshakes的區別。Cover要找真的四次交件，不能讓永不發證的設計假裝完成；也沒有證明所有停等或clear優先權。
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 節。片段尚未編譯，不能把列出性質當成已證明。
logic [3:0] sum; // widen three-bit operands
assign sum = {1'b0, up_q} + {1'b0, down_q};
assign count_bad = (sum != 4);
// work_count_i requires its own integrity/trust justification.
assign progress_bad = (up_q != work_count_i);
assign grant = (up_q == 4) && !count_bad && !progress_bad && !sticky_q;
assign accepted_commit = result_valid && result_ready && grant;
// Reset clears sticky; each edge sets it on count_bad or progress_bad.
assert property (@(posedge clk) disable iff (!rst_n)
accepted_commit |-> reference_handshakes == 4);
cover property (@(posedge clk) disable iff (!rst_n)
reference_handshakes == 4 && accepted_commit);RTL 草稿尚未編譯。產品計數器須定義 set／clear、算術寬度、飽和或回繞，並限制未完成工作數。信任重複暫存器之前，先測共用 enable。第七課會檢查狀態編碼能辨認哪些替換。
故障實驗台
逐拍看up、down、ref，分別讀成已交、還欠、真正收件數，再看result請求那拍的commit。先重設再切目標，確認原來三次交件沒有增加。實驗臺讓這個主線可以手算；匯出摘要的 detected 只總計總和 bad；進度偵測要另看 progressBad 與 sticky。它沒有真的收作業，也沒有模擬四態值、時脈或實體enable故障。
已執行有限、兩態教學模型。RTL 模擬、合成、形式證明與晶片驗證均尚未執行。Reference 欄位是可信測試平台的觀察，不是晶片多出來的防禦。
檢查你的推理
測驗時先問，空等一拍為什么兩欄也可能一起前進？再問已交4但收件簿3能不能發證明。前者說明共同enable，後者說明進度授權。若把stall改成真正交件，ref才應加一；這個遷移問題不能用『總和一直正確』代替實際完成。
1. 錯誤共用 enable 為何仍維持 up＋down＝4？
兩方向改動量相反。
2. 可信工作數應在哪個事件增加？
真正的 valid／ready 握手。
3. Edge 5 的反例是什麼？
DUT 報四步，真正只傳三次。
4. 為何跑四次握手控制？
它能確認正常完成仍可達。
5. 相關配對替換是兩次獨立翻位嗎？
不是；須明寫替換效果，並限定合法暫存器值。
MY ACADEMY · LESSON FILM
教學影片
影片依序說明本課的資料路徑。看完一段，可以回到下面的互動練習，改變輸入或故障條件。動畫呈現教學模型；它沒有替代 RTL 模擬。
旁白使用合成聲音。互動教學與動畫均有模型邊界；請以本課的來源與驗證範圍解讀結果。
本課故障互動實驗
此實驗執行有限、兩態教學模型。RTL／SVA 為待驗證範例，未執行 RTL 模擬、合成、形式證明、時序收斂或晶片驗證。枚舉數量不是實體攻擊機率。
Wrap-up｜把這一課帶回設計審查
收尾時保留那張三份作業的收件簿，與錯誤4／0配對一起交給同事。它們能解釋第5拍為何提早發證明，也讓後面各項模型、根因與界線有同一個對象。這裡沒有順便延長窗口或把可信ref移進真實設計。
- 威脅模型與成立條件
第2拍沒有收件卻多動一次開關，第5拍可領證明。預算是一個共同enable事件，沒有再翻暫存器。
Edge 0～5 內，在閒置拍後發生一次共用 enable 事件；暫存器效果分開測。結果請求前只有三次真正握手。
- 失效原因
桌上4／0總和正確，收件簿只有3。兩欄一起前進保留關係，也一起算入不存在的工作。
相反方向計數仍可能一致，卻一起算入未發生的工作。
- 防護方法
發完成證明前查真正收件簿，再查完整總和。這個ref示範所需證據；產品須另建立可信完成輸入。
把進度綁到另有可信依據的完成事件，並保留算術完整性與當拍阻擋。
- 驗證方式與待做檢查
重跑三份提早發證與四份正常發證，再區分96個提案哪些真的改動。沒有接受不自動等於偵測成功。
Node 已重現提早完成，並查 96 組儲存／替換參數，另跑四步正向及三步負向控制。
- 防護界線與未驗證項目
配對提案超過4便沒有改欄，不能說那次錯配已被檢查員發現。邊界是受限狀態替換，不是實體enable或所有溢位。
配對是受限的抽象替換。超範圍提案不作用。RTL、溢位實作與實體共用 enable 行為尚未驗證。
換個情境再想一次
學生舉著作業卻老師不收是stall，兩欄應保持。再把clear與收件放同拍，先定義誰優先；原排程沒有給出產品答案。
加入 stall 與同時 set／clear。定義優先權，以及哪些事件必須讓進度保持不變。
以上整理對照本課的教學案例、參考資料與實驗範圍；未列為已完成的驗證，都是後續工作。