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
86-- an 8-bit floating-point format (sm_89 and later): E4M3 (4 exponent bits,
87-- 3 mantissa bits, largest finite 448) or E5M2 (5 and 2, 57344)
88family SM86Float8Format : Type 0
89constructor SM86Float8E4M3
90constructor SM86Float8E5M2
91end-family
92
93-- SM86FloatArithmetic's operation: FADD, FMUL or FFMA
94family SM86FloatOperation : Type 0
95constructor SM86FloatOperationAdd
96constructor SM86FloatOperationMultiply
97constructor SM86FloatOperationFusedMultiplyAdd
98end-family
99
100-- a binary32 rounding direction: to nearest even (RN), toward minus
101-- infinity (RM), toward plus infinity (RP), toward zero (RZ)
102family SM86Rounding : Type 0
103constructor SM86RoundNearestEven
104constructor SM86RoundDown
105constructor SM86RoundUp
106constructor SM86RoundTowardZero
107end-family
108
109-- SM86FloatArithmetic's modifiers, each flag 0 or 1: the rounding, .FTZ
110-- (subnormal sources and result flushed to zero, sign kept), .SAT (the
111-- result clamped to [0, 1], NaN to 0), a source negated (-R) or made
112-- absolute (|R|: FADD only).  The negation of the left and right sources
113-- negates FMUL's and FFMA's product.
114family SM86FloatModifiers : Type 0
115constructor SM86FloatModifiersValue
116field unrestricted sm86FloatModifiersRounding : (family SM86Rounding)
117field unrestricted sm86FloatModifiersFlushToZero : Nat
118field unrestricted sm86FloatModifiersSaturate : Nat
119field unrestricted sm86FloatModifiersNegateLeft : Nat
120field unrestricted sm86FloatModifiersAbsoluteLeft : Nat
121field unrestricted sm86FloatModifiersNegateRight : Nat
122field unrestricted sm86FloatModifiersAbsoluteRight : Nat
123field unrestricted sm86FloatModifiersNegateAddend : Nat
124end-family
125
126family SM86InstructionBody : Type 0
127-- SASS MOV (constant bank): destination = c[bank][offset], a 32-bit word from a constant bank.
128constructor SM86MoveConstant
129field unrestricted sm86MoveConstantDestination : (family SM86Register)
130field unrestricted sm86MoveConstantBank : Byte
131field unrestricted sm86MoveConstantOffset : (family SM86Unsigned32)
132field unrestricted sm86MoveConstantControl : (family SM86Control)
133-- SASS S2R: destination = a special register (thread or cooperative-thread-array index).
134constructor SM86SpecialToRegister
135field unrestricted sm86SpecialDestination : (family SM86Register)
136field unrestricted sm86SpecialSource : (family SM86SpecialRegister)
137field unrestricted sm86SpecialControl : (family SM86Control)
138-- SASS MOV (immediate): destination = a 32-bit immediate.
139constructor SM86MoveImmediate
140field unrestricted sm86MoveImmediateDestination : (family SM86Register)
141field unrestricted sm86MoveImmediateValue : (family SM86Unsigned32)
142field unrestricted sm86MoveImmediateControl : (family SM86Control)
143-- SASS IMAD (constant bank): destination = left * c[bank][offset] + addend, 32-bit integer.
144constructor SM86IntegerMultiplyAddConstant
145field unrestricted sm86IMADConstantDestination : (family SM86Register)
146field unrestricted sm86IMADConstantLeft : (family SM86Register)
147field unrestricted sm86IMADConstantBank : Byte
148field unrestricted sm86IMADConstantOffset : (family SM86Unsigned32)
149field unrestricted sm86IMADConstantAddend : (family SM86Register)
150field unrestricted sm86IMADConstantControl : (family SM86Control)
151-- SASS IMAD (immediate): destination = left * immediate + addend, 32-bit integer.
152constructor SM86IntegerMultiplyAddImmediate
153field unrestricted sm86IMADImmediateDestination : (family SM86Register)
154field unrestricted sm86IMADImmediateLeft : (family SM86Register)
155field unrestricted sm86IMADImmediateValue : (family SM86Unsigned32)
156field unrestricted sm86IMADImmediateAddend : (family SM86Register)
157field unrestricted sm86IMADImmediateControl : (family SM86Control)
158-- SASS IMAD.WIDE.U32: destination pair = left * right + c[bank][offset], a 64-bit product plus a 64-bit constant.
159constructor SM86IntegerMultiplyAddWideConstant
160field unrestricted sm86IMADWideDestination : (family SM86Register)
161field unrestricted sm86IMADWideLeft : (family SM86Register)
162field unrestricted sm86IMADWideRight : (family SM86Register)
163field unrestricted sm86IMADWideBank : Byte
164field unrestricted sm86IMADWideOffset : (family SM86Unsigned32)
165field unrestricted sm86IMADWideControl : (family SM86Control)
166-- SASS IADD3 (immediate): destination = left + immediate, the three-input adder with one input zero.
167constructor SM86IntegerAddThreeImmediate
168field unrestricted sm86IADD3ImmediateDestination : (family SM86Register)
169field unrestricted sm86IADD3ImmediateLeft : (family SM86Register)
170field unrestricted sm86IADD3ImmediateValue : (family SM86Unsigned32)
171field unrestricted sm86IADD3ImmediateControl : (family SM86Control)
172-- SASS IADD3 (register): destination = left + right, the three-input adder with one input zero.
173constructor SM86IntegerAddThreeRegister
174field unrestricted sm86IADD3RegisterDestination : (family SM86Register)
175field unrestricted sm86IADD3RegisterLeft : (family SM86Register)
176field unrestricted sm86IADD3RegisterRight : (family SM86Register)
177field unrestricted sm86IADD3RegisterControl : (family SM86Control)
178-- SASS SHF.R.U32.HI: destination = source logically shifted right by an immediate amount.
179constructor SM86ShiftRightImmediate
180field unrestricted sm86ShiftRightDestination : (family SM86Register)
181field unrestricted sm86ShiftRightSource : (family SM86Register)
182field unrestricted sm86ShiftRightAmount : Byte
183field unrestricted sm86ShiftRightControl : (family SM86Control)
184-- SASS LOP3.LUT: destination = truthTable(left, right, zero), any bitwise function of the inputs given as an 8-bit lookup table.
185constructor SM86LogicThreeInputTruthTable
186field unrestricted sm86Logic3Destination : (family SM86Register)
187field unrestricted sm86Logic3Left : (family SM86Register)
188field unrestricted sm86Logic3Right : (family SM86Register)
189field unrestricted sm86Logic3TruthTable : Byte
190field unrestricted sm86Logic3Control : (family SM86Control)
191-- SASS I2FP.F32.S32: destination = the signed 32-bit integer source converted to binary32.
192constructor SM86IntegerToFloat
193field unrestricted sm86IntegerToFloatDestination : (family SM86Register)
194field unrestricted sm86IntegerToFloatSource : (family SM86Register)
195field unrestricted sm86IntegerToFloatControl : (family SM86Control)
196-- SASS FADD: destination = left + right, binary32, round to nearest even.
197constructor SM86FloatAdd
198field unrestricted sm86FloatAddDestination : (family SM86Register)
199field unrestricted sm86FloatAddLeft : (family SM86Register)
200field unrestricted sm86FloatAddRight : (family SM86Register)
201field unrestricted sm86FloatAddControl : (family SM86Control)
202-- SASS FMUL: destination = left * right, binary32, round to nearest even.
203constructor SM86FloatMultiply
204field unrestricted sm86FloatMultiplyDestination : (family SM86Register)
205field unrestricted sm86FloatMultiplyLeft : (family SM86Register)
206field unrestricted sm86FloatMultiplyRight : (family SM86Register)
207field unrestricted sm86FloatMultiplyControl : (family SM86Control)
208-- Binary64 arithmetic has paired operands and separate rounding at every
209-- instruction. It is variable-latency: callers must retire both destination
210-- words and protect both words of every source with scoreboard dependencies.
211constructor SM86Float64Binary
212field unrestricted sm86Float64Operation : (family SM86Float64Operation)
213field unrestricted sm86Float64Destination : (family SM86RegisterPair)
214field unrestricted sm86Float64Left : (family SM86RegisterPair)
215field unrestricted sm86Float64Right : (family SM86RegisterPair)
216field unrestricted sm86Float64Control : (family SM86Control)
217-- F2F with nearest-even rounding and subnormals preserved. Its pair shape,
218-- late sources and late result are explicit; conversion never implies FTZ.
219constructor SM86FloatConvert
220field unrestricted sm86FloatConvertOperation : (family SM86FloatConversion)
221field unrestricted sm86FloatConvertControl : (family SM86Control)
222-- SASS FFMA: destination = left * right + addend, binary32 with a single rounding.
223constructor SM86FloatFusedMultiplyAdd
224field unrestricted sm86FloatFMADestination : (family SM86Register)
225field unrestricted sm86FloatFMALeft : (family SM86Register)
226field unrestricted sm86FloatFMARight : (family SM86Register)
227field unrestricted sm86FloatFMAAddend : (family SM86Register)
228field unrestricted sm86FloatFMAControl : (family SM86Control)
229-- 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.
230constructor SM86MultiFunctionUnitApproximation
231field unrestricted sm86MultiFunctionDestination : (family SM86Register)
232field unrestricted sm86MultiFunctionSource : (family SM86Register)
233field unrestricted sm86MultiFunctionOperation : (family SM86MultiFunction)
234field unrestricted sm86MultiFunctionControl : (family SM86Control)
235-- SASS FMNMX: destination = the minimum or the maximum of left and right, binary32.
236constructor SM86FloatMinimumOrMaximum
237field unrestricted sm86FloatExtremumDestination : (family SM86Register)
238field unrestricted sm86FloatExtremumLeft : (family SM86Register)
239field unrestricted sm86FloatExtremumRight : (family SM86Register)
240field unrestricted sm86FloatExtremumMode : (family SM86FloatExtremum)
241field unrestricted sm86FloatExtremumControl : (family SM86Control)
242-- SASS FADD (negated source, zero addend): destination = -source, binary32.
243constructor SM86FloatNegate
244field unrestricted sm86FloatNegateDestination : (family SM86Register)
245field unrestricted sm86FloatNegateSource : (family SM86Register)
246field unrestricted sm86FloatNegateControl : (family SM86Control)
247-- SASS F2FP.PACK_AB: destination = two binary32 sources converted and packed into one register of two binary16 halves.
248constructor SM86FloatPairToPackedHalfPair
249field unrestricted sm86Float32PairToHalf2Destination : (family SM86Register)
250field unrestricted sm86Float32PairToHalf2SourceHigh : (family SM86Register)
251field unrestricted sm86Float32PairToHalf2SourceLow : (family SM86Register)
252field unrestricted sm86Float32PairToHalf2Control : (family SM86Control)
253-- SASS F2FP.BF16.PACK_AB: destination = two binary32 sources rounded to bfloat16 (to nearest, ties to even) and packed into one register.
254constructor SM86FloatPairToPackedBFloat16Pair
255field unrestricted sm86Float32PairToBFloat16PairDestination : (family SM86Register)
256field unrestricted sm86Float32PairToBFloat16PairSourceHigh : (family SM86Register)
257field unrestricted sm86Float32PairToBFloat16PairSourceLow : (family SM86Register)
258field unrestricted sm86Float32PairToBFloat16PairControl : (family SM86Control)
259-- SASS HADD2.F32: destination = the selected binary16 half of the source widened to binary32.
260-- SASS F2FP.SATFINITE.{E4M3,E5M2}.F32.PACK_AB_MERGE_C (sm_89 and later):
261-- destination = the half of `merge` that `mergeHalf` selects in bits
262-- 16..31, the high source rounded to the 8-bit format in bits 8..15 and
263-- the low source in bits 0..7 (each to nearest, ties to even, saturating to
264-- the format's largest finite magnitude; a NaN stays NaN).
265constructor SM86FloatPairToPackedFloat8Pair
266field unrestricted sm86Float32PairToFloat8Destination : (family SM86Register)
267field unrestricted sm86Float32PairToFloat8SourceHigh : (family SM86Register)
268field unrestricted sm86Float32PairToFloat8SourceLow : (family SM86Register)
269field unrestricted sm86Float32PairToFloat8Merge : (family SM86Register)
270field unrestricted sm86Float32PairToFloat8MergeHalf : (family SM86HalfSelector)
271field unrestricted sm86Float32PairToFloat8Format : (family SM86Float8Format)
272field unrestricted sm86Float32PairToFloat8Control : (family SM86Control)
273-- SASS FADD / FMUL / FFMA with their modifiers (SM86FloatModifiers): the
274-- words of ptxas 12.9 for sm_90a (Proof.FloatArithmeticContract), libdevice's
275-- forms -- __nv_expf's FFMA.FTZ.RM, __nv_tanhf's FFMA.FTZ, FADD.FTZ.SAT.
276-- destination = left + right, left * right, or left * right + addend (the
277-- addend unread unless FFMA), binary32 with one rounding.
278constructor SM86FloatArithmetic
279field unrestricted sm86FloatArithmeticOperation : (family SM86FloatOperation)
280field unrestricted sm86FloatArithmeticDestination : (family SM86Register)
281field unrestricted sm86FloatArithmeticLeft : (family SM86Register)
282field unrestricted sm86FloatArithmeticRight : (family SM86Register)
283field unrestricted sm86FloatArithmeticAddend : (family SM86Register)
284field unrestricted sm86FloatArithmeticModifiers : (family SM86FloatModifiers)
285field unrestricted sm86FloatArithmeticControl : (family SM86Control)
286constructor SM86HalfToFloat
287field unrestricted sm86HalfToFloatDestination : (family SM86Register)
288field unrestricted sm86HalfToFloatSource : (family SM86Register)
289field unrestricted sm86HalfToFloatSelector : (family SM86HalfSelector)
290field unrestricted sm86HalfToFloatControl : (family SM86Control)
291-- 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).
292constructor SM86BFloat16ToFloat
293field unrestricted sm86BFloat16ToFloatDestination : (family SM86Register)
294field unrestricted sm86BFloat16ToFloatSource : (family SM86Register)
295field unrestricted sm86BFloat16ToFloatSelector : (family SM86HalfSelector)
296field unrestricted sm86BFloat16ToFloatControl : (family SM86Control)
297-- SASS HMMA.16816.F32: destination = fragmentA (16x16, binary16) * fragmentB (16x8, binary16) + accumulator (16x8, binary32) on the tensor cores, one warp-wide 16x8x16 tile.
298constructor SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32
299field unrestricted sm86TensorCoreMatrixMultiplyAccumulateDestination : (family SM86Register)
300field unrestricted sm86TensorCoreMatrixMultiplyAccumulateFragmentA : (family SM86Register)
301field unrestricted sm86TensorCoreMatrixMultiplyAccumulateFragmentB : (family SM86Register)
302field unrestricted sm86TensorCoreMatrixMultiplyAccumulateAccumulator : (family SM86Register)
303field unrestricted sm86TensorCoreMatrixMultiplyAccumulateControl : (family SM86Control)
304-- SASS HMMA.16816.F32.BF16: the same tile product with bfloat16 fragments.
305constructor SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32
306field unrestricted sm86TensorCoreBFloat16Destination : (family SM86Register)
307field unrestricted sm86TensorCoreBFloat16FragmentA : (family SM86Register)
308field unrestricted sm86TensorCoreBFloat16FragmentB : (family SM86Register)
309field unrestricted sm86TensorCoreBFloat16Accumulator : (family SM86Register)
310field unrestricted sm86TensorCoreBFloat16Control : (family SM86Control)
311-- SASS LDG.E: destination = the 32-bit word at address + offset in global memory.
312constructor SM86LoadGlobal
313field unrestricted sm86LoadGlobalDestination : (family SM86Register)
314field unrestricted sm86LoadGlobalAddress : (family SM86Register)
315field unrestricted sm86LoadGlobalOffset : (family SM86Unsigned32)
316field unrestricted sm86LoadGlobalControl : (family SM86Control)
317-- SASS LDG.E.128: destination quad = the 128 bits at address + offset in global memory.
318constructor SM86LoadGlobalWide
319field unrestricted sm86LoadGlobalWideDestination : (family SM86Register)
320field unrestricted sm86LoadGlobalWideAddress : (family SM86Register)
321field unrestricted sm86LoadGlobalWideOffset : (family SM86Unsigned32)
322field unrestricted sm86LoadGlobalWideControl : (family SM86Control)
323-- SASS SHFL: destination = the source register of another lane of the warp, selected by index, up, down or butterfly mode.
324constructor SM86WarpShuffle
325field unrestricted sm86ShuffleDestination : (family SM86Register)
326field unrestricted sm86ShuffleSource : (family SM86Register)
327field unrestricted sm86ShuffleLane : Byte
328field unrestricted sm86ShuffleSegment : (family SM86Unsigned32)
329field unrestricted sm86ShuffleMode : (family SM86ShuffleMode)
330field unrestricted sm86ShuffleControl : (family SM86Control)
331-- SASS LDS: destination = the 32-bit word at 4 address + offset in shared memory
332-- (encoded LDS [Ra.X4 + offset]: the register is a WORD index, the offset
333-- bytes -- nvdisasm prints the .X4; a byte address in the register reads 4x
334-- too far, as the Hopper attention key pass did, 2026-10-18).
335constructor SM86LoadShared
336field unrestricted sm86LoadSharedDestination : (family SM86Register)
337field unrestricted sm86LoadSharedAddress : (family SM86Register)
338field unrestricted sm86LoadSharedOffset : (family SM86Unsigned32)
339field unrestricted sm86LoadSharedControl : (family SM86Control)
340-- SASS LDSM: destination = one, two or four 8x8 binary16 matrices loaded from shared memory into tensor-core fragment layout, optionally transposed.
341constructor SM86LoadSharedMatrix
342field unrestricted sm86LoadSharedMatrixDestination : (family SM86Register)
343field unrestricted sm86LoadSharedMatrixAddress : (family SM86Register)
344field unrestricted sm86LoadSharedMatrixOffset : (family SM86Unsigned32)
345field unrestricted sm86LoadSharedMatrixCount : (family SM86SharedMatrixCount)
346field unrestricted sm86LoadSharedMatrixTranspose : (family SM86SharedMatrixTranspose)
347field unrestricted sm86LoadSharedMatrixControl : (family SM86Control)
348-- SASS STS: the 32-bit value stored at 4 address + offset in shared memory
349-- (STS [Ra.X4 + offset]: the register a word index, the offset bytes).
350constructor SM86StoreShared
351field unrestricted sm86StoreSharedAddress : (family SM86Register)
352field unrestricted sm86StoreSharedValue : (family SM86Register)
353field unrestricted sm86StoreSharedOffset : (family SM86Unsigned32)
354field unrestricted sm86StoreSharedControl : (family SM86Control)
355-- SASS LDGSTS.E.BYPASS.128 (cp.async.cg, 16 bytes): the 128 bits at global
356-- source + sourceOffset (a register pair; the offset a signed 12-bit
357-- immediate) copied to shared memory at address + offset, asynchronously:
358-- the copy joins the thread's open group (SM86CommitAsyncGroup closes it),
359-- and nothing may read those shared bytes until SM86WaitAsyncGroups has
360-- retired the group (and, for other threads, a BAR.SYNC after).  Its
361-- registers are read after issue: a read barrier guards them.
362constructor SM86LoadGlobalToShared
363field unrestricted sm86LoadGlobalToSharedAddress : (family SM86Register)
364field unrestricted sm86LoadGlobalToSharedOffset : (family SM86Unsigned32)
365field unrestricted sm86LoadGlobalToSharedSource : (family SM86Register)
366field unrestricted sm86LoadGlobalToSharedSourceOffset : (family SM86Unsigned32)
367field unrestricted sm86LoadGlobalToSharedControl : (family SM86Control)
368-- SASS LDGDEPBAR (cp.async.commit_group): the thread's open group of
369-- asynchronous copies closed; the groups in flight count on scoreboard SB0,
370-- which the control's write barrier names.
371constructor SM86CommitAsyncGroup
372field unrestricted sm86CommitAsyncGroupControl : (family SM86Control)
373-- SASS DEPBAR.LE SB0, count (cp.async.wait_group count): wait until at
374-- most `count` (0..63) groups of asynchronous copies are in flight.
375constructor SM86WaitAsyncGroups
376field unrestricted sm86WaitAsyncGroupsCount : Byte
377field unrestricted sm86WaitAsyncGroupsControl : (family SM86Control)
378-- SASS BAR.SYNC: every thread of the cooperative thread array waits until all have arrived.
379constructor SM86BarrierSynchronize
380field unrestricted sm86BarrierSynchronizeControl : (family SM86Control)
381-- SASS BAR.SYNC b, n: the first `threads` threads to arrive at named barrier
382-- `barrier` (0..15) wait until that many have (a multiple of the warp
383-- size, at most 1024; the others of the CTA run on). Warps that synchronise
384-- among themselves this way leave the CTA's other warps free -- a warp
385-- streaming independent work beside them (Realization.Nvidia.SM86's side
386-- warps).
387constructor SM86BarrierSynchronizeCount
388field unrestricted sm86BarrierSynchronizeCountBarrier : Byte
389field unrestricted sm86BarrierSynchronizeCountThreads : Nat
390field unrestricted sm86BarrierSynchronizeCountControl : (family SM86Control)
391-- SASS STG.E: the 32-bit value stored at address + offset in global memory.
392constructor SM86StoreGlobal
393field unrestricted sm86StoreGlobalAddress : (family SM86Register)
394field unrestricted sm86StoreGlobalValue : (family SM86Register)
395field unrestricted sm86StoreGlobalOffset : (family SM86Unsigned32)
396field unrestricted sm86StoreGlobalControl : (family SM86Control)
397-- SASS STG.E.128: the 128-bit value quad stored at address + offset in global memory.
398constructor SM86StoreGlobalWide
399field unrestricted sm86StoreGlobalWideAddress : (family SM86Register)
400field unrestricted sm86StoreGlobalWideValue : (family SM86Register)
401field unrestricted sm86StoreGlobalWideOffset : (family SM86Unsigned32)
402field unrestricted sm86StoreGlobalWideControl : (family SM86Control)
403-- SASS STG.E.64: the 64-bit value pair stored at address + offset in global memory.
404constructor SM86StoreGlobal64
405field unrestricted sm86StoreGlobal64Address : (family SM86Register)
406field unrestricted sm86StoreGlobal64Value : (family SM86Register)
407field unrestricted sm86StoreGlobal64Offset : (family SM86Unsigned32)
408field unrestricted sm86StoreGlobal64Control : (family SM86Control)
409-- SASS RED.E.ADD.F32: the binary32 value atomically added to the word at address + offset in global memory, no result returned.
410constructor SM86ReduceGlobalAddFloat32
411field unrestricted sm86ReduceGlobalAddress : (family SM86Register)
412field unrestricted sm86ReduceGlobalValue : (family SM86Register)
413field unrestricted sm86ReduceGlobalOffset : (family SM86Unsigned32)
414field unrestricted sm86ReduceGlobalControl : (family SM86Control)
415-- SASS ISETP.GT (immediate): destination predicate = source > immediate, compared as
416-- unsigned 32-bit words in this encoding: the RTX 3070 has 0x80000000 > 0
417-- (Checked.IntegerCompareProbe, Proof.CheckedIntegerCompareSilicon).
418constructor SM86PredicateGreaterThanImmediate
419field unrestricted sm86PredicateGreaterDestination : (family SM86Predicate)
420field unrestricted sm86PredicateGreaterSource : (family SM86Register)
421field unrestricted sm86PredicateGreaterImmediate : (family SM86Unsigned32)
422field unrestricted sm86PredicateGreaterControl : (family SM86Control)
423-- SASS BRA: continue at the instruction offset bytes away, relative to the next instruction.
424constructor SM86Branch
425field unrestricted sm86BranchOffset : (family SM86Unsigned32)
426field unrestricted sm86BranchDescriptor : (family SM86Unsigned32)
427field unrestricted sm86BranchControl : (family SM86Control)
428-- SASS EXIT: this thread finishes the program.
429constructor SM86Exit
430field unrestricted sm86ExitControl : (family SM86Control)
431
432end-family
433
434family SM86Instruction : Type 0
435constructor SM86InstructionValue
436field unrestricted sm86InstructionGuard : (family SM86InstructionGuard)
437field unrestricted sm86InstructionBody : (family SM86InstructionBody)
438
439end-family
440
441family SM86Program : Type 0
442constructor SM86ProgramEnd
443constructor SM86ProgramNext
444field unrestricted sm86ProgramHead : (family SM86Instruction)
445recursive unrestricted sm86ProgramTail
446
447end-family
448
449def sm86Instruction =
450  (lambda unrestricted body : (family SM86InstructionBody) .
451    (constructor
452      SM86Instruction
453      SM86InstructionValue
454      (constructor SM86InstructionGuard SM86InstructionAlways)
455      body))
456
457def sm86PredicatedInstruction =
458  (lambda unrestricted predicate : (family SM86Predicate) .
459    (lambda unrestricted body : (family SM86InstructionBody) .
460      (constructor
461        SM86Instruction
462        SM86InstructionValue
463        (constructor SM86InstructionGuard SM86InstructionWhen predicate)
464        body)))
465
466def sm86NegatedPredicatedInstruction =
467  (lambda unrestricted predicate : (family SM86Predicate) .
468    (lambda unrestricted body : (family SM86InstructionBody) .
469      (constructor
470        SM86Instruction
471        SM86InstructionValue
472        (constructor SM86InstructionGuard SM86InstructionWhenNot predicate)
473        body)))