Accelerator.SM86.HalfFormat

1module Accelerator.SM86.HalfFormat
2
3import Accelerator.SM86.Instruction
4import Accelerator.SM86.Program
5import Std.Natural
6
7-- A program moved to another 16-bit format: every instruction that makes,
8-- reads or multiplies halves -- F2FP (the pack), the widening (HADD2.F32 /
9-- PRMT) and HMMA -- replaced by its twin in the format, every other
10-- instruction kept.  Halves are made and read only by those three (the
11-- model has no other half arithmetic), and moved as bits by the rest (loads,
12-- stores, LDSM, shuffles), so a program whose halves are all its own -- none
13-- read from or written for another program in the other format -- computes
14-- the same thing with its halves in the new format.  A system moves its
15-- images together (Coppelius.Build.DeviceImages).
16def sm86BodyInBFloat16 =
17  (lambda unrestricted body : (family SM86InstructionBody) .
18    (eliminate SM86InstructionBody
19      (lambda unrestricted current : (family SM86InstructionBody) . (family SM86InstructionBody))
20      body
21      (branch SM86MoveConstant destination bank offset control . (constructor SM86InstructionBody SM86MoveConstant destination bank offset control))
22      (branch SM86SpecialToRegister destination source control . (constructor SM86InstructionBody SM86SpecialToRegister destination source control))
23      (branch SM86MoveImmediate destination immediate control . (constructor SM86InstructionBody SM86MoveImmediate destination immediate control))
24      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddConstant destination left bank offset addend control))
25      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate destination left immediate addend control))
26      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant destination left right bank offset control))
27      (branch SM86IntegerAddThreeImmediate destination left immediate control . (constructor SM86InstructionBody SM86IntegerAddThreeImmediate destination left immediate control))
28      (branch SM86IntegerAddThreeRegister destination left right control . (constructor SM86InstructionBody SM86IntegerAddThreeRegister destination left right control))
29      (branch SM86ShiftRightImmediate destination source amount control . (constructor SM86InstructionBody SM86ShiftRightImmediate destination source amount control))
30      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (constructor SM86InstructionBody SM86LogicThreeInputTruthTable destination left right truthTable control))
31      (branch SM86IntegerToFloat destination source control . (constructor SM86InstructionBody SM86IntegerToFloat destination source control))
32      (branch SM86FloatAdd destination left right control . (constructor SM86InstructionBody SM86FloatAdd destination left right control))
33      (branch SM86FloatMultiply destination left right control . (constructor SM86InstructionBody SM86FloatMultiply destination left right control))
34      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd destination left right addend control))
35      (branch SM86MultiFunctionUnitApproximation destination source operation control . (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation destination source operation control))
36      (branch SM86FloatMinimumOrMaximum destination left right mode control . (constructor SM86InstructionBody SM86FloatMinimumOrMaximum destination left right mode control))
37      (branch SM86FloatNegate destination source control . (constructor SM86InstructionBody SM86FloatNegate destination source control))
38      (branch SM86FloatPairToPackedHalfPair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedBFloat16Pair destination high low control))
39      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedBFloat16Pair destination high low control))
40      (branch SM86HalfToFloat destination source selector control . (constructor SM86InstructionBody SM86BFloat16ToFloat destination source selector control))
41      (branch SM86BFloat16ToFloat destination source selector control . (constructor SM86InstructionBody SM86BFloat16ToFloat destination source selector control))
42      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control))
43      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control))
44      (branch SM86LoadGlobal destination address offset control . (constructor SM86InstructionBody SM86LoadGlobal destination address offset control))
45      (branch SM86LoadGlobalWide destination address offset control . (constructor SM86InstructionBody SM86LoadGlobalWide destination address offset control))
46      (branch SM86WarpShuffle destination source lane segment mode control . (constructor SM86InstructionBody SM86WarpShuffle destination source lane segment mode control))
47      (branch SM86LoadShared destination address offset control . (constructor SM86InstructionBody SM86LoadShared destination address offset control))
48      (branch SM86LoadSharedMatrix destination address offset count transpose control . (constructor SM86InstructionBody SM86LoadSharedMatrix destination address offset count transpose control))
49      (branch SM86StoreShared address value offset control . (constructor SM86InstructionBody SM86StoreShared address value offset control))
50      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (constructor SM86InstructionBody SM86LoadGlobalToShared address offset source sourceOffset control))
51      (branch SM86CommitAsyncGroup control . (constructor SM86InstructionBody SM86CommitAsyncGroup control))
52      (branch SM86WaitAsyncGroups count control . (constructor SM86InstructionBody SM86WaitAsyncGroups count control))
53      (branch SM86BarrierSynchronize control . (constructor SM86InstructionBody SM86BarrierSynchronize control))
54      (branch SM86StoreGlobal address value offset control . (constructor SM86InstructionBody SM86StoreGlobal address value offset control))
55      (branch SM86StoreGlobalWide address value offset control . (constructor SM86InstructionBody SM86StoreGlobalWide address value offset control))
56      (branch SM86StoreGlobal64 address value offset control . (constructor SM86InstructionBody SM86StoreGlobal64 address value offset control))
57      (branch SM86ReduceGlobalAddFloat32 address value offset control . (constructor SM86InstructionBody SM86ReduceGlobalAddFloat32 address value offset control))
58      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate predicate source immediate control))
59      (branch SM86Branch offset descriptor control . (constructor SM86InstructionBody SM86Branch offset descriptor control))
60      (branch SM86Exit control . (constructor SM86InstructionBody SM86Exit control))))
61
62def sm86BodyWithHalfFormat =
63  (lambda unrestricted format : (family SM86HalfFormat) .
64    (lambda unrestricted body : (family SM86InstructionBody) .
65      (eliminate SM86HalfFormat (lambda unrestricted current : (family SM86HalfFormat) . (family SM86InstructionBody)) format
66        (branch SM86Binary16 . body)
67        (branch SM86BFloat16 . (sm86BodyInBFloat16 body)))))
68
69def sm86InstructionWithHalfFormat =
70  (lambda unrestricted format : (family SM86HalfFormat) .
71    (lambda unrestricted instruction : (family SM86Instruction) .
72      (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . (family SM86Instruction)) instruction
73        (branch SM86InstructionValue guard body .
74          (constructor SM86Instruction SM86InstructionValue guard (sm86BodyWithHalfFormat format body))))))
75
76def sm86ProgramWithHalfFormat =
77  (lambda unrestricted format : (family SM86HalfFormat) .
78    (lambda unrestricted program : (family SM86Program) .
79      (eliminate SM86Program (lambda unrestricted current : (family SM86Program) . (family SM86Program)) program
80        (branch SM86ProgramEnd . (constructor SM86Program SM86ProgramEnd))
81        (branch SM86ProgramNext instruction rest induction .
82          (constructor SM86Program SM86ProgramNext (sm86InstructionWithHalfFormat format instruction) induction)))))
83
84-- 1 for an instruction that makes, reads or multiplies binary16 halves
85def sm86BodyIsBinary16 =
86  (lambda unrestricted body : (family SM86InstructionBody) .
87    (eliminate SM86InstructionBody
88      (lambda unrestricted current : (family SM86InstructionBody) . Nat)
89      body
90      (branch SM86MoveConstant destination bank offset control . 0)
91      (branch SM86SpecialToRegister destination source control . 0)
92      (branch SM86MoveImmediate destination immediate control . 0)
93      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . 0)
94      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . 0)
95      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . 0)
96      (branch SM86IntegerAddThreeImmediate destination left immediate control . 0)
97      (branch SM86IntegerAddThreeRegister destination left right control . 0)
98      (branch SM86ShiftRightImmediate destination source amount control . 0)
99      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . 0)
100      (branch SM86IntegerToFloat destination source control . 0)
101      (branch SM86FloatAdd destination left right control . 0)
102      (branch SM86FloatMultiply destination left right control . 0)
103      (branch SM86FloatFusedMultiplyAdd destination left right addend control . 0)
104      (branch SM86MultiFunctionUnitApproximation destination source operation control . 0)
105      (branch SM86FloatMinimumOrMaximum destination left right mode control . 0)
106      (branch SM86FloatNegate destination source control . 0)
107      (branch SM86FloatPairToPackedHalfPair destination high low control . 1)
108      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . 0)
109      (branch SM86HalfToFloat destination source selector control . 1)
110      (branch SM86BFloat16ToFloat destination source selector control . 0)
111      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . 1)
112      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . 0)
113      (branch SM86LoadGlobal destination address offset control . 0)
114      (branch SM86LoadGlobalWide destination address offset control . 0)
115      (branch SM86WarpShuffle destination source lane segment mode control . 0)
116      (branch SM86LoadShared destination address offset control . 0)
117      (branch SM86LoadSharedMatrix destination address offset count transpose control . 0)
118      (branch SM86StoreShared address value offset control . 0)
119      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 0)
120      (branch SM86CommitAsyncGroup control . 0)
121      (branch SM86WaitAsyncGroups count control . 0)
122      (branch SM86BarrierSynchronize control . 0)
123      (branch SM86StoreGlobal address value offset control . 0)
124      (branch SM86StoreGlobalWide address value offset control . 0)
125      (branch SM86StoreGlobal64 address value offset control . 0)
126      (branch SM86ReduceGlobalAddFloat32 address value offset control . 0)
127      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . 0)
128      (branch SM86Branch offset descriptor control . 0)
129      (branch SM86Exit control . 0)))
130
131-- 1 for one that makes, reads or multiplies bfloat16 halves
132def sm86BodyIsBFloat16 =
133  (lambda unrestricted body : (family SM86InstructionBody) .
134    (eliminate SM86InstructionBody
135      (lambda unrestricted current : (family SM86InstructionBody) . Nat)
136      body
137      (branch SM86MoveConstant destination bank offset control . 0)
138      (branch SM86SpecialToRegister destination source control . 0)
139      (branch SM86MoveImmediate destination immediate control . 0)
140      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . 0)
141      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . 0)
142      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . 0)
143      (branch SM86IntegerAddThreeImmediate destination left immediate control . 0)
144      (branch SM86IntegerAddThreeRegister destination left right control . 0)
145      (branch SM86ShiftRightImmediate destination source amount control . 0)
146      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . 0)
147      (branch SM86IntegerToFloat destination source control . 0)
148      (branch SM86FloatAdd destination left right control . 0)
149      (branch SM86FloatMultiply destination left right control . 0)
150      (branch SM86FloatFusedMultiplyAdd destination left right addend control . 0)
151      (branch SM86MultiFunctionUnitApproximation destination source operation control . 0)
152      (branch SM86FloatMinimumOrMaximum destination left right mode control . 0)
153      (branch SM86FloatNegate destination source control . 0)
154      (branch SM86FloatPairToPackedHalfPair destination high low control . 0)
155      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . 1)
156      (branch SM86HalfToFloat destination source selector control . 0)
157      (branch SM86BFloat16ToFloat destination source selector control . 1)
158      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . 0)
159      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . 1)
160      (branch SM86LoadGlobal destination address offset control . 0)
161      (branch SM86LoadGlobalWide destination address offset control . 0)
162      (branch SM86WarpShuffle destination source lane segment mode control . 0)
163      (branch SM86LoadShared destination address offset control . 0)
164      (branch SM86LoadSharedMatrix destination address offset count transpose control . 0)
165      (branch SM86StoreShared address value offset control . 0)
166      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 0)
167      (branch SM86CommitAsyncGroup control . 0)
168      (branch SM86WaitAsyncGroups count control . 0)
169      (branch SM86BarrierSynchronize control . 0)
170      (branch SM86StoreGlobal address value offset control . 0)
171      (branch SM86StoreGlobalWide address value offset control . 0)
172      (branch SM86StoreGlobal64 address value offset control . 0)
173      (branch SM86ReduceGlobalAddFloat32 address value offset control . 0)
174      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . 0)
175      (branch SM86Branch offset descriptor control . 0)
176      (branch SM86Exit control . 0)))
177
178-- how many of a program's instructions are of a format's
179def sm86ProgramCountOf =
180  (lambda unrestricted of : (pi unrestricted body : (family SM86InstructionBody) . Nat) .
181    (lambda unrestricted program : (family SM86Program) .
182      (eliminate SM86Program (lambda unrestricted current : (family SM86Program) . Nat) program
183        (branch SM86ProgramEnd . 0)
184        (branch SM86ProgramNext instruction rest induction .
185          (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . Nat) instruction
186            (branch SM86InstructionValue guard body . (naturalAdd (of body) induction)))))))
187
188def sm86ProgramBinary16Count = (sm86ProgramCountOf sm86BodyIsBinary16)
189def sm86ProgramBFloat16Count = (sm86ProgramCountOf sm86BodyIsBFloat16)