WEBVTT

1
00:00:00.000 --> 00:00:03.260
控制器必須完成四筆傳輸，才交出結果。

2
00:00:03.260 --> 00:00:09.780
正數計數器已到四，倒數計數器也到零，兩者相加仍是四。

3
00:00:09.780 --> 00:00:12.100
但真正只完成三筆。

4
00:00:12.100 --> 00:00:15.720
共用 enable 讓兩份計數一起提早前進。

5
00:00:16.042 --> 00:00:18.962
交叉計數器以相反方向保存進度。

6
00:00:18.962 --> 00:00:23.242
本課三位元暫存器從 up＝0、down＝4 開始。

7
00:00:23.242 --> 00:00:26.402
每次計數，up 加一、down 減一。

8
00:00:26.402 --> 00:00:28.742
非模數相加必須維持四。

9
00:00:28.742 --> 00:00:33.002
比較時須加寬，避免截斷溢位而掩蓋錯誤。

10
00:00:33.002 --> 00:00:35.202
單獨改 up，通常會破壞總和。

11
00:00:35.202 --> 00:00:38.562
偵測器可以當拍擋完成，並記住錯誤。

12
00:00:38.562 --> 00:00:42.542
但總和仍成立時，檢查器不知道數值怎麼到達這裡。

13
00:00:42.542 --> 00:00:45.582
協同錯誤更新能躲過這種關係檢查。

14
00:00:45.582 --> 00:00:48.262
OpenTitan 提供交叉計數器。

15
00:00:48.262 --> 00:00:51.322
SYNFI 也討論共用 increment 與 clear 的保護邊界。

16
00:00:51.322 --> 00:00:57.442
以下小排程說明這個機制；本課沒有執行 SYNFI，也沒有重現論文的 netlist 實驗。

17
00:00:57.762 --> 00:01:03.922
真正一步是傳輸已被接受：valid 與 ready 在約定上升緣同時成立。

18
00:01:03.922 --> 00:01:06.222
停等一拍沒有完成工作。

19
00:01:06.222 --> 00:01:10.502
獨立 reference 只在真正握手時加一，並排除於故障範圍外。

20
00:01:11.442 --> 00:01:17.202
負向排程在 edge 1、3、4 有真正握手，edge 2 閒置。

21
00:01:17.202 --> 00:01:21.882
一次錯誤共用 enable 在 edge 2 後仍更新兩份計數。

22
00:01:21.882 --> 00:01:26.402
Edge 4 後，DUT 成為 4／0，reference 進度卻只有三。

23
00:01:27.142 --> 00:01:29.842
結果請求在 edge 5 到達。

24
00:01:29.842 --> 00:01:32.462
只檢查總和的版本會放行。

25
00:01:32.462 --> 00:01:36.742
授權 reference 要求四次真正傳輸，因此判為越權。

26
00:01:36.742 --> 00:01:42.302
總和檢查正確地回報沒有錯誤；它漏看未完成工作，並非算術計算壞掉。

27
00:01:42.762 --> 00:01:47.342
主要反例只在共用 enable 發生一次事件，沒有暫存器 XOR。

28
00:01:47.342 --> 00:01:50.442
窗口固定為 edge 0～5。

29
00:01:50.442 --> 00:01:53.022
兩份計數到端點即停。

30
00:01:53.022 --> 00:01:59.682
時脈、重置與工作負載可信；握手觀察器、reference、總和檢查與接收端也不受擾。

31
00:02:00.102 --> 00:02:06.602
實驗另提供三位元 up 暫存器 XOR，也能替換配對，使 down＝4−up。

32
00:02:06.602 --> 00:02:11.182
配對替換只接受 up 在 0～4 內的提案，超出範圍便不作用。

33
00:02:11.182 --> 00:02:15.702
這是受限的相關替換，不能叫兩次獨立 bit flip。

34
00:02:15.702 --> 00:02:19.102
提交參數與實際生效要分開記錄。

35
00:02:19.102 --> 00:02:23.102
進度版本另比較 up 與獨立進度輸入，並記住差異。

36
00:02:23.102 --> 00:02:27.202
可執行模型借可信 reference 示範所需條件。

37
00:02:27.202 --> 00:02:30.182
產品必須另建立可信的工作完成觀察。

38
00:02:30.182 --> 00:02:34.162
把 testbench 判準接到 grant，不等於完成硬體防護。

39
00:02:34.522 --> 00:02:39.942
選 enable、fault edge＝2 與 sum 政策，逐拍看表。

40
00:02:39.942 --> 00:02:43.722
Edge 3 的配對已包含錯誤一步，ref 沒有增加。

41
00:02:43.722 --> 00:02:47.122
Edge 5 的 commit 為 true，reference 為 false。

42
00:02:47.122 --> 00:02:51.502
改 progress 政策，工作負載不變，這條反例會被擋住。

43
00:02:51.502 --> 00:02:57.502
三次交握排程的 96 組 up／pair 測試，在 progress 政策下都不提交。

44
00:02:57.502 --> 00:03:01.962
這本身不能證明故障被偵測，因為 reference 根本沒有到四。

45
00:03:01.962 --> 00:03:10.182
另有斷言檢查共用 enable 的進度不一致、up XOR 打破總和，以及配對替換繞過總和檢查。

46
00:03:10.182 --> 00:03:13.022
無故障四次交握控制會在 edge 5 接受。

47
00:03:13.742 --> 00:03:15.682
試著在 edge 5 後注入。

48
00:03:15.682 --> 00:03:20.002
這個窗口沒有後續請求，因此沒有越權只說明觀察已結束。

49
00:03:20.002 --> 00:03:24.002
若要判定錯誤進度無害，先把請求移晚。

50
00:03:24.002 --> 00:03:26.382
也要記錄注入是否真的改動配對。

51
00:03:26.772 --> 00:03:28.592
RTL 草稿尚未編譯。

52
00:03:28.592 --> 00:03:35.672
產品計數器須定義 set／clear、算術寬度、飽和或回繞，並限制未完成工作數。

53
00:03:35.672 --> 00:03:39.332
信任重複暫存器之前，先測共用 enable。

54
00:03:39.332 --> 00:03:42.952
第七課會檢查狀態編碼能辨認哪些替換。

55
00:03:43.412 --> 00:03:49.872
Edge 0～5 內，在閒置拍後發生一次共用 enable 事件；暫存器效果分開測。

56
00:03:49.872 --> 00:03:52.412
結果請求前只有三次真正握手。

57
00:03:53.052 --> 00:04:01.272
Node 已重現提早完成，並查 96 組儲存／替換參數，另跑四步正向及三步負向控制。

58
00:04:01.732 --> 00:04:04.392
配對是受限的抽象替換。

59
00:04:04.392 --> 00:04:06.572
超範圍提案不作用。

60
00:04:06.572 --> 00:04:10.872
RTL、溢位實作與實體共用 enable 行為尚未驗證。