Accelerator.SM86.Instruction

1module Accelerator.SM86.Instruction
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.NumericSemantics
6import Accelerator.SM86.Types
7
8family SM86SpecialRegister : Type 0
9-- SASS SR_CTAID.X: the cooperative thread array (block) index on x.
10constructor SM86CooperativeThreadArrayIdX
11-- SASS SR_CTAID.Y: the cooperative thread array (block) index on y.
12constructor SM86CooperativeThreadArrayIdY
13-- SASS SR_CTAID.Z: the cooperative thread array (block) index on z.
14constructor SM86CooperativeThreadArrayIdZ
15-- SASS SR_TID.X: the thread index on x within its cooperative thread array.
16constructor SM86ThreadIdX
17-- SASS SR_CLOCKLO: the low word of the SM's cycle counter.
18constructor SM86ClockLow
19-- SASS SR_GLOBALTIMERLO: the low word of the device's global timer, in
20-- nanoseconds -- the clock the semaphore releases stamp.
21constructor SM86GlobalTimerLow
22-- SASS SR_GLOBALTIMERHI: its high word.
23constructor SM86GlobalTimerHigh
24
25end-family
26
27family SM86InstructionGuard : Type 0
28-- no guard: the instruction always executes.
29constructor SM86InstructionAlways
30-- SASS @P: the instruction executes only in threads where the predicate is true.
31constructor SM86InstructionWhen
32field unrestricted sm86InstructionGuardPredicate : (family SM86Predicate)
33-- SASS @!P: the instruction executes only in threads where the predicate is false.
34constructor SM86InstructionWhenNot
35field unrestricted sm86InstructionGuardNotPredicate : (family SM86Predicate)
36
37end-family
38
39family SM86ShuffleMode : Type 0
40-- SASS SHFL.IDX: read the lane named by the lane operand.
41constructor SM86ShuffleIndex
42-- SASS SHFL.UP: read the lane that is lane places below this one.
43constructor SM86ShuffleUp
44-- SASS SHFL.DOWN: read the lane that is lane places above this one.
45constructor SM86ShuffleDown
46-- SASS SHFL.BFLY: read the lane whose index is this lane's index xor the lane operand.
47constructor SM86ShuffleButterfly
48
49end-family
50
51family SM86HalfSelector : Type 0
52-- the low binary16 half (H0) of a 32-bit register.
53constructor SM86LowHalf
54-- the high binary16 half (H1) of a 32-bit register.
55constructor SM86HighHalf
56
57end-family
58
59-- the 16-bit floating-point format a program's halves are in: binary16
60-- (5 exponent bits, 10 fraction bits) or bfloat16 (8 and 7: binary32's
61-- range).  Accelerator.SM86.HalfFormat moves a program between them.
62family SM86HalfFormat : Type 0
63constructor SM86Binary16
64constructor SM86BFloat16
65
66end-family
67
68family SM86SharedMatrixCount : Type 0
69-- SASS LDSM.x1: one 8x8 matrix.
70constructor SM86SharedMatrix1
71-- SASS LDSM.x2: two 8x8 matrices.
72constructor SM86SharedMatrix2
73-- SASS LDSM.x4: four 8x8 matrices.
74constructor SM86SharedMatrix4
75
76end-family
77
78family SM86SharedMatrixTranspose : Type 0
79-- SASS LDSM (no .T): rows as stored.
80constructor SM86SharedMatrixNotTransposed
81-- SASS LDSM.T: each matrix transposed while loading.
82constructor SM86SharedMatrixTransposed
83
84end-family
85
86family SM86InstructionBody : Type 0
87-- SASS MOV (constant bank): destination = c[bank][offset], a 32-bit word from a constant bank.
88constructor SM86MoveConstant
89field unrestricted sm86MoveConstantDestination : (family SM86Register)
90field unrestricted sm86MoveConstantBank : Byte
91field unrestricted sm86MoveConstantOffset : (family SM86Unsigned32)
92field unrestricted sm86MoveConstantControl : (family SM86Control)
93-- SASS S2R: destination = a special register (thread or cooperative-thread-array index).
94constructor SM86SpecialToRegister
95field unrestricted sm86SpecialDestination : (family SM86Register)
96field unrestricted sm86SpecialSource : (family SM86SpecialRegister)
97field unrestricted sm86SpecialControl : (family SM86Control)
98-- SASS MOV (immediate): destination = a 32-bit immediate.
99constructor SM86MoveImmediate
100field unrestricted sm86MoveImmediateDestination : (family SM86Register)
101field unrestricted sm86MoveImmediateValue : (family SM86Unsigned32)
102field unrestricted sm86MoveImmediateControl : (family SM86Control)
103-- SASS IMAD (constant bank): destination = left * c[bank][offset] + addend, 32-bit integer.
104constructor SM86IntegerMultiplyAddConstant
105field unrestricted sm86IMADConstantDestination : (family SM86Register)
106field unrestricted sm86IMADConstantLeft : (family SM86Register)
107field unrestricted sm86IMADConstantBank : Byte
108field unrestricted sm86IMADConstantOffset : (family SM86Unsigned32)
109field unrestricted sm86IMADConstantAddend : (family SM86Register)
110field unrestricted sm86IMADConstantControl : (family SM86Control)
111-- SASS IMAD (immediate): destination = left * immediate + addend, 32-bit integer.
112constructor SM86IntegerMultiplyAddImmediate
113field unrestricted sm86IMADImmediateDestination : (family SM86Register)
114field unrestricted sm86IMADImmediateLeft : (family SM86Register)
115field unrestricted sm86IMADImmediateValue : (family SM86Unsigned32)
116field unrestricted sm86IMADImmediateAddend : (family SM86Register)
117field unrestricted sm86IMADImmediateControl : (family SM86Control)
118-- SASS IMAD.WIDE.U32: destination pair = left * right + c[bank][offset], a 64-bit product plus a 64-bit constant.
119constructor SM86IntegerMultiplyAddWideConstant
120field unrestricted sm86IMADWideDestination : (family SM86Register)
121field unrestricted sm86IMADWideLeft : (family SM86Register)
122field unrestricted sm86IMADWideRight : (family SM86Register)
123field unrestricted sm86IMADWideBank : Byte
124field unrestricted sm86IMADWideOffset : (family SM86Unsigned32)
125field unrestricted sm86IMADWideControl : (family SM86Control)
126-- SASS IADD3 (immediate): destination = left + immediate, the three-input adder with one input zero.
127constructor SM86IntegerAddThreeImmediate
128field unrestricted sm86IADD3ImmediateDestination : (family SM86Register)
129field unrestricted sm86IADD3ImmediateLeft : (family SM86Register)
130field unrestricted sm86IADD3ImmediateValue : (family SM86Unsigned32)
131field unrestricted sm86IADD3ImmediateControl : (family SM86Control)
132-- SASS IADD3 (register): destination = left + right, the three-input adder with one input zero.
133constructor SM86IntegerAddThreeRegister
134field unrestricted sm86IADD3RegisterDestination : (family SM86Register)
135field unrestricted sm86IADD3RegisterLeft : (family SM86Register)
136field unrestricted sm86IADD3RegisterRight : (family SM86Register)
137field unrestricted sm86IADD3RegisterControl : (family SM86Control)
138-- SASS SHF.R.U32.HI: destination = source logically shifted right by an immediate amount.
139constructor SM86ShiftRightImmediate
140field unrestricted sm86ShiftRightDestination : (family SM86Register)
141field unrestricted sm86ShiftRightSource : (family SM86Register)
142field unrestricted sm86ShiftRightAmount : Byte
143field unrestricted sm86ShiftRightControl : (family SM86Control)
144-- SASS LOP3.LUT: destination = truthTable(left, right, zero), any bitwise function of the inputs given as an 8-bit lookup table.
145constructor SM86LogicThreeInputTruthTable
146field unrestricted sm86Logic3Destination : (family SM86Register)
147field unrestricted sm86Logic3Left : (family SM86Register)
148field unrestricted sm86Logic3Right : (family SM86Register)
149field unrestricted sm86Logic3TruthTable : Byte
150field unrestricted sm86Logic3Control : (family SM86Control)
151-- SASS I2FP.F32.S32: destination = the signed 32-bit integer source converted to binary32.
152constructor SM86IntegerToFloat
153field unrestricted sm86IntegerToFloatDestination : (family SM86Register)
154field unrestricted sm86IntegerToFloatSource : (family SM86Register)
155field unrestricted sm86IntegerToFloatControl : (family SM86Control)
156-- SASS FADD: destination = left + right, binary32, round to nearest even.
157constructor SM86FloatAdd
158field unrestricted sm86FloatAddDestination : (family SM86Register)
159field unrestricted sm86FloatAddLeft : (family SM86Register)
160field unrestricted sm86FloatAddRight : (family SM86Register)
161field unrestricted sm86FloatAddControl : (family SM86Control)
162-- SASS FMUL: destination = left * right, binary32, round to nearest even.
163constructor SM86FloatMultiply
164field unrestricted sm86FloatMultiplyDestination : (family SM86Register)
165field unrestricted sm86FloatMultiplyLeft : (family SM86Register)
166field unrestricted sm86FloatMultiplyRight : (family SM86Register)
167field unrestricted sm86FloatMultiplyControl : (family SM86Control)
168-- SASS FFMA: destination = left * right + addend, binary32 with a single rounding.
169constructor SM86FloatFusedMultiplyAdd
170field unrestricted sm86FloatFMADestination : (family SM86Register)
171field unrestricted sm86FloatFMALeft : (family SM86Register)
172field unrestricted sm86FloatFMARight : (family SM86Register)
173field unrestricted sm86FloatFMAAddend : (family SM86Register)
174field unrestricted sm86FloatFMAControl : (family SM86Control)
175-- SASS MUFU: destination = an approximate transcendental of the source (cosine, sine, exp2, log2, reciprocal, reciprocal square root, square root, tanh) from the multi-function unit.
176constructor SM86MultiFunctionUnitApproximation
177field unrestricted sm86MultiFunctionDestination : (family SM86Register)
178field unrestricted sm86MultiFunctionSource : (family SM86Register)
179field unrestricted sm86MultiFunctionOperation : (family SM86MultiFunction)
180field unrestricted sm86MultiFunctionControl : (family SM86Control)
181-- SASS FMNMX: destination = the minimum or the maximum of left and right, binary32.
182constructor SM86FloatMinimumOrMaximum
183field unrestricted sm86FloatExtremumDestination : (family SM86Register)
184field unrestricted sm86FloatExtremumLeft : (family SM86Register)
185field unrestricted sm86FloatExtremumRight : (family SM86Register)
186field unrestricted sm86FloatExtremumMode : (family SM86FloatExtremum)
187field unrestricted sm86FloatExtremumControl : (family SM86Control)
188-- SASS FADD (negated source, zero addend): destination = -source, binary32.
189constructor SM86FloatNegate
190field unrestricted sm86FloatNegateDestination : (family SM86Register)
191field unrestricted sm86FloatNegateSource : (family SM86Register)
192field unrestricted sm86FloatNegateControl : (family SM86Control)
193-- SASS F2FP.PACK_AB: destination = two binary32 sources converted and packed into one register of two binary16 halves.
194constructor SM86FloatPairToPackedHalfPair
195field unrestricted sm86Float32PairToHalf2Destination : (family SM86Register)
196field unrestricted sm86Float32PairToHalf2SourceHigh : (family SM86Register)
197field unrestricted sm86Float32PairToHalf2SourceLow : (family SM86Register)
198field unrestricted sm86Float32PairToHalf2Control : (family SM86Control)
199-- SASS F2FP.BF16.PACK_AB: destination = two binary32 sources rounded to bfloat16 (to nearest, ties to even) and packed into one register.
200constructor SM86FloatPairToPackedBFloat16Pair
201field unrestricted sm86Float32PairToBFloat16PairDestination : (family SM86Register)
202field unrestricted sm86Float32PairToBFloat16PairSourceHigh : (family SM86Register)
203field unrestricted sm86Float32PairToBFloat16PairSourceLow : (family SM86Register)
204field unrestricted sm86Float32PairToBFloat16PairControl : (family SM86Control)
205-- SASS HADD2.F32: destination = the selected binary16 half of the source widened to binary32.
206constructor SM86HalfToFloat
207field unrestricted sm86HalfToFloatDestination : (family SM86Register)
208field unrestricted sm86HalfToFloatSource : (family SM86Register)
209field unrestricted sm86HalfToFloatSelector : (family SM86HalfSelector)
210field unrestricted sm86HalfToFloatControl : (family SM86Control)
211-- SASS PRMT Rd, Ra, 0x1044 (H0) or 0x3244 (H1), RZ: destination = the selected bfloat16 half of the source widened to binary32 (its bits moved to the high half, the low half zero: exact).
212constructor SM86BFloat16ToFloat
213field unrestricted sm86BFloat16ToFloatDestination : (family SM86Register)
214field unrestricted sm86BFloat16ToFloatSource : (family SM86Register)
215field unrestricted sm86BFloat16ToFloatSelector : (family SM86HalfSelector)
216field unrestricted sm86BFloat16ToFloatControl : (family SM86Control)
217-- SASS HMMA.16816.F32: destination = fragmentA (16x16, binary16) * fragmentB (16x8, binary16) + accumulator (16x8, binary32) on the tensor cores, one warp-wide 16x8x16 tile.
218constructor SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32
219field unrestricted sm86TensorCoreMatrixMultiplyAccumulateDestination : (family SM86Register)
220field unrestricted sm86TensorCoreMatrixMultiplyAccumulateFragmentA : (family SM86Register)
221field unrestricted sm86TensorCoreMatrixMultiplyAccumulateFragmentB : (family SM86Register)
222field unrestricted sm86TensorCoreMatrixMultiplyAccumulateAccumulator : (family SM86Register)
223field unrestricted sm86TensorCoreMatrixMultiplyAccumulateControl : (family SM86Control)
224-- SASS HMMA.16816.F32.BF16: the same tile product with bfloat16 fragments.
225constructor SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32
226field unrestricted sm86TensorCoreBFloat16Destination : (family SM86Register)
227field unrestricted sm86TensorCoreBFloat16FragmentA : (family SM86Register)
228field unrestricted sm86TensorCoreBFloat16FragmentB : (family SM86Register)
229field unrestricted sm86TensorCoreBFloat16Accumulator : (family SM86Register)
230field unrestricted sm86TensorCoreBFloat16Control : (family SM86Control)
231-- SASS LDG.E: destination = the 32-bit word at address + offset in global memory.
232constructor SM86LoadGlobal
233field unrestricted sm86LoadGlobalDestination : (family SM86Register)
234field unrestricted sm86LoadGlobalAddress : (family SM86Register)
235field unrestricted sm86LoadGlobalOffset : (family SM86Unsigned32)
236field unrestricted sm86LoadGlobalControl : (family SM86Control)
237-- SASS LDG.E.128: destination quad = the 128 bits at address + offset in global memory.
238constructor SM86LoadGlobalWide
239field unrestricted sm86LoadGlobalWideDestination : (family SM86Register)
240field unrestricted sm86LoadGlobalWideAddress : (family SM86Register)
241field unrestricted sm86LoadGlobalWideOffset : (family SM86Unsigned32)
242field unrestricted sm86LoadGlobalWideControl : (family SM86Control)
243-- SASS SHFL: destination = the source register of another lane of the warp, selected by index, up, down or butterfly mode.
244constructor SM86WarpShuffle
245field unrestricted sm86ShuffleDestination : (family SM86Register)
246field unrestricted sm86ShuffleSource : (family SM86Register)
247field unrestricted sm86ShuffleLane : Byte
248field unrestricted sm86ShuffleSegment : (family SM86Unsigned32)
249field unrestricted sm86ShuffleMode : (family SM86ShuffleMode)
250field unrestricted sm86ShuffleControl : (family SM86Control)
251-- SASS LDS: destination = the 32-bit word at address + offset in shared memory.
252constructor SM86LoadShared
253field unrestricted sm86LoadSharedDestination : (family SM86Register)
254field unrestricted sm86LoadSharedAddress : (family SM86Register)
255field unrestricted sm86LoadSharedOffset : (family SM86Unsigned32)
256field unrestricted sm86LoadSharedControl : (family SM86Control)
257-- SASS LDSM: destination = one, two or four 8x8 binary16 matrices loaded from shared memory into tensor-core fragment layout, optionally transposed.
258constructor SM86LoadSharedMatrix
259field unrestricted sm86LoadSharedMatrixDestination : (family SM86Register)
260field unrestricted sm86LoadSharedMatrixAddress : (family SM86Register)
261field unrestricted sm86LoadSharedMatrixOffset : (family SM86Unsigned32)
262field unrestricted sm86LoadSharedMatrixCount : (family SM86SharedMatrixCount)
263field unrestricted sm86LoadSharedMatrixTranspose : (family SM86SharedMatrixTranspose)
264field unrestricted sm86LoadSharedMatrixControl : (family SM86Control)
265-- SASS STS: the 32-bit value stored at address + offset in shared memory.
266constructor SM86StoreShared
267field unrestricted sm86StoreSharedAddress : (family SM86Register)
268field unrestricted sm86StoreSharedValue : (family SM86Register)
269field unrestricted sm86StoreSharedOffset : (family SM86Unsigned32)
270field unrestricted sm86StoreSharedControl : (family SM86Control)
271-- SASS LDGSTS.E.BYPASS.128 (cp.async.cg, 16 bytes): the 128 bits at global
272-- source + sourceOffset (a register pair; the offset a signed 12-bit
273-- immediate) copied to shared memory at address + offset, asynchronously:
274-- the copy joins the thread's open group (SM86CommitAsyncGroup closes it),
275-- and nothing may read those shared bytes until SM86WaitAsyncGroups has
276-- retired the group (and, for other threads, a BAR.SYNC after).  Its
277-- registers are read after issue: a read barrier guards them.
278constructor SM86LoadGlobalToShared
279field unrestricted sm86LoadGlobalToSharedAddress : (family SM86Register)
280field unrestricted sm86LoadGlobalToSharedOffset : (family SM86Unsigned32)
281field unrestricted sm86LoadGlobalToSharedSource : (family SM86Register)
282field unrestricted sm86LoadGlobalToSharedSourceOffset : (family SM86Unsigned32)
283field unrestricted sm86LoadGlobalToSharedControl : (family SM86Control)
284-- SASS LDGDEPBAR (cp.async.commit_group): the thread's open group of
285-- asynchronous copies closed; the groups in flight count on scoreboard SB0,
286-- which the control's write barrier names.
287constructor SM86CommitAsyncGroup
288field unrestricted sm86CommitAsyncGroupControl : (family SM86Control)
289-- SASS DEPBAR.LE SB0, count (cp.async.wait_group count): wait until at
290-- most `count` (0..63) groups of asynchronous copies are in flight.
291constructor SM86WaitAsyncGroups
292field unrestricted sm86WaitAsyncGroupsCount : Byte
293field unrestricted sm86WaitAsyncGroupsControl : (family SM86Control)
294-- SASS BAR.SYNC: every thread of the cooperative thread array waits until all have arrived.
295constructor SM86BarrierSynchronize
296field unrestricted sm86BarrierSynchronizeControl : (family SM86Control)
297-- SASS STG.E: the 32-bit value stored at address + offset in global memory.
298constructor SM86StoreGlobal
299field unrestricted sm86StoreGlobalAddress : (family SM86Register)
300field unrestricted sm86StoreGlobalValue : (family SM86Register)
301field unrestricted sm86StoreGlobalOffset : (family SM86Unsigned32)
302field unrestricted sm86StoreGlobalControl : (family SM86Control)
303-- SASS STG.E.128: the 128-bit value quad stored at address + offset in global memory.
304constructor SM86StoreGlobalWide
305field unrestricted sm86StoreGlobalWideAddress : (family SM86Register)
306field unrestricted sm86StoreGlobalWideValue : (family SM86Register)
307field unrestricted sm86StoreGlobalWideOffset : (family SM86Unsigned32)
308field unrestricted sm86StoreGlobalWideControl : (family SM86Control)
309-- SASS STG.E.64: the 64-bit value pair stored at address + offset in global memory.
310constructor SM86StoreGlobal64
311field unrestricted sm86StoreGlobal64Address : (family SM86Register)
312field unrestricted sm86StoreGlobal64Value : (family SM86Register)
313field unrestricted sm86StoreGlobal64Offset : (family SM86Unsigned32)
314field unrestricted sm86StoreGlobal64Control : (family SM86Control)
315-- SASS RED.E.ADD.F32: the binary32 value atomically added to the word at address + offset in global memory, no result returned.
316constructor SM86ReduceGlobalAddFloat32
317field unrestricted sm86ReduceGlobalAddress : (family SM86Register)
318field unrestricted sm86ReduceGlobalValue : (family SM86Register)
319field unrestricted sm86ReduceGlobalOffset : (family SM86Unsigned32)
320field unrestricted sm86ReduceGlobalControl : (family SM86Control)
321-- SASS ISETP.GT (immediate): destination predicate = source > immediate, compared as
322-- unsigned 32-bit words in this encoding: the RTX 3070 has 0x80000000 > 0
323-- (Checked.IntegerCompareProbe, Proof.CheckedIntegerCompareSilicon).
324constructor SM86PredicateGreaterThanImmediate
325field unrestricted sm86PredicateGreaterDestination : (family SM86Predicate)
326field unrestricted sm86PredicateGreaterSource : (family SM86Register)
327field unrestricted sm86PredicateGreaterImmediate : (family SM86Unsigned32)
328field unrestricted sm86PredicateGreaterControl : (family SM86Control)
329-- SASS BRA: continue at the instruction offset bytes away, relative to the next instruction.
330constructor SM86Branch
331field unrestricted sm86BranchOffset : (family SM86Unsigned32)
332field unrestricted sm86BranchDescriptor : (family SM86Unsigned32)
333field unrestricted sm86BranchControl : (family SM86Control)
334-- SASS EXIT: this thread finishes the program.
335constructor SM86Exit
336field unrestricted sm86ExitControl : (family SM86Control)
337
338end-family
339
340family SM86Instruction : Type 0
341constructor SM86InstructionValue
342field unrestricted sm86InstructionGuard : (family SM86InstructionGuard)
343field unrestricted sm86InstructionBody : (family SM86InstructionBody)
344
345end-family
346
347family SM86Program : Type 0
348constructor SM86ProgramEnd
349constructor SM86ProgramNext
350field unrestricted sm86ProgramHead : (family SM86Instruction)
351recursive unrestricted sm86ProgramTail
352
353end-family
354
355def sm86Instruction =
356  (lambda unrestricted body : (family SM86InstructionBody) .
357    (constructor
358      SM86Instruction
359      SM86InstructionValue
360      (constructor SM86InstructionGuard SM86InstructionAlways)
361      body))
362
363def sm86PredicatedInstruction =
364  (lambda unrestricted predicate : (family SM86Predicate) .
365    (lambda unrestricted body : (family SM86InstructionBody) .
366      (constructor
367        SM86Instruction
368        SM86InstructionValue
369        (constructor SM86InstructionGuard SM86InstructionWhen predicate)
370        body)))
371
372def sm86NegatedPredicatedInstruction =
373  (lambda unrestricted predicate : (family SM86Predicate) .
374    (lambda unrestricted body : (family SM86InstructionBody) .
375      (constructor
376        SM86Instruction
377        SM86InstructionValue
378        (constructor SM86InstructionGuard SM86InstructionWhenNot predicate)
379        body)))