Accelerator.SM86.Control

1module Accelerator.SM86.Control
2
3import Accelerator.SM86.Types
4
5family SM86Barrier : Type 0
6constructor SM86Barrier0
7constructor SM86Barrier1
8constructor SM86Barrier2
9constructor SM86Barrier3
10constructor SM86Barrier4
11constructor SM86Barrier5
12constructor SM86Barrier6
13constructor SM86BarrierNone
14
15end-family
16
17family SM86WaitBarrier : Type 0
18constructor SM86WaitBarrier0
19constructor SM86WaitBarrier1
20constructor SM86WaitBarrier2
21constructor SM86WaitBarrier3
22constructor SM86WaitBarrier4
23constructor SM86WaitBarrier5
24
25end-family
26
27family SM86YieldMode : Type 0
28constructor SM86Continue
29constructor SM86Yield
30
31end-family
32
33family SM86Control : Type 0
34constructor SM86ControlValue
35field unrestricted sm86ControlStall : Byte
36field unrestricted sm86ControlYield : (family SM86YieldMode)
37field unrestricted sm86ControlWriteBarrier : (family SM86Barrier)
38field unrestricted sm86ControlReadBarrier : (family SM86Barrier)
39field unrestricted sm86ControlWaitMask : Byte
40field unrestricted sm86ControlReuseMask : Byte
41
42end-family
43
44family SM86ControlResult : Type 0
45constructor SM86ControlValidated
46field unrestricted validatedSM86Control : (family SM86Control)
47constructor SM86ControlFailed
48field unrestricted sm86ControlFailureCode : Nat
49
50end-family
51
52def sm86ControlStallCode =
53  (succ zero)
54
55def sm86ControlWaitMaskCode =
56  (succ sm86ControlStallCode)
57
58def sm86ControlReuseMaskCode =
59  (succ sm86ControlWaitMaskCode)
60
61def sm86ControlFailure =
62  (lambda unrestricted code : Nat . (constructor SM86ControlResult SM86ControlFailed code))
63
64def sm86ControlCheck =
65  (lambda unrestricted condition : Nat .
66    (lambda unrestricted code : Nat .
67      (lambda unrestricted success : (pi unrestricted witness : Nat . (family SM86ControlResult)) .
68        (nat-eliminate
69          (lambda unrestricted valid : Nat . (family SM86ControlResult))
70          (sm86ControlFailure code)
71          (lambda unrestricted predecessor : Nat .
72            (lambda unrestricted induction : (family SM86ControlResult) . (success zero)))
73          condition))))
74
75def makeSM86Control =
76  (lambda unrestricted stall : Byte .
77    (lambda unrestricted yieldMode : (family SM86YieldMode) .
78      (lambda unrestricted writeBarrier : (family SM86Barrier) .
79        (lambda unrestricted readBarrier : (family SM86Barrier) .
80          (lambda unrestricted waitMask : Byte .
81            (lambda unrestricted reuseMask : Byte .
82              (sm86ControlCheck
83                (nat-less-than (byte-to-nat stall) (byte-to-nat (byte 16)))
84                sm86ControlStallCode
85                (lambda unrestricted stallWitness : Nat .
86                  (sm86ControlCheck
87                    (nat-less-than (byte-to-nat waitMask) (byte-to-nat (byte 64)))
88                    sm86ControlWaitMaskCode
89                    (lambda unrestricted waitWitness : Nat .
90                      (sm86ControlCheck
91                        (nat-less-than (byte-to-nat reuseMask) (byte-to-nat (byte 16)))
92                        sm86ControlReuseMaskCode
93                        (lambda unrestricted reuseWitness : Nat .
94                          (constructor
95                            SM86ControlResult
96                            SM86ControlValidated
97                            (constructor
98                              SM86Control
99                              SM86ControlValue
100                              stall
101                              yieldMode
102                              writeBarrier
103                              readBarrier
104                              waitMask
105                              reuseMask))))))))))))))
106
107def sm86SafeControl : (family SM86Control) =
108  (constructor
109    SM86Control
110    SM86ControlValue
111    (byte 7)
112    (constructor SM86YieldMode SM86Continue)
113    (constructor SM86Barrier SM86BarrierNone)
114    (constructor SM86Barrier SM86BarrierNone)
115    (byte 0)
116    (byte 0))
117
118def sm86SetBarrierControl =
119  (lambda unrestricted barrier : (family SM86Barrier) .
120    (constructor
121      SM86Control
122      SM86ControlValue
123      (byte 1)
124      (constructor SM86YieldMode SM86Continue)
125      barrier
126      (constructor SM86Barrier SM86BarrierNone)
127      (byte 0)
128      (byte 0)))
129
130def sm86WaitBarrierMask =
131  (lambda unrestricted barrier : (family SM86WaitBarrier) .
132    (eliminate
133      SM86WaitBarrier
134      (lambda unrestricted value : (family SM86WaitBarrier) . Byte)
135      barrier
136      (branch SM86WaitBarrier0 . (byte 1))
137      (branch SM86WaitBarrier1 . (byte 2))
138      (branch SM86WaitBarrier2 . (byte 4))
139      (branch SM86WaitBarrier3 . (byte 8))
140      (branch SM86WaitBarrier4 . (byte 16))
141      (branch SM86WaitBarrier5 . (byte 32))))
142
143def sm86WaitBarrierControl =
144  (lambda unrestricted barrier : (family SM86WaitBarrier) .
145    (constructor
146      SM86Control
147      SM86ControlValue
148      (byte 7)
149      (constructor SM86YieldMode SM86Continue)
150      (constructor SM86Barrier SM86BarrierNone)
151      (constructor SM86Barrier SM86BarrierNone)
152      (sm86WaitBarrierMask barrier)
153      (byte 0)))
154
155def sm86BranchControl : (family SM86Control) =
156  (constructor
157    SM86Control
158    SM86ControlValue
159    (byte 5)
160    (constructor SM86YieldMode SM86Yield)
161    (constructor SM86Barrier SM86BarrierNone)
162    (constructor SM86Barrier SM86BarrierNone)
163    (byte 0)
164    (byte 0))