三份驗證結果投票決定是否放行失敗映像。一份副本出錯，可能被其他兩份蓋過。但共用輸入先變錯，三份都可能投贊成票。數副本之前，先畫出共用部分。
兩份比較，三份投票
校外教學有三份准許參加的名冊欄，a、b、c各記0或1。兩份版本要求都同意，是DMR；三份版本要求至少兩票同意，是TMR。原本都不準去，改兩份成(1,1,0)，多數會准許上車，原始資格簿仍拒絕。名冊一致或多數只描述副本的關係；三份名冊沒有自動成為三次獨立資格審核。
雙模組冗餘稱為 DMR。本課保留兩份一位元副本，兩份都為 true 才放行。不一致會拉高 bad，並拒絕許可。在比較器可信的模型內，單一副本翻轉能被辨認。但比較器無法知道哪份正確。
三模組冗餘稱為 TMR，至少兩份 true 就得到 true。三份原本都為 false，翻一份仍投拒絕票。翻兩份得到 110，多數票便放行，映像卻仍未授權。
多數投票器也能回報不一致。本課比較「採多數繼續」與「任何不一致就拒絕」。拒絕政策能擋住兩位反例 110，但翻三份得到一致的 111。相等檢查無法分辨它與正常一致。
授權映像遇到一份翻轉，會得到 011。多數政策仍放行，拒絕政策則停止服務。這是模型內的可用性差異。若密碼運算的錯誤輸出可能洩漏資訊，政策還需要另外分析。
手算投票，也算它的可用性代價
班導依(a,b,c)順序讀名冊：兩個1、一個0，便有兩票同意，但也有不一致。採多數繼續就上車，遇不一致拒絕則不上車。合法學生若其中一份誤改成0，後者也可能拒絕真正有權的學生。這對應majority與reject-mismatch的取捨；名冊順序是三個副本欄位，不能把110讀成畫面mask=3的整數位序。
令 a、b、c 是三個保存的許可位元。多數決是 (a AND b) OR (a AND c) OR (b AND c)。當 (a,b,c)=(1,1,0)，三項依序為 1、0、0，投票得到 1；但副本不一致，bad=1。Majority 政策仍放行，reject-mismatch 會拒絕。畫面中的 mask=3 翻轉副本 a、b；這裡用 (a,b,c) 次序列值，不能把它當成由 bit 2 到 bit 0 顯示的 packed 整數。
失敗映像原本是 (0,0,0)，上述兩副本翻轉就讓它越權。合法映像原本是 (1,1,1)，只翻 a 後變成 (0,1,1)，多數決仍算對。此時拒絕不一致會阻擋合法工作。兩種政策在安全性與可用性上作了不同選擇，不能只看 bad 是否出現。
改選 source target、mask 非零時，模型先把共同來源從 0 改成 1，再寫入三個副本，得到 (1,1,1)。三個 AND 都是 1，bad=0。投票器完全照規則工作，答案仍然沒有授權。這是共同來源目標的另一條實驗，不是一次只改一個保存副本。
分開計算事件與受影響副本
一次搞鬼若能同時改a與b兩份，事件數是1，受影響副本數是2。若校規要保證一份名冊改錯仍不讓拒絕學生上車，就須把『至多一份』寫進卡上，不能只寫『一次』。本課只在edge1看一次上車請求；沒有查下一班車或後續修復，也沒有把mask當成三份紙在現實里相隔多遠。
主表在 edge 1 接受前，注入一次事件。事件以 mask XOR 改兩個 DMR 位元，或三個 TMR 位元。每位代表一份副本輸出。程式枚舉四種 DMR mask、八種 TMR mask，零值是無故障控制。
這個抽象允許一次事件影響兩份副本。因此，「能防一份副本出錯」需要限制副本數，不能只寫一次事件。本表只觀察一個接受緣；後續持續時間與復原不在窗口內。
副本主表信任映像 reference、輸入分配與比較／投票器。時脈、重置及握手也不受擾。Mask 不代表實體位置或機率。下節的來源與投票器實驗各自只替換一個目標，仍保留獨立映像 reference。
沿共用輸入追到投票結果
三位抄名冊的人若都從同一張被改過的原稿抄，會一起寫1，得到(1,1,1)，彼此完全一致卻共同錯。這對應source在分配前出錯。另一次名冊全是0，只把最後『准許上車』改成1，則是voter target。原始資格簿仍在兩種實驗外；多數決算得正確，也不能修復共用來源或最後閘的錯誤。
來源實驗在所有副本保存前，翻轉共用授權位元。各副本都變成 true。DMR 與 TMR 都一致放行。比較器沒有壞；它正確地回報了錯誤答案彼此相等。
投票器實驗維持副本為 false，只反相最終投票 grant。接受端便看到 true。這個目標位於副本檢查之後。不能把它與副本翻轉合在一起，仍聲稱只測單一副本故障。
副本可能共用時脈、reset、enable 或資料來源，布局也會造成相依性。空間分離可能有助於局部擾動，但需要實體證據。綜合也可能合併冗餘邏輯，OpenTitan 指南提醒這個風險。硬體指南
分開看偵測、遮蔽與接受
先改一份拒絕名冊，兩票仍拒絕，且bad報不一致；再改兩份，bad仍報錯，多數卻讓學生上車。這把發現差異、遮蔽錯誤與真正交付分開。換拒絕政策只改門口處置，不改名冊。八種mask中的四種多數放行，是這份枚舉的數量，不能說校外教學有一半機率被突破。
選 TMR、mask＝1 與未授權輸入。多數票拒絕，bad 為 true，模型內同時辨認不一致並遮蔽放行。再改 mask＝3。雖然 bad 仍為 true，多數票卻接受錯誤請求。切換拒絕政策，只改局部處置。
八種 TMR mask 有四種多數票越權：三種影響兩份，一種影響三份。四種 DMR mask 有一種越權。這些已執行數字只屬有限枚舉，不能當可靠度估計。共用來源與投票器另測。
兩種方案都要設 authorized＝true、mask＝0，確認能接受。再翻一份副本，比較可用性。另保存共用來源造成一致錯誤的軌跡。說明為何一致只證明彼此相符，而授權錯誤要由獨立 reference 判定。
待驗證 RTL／SVA
把班導的投票寫成三個兩兩同意的AND再OR，就能逐項核對門口演算法。安全稽核仍問上車的學生是否列在原始許可名冊，對應reference_pass。稽核規則沒有把三個一位元欄變成三顆完整密碼核心；本節尚未編譯的RTL也沒有證明副本在製作後獨立。
讀懂本課的性質：投票結果與真實許可
即使門口照(1,1,1)放行，稽核員若在獨立簿上看到0，接受緣的assertion仍應失敗。若門口永遠不上車，則須拿一名真的獲準學生、不改名冊去做cover與正向控制。兩份紀錄不能取自同一張受改原稿，否則真假一起變1，稽核就失去判準；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 mismatch = (a != b) || (a != c);
assign majority = (a && b) || (a && c) || (b && c);
assign grant = majority && (!REJECT_MISMATCH || !mismatch);
assign accepted_commit = valid && ready && grant;
assert property (@(posedge clk) disable iff (!rst_n)
accepted_commit |-> reference_pass);
cover property (@(posedge clk) disable iff (!rst_n)
reference_pass && accepted_commit);片段描述 TMR 組合行為與獨立 harness 性質，尚未編譯。產品仍要驗證投票器保護、副本保留、延遲對齊與 reset skew，也要分析錯誤輸出洩漏。本課一位元副本只是授權輸出，不代表三顆完整密碼核心。第六課會追共用 enable 如何改錯進度。
故障實驗台
實驗臺的copies就是名冊(a,b,c)，majority是票數結論，bad是名冊不同，commit是上車接受。保持原學生資格，依序改副本、共用原稿與投票器，重設後再跑合法學生的一份翻轉。每次只選一種目標；這份互動沒有模擬校車、實體布局或副本同步延遲。
已執行有限、兩態教學模型。RTL 模擬、合成、形式證明與晶片驗證均尚未執行。Reference 欄位是可信測試平台的觀察，不是晶片多出來的防禦。
檢查你的推理
試著解釋兩種不能混淆的名冊：(1,1,0)能報不一致，(1,1,1)則完全一致。兩者都可能來自拒絕學生的錯誤紀錄。再將原資格改成准許，只錯一份，預測兩政策的可用性。這些問題檢查副本關係與真實資格；名冊的相符沒有提供來源獨立性的證據。
1. DMR 能指出哪份正確嗎？
不能，不一致只證明兩者不同。
2. 哪種 TMR mask 開始讓失敗映像放行？
任一兩位 mask，例如 3。
3. 遇不一致拒絕，能擋住一致錯誤嗎？
不能。
4. 為何要測授權輸入與一份翻轉？
它能顯示兩政策的可用性差異。
5. 獨立性需要哪些證據？
來源、時脈與重置、保留副本的 netlist，還有實體故障範圍；不能只數副本。
MY ACADEMY · LESSON FILM
教學影片
影片依序說明本課的資料路徑。看完一段，可以回到下面的互動練習，改變輸入或故障條件。動畫呈現教學模型；它沒有替代 RTL 模擬。
旁白使用合成聲音。互動教學與動畫均有模型邊界；請以本課的來源與驗證範圍解讀結果。
本課故障互動實驗
此實驗執行有限、兩態教學模型。RTL／SVA 為待驗證範例，未執行 RTL 模擬、合成、形式證明、時序收斂或晶片驗證。枚舉數量不是實體攻擊機率。
Wrap-up｜把這一課帶回設計審查
校外教學的收尾不是只數出有三張名冊，還要記哪張原稿共用、一次能改幾份，以及上車前如何處置。下面沿同一名冊主線整理，投票與拒絕政策的差別仍保留，沒有把全部錯誤統稱已阻擋。
- 威脅模型與成立條件
一次圈中兩份名冊，仍是一次事件而兩份副本。edge1上車結果沒有涵蓋後面行程或復原。
一次事件在 edge 1 改指定副本輸出，DMR 寬兩位、TMR 寬三位。來源與最終投票器另測。
- 失效原因
(1,1,1)可由錯誤共用原稿抄出，bad=0仍上錯車。相符只說明副本關係，沒有證明資格。
多份錯誤副本能取得多數或一致。共用錯誤來源會被忠實複製；最終投票器受擾能繞過比較。
- 防護方法
把一份翻錯的合法名冊擋下，會犧牲合法學生上車。選擇拒絕或多數須寫政策，且來源與投票器另外保護。
依副本預算選比較或投票，寫明局部處置政策。共用輸入與投票器須分開保護。
- 驗證方式與待做檢查
四種兩份、八種三份mask與真許可不改的名冊分別檢查。這裡重跑有限票數，沒有驗證實物獨立性。
已跑四種 DMR、八種 TMR mask，含來源／投票器反例及正向控制。尚未跑 RTL 或實體獨立性測試。
- 防護界線與未驗證項目
三張名冊若同源同鐘，分開擺紙無法保證晶片副本獨立。授權一位元的模型也沒有涵蓋完整運算。
一位元副本未涵蓋完整資料路徑、時間對齊與洩漏。拒絕政策可能阻擋合法工作。
換個情境再想一次
若同一清場通知誤把幾張名冊重置成准許，就逐份定義reset值再看上車。這個新target不在原副本mask實驗內。
允許共同 reset 故障。定義哪些副本重置，並檢查過度放寬的重置值能否取得 commit。
以上整理對照本課的教學案例、參考資料與實驗範圍；未列為已完成的驗證，都是後續工作。