WEBVTT

1
00:00:00.000 --> 00:00:04.560
三份驗證結果投票決定是否放行失敗映像。

2
00:00:04.560 --> 00:00:07.720
一份副本出錯，可能被其他兩份蓋過。

3
00:00:07.720 --> 00:00:12.120
但共用輸入先變錯，三份都可能投贊成票。

4
00:00:12.120 --> 00:00:14.420
數副本之前，先畫出共用部分。

5
00:00:14.800 --> 00:00:17.600
雙模組冗餘稱為 DMR。

6
00:00:17.600 --> 00:00:22.080
本課保留兩份一位元副本，兩份都為 true 才放行。

7
00:00:22.080 --> 00:00:25.300
不一致會拉高 bad，並拒絕許可。

8
00:00:25.300 --> 00:00:29.660
在比較器可信的模型內，單一副本翻轉能被辨認。

9
00:00:29.660 --> 00:00:31.760
但比較器無法知道哪份正確。

10
00:00:32.560 --> 00:00:37.260
三模組冗餘稱為 TMR，至少兩份 true 就得到 true。

11
00:00:37.260 --> 00:00:41.000
三份原本都為 false，翻一份仍投拒絕票。

12
00:00:41.000 --> 00:00:45.880
翻兩份得到 110，多數票便放行，映像卻仍未授權。

13
00:00:46.440 --> 00:00:49.080
多數投票器也能回報不一致。

14
00:00:49.080 --> 00:00:53.260
本課比較「採多數繼續」與「任何不一致就拒絕」。

15
00:00:53.260 --> 00:00:58.860
拒絕政策能擋住兩位反例 110，但翻三份得到一致的 111。

16
00:00:58.860 --> 00:01:01.660
相等檢查無法分辨它與正常一致。

17
00:01:02.280 --> 00:01:05.640
授權映像遇到一份翻轉，會得到 011。

18
00:01:05.640 --> 00:01:09.240
多數政策仍放行，拒絕政策則停止服務。

19
00:01:09.240 --> 00:01:12.400
這是模型內的可用性差異。

20
00:01:12.400 --> 00:01:16.660
若密碼運算的錯誤輸出可能洩漏資訊，政策還需要另外分析。

21
00:01:16.925 --> 00:01:20.525
主表在 edge 1 接受前，注入一次事件。

22
00:01:20.525 --> 00:01:26.185
事件以 mask XOR 改兩個 DMR 位元，或三個 TMR 位元。

23
00:01:26.185 --> 00:01:29.265
每位代表一份副本輸出。

24
00:01:29.265 --> 00:01:34.145
程式枚舉四種 DMR mask、八種 TMR mask，零值是無故障控制。

25
00:01:34.925 --> 00:01:38.445
這個抽象允許一次事件影響兩份副本。

26
00:01:38.445 --> 00:01:43.765
因此，「能防一份副本出錯」需要限制副本數，不能只寫一次事件。

27
00:01:43.765 --> 00:01:48.665
本表只觀察一個接受緣；後續持續時間與復原不在窗口內。

28
00:01:49.205 --> 00:01:55.225
副本主表信任映像 reference、輸入分配與比較／投票器。

29
00:01:55.225 --> 00:01:57.565
時脈、重置及握手也不受擾。

30
00:01:57.565 --> 00:02:00.445
Mask 不代表實體位置或機率。

31
00:02:00.445 --> 00:02:06.165
下節的來源與投票器實驗各自只替換一個目標，仍保留獨立映像 reference。

32
00:02:06.645 --> 00:02:10.705
來源實驗在所有副本保存前，翻轉共用授權位元。

33
00:02:10.705 --> 00:02:12.765
各副本都變成 true。

34
00:02:12.765 --> 00:02:15.605
DMR 與 TMR 都一致放行。

35
00:02:15.605 --> 00:02:19.725
比較器沒有壞；它正確地回報了錯誤答案彼此相等。

36
00:02:20.165 --> 00:02:24.945
投票器實驗維持副本為 false，只反相最終投票 grant。

37
00:02:24.945 --> 00:02:27.165
接受端便看到 true。

38
00:02:27.165 --> 00:02:29.785
這個目標位於副本檢查之後。

39
00:02:29.785 --> 00:02:34.265
不能把它與副本翻轉合在一起，仍聲稱只測單一副本故障。

40
00:02:34.845 --> 00:02:40.885
副本可能共用時脈、reset、enable 或資料來源，布局也會造成相依性。

41
00:02:40.885 --> 00:02:45.325
空間分離可能有助於局部擾動，但需要實體證據。

42
00:02:45.325 --> 00:02:49.645
綜合也可能合併冗餘邏輯，OpenTitan 指南提醒這個風險。

43
00:02:49.978 --> 00:02:54.078
選 TMR、mask＝1 與未授權輸入。

44
00:02:54.078 --> 00:03:00.798
多數票拒絕，bad 為 true，模型內同時辨認不一致並遮蔽放行。

45
00:03:00.798 --> 00:03:02.718
再改 mask＝3。

46
00:03:02.718 --> 00:03:07.038
雖然 bad 仍為 true，多數票卻接受錯誤請求。

47
00:03:07.038 --> 00:03:09.538
切換拒絕政策，只改局部處置。

48
00:03:10.598 --> 00:03:16.898
八種 TMR mask 有四種多數票越權：三種影響兩份，一種影響三份。

49
00:03:16.898 --> 00:03:20.018
四種 DMR mask 有一種越權。

50
00:03:20.018 --> 00:03:24.738
這些已執行數字只屬有限枚舉，不能當可靠度估計。

51
00:03:24.738 --> 00:03:26.838
共用來源與投票器另測。

52
00:03:27.678 --> 00:03:33.418
兩種方案都要設 authorized＝true、mask＝0，確認能接受。

53
00:03:33.418 --> 00:03:36.538
再翻一份副本，比較可用性。

54
00:03:36.538 --> 00:03:39.938
另保存共用來源造成一致錯誤的軌跡。

55
00:03:39.938 --> 00:03:45.718
說明為何一致只證明彼此相符，而授權錯誤要由獨立 reference 判定。

56
00:03:46.062 --> 00:03:51.822
片段描述 TMR 組合行為與獨立 harness 性質，尚未編譯。

57
00:03:51.822 --> 00:04:00.122
產品仍要驗證投票器保護、副本保留、延遲對齊與 reset skew，也要分析錯誤輸出洩漏。

58
00:04:00.122 --> 00:04:05.802
本課一位元副本只是授權輸出，不代表三顆完整密碼核心。

59
00:04:05.802 --> 00:04:08.822
第六課會追共用 enable 如何改錯進度。

60
00:04:09.705 --> 00:04:16.005
一次事件在 edge 1 改指定副本輸出，DMR 寬兩位、TMR 寬三位。

61
00:04:16.005 --> 00:04:17.845
來源與最終投票器另測。

62
00:04:19.225 --> 00:04:25.965
已跑四種 DMR、八種 TMR mask，含來源／投票器反例及正向控制。

63
00:04:25.965 --> 00:04:29.145
尚未跑 RTL 或實體獨立性測試。

64
00:04:29.145 --> 00:04:34.345
一位元副本未涵蓋完整資料路徑、時間對齊與洩漏。

65
00:04:34.345 --> 00:04:36.545
拒絕政策可能阻擋合法工作。