module Accelerator.SM86.Instruction import Accelerator.SM86.Control import Accelerator.SM86.Immediate import Accelerator.SM86.NumericSemantics import Accelerator.SM86.Types family SM86SpecialRegister : Type 0 -- SASS SR_CTAID.X: the cooperative thread array (block) index on x. constructor SM86CooperativeThreadArrayIdX -- SASS SR_CTAID.Y: the cooperative thread array (block) index on y. constructor SM86CooperativeThreadArrayIdY -- SASS SR_CTAID.Z: the cooperative thread array (block) index on z. constructor SM86CooperativeThreadArrayIdZ -- SASS SR_TID.X: the thread index on x within its cooperative thread array. constructor SM86ThreadIdX -- SASS SR_CLOCKLO: the low word of the SM's cycle counter. constructor SM86ClockLow -- SASS SR_GLOBALTIMERLO: the low word of the device's global timer, in -- nanoseconds -- the clock the semaphore releases stamp. constructor SM86GlobalTimerLow -- SASS SR_GLOBALTIMERHI: its high word. constructor SM86GlobalTimerHigh end-family family SM86InstructionGuard : Type 0 -- no guard: the instruction always executes. constructor SM86InstructionAlways -- SASS @P: the instruction executes only in threads where the predicate is true. constructor SM86InstructionWhen field unrestricted sm86InstructionGuardPredicate : (family SM86Predicate) -- SASS @!P: the instruction executes only in threads where the predicate is false. constructor SM86InstructionWhenNot field unrestricted sm86InstructionGuardNotPredicate : (family SM86Predicate) end-family family SM86ShuffleMode : Type 0 -- SASS SHFL.IDX: read the lane named by the lane operand. constructor SM86ShuffleIndex -- SASS SHFL.UP: read the lane that is lane places below this one. constructor SM86ShuffleUp -- SASS SHFL.DOWN: read the lane that is lane places above this one. constructor SM86ShuffleDown -- SASS SHFL.BFLY: read the lane whose index is this lane's index xor the lane operand. constructor SM86ShuffleButterfly end-family family SM86HalfSelector : Type 0 -- the low binary16 half (H0) of a 32-bit register. constructor SM86LowHalf -- the high binary16 half (H1) of a 32-bit register. constructor SM86HighHalf end-family -- the 16-bit floating-point format a program's halves are in: binary16 -- (5 exponent bits, 10 fraction bits) or bfloat16 (8 and 7: binary32's -- range). Accelerator.SM86.HalfFormat moves a program between them. family SM86HalfFormat : Type 0 constructor SM86Binary16 constructor SM86BFloat16 end-family family SM86SharedMatrixCount : Type 0 -- SASS LDSM.x1: one 8x8 matrix. constructor SM86SharedMatrix1 -- SASS LDSM.x2: two 8x8 matrices. constructor SM86SharedMatrix2 -- SASS LDSM.x4: four 8x8 matrices. constructor SM86SharedMatrix4 end-family family SM86SharedMatrixTranspose : Type 0 -- SASS LDSM (no .T): rows as stored. constructor SM86SharedMatrixNotTransposed -- SASS LDSM.T: each matrix transposed while loading. constructor SM86SharedMatrixTransposed end-family family SM86InstructionBody : Type 0 -- SASS MOV (constant bank): destination = c[bank][offset], a 32-bit word from a constant bank. constructor SM86MoveConstant field unrestricted sm86MoveConstantDestination : (family SM86Register) field unrestricted sm86MoveConstantBank : Byte field unrestricted sm86MoveConstantOffset : (family SM86Unsigned32) field unrestricted sm86MoveConstantControl : (family SM86Control) -- SASS S2R: destination = a special register (thread or cooperative-thread-array index). constructor SM86SpecialToRegister field unrestricted sm86SpecialDestination : (family SM86Register) field unrestricted sm86SpecialSource : (family SM86SpecialRegister) field unrestricted sm86SpecialControl : (family SM86Control) -- SASS MOV (immediate): destination = a 32-bit immediate. constructor SM86MoveImmediate field unrestricted sm86MoveImmediateDestination : (family SM86Register) field unrestricted sm86MoveImmediateValue : (family SM86Unsigned32) field unrestricted sm86MoveImmediateControl : (family SM86Control) -- SASS IMAD (constant bank): destination = left * c[bank][offset] + addend, 32-bit integer. constructor SM86IntegerMultiplyAddConstant field unrestricted sm86IMADConstantDestination : (family SM86Register) field unrestricted sm86IMADConstantLeft : (family SM86Register) field unrestricted sm86IMADConstantBank : Byte field unrestricted sm86IMADConstantOffset : (family SM86Unsigned32) field unrestricted sm86IMADConstantAddend : (family SM86Register) field unrestricted sm86IMADConstantControl : (family SM86Control) -- SASS IMAD (immediate): destination = left * immediate + addend, 32-bit integer. constructor SM86IntegerMultiplyAddImmediate field unrestricted sm86IMADImmediateDestination : (family SM86Register) field unrestricted sm86IMADImmediateLeft : (family SM86Register) field unrestricted sm86IMADImmediateValue : (family SM86Unsigned32) field unrestricted sm86IMADImmediateAddend : (family SM86Register) field unrestricted sm86IMADImmediateControl : (family SM86Control) -- SASS IMAD.WIDE.U32: destination pair = left * right + c[bank][offset], a 64-bit product plus a 64-bit constant. constructor SM86IntegerMultiplyAddWideConstant field unrestricted sm86IMADWideDestination : (family SM86Register) field unrestricted sm86IMADWideLeft : (family SM86Register) field unrestricted sm86IMADWideRight : (family SM86Register) field unrestricted sm86IMADWideBank : Byte field unrestricted sm86IMADWideOffset : (family SM86Unsigned32) field unrestricted sm86IMADWideControl : (family SM86Control) -- SASS IADD3 (immediate): destination = left + immediate, the three-input adder with one input zero. constructor SM86IntegerAddThreeImmediate field unrestricted sm86IADD3ImmediateDestination : (family SM86Register) field unrestricted sm86IADD3ImmediateLeft : (family SM86Register) field unrestricted sm86IADD3ImmediateValue : (family SM86Unsigned32) field unrestricted sm86IADD3ImmediateControl : (family SM86Control) -- SASS IADD3 (register): destination = left + right, the three-input adder with one input zero. constructor SM86IntegerAddThreeRegister field unrestricted sm86IADD3RegisterDestination : (family SM86Register) field unrestricted sm86IADD3RegisterLeft : (family SM86Register) field unrestricted sm86IADD3RegisterRight : (family SM86Register) field unrestricted sm86IADD3RegisterControl : (family SM86Control) -- SASS SHF.R.U32.HI: destination = source logically shifted right by an immediate amount. constructor SM86ShiftRightImmediate field unrestricted sm86ShiftRightDestination : (family SM86Register) field unrestricted sm86ShiftRightSource : (family SM86Register) field unrestricted sm86ShiftRightAmount : Byte field unrestricted sm86ShiftRightControl : (family SM86Control) -- SASS LOP3.LUT: destination = truthTable(left, right, zero), any bitwise function of the inputs given as an 8-bit lookup table. constructor SM86LogicThreeInputTruthTable field unrestricted sm86Logic3Destination : (family SM86Register) field unrestricted sm86Logic3Left : (family SM86Register) field unrestricted sm86Logic3Right : (family SM86Register) field unrestricted sm86Logic3TruthTable : Byte field unrestricted sm86Logic3Control : (family SM86Control) -- SASS I2FP.F32.S32: destination = the signed 32-bit integer source converted to binary32. constructor SM86IntegerToFloat field unrestricted sm86IntegerToFloatDestination : (family SM86Register) field unrestricted sm86IntegerToFloatSource : (family SM86Register) field unrestricted sm86IntegerToFloatControl : (family SM86Control) -- SASS FADD: destination = left + right, binary32, round to nearest even. constructor SM86FloatAdd field unrestricted sm86FloatAddDestination : (family SM86Register) field unrestricted sm86FloatAddLeft : (family SM86Register) field unrestricted sm86FloatAddRight : (family SM86Register) field unrestricted sm86FloatAddControl : (family SM86Control) -- SASS FMUL: destination = left * right, binary32, round to nearest even. constructor SM86FloatMultiply field unrestricted sm86FloatMultiplyDestination : (family SM86Register) field unrestricted sm86FloatMultiplyLeft : (family SM86Register) field unrestricted sm86FloatMultiplyRight : (family SM86Register) field unrestricted sm86FloatMultiplyControl : (family SM86Control) -- SASS FFMA: destination = left * right + addend, binary32 with a single rounding. constructor SM86FloatFusedMultiplyAdd field unrestricted sm86FloatFMADestination : (family SM86Register) field unrestricted sm86FloatFMALeft : (family SM86Register) field unrestricted sm86FloatFMARight : (family SM86Register) field unrestricted sm86FloatFMAAddend : (family SM86Register) field unrestricted sm86FloatFMAControl : (family SM86Control) -- 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. constructor SM86MultiFunctionUnitApproximation field unrestricted sm86MultiFunctionDestination : (family SM86Register) field unrestricted sm86MultiFunctionSource : (family SM86Register) field unrestricted sm86MultiFunctionOperation : (family SM86MultiFunction) field unrestricted sm86MultiFunctionControl : (family SM86Control) -- SASS FMNMX: destination = the minimum or the maximum of left and right, binary32. constructor SM86FloatMinimumOrMaximum field unrestricted sm86FloatExtremumDestination : (family SM86Register) field unrestricted sm86FloatExtremumLeft : (family SM86Register) field unrestricted sm86FloatExtremumRight : (family SM86Register) field unrestricted sm86FloatExtremumMode : (family SM86FloatExtremum) field unrestricted sm86FloatExtremumControl : (family SM86Control) -- SASS FADD (negated source, zero addend): destination = -source, binary32. constructor SM86FloatNegate field unrestricted sm86FloatNegateDestination : (family SM86Register) field unrestricted sm86FloatNegateSource : (family SM86Register) field unrestricted sm86FloatNegateControl : (family SM86Control) -- SASS F2FP.PACK_AB: destination = two binary32 sources converted and packed into one register of two binary16 halves. constructor SM86FloatPairToPackedHalfPair field unrestricted sm86Float32PairToHalf2Destination : (family SM86Register) field unrestricted sm86Float32PairToHalf2SourceHigh : (family SM86Register) field unrestricted sm86Float32PairToHalf2SourceLow : (family SM86Register) field unrestricted sm86Float32PairToHalf2Control : (family SM86Control) -- SASS F2FP.BF16.PACK_AB: destination = two binary32 sources rounded to bfloat16 (to nearest, ties to even) and packed into one register. constructor SM86FloatPairToPackedBFloat16Pair field unrestricted sm86Float32PairToBFloat16PairDestination : (family SM86Register) field unrestricted sm86Float32PairToBFloat16PairSourceHigh : (family SM86Register) field unrestricted sm86Float32PairToBFloat16PairSourceLow : (family SM86Register) field unrestricted sm86Float32PairToBFloat16PairControl : (family SM86Control) -- SASS HADD2.F32: destination = the selected binary16 half of the source widened to binary32. constructor SM86HalfToFloat field unrestricted sm86HalfToFloatDestination : (family SM86Register) field unrestricted sm86HalfToFloatSource : (family SM86Register) field unrestricted sm86HalfToFloatSelector : (family SM86HalfSelector) field unrestricted sm86HalfToFloatControl : (family SM86Control) -- 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). constructor SM86BFloat16ToFloat field unrestricted sm86BFloat16ToFloatDestination : (family SM86Register) field unrestricted sm86BFloat16ToFloatSource : (family SM86Register) field unrestricted sm86BFloat16ToFloatSelector : (family SM86HalfSelector) field unrestricted sm86BFloat16ToFloatControl : (family SM86Control) -- SASS HMMA.16816.F32: destination = fragmentA (16x16, binary16) * fragmentB (16x8, binary16) + accumulator (16x8, binary32) on the tensor cores, one warp-wide 16x8x16 tile. constructor SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 field unrestricted sm86TensorCoreMatrixMultiplyAccumulateDestination : (family SM86Register) field unrestricted sm86TensorCoreMatrixMultiplyAccumulateFragmentA : (family SM86Register) field unrestricted sm86TensorCoreMatrixMultiplyAccumulateFragmentB : (family SM86Register) field unrestricted sm86TensorCoreMatrixMultiplyAccumulateAccumulator : (family SM86Register) field unrestricted sm86TensorCoreMatrixMultiplyAccumulateControl : (family SM86Control) -- SASS HMMA.16816.F32.BF16: the same tile product with bfloat16 fragments. constructor SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 field unrestricted sm86TensorCoreBFloat16Destination : (family SM86Register) field unrestricted sm86TensorCoreBFloat16FragmentA : (family SM86Register) field unrestricted sm86TensorCoreBFloat16FragmentB : (family SM86Register) field unrestricted sm86TensorCoreBFloat16Accumulator : (family SM86Register) field unrestricted sm86TensorCoreBFloat16Control : (family SM86Control) -- SASS LDG.E: destination = the 32-bit word at address + offset in global memory. constructor SM86LoadGlobal field unrestricted sm86LoadGlobalDestination : (family SM86Register) field unrestricted sm86LoadGlobalAddress : (family SM86Register) field unrestricted sm86LoadGlobalOffset : (family SM86Unsigned32) field unrestricted sm86LoadGlobalControl : (family SM86Control) -- SASS LDG.E.128: destination quad = the 128 bits at address + offset in global memory. constructor SM86LoadGlobalWide field unrestricted sm86LoadGlobalWideDestination : (family SM86Register) field unrestricted sm86LoadGlobalWideAddress : (family SM86Register) field unrestricted sm86LoadGlobalWideOffset : (family SM86Unsigned32) field unrestricted sm86LoadGlobalWideControl : (family SM86Control) -- SASS SHFL: destination = the source register of another lane of the warp, selected by index, up, down or butterfly mode. constructor SM86WarpShuffle field unrestricted sm86ShuffleDestination : (family SM86Register) field unrestricted sm86ShuffleSource : (family SM86Register) field unrestricted sm86ShuffleLane : Byte field unrestricted sm86ShuffleSegment : (family SM86Unsigned32) field unrestricted sm86ShuffleMode : (family SM86ShuffleMode) field unrestricted sm86ShuffleControl : (family SM86Control) -- SASS LDS: destination = the 32-bit word at address + offset in shared memory. constructor SM86LoadShared field unrestricted sm86LoadSharedDestination : (family SM86Register) field unrestricted sm86LoadSharedAddress : (family SM86Register) field unrestricted sm86LoadSharedOffset : (family SM86Unsigned32) field unrestricted sm86LoadSharedControl : (family SM86Control) -- SASS LDSM: destination = one, two or four 8x8 binary16 matrices loaded from shared memory into tensor-core fragment layout, optionally transposed. constructor SM86LoadSharedMatrix field unrestricted sm86LoadSharedMatrixDestination : (family SM86Register) field unrestricted sm86LoadSharedMatrixAddress : (family SM86Register) field unrestricted sm86LoadSharedMatrixOffset : (family SM86Unsigned32) field unrestricted sm86LoadSharedMatrixCount : (family SM86SharedMatrixCount) field unrestricted sm86LoadSharedMatrixTranspose : (family SM86SharedMatrixTranspose) field unrestricted sm86LoadSharedMatrixControl : (family SM86Control) -- SASS STS: the 32-bit value stored at address + offset in shared memory. constructor SM86StoreShared field unrestricted sm86StoreSharedAddress : (family SM86Register) field unrestricted sm86StoreSharedValue : (family SM86Register) field unrestricted sm86StoreSharedOffset : (family SM86Unsigned32) field unrestricted sm86StoreSharedControl : (family SM86Control) -- SASS LDGSTS.E.BYPASS.128 (cp.async.cg, 16 bytes): the 128 bits at global -- source + sourceOffset (a register pair; the offset a signed 12-bit -- immediate) copied to shared memory at address + offset, asynchronously: -- the copy joins the thread's open group (SM86CommitAsyncGroup closes it), -- and nothing may read those shared bytes until SM86WaitAsyncGroups has -- retired the group (and, for other threads, a BAR.SYNC after). Its -- registers are read after issue: a read barrier guards them. constructor SM86LoadGlobalToShared field unrestricted sm86LoadGlobalToSharedAddress : (family SM86Register) field unrestricted sm86LoadGlobalToSharedOffset : (family SM86Unsigned32) field unrestricted sm86LoadGlobalToSharedSource : (family SM86Register) field unrestricted sm86LoadGlobalToSharedSourceOffset : (family SM86Unsigned32) field unrestricted sm86LoadGlobalToSharedControl : (family SM86Control) -- SASS LDGDEPBAR (cp.async.commit_group): the thread's open group of -- asynchronous copies closed; the groups in flight count on scoreboard SB0, -- which the control's write barrier names. constructor SM86CommitAsyncGroup field unrestricted sm86CommitAsyncGroupControl : (family SM86Control) -- SASS DEPBAR.LE SB0, count (cp.async.wait_group count): wait until at -- most `count` (0..63) groups of asynchronous copies are in flight. constructor SM86WaitAsyncGroups field unrestricted sm86WaitAsyncGroupsCount : Byte field unrestricted sm86WaitAsyncGroupsControl : (family SM86Control) -- SASS BAR.SYNC: every thread of the cooperative thread array waits until all have arrived. constructor SM86BarrierSynchronize field unrestricted sm86BarrierSynchronizeControl : (family SM86Control) -- SASS STG.E: the 32-bit value stored at address + offset in global memory. constructor SM86StoreGlobal field unrestricted sm86StoreGlobalAddress : (family SM86Register) field unrestricted sm86StoreGlobalValue : (family SM86Register) field unrestricted sm86StoreGlobalOffset : (family SM86Unsigned32) field unrestricted sm86StoreGlobalControl : (family SM86Control) -- SASS STG.E.128: the 128-bit value quad stored at address + offset in global memory. constructor SM86StoreGlobalWide field unrestricted sm86StoreGlobalWideAddress : (family SM86Register) field unrestricted sm86StoreGlobalWideValue : (family SM86Register) field unrestricted sm86StoreGlobalWideOffset : (family SM86Unsigned32) field unrestricted sm86StoreGlobalWideControl : (family SM86Control) -- SASS STG.E.64: the 64-bit value pair stored at address + offset in global memory. constructor SM86StoreGlobal64 field unrestricted sm86StoreGlobal64Address : (family SM86Register) field unrestricted sm86StoreGlobal64Value : (family SM86Register) field unrestricted sm86StoreGlobal64Offset : (family SM86Unsigned32) field unrestricted sm86StoreGlobal64Control : (family SM86Control) -- SASS RED.E.ADD.F32: the binary32 value atomically added to the word at address + offset in global memory, no result returned. constructor SM86ReduceGlobalAddFloat32 field unrestricted sm86ReduceGlobalAddress : (family SM86Register) field unrestricted sm86ReduceGlobalValue : (family SM86Register) field unrestricted sm86ReduceGlobalOffset : (family SM86Unsigned32) field unrestricted sm86ReduceGlobalControl : (family SM86Control) -- SASS ISETP.GT (immediate): destination predicate = source > immediate, compared as -- unsigned 32-bit words in this encoding: the RTX 3070 has 0x80000000 > 0 -- (Checked.IntegerCompareProbe, Proof.CheckedIntegerCompareSilicon). constructor SM86PredicateGreaterThanImmediate field unrestricted sm86PredicateGreaterDestination : (family SM86Predicate) field unrestricted sm86PredicateGreaterSource : (family SM86Register) field unrestricted sm86PredicateGreaterImmediate : (family SM86Unsigned32) field unrestricted sm86PredicateGreaterControl : (family SM86Control) -- SASS BRA: continue at the instruction offset bytes away, relative to the next instruction. constructor SM86Branch field unrestricted sm86BranchOffset : (family SM86Unsigned32) field unrestricted sm86BranchDescriptor : (family SM86Unsigned32) field unrestricted sm86BranchControl : (family SM86Control) -- SASS EXIT: this thread finishes the program. constructor SM86Exit field unrestricted sm86ExitControl : (family SM86Control) end-family family SM86Instruction : Type 0 constructor SM86InstructionValue field unrestricted sm86InstructionGuard : (family SM86InstructionGuard) field unrestricted sm86InstructionBody : (family SM86InstructionBody) end-family family SM86Program : Type 0 constructor SM86ProgramEnd constructor SM86ProgramNext field unrestricted sm86ProgramHead : (family SM86Instruction) recursive unrestricted sm86ProgramTail end-family def sm86Instruction = (lambda unrestricted body : (family SM86InstructionBody) . (constructor SM86Instruction SM86InstructionValue (constructor SM86InstructionGuard SM86InstructionAlways) body)) def sm86PredicatedInstruction = (lambda unrestricted predicate : (family SM86Predicate) . (lambda unrestricted body : (family SM86InstructionBody) . (constructor SM86Instruction SM86InstructionValue (constructor SM86InstructionGuard SM86InstructionWhen predicate) body))) def sm86NegatedPredicatedInstruction = (lambda unrestricted predicate : (family SM86Predicate) . (lambda unrestricted body : (family SM86InstructionBody) . (constructor SM86Instruction SM86InstructionValue (constructor SM86InstructionGuard SM86InstructionWhenNot predicate) body)))