Alert 與局部回應：偵測是否趕上接受？

分開標出偵測、阻擋與復原

偵測器辨認異常。局部阻擋防止這個區塊交出操作。Alert 把報告送到系統政策，後者可能中斷、清除或重置。這些是不同事件，延遲也可能不同。

儲存 upset 在 edge f 後作用。錯誤許可最早在 f＋1 出現。偵測在 f＋1＋D 出現，D 為零到四的整數延遲。系統阻擋再晚 R 個緣。請求只在指定緣接受。

這些是教學緣數，沒有量測 OpenTitan。它的 alert handler 文件描述系統升級機制。產品須從實作與時序證據導出延遲上限，也要包含來源到接收端路徑。Alert handler 文件

舊 sticky 趕不上第一個錯誤緣

F＝1、D＝0 時，edge 2 的目前 bad 為 true，舊 sticky 卻為 false。Local 政策要求兩者皆清零，因此會擋。只看 sticky 則接受。Sticky 之後才更新，無法改掉已記錄的接受。

D＝1 時，local 在 edge 2 也還沒偵測。錯誤 grant 已可見，因此請求先 commit，edge 3 才報錯。當拍錯誤閘要有用，該錯誤本身就必須先到。

System 政策等到 f＋1＋D＋R 才阻擋。較晚 reset 能停止後續工作並協助復原，但無法撤銷不可逆交付。第一次越權接受與後續成功通報，必須分開報告。

把第一個錯誤緣展開

固定未授權映像、f=1、D=0、R=2。故障在 edge 1 後改壞保存值；edge 2 前 corrupt=1、bad=1，但 sticky 尚未保存它。D=0 的意思是模型假設 bad 在 edge 2 取樣前已穩定，不是宣稱實體 detector 沒有延遲。

Edge 2 更新後 sticky 才變成 1，所以不能阻止 edge 2 已發生的接受。System 回應再等 R=2，到 edge 4 才阻擋。先把 acceptEdge 設為 2 比較三政策，再設為 4；改 acceptEdge 是另外重跑的請求排程，不是撤回先前的 commit。

對持續 corrupt，本模型的可接受錯誤窗口是：local 從 f+1 到 f+1+D 之前；sticky-only 到 f+2+D 之前；system 到 f+1+D+R 之前。起點包含，阻擋終點不包含。D=0 時 local 窗口為空；sticky-only 仍多一個取樣緣。這些是指定離散排程的結果，不涵蓋拍內 glitch、下游 grant 故障或實際閘延遲。

寫出可信回應邊界

儲存主表只注入一次持續 upset，f 為 0～5。D 為 0～4，請求緣為 0～8，完整表固定 R＝2。觀察到 edge 8，sticky 初始 false。映像 reference 與非目標偵測／回應電路保持可信。

最終 grant 另測：儲存維持正確，只在接受緣反相 grant。前面的局部阻擋無法控制這個下游強制。這沒有測請求 buffer 或接受機制內部故障。

時脈與 reset 故障、alert 連線失效、clear／wipe 順序、拍內 pulse 及類比感測器，都不在兩態緣模型內。可信偵測器是假設，沒有證明實體偵測來得及。真正訊號必須在接受緣前穩定。

只移一個延遲，查第一次 commit

從 f＝1、D＝0、request edge＝2、local 開始。看到 edge 2：bad 為 true、sticky 為 false、commit 為 false。改 sticky，匯出越權軌跡。再回 local，把 D 改為一。第一筆此時也能繞過局部阻擋。

已執行 810 條儲存時序流跡：六個故障緣、五種偵測延遲、九個請求緣與三政策，R＝2。另一組系統政策枚舉涵蓋 R＝0～4，共 1,350 條；local 與 sticky 不使用 R。獨立區間斷言核對越權窗口，並以直接邊緣反例檢查公式。Corrupt 是另一個時序模型，沒有接上第四到九課的偵測器。

三政策的無故障授權控制都接受，無故障未授權都拒絕。故障生效前沒有越權，是錯誤許可還未可見；阻擋後拒絕，則是處置生效。兩種沒有 commit 的原因，應分開解釋。

待驗證 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 節。片段尚未編譯，不能把列出性質當成已證明。

always_ff @(posedge clk or negedge rst_n)
  if (!rst_n) sticky_q <= 1'b0;
  else sticky_q <= sticky_q || local_bad;
assign grant = permission_q && !local_bad && !sticky_q;
assign accepted_commit = valid && ready && grant;
assert property (@(posedge clk) disable iff (!rst_n)
  local_bad |-> !accepted_commit);
assert property (@(posedge clk) disable iff (!rst_n)
  accepted_commit |-> reference_pass);
cover property (@(posedge clk) disable iff (!rst_n)
  reference_pass && accepted_commit);

RTL／SVA 尚未編譯，需要明確的組合時序路徑與可信接受端。系統回應要分別限制偵測到 alert、alert 到動作，也要驗證持續阻擋。第十一課會加入 reset、clock、CDC 與生命週期，這些目前仍為規劃。

檢查你的推理