WEBVTT

1
00:00:00.000 --> 00:00:02.660
控制器正在檢查未授權映像。

2
00:00:02.660 --> 00:00:07.400
六位元狀態從 CHECK 變成 RELEASE，授權卻沒有完成。

3
00:00:07.400 --> 00:00:11.200
新碼字合法，狀態解碼器認得它，也因此開閘。

4
00:00:11.200 --> 00:00:14.460
本課先算哪些替換能造成這個結果。

5
00:00:14.720 --> 00:00:20.580
有限狀態機稱為 FSM，用暫存器保存目前階段。

6
00:00:20.580 --> 00:00:24.840
稀疏編碼在大位元空間中，只指定少數合法值。

7
00:00:24.840 --> 00:00:31.020
其他值能協助辨認錯誤，前提是實作真的識別它們，並拒絕不安全輸出。

8
00:00:31.680 --> 00:00:39.060
本課六位元表為 WAIT＝000000、CHECK＝001111、RELEASE＝

9
00:00:39.060 --> 00:00:42.940
110011、ERROR＝111100。

10
00:00:42.940 --> 00:00:46.200
六組不同狀態配對都相差四位。

11
00:00:46.200 --> 00:00:51.880
只查 CHECK 到 RELEASE，可能漏掉其他較近配對；最小距離要遍歷整張表。

12
00:00:52.620 --> 00:01:00.120
這張表中，一、二或三位儲存翻轉無法變成另一個命名狀態，只會得到非法值。

13
00:01:00.120 --> 00:01:03.120
四位則可能變成另一個合法態。

14
00:01:03.120 --> 00:01:09.140
因此，碼距支持的是有預算的替換主張，且仍須信任合法性檢查與輸出閘。

15
00:01:09.720 --> 00:01:14.900
Default 分支把下一態送進 ERROR，影響的是目前接受緣之後。

16
00:01:14.900 --> 00:01:19.060
若輸出解碼器已讓非法目前態放行，下一拍復原就太晚。

17
00:01:19.060 --> 00:01:23.300
RELEASE 要完整比對，當下非法態也要擋住同一接受緣。

18
00:01:23.940 --> 00:01:26.640
小模型只在 state＝RELEASE 時放行。

19
00:01:26.640 --> 00:01:29.080
非法態另以 bad 回報。

20
00:01:29.080 --> 00:01:33.280
Sticky 能保存歷史供後續復原，不能代替當拍阻擋。

21
00:01:33.280 --> 00:01:38.280
此解碼的完整相等已拒絕非法態，不要把另一個閘說成額外獨立覆蓋。

22
00:01:38.920 --> 00:01:42.360
RTL 常數不保證綜合後編碼相同。

23
00:01:42.360 --> 00:01:47.020
須檢查產出的 netlist 是否重編碼、暫存器寬度及輸出邏輯。

24
00:01:47.020 --> 00:01:50.960
OpenTitan 提供稀疏 FSM 儲存用的 flop wrapper，但

25
00:01:50.960 --> 00:01:54.140
wrapper 與 assertion 本身不能證明整個控制器安全。

26
00:01:54.640 --> 00:01:57.620
主實驗從已保存 CHECK 開始。

27
00:01:57.620 --> 00:02:04.460
在 edge 1 接受前，一次事件 XOR 六個保存位元，遍歷六十四種 mask。

28
00:02:04.460 --> 00:02:06.740
Reference 映像未授權。

29
00:02:06.740 --> 00:02:11.240
狀態解碼、來源、時脈與重置，以及最終接受端保持可信。

30
00:02:12.120 --> 00:02:19.420
Mask＝111100，也就是十六進位 3c，把 001111 改成 110011。

31
00:02:19.420 --> 00:02:23.900
解碼器看到合法 RELEASE，bad 維持 false，請求便 commit。

32
00:02:23.900 --> 00:02:28.640
它影響四位，超出三位主張，但落在擴大後的四位預算內。

33
00:02:28.640 --> 00:02:31.700
Bind 政策另要求獨立授權。

34
00:02:31.700 --> 00:02:35.760
因目前映像未獲許可，它能擋住合法態反例。

35
00:02:35.760 --> 00:02:38.620
模型從可信 harness 提供這個值。

36
00:02:38.620 --> 00:02:43.220
練習指出欠缺條件；真正設計仍須建立來源與完整性。

37
00:02:43.520 --> 00:02:47.460
選 CHECK、mask＝1 並關閉 binding。

38
00:02:47.460 --> 00:02:50.100
結果非法，commit 為 false。

39
00:02:50.100 --> 00:02:52.940
再試兩位或三位 mask。

40
00:02:52.940 --> 00:02:57.240
接著輸入 60，即 0x3c 的十進位。

41
00:02:57.240 --> 00:03:00.380
顯示碼變成 RELEASE，請求也被接受。

42
00:03:00.380 --> 00:03:02.160
把軌跡與狀態表一起保存。

43
00:03:03.080 --> 00:03:07.320
已執行枚舉遍歷 CHECK 的每個 mask，並查所有配對距離。

44
00:03:07.320 --> 00:03:11.040
六十四種 CHECK mask 中，只有一種到未授權 RELEASE。

45
00:03:11.040 --> 00:03:14.520
其他四位 mask 可能到合法 WAIT 或 ERROR。

46
00:03:14.520 --> 00:03:17.640
因此，沒有 commit 的軌跡不能一律標為已偵測。

47
00:03:18.400 --> 00:03:24.160
解碼正向控制設 RELEASE、授權 true、binding true、mask＝0。

48
00:03:24.160 --> 00:03:28.180
第八課另跑正常 WAIT→CHECK→RELEASE 交易。

49
00:03:28.180 --> 00:03:32.900
單獨解碼控制不能證明完整控制器可達放行，也沒有證明轉移條件可信。

50
00:03:33.240 --> 00:03:35.700
RTL／SVA 尚未編譯。

51
00:03:35.700 --> 00:03:41.200
ERROR 可達性、輸出解碼故障、scan 存取與綜合重編碼，都要另查。

52
00:03:41.200 --> 00:03:47.760
請回第四課，用獨立 grant 目標檢查解碼後輸出受擾；本課儲存枚舉沒有涵蓋它。

53
00:03:47.760 --> 00:03:52.060
最小距離四，也沒有涵蓋錯誤 CHECK 條件選到合法下一態。

54
00:03:52.060 --> 00:03:53.720
下一課會處理這個問題。

55
00:03:54.160 --> 00:04:02.260
Edge 1 前一次六位元狀態 XOR，從 CHECK 枚舉六十四種 mask；碼距主張限定低於四位。

56
00:04:02.260 --> 00:04:04.620
其他邏輯與 reference 可信。

57
00:04:05.160 --> 00:04:11.540
Node 已查全部配對距離、六十四種 CHECK mask 及授權 RELEASE 解碼。

58
00:04:11.540 --> 00:04:13.640
正常流程另在第八課測。

59
00:04:14.160 --> 00:04:19.800
解碼枚舉不能支持轉移、netlist、scan、實體或形式驗證結果。