FSM 轉移與歷史：許可必須屬於這次交易

CHECK→RELEASE 是合法轉移，但故障改掉了選路條件。另一個請求拿交易 1 的 token，來放行交易 2。兩種請求都可能看起來合乎結構。本課追每次接受事件應具備的證據。

合法轉移也能使用錯誤條件

學校借器材先排隊、查借用資格，再交器材。這是WAIT→CHECK→RELEASE。若把檢查時讀到的成功條件改成真，管理員仍沿校規允許的CHECK→RELEASE走，借用資格卻沒通過。Arc像檢查流程路線，state像檢查現在的牌子，二者都不會自己重新審核申請。跳過排隊直接到交付另測，不能和假條件當成同一種故障。

轉移關係列出允許的狀態配對。WAIT 能進 CHECK；CHECK 依成功或失敗，選 RELEASE 或 ERROR。這張表能拒絕 WAIT 直接跳 RELEASE，卻不能證明 success 輸入本身可信。

條件實驗的目前映像未授權。一次錯誤成功判斷讓 CHECK 選 RELEASE。轉移檢查器仍認得 CHECK→RELEASE。只查狀態或弧的接收端，在 edge 3 便接受。接收端還需要這次授權條件。

狀態跳躍另測。一次事件在 edge 0 後把狀態設為 RELEASE，而不是 CHECK。Arc 政策在 edge 3 請求前送它進 ERROR。這條軌跡顯示弧檢查有用，但沒有消除偽造條件的反例。

把證據綁到身分與使用紀錄

借用單還要寫是哪一次借用，以及是否已領。這次編號2，上次編號1的有效單不能用。第3拍交出器材時才把單標成已用，第4拍再拿同一單就應拒絕。這分別對應token_id、valid與consumed。一次許可只准一次交付是本課契約，不是所有借用系統或所有CPU取指的通則；這張單也沒有密碼學認證。

本課 token 包含 valid、交易 id 與已使用旗標。目前交易 id 為二。上一筆 id＝一的 token，即使 valid 為 true，仍已過期。有效許可要求 valid、id 相符且未使用。這些只是邏輯欄位，沒有密碼認證。

合法目前交易在 edge 1 後，由可信驗證產生 token。請求可在 edge 3 commit。該緣之後標為已使用。Edge 4 再來一筆，接受前可見的 consumed 狀態就必須拒絕。

獨立 monitor 也記錄一次交付是否已發生，不複製 DUT 的 consumed。重複請求情境若只看狀態，會接受兩次。依本課只准一次交付的契約，第二次便越權。

同一個 RELEASE，逐欄核對許可

管理員在RELEASE逐欄查單：有紀錄嗎、編號是否2、是否還沒用。只有valid=1、id=2、consumed=0的單符合fresh。第3拍取樣仍未用，交付後才標記，所以第4拍能看到已用。獨立稽核簿另記交過一次，不抄單上的used；這個故事沒有覆蓋編號重用、同時兩份借用或reset後舊單回來的問題。

Token 在這裡是保存檢查結果與交易身分的欄位，不是密碼學認證 token。Current id 固定為 2。Fresh 的定義是 valid AND (token_id==2) AND NOT consumed。

valid	token_id	consumed	fresh	在 RELEASE 能否通過 bound
0	2	0	0	否：沒有有效證據
1	1	0	0	否：證據屬於舊交易
1	2	1	0	否：已使用
1	2	0	1	是：欄位符合本課契約

正向控制在 edge 1 更新後產生 id=2 的有效證據。Edge 3 取樣前，consumed=0，所以第一次請求可接受；edge 3 更新後 consumed=1。保持 RELEASE 並在 edge 4 重複請求，fresh 變成 0，第二次不能接受。獨立 monitor 另記第一次交付；它不靠 DUT 的 consumed 來判定自己的期待結果。

Arc 政策回答「這條狀態轉移是否允許」，bound 回答「證據是否屬於這次交易且未使用」。本實驗把它們分開比較，bound 沒有自動加上 arc checker。產品若同時需要兩項，必須把兩項都接上，再驗證 id 重用、reset、abort 與並行；這些情境不在本課固定 id=2 的模型內。

分開測過期、假條件與重複請求

假條件、舊借用單、跳過流程與重複領取各用一份演練。舊單情境包含保留id1並錯誤信任它，不是只翻一個保存bit；重復領取則改工作負載，沒有多算一次故障。Bound先信任單的欄位與產生者。這個邊界讓我們檢查證據綁定，沒有證明借用單自己不會被改。

每條軌跡從 WAIT 到 edge 4。各自只有一種命名故障效果，或重複工作負載。Condition 與 stale 在 CHECK 後選 RELEASE；state 在 edge 0 後跳態；repeat 保留 RELEASE 給第二筆。它們沒有同時注入。

Stale 實驗帶入 valid、id＝一的舊 token，目前 id＝二。情境包含保留舊證據及信任它的寬鬆判斷。這是協定邊界情境，不能叫單一儲存 bit XOR。Bound 測試中，token 欄位、可信驗證及最終 grant 不受擾。

SCFI 在強化的下一態函數中納入控制訊號與執行歷史。本課普通 token 示範這個區別，沒有實作 SCFI，也不能沿用它的機率性保證。SCFI 作者摘要

把 token 與接受緣放在一起看

先用拒絕申請配假成功條件，arc認得路線仍在第3拍交付；換bound，沒有本次許可就不交。再用真正許可與重復領取，state交兩次，bound只交第3拍。已授權的跳態在bound下也可能交，而arc會拒絕：校規查路線與查單據是兩條獨立要求，需要都滿足時就要明確組合。門口一度顯示准許還不等於有人領走器材。

選 condition、arc 政策及未授權。Edge 3 的 RELEASE 與 commit 成立，獨立 reference 卻是 false。改 bound，因沒有目前有效 token，便不 commit。再選 stale，把 tokenId＝1 與 id＝2 一起看。

重複請求設授權 true。State 在 edge 3、4 都接受，bound 只接受 edge 3。Bound 查授權歷史，沒有合併轉移合法性。因此已授權的 state jump 在 bound 下提交，arc 則拒絕。Arc 流跡的 edge 1 可先看到 grant，更新後才進 ERROR；請求從 edge 3 開始，先前 grant 不代表接受。這些案例都有分開執行的斷言。

正常正向交易依序經 WAIT、CHECK、RELEASE，接受一次。故障復原不必走一條完全沒有故障的歷史。產品可以在錯誤後合法復原，但後續敏感接受前，復原政策仍須建立新的授權。

待驗證 RTL／SVA

RTL裡的fresh就是有效、當前編號、未用三項同時成立。接受那拍之後設置consumed，下次請求才讀到新值。稽核簿問這次許可與先前交付歷史，對應reference_pass與reference_used。普通借用單不等於SCFI方案；這段草稿也尚未定義新申請與abort，不能替完整產品協議作保證。

讀懂本課的性質：新鮮證據與單次交付

『每次交付都有許可且沒領過』要在交器材那拍查。只看最後單據已用，會漏掉第3、4拍都交過的歷史；只看RELEASE牌也一樣。這對應同緣assertion與獨立reference_used。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 節。片段尚未編譯，不能把列出性質當成已證明。

assign fresh = token_valid_q && (token_id_q == current_id_i) && !consumed_q;
assign local_bad = 1'b0; // bound-only teaching model; no arc checker
assign accepted_commit = req_valid && req_ready && grant;
assign grant = (state_q == Release) && fresh && !local_bad;
always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) consumed_q <= 1'b0;
  else if (accepted_commit) consumed_q <= 1'b1;
// A real design also specifies new-transaction and abort behavior.
assert property (@(posedge clk) disable iff (!rst_n)
  accepted_commit |-> reference_pass && !reference_used);
cover property (@(posedge clk) disable iff (!rst_n)
  reference_pass && accepted_commit);

草稿尚未編譯。Token 儲存完整性、id 回繞、abort、reset 與並行交易，先排除。真正綁定方案須有足夠身分空間，避免保留窗口內碰撞。復原與活性也要另寫性質。第九課會把協定推理用於組態寫入。

檢查你的推理

把『id1有效單給id2用』與『id2單第二次用』分開回答：前者身分不符，後者歷史已消費。再問沿合法CHECK→RELEASE為什么還可能交錯人。三個問題對應id、consumed與真實授權，不是把路線合法或單據有效當成完整資格。

1. 弧檢查為何漏掉假 CHECK 條件？

CHECK→RELEASE 本來就在允許關係內。

2. Id＝一的 valid token 對 id＝二有效嗎？

無效。

3. Consumed 何時可用來阻擋？

Edge 3 更新後，edge 4 請求前。

4. Token 模型實作了 SCFI 嗎？

沒有。

5. 並行交易會改什麼？

須逐筆追未完成交易的 token 身分、保存與使用。

工程收尾

把同一借用紀錄從排隊追到第3、4拍，分別留路線、單據與交付歷史。下面收尾沿這三欄整理；沒有把『能合法復原』誤寫成『必須永遠沒有故障』，也沒有把普通單據補成未實現的密碼認證。

威脅與故障模型: 假判斷、舊單、跳流程各另跑；重復領取是一份工作負載。先信任單據字段，不能說它們已受保護。

Edge 0～4；條件強制、狀態替換、舊 token 與重複工作負載分開。Bound 情境信任 token、驗證器及最終 grant。
根因: 舊id1單完整也不屬於id2，第二次領的id2單已經用過。valid與合法路線無法代替身分和交付歷史。

合法態與合法弧仍可使用假判斷。過期或重用證據，可能放行不同交付。
防禦: 第3拍交付後給單標已用，第4拍讀這個歷史。需要同時查路線時還須加arc；bound沒有暗含它。

把 token 綁到目前身分，接受後即消耗；產生與保存另行保護。
驗證: 把合法一次借用、假條件與重復領取各留交付簿。有限十組bound控制沒有測id回繞或並行借用。

Node 已跑十組 bound 控制，另重現假條件、舊 token 與重複接受；正常授權流程接受一次。
界線: 單據本課沒有被改，也沒有加密碼簽章。固定id2不支持編號長期重用或真實許可的保證。

沒有建立 SCFI、id 回繞、多交易或實體保證。Token 欄位仍保持可信。
遷移練習: 若准許把未授權id2單的valid從0改1，檢查id與未用是否還夠。另寫token目標與時間，不能沿用字段可信結論。

允許 token valid 受擾。查只靠 id 與 consumed，是否仍能拒絕第一次未授權交付。