WEBVTT

1
00:00:00.000 --> 00:00:05.760
A controller must observe four completed
transfers before releasing a result.

2
00:00:05.760 --> 00:00:09.577
Its up counter says four and its down counter
says zero.

3
00:00:09.577 --> 00:00:11.237
Their sum is still four.

4
00:00:11.237 --> 00:00:14.141
Only three transfers actually occurred.

5
00:00:14.141 --> 00:00:18.462
A shared enable has advanced both counters
together.

6
00:00:18.750 --> 00:00:23.024
A cross-counter stores progress in opposite
directions.

7
00:00:23.024 --> 00:00:26.516
Our three-bit registers start at up=0 and down=4.

8
00:00:26.516 --> 00:00:30.341
On each counted step, up increases and down
decreases.

9
00:00:30.341 --> 00:00:33.584
The non-modular sum up+down must remain four.

10
00:00:33.584 --> 00:00:38.135
We use a widened sum to avoid hiding overflow
through truncation.

11
00:00:38.417 --> 00:00:41.876
An isolated change to up usually breaks the sum.

12
00:00:41.876 --> 00:00:46.603
A detector can block completion immediately and
remember the error.

13
00:00:46.603 --> 00:00:52.388
However, a relation that remains true cannot
reveal how the pair reached its values.

14
00:00:52.388 --> 00:00:58.185
A coordinated wrong update is invisible to this
particular check.

15
00:00:58.458 --> 00:01:01.644
OpenTitan publishes a cross-counter primitive.

16
00:01:01.644 --> 00:01:07.047
SYNFI discusses shared increment and clear
signals as boundaries of counter protection.

17
00:01:07.047 --> 00:01:12.450
Our small schedule below illustrates that
mechanism; we did not run SYNFI or reproduce its

18
00:01:12.450 --> 00:01:14.151
netlist experiments.

19
00:01:14.417 --> 00:01:21.359
A genuine step means a transfer was accepted:
valid and ready were both true at the agreed

20
00:01:21.359 --> 00:01:22.361
rising edge.

21
00:01:22.361 --> 00:01:26.005
Waiting through a stall does not complete work.

22
00:01:26.005 --> 00:01:32.609
The independent reference increments only on
those genuine handshakes and remains outside the

23
00:01:32.609 --> 00:01:33.801
fault scope.

24
00:01:34.083 --> 00:01:40.401
In the negative schedule, genuine handshakes
occur at edges 1, 3 and 4.

25
00:01:40.401 --> 00:01:41.645
Edge 2 is idle.

26
00:01:41.645 --> 00:01:48.696
One false common enable after edge 2 advances up
and down despite that idle cycle.

27
00:01:48.696 --> 00:01:54.853
After edge 4, the DUT pair is 4/0 while reference
progress is three.

28
00:01:55.125 --> 00:01:57.667
The result request arrives at edge 5.

29
00:01:57.667 --> 00:01:59.782
Sum-only completion permits it.

30
00:01:59.782 --> 00:02:05.977
The authorization reference requires four genuine
transfers and therefore marks that commit as

31
00:02:05.977 --> 00:02:06.959
unauthorized.

32
00:02:06.959 --> 00:02:14.048
The checker correctly reports no sum error; it is
blind to missing work, not broken arithmetic.

33
00:02:14.333 --> 00:02:20.480
The main witness has one event at the common
enable, no register XOR, and a fixed edge-0-to-5

34
00:02:20.480 --> 00:02:21.021
window.

35
00:02:21.021 --> 00:02:24.187
Both counters stop at their intended endpoints.

36
00:02:24.187 --> 00:02:30.442
Clock/reset, workload, handshake observer,
reference, sum checker and final consumer remain

37
00:02:30.442 --> 00:02:31.410
trusted.

38
00:02:31.667 --> 00:02:34.795
The lab also offers an up-register XOR.

39
00:02:34.795 --> 00:02:37.545
Its mask is restricted to three bits.

40
00:02:37.545 --> 00:02:43.757
Another option substitutes the pair so down=4-up,
only if the proposed up lies in 0.

41
00:02:43.757 --> 00:02:43.845
.

42
00:02:43.845 --> 00:02:44.023
4.

43
00:02:44.023 --> 00:02:47.395
Out-of-range pair proposals have no effect.

44
00:02:47.395 --> 00:02:52.321
This is a constrained correlated substitution,
not two independent bit flips.

45
00:02:52.321 --> 00:02:56.590
Record effective injection separately from a
submitted parameter.

46
00:02:56.875 --> 00:03:02.274
The progress variant additionally compares up
with an independent progress input and remembers

47
00:03:02.274 --> 00:03:03.162
discrepancies.

48
00:03:03.162 --> 00:03:08.171
The executable model uses trusted reference
progress to demonstrate the needed obligation.

49
00:03:08.171 --> 00:03:13.881
A product needs a separately justified
work-completion observation; attaching a

50
00:03:13.881 --> 00:03:17.644
testbench oracle to grant is not a hardware
solution.

51
00:03:17.917 --> 00:03:21.599
Select enable, fault edge 2 and sum policy.

52
00:03:21.599 --> 00:03:23.533
Step through the table.

53
00:03:23.533 --> 00:03:29.820
At edge 3, the pair already reflects the false
step while ref has not advanced.

54
00:03:29.820 --> 00:03:33.688
At edge 5, commit is true and reference is false.

55
00:03:33.688 --> 00:03:40.071
Switching to progress policy blocks this witness
without changing its workload.

56
00:03:40.333 --> 00:03:46.407
The 96 up/pair parameter runs never commit under
progress policy on the three-handshake schedule.

57
00:03:46.407 --> 00:03:50.742
That alone does not prove fault detection:
reference never reaches four.

58
00:03:50.742 --> 00:03:56.921
Separate assertions check the common-enable
progress mismatch, an up XOR breaking the sum,

59
00:03:56.921 --> 00:04:01.145
and a coordinated pair substitution bypassing
sum-only checking.

60
00:04:01.145 --> 00:04:05.125
The fault-free four-handshake control accepts at
edge 5.

61
00:04:05.375 --> 00:04:07.630
Try an injection after edge 5.

62
00:04:07.630 --> 00:04:10.343
No later request exists in this window.

63
00:04:10.343 --> 00:04:15.523
A missing unauthorized commit now proves only
that the observation ended.

64
00:04:15.523 --> 00:04:20.785
Move the request later before claiming the
corrupted progress is harmless.

65
00:04:20.785 --> 00:04:25.683
Also record whether the injection actually
changes the pair.

66
00:04:25.958 --> 00:04:28.038
The RTL sketch is uncompiled.

67
00:04:28.038 --> 00:04:33.980
A production counter needs legal set/clear
behavior, arithmetic widths, saturation or wrap

68
00:04:33.980 --> 00:04:36.386
rules and a bound on outstanding work.

69
00:04:36.386 --> 00:04:40.447
Test the common enable before relying on
duplicated registers.

70
00:04:40.447 --> 00:04:45.804
Lesson 7 asks which state substitutions an
encoding can recognize.

71
00:04:46.083 --> 00:04:52.267
One common-enable event after an idle edge, or
separately bounded register effects, in edges 0.

72
00:04:52.267 --> 00:04:52.341
.

73
00:04:52.341 --> 00:04:52.489
5.

74
00:04:52.489 --> 00:04:56.237
Three genuine handshakes precede the result
request.

75
00:04:56.500 --> 00:05:01.295
Node reproduced early completion and checked 96
storage/substitution parameters; separate

76
00:05:01.295 --> 00:05:04.517
four-step positive and three-step negative
controls ran.

77
00:05:04.792 --> 00:05:07.985
The pair option is a constrained abstract
substitution.

78
00:05:07.985 --> 00:05:10.105
Out-of-range proposals have no effect.

79
00:05:10.105 --> 00:05:14.946
RTL, overflow implementation and physical
shared-enable behavior are unverified.