Accelerator.SM86.Operands

1module Accelerator.SM86.Operands
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.Types
7import Std.List
8import Std.Natural
9
10-- The registers each instruction reads and writes, and the register demand
11-- of a program: one owner for both the scoreboard pass (SM86.Scoreboard) and
12-- the register count a launch declares.  A 64-bit address or value occupies
13-- the named register and the next; the tensor core's A, C and D fragments
14-- are four registers from the named one and its B fragment two; LDSM writes
15-- one, two or four.  RZ (255) is not a register: it reads zero, absorbs
16-- writes, and a fragment based at it names nothing.
17--
18-- The demand: the highest register named, plus one.  A launch's allocation
19-- is the demand plus TWO the hardware reserves, rounded up to the
20-- allocation granule of eight; the QMD encoders add the reservation (the
21-- runtime's SM86 QMD V03, NvidiaQMD5 for sm_121), the one place it is
22-- counted, as they do for the counts the register allocator
23-- (NvidiaDeviceAllocatedProgramRegion) and literal region counts declare.
24-- Found on an RTX 3070 (2026-09-23): the generated linear step at 2 x 6,
25-- 6 x 2 and 4 x 4 -- every shape whose allocation left exactly one register
26-- above the highest named -- hung on the card with the GPU at 100 %,
27-- deterministically, while every shape with two or more to spare ran;
28-- allocating the two reserved registers made all three run.  The machine
29-- model cannot see it.  (Until 2026-10-09 the demand itself included the
30-- two and the granule and the encoder added them again: every program
31-- region was allocated eight registers more than it needed, and no program
32-- could name more than 246.)
33
34-- ---- one elimination per instruction ----
35-- The schedule tools (SM86.Scoreboard's two passes,
36-- Realization.Nvidia.SM86.StallCompaction) used to eliminate every
37-- instruction body five or more times -- reads, writes, predicate writes,
38-- latency class, fixed latency -- one 37-branch case split each.  The
39-- summary answers them all in one split: each field below is the same
40-- branch body the corresponding function above uses, tupled, so every
41-- field is definitionally the old answer and a pass walks each
42-- instruction's body once instead of five times.
43family SM86OpSummary : Type 0
44constructor SM86OpSummaryValue
45field unrestricted sm86OpSummaryReads : (family StdList Nat)
46field unrestricted sm86OpSummaryWrites : (family StdList Nat)
47field unrestricted sm86OpSummaryPredicateWrites : (family StdList Nat)
48field unrestricted sm86OpSummaryWaitKeys : (family StdList Nat)
49field unrestricted sm86OpSummarySetKeys : (family StdList Nat)
50field unrestricted sm86OpSummaryStall : Nat
51field unrestricted sm86OpSummaryLatency : Nat
52field unrestricted sm86OpSummaryVariable : Nat
53-- sm86MinimumStall's
54field unrestricted sm86OpSummaryMinimumStall : Nat
55field unrestricted sm86OpSummaryControl : (family SM86Control)
56end-family
57
58def sm86RegisterZero : Nat = 255
59def sm86RegisterGranule : Nat = 8
60def sm86ReservedRegisters : Nat = 2
61
62-- The most registers a thread's allocation holds: 256 (the QMD's count
63-- in granules; CUDA's own kernels on the RTX 3070 name up to R253 and are
64-- allocated 256, e.g. cuBLAS's 254-register s1688 products).  A register
65-- index is a byte, so a generator that numbers registers past it does not
66-- fail -- its indices wrap onto registers already in use; a generator
67-- states its span and is admitted against this.
68def sm86RegisterLimit : Nat = 256
69
70-- 1 when a program naming registers below `span` fits the register file
71-- with the reserved two
72def sm86RegisterSpanAdmitted =
73  (lambda unrestricted span : Nat .
74    (naturalLessOrEqual (naturalAdd span sm86ReservedRegisters) sm86RegisterLimit))
75
76def sm86RegisterIndex =
77  (lambda unrestricted register : (family SM86Register) .
78    (eliminate SM86Register (lambda unrestricted current : (family SM86Register) . Nat) register
79      (branch SM86RegisterValue index . (byte-to-nat index))))
80
81def sm86NoRegisters : (family StdList Nat) = (constructor StdList StdListEmpty Nat)
82
83-- `count` consecutive registers from `register`, prepended; none from RZ
84def sm86RegisterRun =
85  (lambda unrestricted register : (family SM86Register) .
86    (lambda unrestricted count : Nat .
87      (lambda unrestricted rest : (family StdList Nat) .
88        (let unrestricted index = (sm86RegisterIndex register) in
89        (nat-eliminate
90          (lambda unrestricted current : Nat . (family StdList Nat))
91          rest
92          (lambda unrestricted named : Nat . (lambda unrestricted ignored : (family StdList Nat) .
93            (nat-eliminate
94              (lambda unrestricted current : Nat . (family StdList Nat))
95              rest
96              (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family StdList Nat) .
97                (constructor StdList StdListCons Nat
98                  (nat-add index (nat-subtract (nat-subtract count 1) predecessor))
99                  induction)))
100              count)))
101          (nat-add (nat-less-than index sm86RegisterZero) (nat-less-than sm86RegisterZero index)))))))
102
103def sm86One = (lambda unrestricted register : (family SM86Register) . (lambda unrestricted rest : (family StdList Nat) . (sm86RegisterRun register 1 rest)))
104def sm86Pair = (lambda unrestricted register : (family SM86Register) . (lambda unrestricted rest : (family StdList Nat) . (sm86RegisterRun register 2 rest)))
105def sm86Quad = (lambda unrestricted register : (family SM86Register) . (lambda unrestricted rest : (family StdList Nat) . (sm86RegisterRun register 4 rest)))
106
107def sm86SharedMatrixRegisters =
108  (lambda unrestricted count : (family SM86SharedMatrixCount) .
109    (eliminate SM86SharedMatrixCount (lambda unrestricted current : (family SM86SharedMatrixCount) . Nat) count
110      (branch SM86SharedMatrix1 . 1)
111      (branch SM86SharedMatrix2 . 2)
112      (branch SM86SharedMatrix4 . 4)))
113
114-- Conversion dependencies follow the typed endpoint widths, including the
115-- upper source word of a narrowing operation and both widening result words.
116def sm86ConversionReads =
117  (lambda unrestricted conversion : (family SM86FloatConversion) .
118    (eliminate SM86FloatConversion (lambda unrestricted current : (family SM86FloatConversion) . (family StdList Nat)) conversion
119      (branch SM86NarrowBinary64 destination source . (sm86Pair (sm86RegisterPairBase source) sm86NoRegisters))
120      (branch SM86WidenBinary32 destination source . (sm86One source sm86NoRegisters))))
121def sm86ConversionWrites =
122  (lambda unrestricted conversion : (family SM86FloatConversion) .
123    (eliminate SM86FloatConversion (lambda unrestricted current : (family SM86FloatConversion) . (family StdList Nat)) conversion
124      (branch SM86NarrowBinary64 destination source . (sm86One destination sm86NoRegisters))
125      (branch SM86WidenBinary32 destination source . (sm86Pair (sm86RegisterPairBase destination) sm86NoRegisters))))
126
127def sm86ReadRegisters =
128  (lambda unrestricted body : (family SM86InstructionBody) .
129    (eliminate SM86InstructionBody
130      (lambda unrestricted current : (family SM86InstructionBody) . (family StdList Nat))
131      body
132      (branch SM86MoveConstant destination bank offset control . sm86NoRegisters)
133      (branch SM86SpecialToRegister destination source control . sm86NoRegisters)
134      (branch SM86MoveImmediate destination immediate control . sm86NoRegisters)
135      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (sm86One left (sm86One addend sm86NoRegisters)))
136      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (sm86One left (sm86One addend sm86NoRegisters)))
137      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (sm86One left (sm86One right sm86NoRegisters)))
138      (branch SM86IntegerAddThreeImmediate destination left immediate control . (sm86One left sm86NoRegisters))
139      (branch SM86IntegerAddThreeRegister destination left right control . (sm86One left (sm86One right sm86NoRegisters)))
140      (branch SM86ShiftRightImmediate destination source amount control . (sm86One source sm86NoRegisters))
141      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (sm86One left (sm86One right sm86NoRegisters)))
142      (branch SM86IntegerToFloat destination source control . (sm86One source sm86NoRegisters))
143      (branch SM86FloatAdd destination left right control . (sm86One left (sm86One right sm86NoRegisters)))
144      (branch SM86FloatMultiply destination left right control . (sm86One left (sm86One right sm86NoRegisters)))
145      (branch SM86Float64Binary operation destination left right control . (sm86Pair (sm86RegisterPairBase left) (sm86Pair (sm86RegisterPairBase right) sm86NoRegisters)))
146      (branch SM86FloatConvert conversion control . (sm86ConversionReads conversion))
147      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (sm86One left (sm86One right (sm86One addend sm86NoRegisters))))
148      (branch SM86MultiFunctionUnitApproximation destination source operation control . (sm86One source sm86NoRegisters))
149      (branch SM86FloatMinimumOrMaximum destination left right mode control . (sm86One left (sm86One right sm86NoRegisters)))
150      (branch SM86FloatNegate destination source control . (sm86One source sm86NoRegisters))
151      (branch SM86FloatPairToPackedHalfPair destination high low control . (sm86One high (sm86One low sm86NoRegisters)))
152      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (sm86One high (sm86One low sm86NoRegisters)))
153      (branch SM86FloatPairToPackedFloat8Pair destination high low merge half format control . (sm86One high (sm86One low (sm86One merge sm86NoRegisters))))
154      (branch SM86FloatArithmetic operation destination left right addend modifiers control . (sm86One left (sm86One right (sm86One addend sm86NoRegisters))))
155      (branch SM86HalfToFloat destination source selector control . (sm86One source sm86NoRegisters))
156      (branch SM86BFloat16ToFloat destination source selector control . (sm86One source sm86NoRegisters))
157      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
158        (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))))
159      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
160        (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))))
161      (branch SM86LoadGlobal destination address offset control . (sm86Pair address sm86NoRegisters))
162      (branch SM86LoadGlobalWide destination address offset control . (sm86Pair address sm86NoRegisters))
163      (branch SM86WarpShuffle destination source lane segment mode control . (sm86One source sm86NoRegisters))
164      (branch SM86LoadShared destination address offset control . (sm86One address sm86NoRegisters))
165      (branch SM86LoadSharedMatrix destination address offset count transpose control . (sm86One address sm86NoRegisters))
166      (branch SM86StoreShared address value offset control . (sm86One address (sm86One value sm86NoRegisters)))
167      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (sm86One address (sm86Pair source sm86NoRegisters)))
168      (branch SM86CommitAsyncGroup control . sm86NoRegisters)
169      (branch SM86WaitAsyncGroups count control . sm86NoRegisters)
170      (branch SM86BarrierSynchronize control . sm86NoRegisters)
171      (branch SM86BarrierSynchronizeCount barrier threads control . sm86NoRegisters)
172      (branch SM86StoreGlobal address value offset control . (sm86Pair address (sm86One value sm86NoRegisters)))
173      (branch SM86StoreGlobalWide address value offset control . (sm86Pair address (sm86Quad value sm86NoRegisters)))
174      (branch SM86StoreGlobal64 address value offset control . (sm86Pair address (sm86Pair value sm86NoRegisters)))
175      (branch SM86ReduceGlobalAddFloat32 address value offset control . (sm86Pair address (sm86One value sm86NoRegisters)))
176      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (sm86One source sm86NoRegisters))
177      (branch SM86Branch offset descriptor control . sm86NoRegisters)
178      (branch SM86Exit control . sm86NoRegisters)))
179
180def sm86WriteRegisters =
181  (lambda unrestricted body : (family SM86InstructionBody) .
182    (eliminate SM86InstructionBody
183      (lambda unrestricted current : (family SM86InstructionBody) . (family StdList Nat))
184      body
185      (branch SM86MoveConstant destination bank offset control . (sm86One destination sm86NoRegisters))
186      (branch SM86SpecialToRegister destination source control . (sm86One destination sm86NoRegisters))
187      (branch SM86MoveImmediate destination immediate control . (sm86One destination sm86NoRegisters))
188      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (sm86One destination sm86NoRegisters))
189      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (sm86One destination sm86NoRegisters))
190      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (sm86Pair destination sm86NoRegisters))
191      (branch SM86IntegerAddThreeImmediate destination left immediate control . (sm86One destination sm86NoRegisters))
192      (branch SM86IntegerAddThreeRegister destination left right control . (sm86One destination sm86NoRegisters))
193      (branch SM86ShiftRightImmediate destination source amount control . (sm86One destination sm86NoRegisters))
194      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (sm86One destination sm86NoRegisters))
195      (branch SM86IntegerToFloat destination source control . (sm86One destination sm86NoRegisters))
196      (branch SM86FloatAdd destination left right control . (sm86One destination sm86NoRegisters))
197      (branch SM86FloatMultiply destination left right control . (sm86One destination sm86NoRegisters))
198      (branch SM86Float64Binary operation destination left right control . (sm86Pair (sm86RegisterPairBase destination) sm86NoRegisters))
199      (branch SM86FloatConvert conversion control . (sm86ConversionWrites conversion))
200      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (sm86One destination sm86NoRegisters))
201      (branch SM86MultiFunctionUnitApproximation destination source operation control . (sm86One destination sm86NoRegisters))
202      (branch SM86FloatMinimumOrMaximum destination left right mode control . (sm86One destination sm86NoRegisters))
203      (branch SM86FloatNegate destination source control . (sm86One destination sm86NoRegisters))
204      (branch SM86FloatPairToPackedHalfPair destination high low control . (sm86One destination sm86NoRegisters))
205      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (sm86One destination sm86NoRegisters))
206      (branch SM86FloatPairToPackedFloat8Pair destination high low merge half format control . (sm86One destination sm86NoRegisters))
207      (branch SM86FloatArithmetic operation destination left right addend modifiers control . (sm86One destination sm86NoRegisters))
208      (branch SM86HalfToFloat destination source selector control . (sm86One destination sm86NoRegisters))
209      (branch SM86BFloat16ToFloat destination source selector control . (sm86One destination sm86NoRegisters))
210      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86Quad destination sm86NoRegisters))
211      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86Quad destination sm86NoRegisters))
212      (branch SM86LoadGlobal destination address offset control . (sm86One destination sm86NoRegisters))
213      (branch SM86LoadGlobalWide destination address offset control . (sm86Quad destination sm86NoRegisters))
214      (branch SM86WarpShuffle destination source lane segment mode control . (sm86One destination sm86NoRegisters))
215      (branch SM86LoadShared destination address offset control . (sm86One destination sm86NoRegisters))
216      (branch SM86LoadSharedMatrix destination address offset count transpose control .
217        (sm86RegisterRun destination (sm86SharedMatrixRegisters count) sm86NoRegisters))
218      (branch SM86StoreShared address value offset control . sm86NoRegisters)
219      (branch SM86LoadGlobalToShared address offset source sourceOffset control . sm86NoRegisters)
220      (branch SM86CommitAsyncGroup control . sm86NoRegisters)
221      (branch SM86WaitAsyncGroups count control . sm86NoRegisters)
222      (branch SM86BarrierSynchronize control . sm86NoRegisters)
223      (branch SM86BarrierSynchronizeCount barrier threads control . sm86NoRegisters)
224      (branch SM86StoreGlobal address value offset control . sm86NoRegisters)
225      (branch SM86StoreGlobalWide address value offset control . sm86NoRegisters)
226      (branch SM86StoreGlobal64 address value offset control . sm86NoRegisters)
227      (branch SM86ReduceGlobalAddFloat32 address value offset control . sm86NoRegisters)
228      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . sm86NoRegisters)
229      (branch SM86Branch offset descriptor control . sm86NoRegisters)
230      (branch SM86Exit control . sm86NoRegisters)))
231
232def sm86InstructionBodyOf =
233  (lambda unrestricted instruction : (family SM86Instruction) .
234    (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . (family SM86InstructionBody)) instruction
235      (branch SM86InstructionValue guard body . body)))
236
237-- one past the highest of the values, or start if that is higher
238def sm86SpanOf =
239  (lambda unrestricted values : (family StdList Nat) . (lambda unrestricted start : Nat .
240    (eliminate StdList (lambda unrestricted current : (family StdList Nat) . Nat) values
241      (branch StdListEmpty . start)
242      (branch StdListCons head tail induction . (naturalSelect (naturalLess induction (succ head)) (succ head) induction)))))
243
244-- one past the highest register the program names (0 for none)
245def sm86RegisterSpan =
246  (lambda unrestricted program : (family SM86Program) .
247    (eliminate SM86Program (lambda unrestricted current : (family SM86Program) . Nat) program
248      (branch SM86ProgramEnd . 0)
249      (branch SM86ProgramNext head tail induction .
250        (sm86SpanOf (sm86ReadRegisters (sm86InstructionBodyOf head))
251          (sm86SpanOf (sm86WriteRegisters (sm86InstructionBodyOf head)) induction)))))
252
253-- the register count a launch of the program declares: the registers it
254-- names (the QMD encoder adds the reserved two and rounds to the granule)
255def sm86RegisterDemand =
256  (lambda unrestricted program : (family SM86Program) . (sm86RegisterSpan program))
257-- the registers a thread of a launch declaring `demand` is allocated
258def sm86RegisterAllocation =
259  (lambda unrestricted demand : Nat .
260    (naturalMultiply sm86RegisterGranule
261      (naturalDivideUnchecked
262        (naturalAdd (naturalAdd demand sm86ReservedRegisters) (naturalSaturatingSubtract sm86RegisterGranule 1))
263        sm86RegisterGranule)))
264
265-- ---- control words, predicates as hazard keys, fixed latency ----
266
267-- an instruction body's control word
268def sm86BodyControlOf =
269  (lambda unrestricted body : (family SM86InstructionBody) .
270    (eliminate SM86InstructionBody
271      (lambda unrestricted current : (family SM86InstructionBody) . (family SM86Control))
272      body
273      (branch SM86MoveConstant destination bank offset control . control)
274      (branch SM86SpecialToRegister destination source control . control)
275      (branch SM86MoveImmediate destination immediate control . control)
276      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . control)
277      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . control)
278      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . control)
279      (branch SM86IntegerAddThreeImmediate destination left immediate control . control)
280      (branch SM86IntegerAddThreeRegister destination left right control . control)
281      (branch SM86ShiftRightImmediate destination source amount control . control)
282      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . control)
283      (branch SM86IntegerToFloat destination source control . control)
284      (branch SM86FloatAdd destination left right control . control)
285      (branch SM86FloatMultiply destination left right control . control)
286      (branch SM86Float64Binary operation destination left right control . control)
287      (branch SM86FloatConvert conversion control . control)
288      (branch SM86FloatFusedMultiplyAdd destination left right addend control . control)
289      (branch SM86MultiFunctionUnitApproximation destination source operation control . control)
290      (branch SM86FloatMinimumOrMaximum destination left right mode control . control)
291      (branch SM86FloatNegate destination source control . control)
292      (branch SM86FloatPairToPackedHalfPair destination high low control . control)
293      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . control)
294      (branch SM86FloatPairToPackedFloat8Pair destination high low merge half format control . control)
295      (branch SM86FloatArithmetic operation destination left right addend modifiers control . control)
296      (branch SM86HalfToFloat destination source selector control . control)
297      (branch SM86BFloat16ToFloat destination source selector control . control)
298      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . control)
299      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . control)
300      (branch SM86LoadGlobal destination address offset control . control)
301      (branch SM86LoadGlobalWide destination address offset control . control)
302      (branch SM86WarpShuffle destination source lane segment mode control . control)
303      (branch SM86LoadShared destination address offset control . control)
304      (branch SM86LoadSharedMatrix destination address offset count transpose control . control)
305      (branch SM86StoreShared address value offset control . control)
306      (branch SM86LoadGlobalToShared address offset source sourceOffset control . control)
307      (branch SM86CommitAsyncGroup control . control)
308      (branch SM86WaitAsyncGroups count control . control)
309      (branch SM86BarrierSynchronize control . control)
310      (branch SM86BarrierSynchronizeCount barrier threads control . control)
311      (branch SM86StoreGlobal address value offset control . control)
312      (branch SM86StoreGlobalWide address value offset control . control)
313      (branch SM86StoreGlobal64 address value offset control . control)
314      (branch SM86ReduceGlobalAddFloat32 address value offset control . control)
315      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . control)
316      (branch SM86Branch offset descriptor control . control)
317      (branch SM86Exit control . control)))
318
319-- the body with another control word
320def sm86BodyWithControl =
321  (lambda unrestricted body : (family SM86InstructionBody) .
322    (lambda unrestricted replacement : (family SM86Control) .
323      (eliminate SM86InstructionBody
324        (lambda unrestricted current : (family SM86InstructionBody) . (family SM86InstructionBody))
325        body
326      (branch SM86MoveConstant destination bank offset control . (constructor SM86InstructionBody SM86MoveConstant destination bank offset replacement))
327      (branch SM86SpecialToRegister destination source control . (constructor SM86InstructionBody SM86SpecialToRegister destination source replacement))
328      (branch SM86MoveImmediate destination immediate control . (constructor SM86InstructionBody SM86MoveImmediate destination immediate replacement))
329      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddConstant destination left bank offset addend replacement))
330      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate destination left immediate addend replacement))
331      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant destination left right bank offset replacement))
332      (branch SM86IntegerAddThreeImmediate destination left immediate control . (constructor SM86InstructionBody SM86IntegerAddThreeImmediate destination left immediate replacement))
333      (branch SM86IntegerAddThreeRegister destination left right control . (constructor SM86InstructionBody SM86IntegerAddThreeRegister destination left right replacement))
334      (branch SM86ShiftRightImmediate destination source amount control . (constructor SM86InstructionBody SM86ShiftRightImmediate destination source amount replacement))
335      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (constructor SM86InstructionBody SM86LogicThreeInputTruthTable destination left right truthTable replacement))
336      (branch SM86IntegerToFloat destination source control . (constructor SM86InstructionBody SM86IntegerToFloat destination source replacement))
337      (branch SM86FloatAdd destination left right control . (constructor SM86InstructionBody SM86FloatAdd destination left right replacement))
338      (branch SM86FloatMultiply destination left right control . (constructor SM86InstructionBody SM86FloatMultiply destination left right replacement))
339      (branch SM86Float64Binary operation destination left right control . (constructor SM86InstructionBody SM86Float64Binary operation destination left right replacement))
340      (branch SM86FloatConvert conversion control . (constructor SM86InstructionBody SM86FloatConvert conversion replacement))
341      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd destination left right addend replacement))
342      (branch SM86MultiFunctionUnitApproximation destination source operation control . (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation destination source operation replacement))
343      (branch SM86FloatMinimumOrMaximum destination left right mode control . (constructor SM86InstructionBody SM86FloatMinimumOrMaximum destination left right mode replacement))
344      (branch SM86FloatNegate destination source control . (constructor SM86InstructionBody SM86FloatNegate destination source replacement))
345      (branch SM86FloatPairToPackedHalfPair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedHalfPair destination high low replacement))
346      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedBFloat16Pair destination high low replacement))
347      (branch SM86FloatPairToPackedFloat8Pair destination high low merge half format control . (constructor SM86InstructionBody SM86FloatPairToPackedFloat8Pair destination high low merge half format replacement))
348      (branch SM86FloatArithmetic operation destination left right addend modifiers control . (constructor SM86InstructionBody SM86FloatArithmetic operation destination left right addend modifiers replacement))
349      (branch SM86HalfToFloat destination source selector control . (constructor SM86InstructionBody SM86HalfToFloat destination source selector replacement))
350      (branch SM86BFloat16ToFloat destination source selector control . (constructor SM86InstructionBody SM86BFloat16ToFloat destination source selector replacement))
351      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator replacement))
352      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator replacement))
353      (branch SM86LoadGlobal destination address offset control . (constructor SM86InstructionBody SM86LoadGlobal destination address offset replacement))
354      (branch SM86LoadGlobalWide destination address offset control . (constructor SM86InstructionBody SM86LoadGlobalWide destination address offset replacement))
355      (branch SM86WarpShuffle destination source lane segment mode control . (constructor SM86InstructionBody SM86WarpShuffle destination source lane segment mode replacement))
356      (branch SM86LoadShared destination address offset control . (constructor SM86InstructionBody SM86LoadShared destination address offset replacement))
357      (branch SM86LoadSharedMatrix destination address offset count transpose control . (constructor SM86InstructionBody SM86LoadSharedMatrix destination address offset count transpose replacement))
358      (branch SM86StoreShared address value offset control . (constructor SM86InstructionBody SM86StoreShared address value offset replacement))
359      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (constructor SM86InstructionBody SM86LoadGlobalToShared address offset source sourceOffset replacement))
360      (branch SM86CommitAsyncGroup control . (constructor SM86InstructionBody SM86CommitAsyncGroup replacement))
361      (branch SM86WaitAsyncGroups count control . (constructor SM86InstructionBody SM86WaitAsyncGroups count replacement))
362      (branch SM86BarrierSynchronize control . (constructor SM86InstructionBody SM86BarrierSynchronize replacement))
363      (branch SM86BarrierSynchronizeCount barrier threads control . (constructor SM86InstructionBody SM86BarrierSynchronizeCount barrier threads replacement))
364      (branch SM86StoreGlobal address value offset control . (constructor SM86InstructionBody SM86StoreGlobal address value offset replacement))
365      (branch SM86StoreGlobalWide address value offset control . (constructor SM86InstructionBody SM86StoreGlobalWide address value offset replacement))
366      (branch SM86StoreGlobal64 address value offset control . (constructor SM86InstructionBody SM86StoreGlobal64 address value offset replacement))
367      (branch SM86ReduceGlobalAddFloat32 address value offset control . (constructor SM86InstructionBody SM86ReduceGlobalAddFloat32 address value offset replacement))
368      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate predicate source immediate replacement))
369      (branch SM86Branch offset descriptor control . (constructor SM86InstructionBody SM86Branch offset descriptor replacement))
370      (branch SM86Exit control . (constructor SM86InstructionBody SM86Exit replacement)))))
371
372def sm86ControlStallOf =
373  (lambda unrestricted control : (family SM86Control) .
374    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . Nat) control
375      (branch SM86ControlValue stall yield write read wait reuse . (byte-to-nat stall))))
376
377def sm86ControlWithStall =
378  (lambda unrestricted control : (family SM86Control) . (lambda unrestricted stall : Nat .
379    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . (family SM86Control)) control
380      (branch SM86ControlValue old yield write read wait reuse .
381        (constructor SM86Control SM86ControlValue (nat-to-byte stall) yield write read wait reuse)))))
382
383-- A predicate as a hazard key beside the registers: 256 + its index (P0 ..
384-- P6; PT, which reads true and absorbs writes, is none).
385def sm86PredicateKeys =
386  (lambda unrestricted predicate : (family SM86Predicate) .
387    (eliminate SM86Predicate (lambda unrestricted current : (family SM86Predicate) . (family StdList Nat)) predicate
388      (branch SM86Predicate0 . (constructor StdList StdListCons Nat 256 sm86NoRegisters))
389      (branch SM86Predicate1 . (constructor StdList StdListCons Nat 257 sm86NoRegisters))
390      (branch SM86Predicate2 . (constructor StdList StdListCons Nat 258 sm86NoRegisters))
391      (branch SM86Predicate3 . (constructor StdList StdListCons Nat 259 sm86NoRegisters))
392      (branch SM86Predicate4 . (constructor StdList StdListCons Nat 260 sm86NoRegisters))
393      (branch SM86Predicate5 . (constructor StdList StdListCons Nat 261 sm86NoRegisters))
394      (branch SM86Predicate6 . (constructor StdList StdListCons Nat 262 sm86NoRegisters))
395      (branch SM86PredicateTrue . sm86NoRegisters)))
396
397-- the predicate an instruction's guard reads
398def sm86GuardKeys =
399  (lambda unrestricted instruction : (family SM86Instruction) .
400    (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . (family StdList Nat)) instruction
401      (branch SM86InstructionValue guard body .
402        (eliminate SM86InstructionGuard (lambda unrestricted current : (family SM86InstructionGuard) . (family StdList Nat)) guard
403          (branch SM86InstructionAlways . sm86NoRegisters)
404          (branch SM86InstructionWhen predicate . (sm86PredicateKeys predicate))
405          (branch SM86InstructionWhenNot predicate . (sm86PredicateKeys predicate))))))
406
407-- the predicate a body writes
408def sm86PredicateWriteKeys =
409  (lambda unrestricted body : (family SM86InstructionBody) .
410    (eliminate SM86InstructionBody (lambda unrestricted current : (family SM86InstructionBody) . (family StdList Nat)) body
411      (branch SM86MoveConstant destination bank offset control . sm86NoRegisters)
412      (branch SM86SpecialToRegister destination source control . sm86NoRegisters)
413      (branch SM86MoveImmediate destination immediate control . sm86NoRegisters)
414      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . sm86NoRegisters)
415      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . sm86NoRegisters)
416      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . sm86NoRegisters)
417      (branch SM86IntegerAddThreeImmediate destination left immediate control . sm86NoRegisters)
418      (branch SM86IntegerAddThreeRegister destination left right control . sm86NoRegisters)
419      (branch SM86ShiftRightImmediate destination source amount control . sm86NoRegisters)
420      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . sm86NoRegisters)
421      (branch SM86IntegerToFloat destination source control . sm86NoRegisters)
422      (branch SM86FloatAdd destination left right control . sm86NoRegisters)
423      (branch SM86FloatMultiply destination left right control . sm86NoRegisters)
424      (branch SM86Float64Binary operation destination left right control . sm86NoRegisters)
425      (branch SM86FloatConvert conversion control . sm86NoRegisters)
426      (branch SM86FloatFusedMultiplyAdd destination left right addend control . sm86NoRegisters)
427      (branch SM86MultiFunctionUnitApproximation destination source operation control . sm86NoRegisters)
428      (branch SM86FloatMinimumOrMaximum destination left right mode control . sm86NoRegisters)
429      (branch SM86FloatNegate destination source control . sm86NoRegisters)
430      (branch SM86FloatPairToPackedHalfPair destination high low control . sm86NoRegisters)
431      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . sm86NoRegisters)
432      (branch SM86FloatPairToPackedFloat8Pair destination high low merge half format control . sm86NoRegisters)
433      (branch SM86FloatArithmetic operation destination left right addend modifiers control . sm86NoRegisters)
434      (branch SM86HalfToFloat destination source selector control . sm86NoRegisters)
435      (branch SM86BFloat16ToFloat destination source selector control . sm86NoRegisters)
436      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . sm86NoRegisters)
437      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . sm86NoRegisters)
438      (branch SM86LoadGlobal destination address offset control . sm86NoRegisters)
439      (branch SM86LoadGlobalWide destination address offset control . sm86NoRegisters)
440      (branch SM86WarpShuffle destination source lane segment mode control . sm86NoRegisters)
441      (branch SM86LoadShared destination address offset control . sm86NoRegisters)
442      (branch SM86LoadSharedMatrix destination address offset count transpose control . sm86NoRegisters)
443      (branch SM86StoreShared address value offset control . sm86NoRegisters)
444      (branch SM86LoadGlobalToShared address offset source sourceOffset control . sm86NoRegisters)
445      (branch SM86CommitAsyncGroup control . sm86NoRegisters)
446      (branch SM86WaitAsyncGroups count control . sm86NoRegisters)
447      (branch SM86BarrierSynchronize control . sm86NoRegisters)
448      (branch SM86BarrierSynchronizeCount barrier threads control . sm86NoRegisters)
449      (branch SM86StoreGlobal address value offset control . sm86NoRegisters)
450      (branch SM86StoreGlobalWide address value offset control . sm86NoRegisters)
451      (branch SM86StoreGlobal64 address value offset control . sm86NoRegisters)
452      (branch SM86ReduceGlobalAddFloat32 address value offset control . sm86NoRegisters)
453      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (sm86PredicateKeys predicate))
454      (branch SM86Branch offset descriptor control . sm86NoRegisters)
455      (branch SM86Exit control . sm86NoRegisters)))
456
457-- ASSUMED, and stated as an assumption: the cycles after issue before a
458-- fixed-latency form's destination (register or predicate) may be read --
459-- 6 for every such form, above the 4 published for Ampere's FP32 and
460-- integer pipes.  Variable-latency forms (loads, S2R, SHFL, MUFU, HMMA)
461-- deliver through a scoreboard barrier instead, and forms with no
462-- destination deliver nothing (0).  A program accepted under this table
463-- that a card computes wrongly refutes it: silicon runs of stall-compacted
464-- programs are its evidence.
465def sm86FixedLatencyCycles : Nat = 6
466
467-- HMMA.16816.F32: a fixed-latency result, as ptxas schedules it for sm_86
468-- (no scoreboard; a dependent HMMA 24 cycles after its producer, a store
469-- of the result 23 -- nvdisasm -hex of a dependent mma.sync chain on the
470-- DGX Spark, 2026-09-26; sm_121's is 29, Accelerator.SM121.Lowering's
471-- tensor class).  Its sources are read at issue.  An HMMA that declares a
472-- write barrier is ordered by it instead (the older products do).
473def sm86TensorLatencyCycles : Nat = 24
474
475-- 1 when a control word declares a write barrier
476def sm86ControlWritesBarrier =
477  (lambda unrestricted control : (family SM86Control) .
478    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . Nat) control
479      (branch SM86ControlValue stall yield write read wait reuse .
480        (eliminate SM86Barrier (lambda unrestricted current : (family SM86Barrier) . Nat) write
481          (branch SM86Barrier0 . 1) (branch SM86Barrier1 . 1) (branch SM86Barrier2 . 1) (branch SM86Barrier3 . 1)
482          (branch SM86Barrier4 . 1) (branch SM86Barrier5 . 1) (branch SM86Barrier6 . 1) (branch SM86BarrierNone . 0)))))
483
484def sm86FixedLatency =
485  (lambda unrestricted body : (family SM86InstructionBody) .
486    (eliminate SM86InstructionBody (lambda unrestricted current : (family SM86InstructionBody) . Nat) body
487      (branch SM86MoveConstant destination bank offset control . sm86FixedLatencyCycles)
488      (branch SM86SpecialToRegister destination source control . 0)
489      (branch SM86MoveImmediate destination immediate control . sm86FixedLatencyCycles)
490      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . sm86FixedLatencyCycles)
491      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . sm86FixedLatencyCycles)
492      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . sm86FixedLatencyCycles)
493      (branch SM86IntegerAddThreeImmediate destination left immediate control . sm86FixedLatencyCycles)
494      (branch SM86IntegerAddThreeRegister destination left right control . sm86FixedLatencyCycles)
495      (branch SM86ShiftRightImmediate destination source amount control . sm86FixedLatencyCycles)
496      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . sm86FixedLatencyCycles)
497      (branch SM86IntegerToFloat destination source control . sm86FixedLatencyCycles)
498      (branch SM86FloatAdd destination left right control . sm86FixedLatencyCycles)
499      (branch SM86FloatMultiply destination left right control . sm86FixedLatencyCycles)
500      (branch SM86Float64Binary operation destination left right control . 0)
501      (branch SM86FloatConvert conversion control . 0)
502      (branch SM86FloatFusedMultiplyAdd destination left right addend control . sm86FixedLatencyCycles)
503      (branch SM86MultiFunctionUnitApproximation destination source operation control . 0)
504      (branch SM86FloatMinimumOrMaximum destination left right mode control . sm86FixedLatencyCycles)
505      (branch SM86FloatNegate destination source control . sm86FixedLatencyCycles)
506      (branch SM86FloatPairToPackedHalfPair destination high low control . sm86FixedLatencyCycles)
507      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . sm86FixedLatencyCycles)
508      (branch SM86FloatPairToPackedFloat8Pair destination high low merge half format control . sm86FixedLatencyCycles)
509      (branch SM86FloatArithmetic operation destination left right addend modifiers control . sm86FixedLatencyCycles)
510      (branch SM86HalfToFloat destination source selector control . sm86FixedLatencyCycles)
511      (branch SM86BFloat16ToFloat destination source selector control . sm86FixedLatencyCycles)
512      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
513        (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles))
514      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
515        (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles))
516      (branch SM86LoadGlobal destination address offset control . 0)
517      (branch SM86LoadGlobalWide destination address offset control . 0)
518      (branch SM86WarpShuffle destination source lane segment mode control . 0)
519      (branch SM86LoadShared destination address offset control . 0)
520      (branch SM86LoadSharedMatrix destination address offset count transpose control . 0)
521      (branch SM86StoreShared address value offset control . 0)
522      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 0)
523      (branch SM86CommitAsyncGroup control . 0)
524      (branch SM86WaitAsyncGroups count control . 0)
525      (branch SM86BarrierSynchronize control . 0)
526      (branch SM86BarrierSynchronizeCount barrier threads control . 0)
527      (branch SM86StoreGlobal address value offset control . 0)
528      (branch SM86StoreGlobalWide address value offset control . 0)
529      (branch SM86StoreGlobal64 address value offset control . 0)
530      (branch SM86ReduceGlobalAddFloat32 address value offset control . 0)
531      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . sm86FixedLatencyCycles)
532      (branch SM86Branch offset descriptor control . 0)
533      (branch SM86Exit control . 0)))
534
535-- The fewest cycles an instruction must stall before the next issues, from
536-- its own issue rather than a result: 1, except BAR.SYNC.DEFER_BLOCKING
537-- (6) and an HMMA ordered by its fixed latency (8).  ptxas always gives
538-- the barrier 6 (sm_86 and sm_121, every bar.sync read off nvdisasm -hex on
539-- the DGX Spark, 2026-09-26).  With 1 the GB10 let a warp's
540-- shared-matrix load right after the barrier read, now and then, what
541-- another warp had stored before it: the tiled product's last k-step (its
542-- loads follow the barrier directly) read the buffer's previous tile.
543def sm86BarrierSynchronizeStall : Nat = 6
544-- ptxas gives DEPBAR.LE SB0, n (cp.async.wait_group) 4 on sm_86 and sm_121
545-- (every wait read off nvdisasm -hex on the DGX Spark, 2026-09-26, research
546-- p4-hmma/cp_async*.cu); the realization keeps it.
547def sm86WaitAsyncGroupsStall : Nat = 4
548-- ptxas never issues an HMMA.16816 within 8 cycles of the one before on
549-- sm_86 (16 on sm_121: the tensor pipe's rate); the model asks every
550-- instruction after an HMMA to wait 8, which is stricter (ptxas fills the gap
551-- with other work) and puts a product's dependent, however few products
552-- apart, past sm86TensorLatencyCycles.
553def sm86TensorIssueStall : Nat = 8
554def sm86MinimumStall =
555  (lambda unrestricted body : (family SM86InstructionBody) .
556    (eliminate SM86InstructionBody (lambda unrestricted current : (family SM86InstructionBody) . Nat) body
557      (branch SM86MoveConstant destination bank offset control . 1)
558      (branch SM86SpecialToRegister destination source control . 1)
559      (branch SM86MoveImmediate destination immediate control . 1)
560      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . 1)
561      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . 1)
562      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . 1)
563      (branch SM86IntegerAddThreeImmediate destination left immediate control . 1)
564      (branch SM86IntegerAddThreeRegister destination left right control . 1)
565      (branch SM86ShiftRightImmediate destination source amount control . 1)
566      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . 1)
567      (branch SM86IntegerToFloat destination source control . 1)
568      (branch SM86FloatAdd destination left right control . 1)
569      (branch SM86FloatMultiply destination left right control . 1)
570      (branch SM86Float64Binary operation destination left right control . 1)
571      (branch SM86FloatConvert conversion control . 1)
572      (branch SM86FloatFusedMultiplyAdd destination left right addend control . 1)
573      (branch SM86MultiFunctionUnitApproximation destination source operation control . 1)
574      (branch SM86FloatMinimumOrMaximum destination left right mode control . 1)
575      (branch SM86FloatNegate destination source control . 1)
576      (branch SM86FloatPairToPackedHalfPair destination high low control . 1)
577      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . 1)
578      (branch SM86FloatPairToPackedFloat8Pair destination high low merge half format control . 1)
579      (branch SM86FloatArithmetic operation destination left right addend modifiers control . 1)
580      (branch SM86HalfToFloat destination source selector control . 1)
581      (branch SM86BFloat16ToFloat destination source selector control . 1)
582      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
583        (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall))
584      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
585        (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall))
586      (branch SM86LoadGlobal destination address offset control . 1)
587      (branch SM86LoadGlobalWide destination address offset control . 1)
588      (branch SM86WarpShuffle destination source lane segment mode control . 1)
589      (branch SM86LoadShared destination address offset control . 1)
590      (branch SM86LoadSharedMatrix destination address offset count transpose control . 1)
591      (branch SM86StoreShared address value offset control . 1)
592      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 1)
593      (branch SM86CommitAsyncGroup control . 1)
594      (branch SM86WaitAsyncGroups count control . sm86WaitAsyncGroupsStall)
595      (branch SM86BarrierSynchronize control . sm86BarrierSynchronizeStall)
596      (branch SM86BarrierSynchronizeCount barrier threads control . sm86BarrierSynchronizeStall)
597      (branch SM86StoreGlobal address value offset control . 1)
598      (branch SM86StoreGlobalWide address value offset control . 1)
599      (branch SM86StoreGlobal64 address value offset control . 1)
600      (branch SM86ReduceGlobalAddFloat32 address value offset control . 1)
601      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . 1)
602      (branch SM86Branch offset descriptor control . 1)
603      (branch SM86Exit control . 1)))
604
605-- A scoreboard barrier as a hazard key: 300 + its number (SB0 .. SB5).  An
606-- instruction that sets one (write or read barrier) makes it pending
607-- sm86BarrierSetCycles after issue -- ASSUMED, like the table above: a
608-- waiter issued sooner could miss it -- and an instruction whose wait mask
609-- names it reads it.
610def sm86BarrierSetCycles : Nat = 2
611
612def sm86BarrierKeys =
613  (lambda unrestricted barrier : (family SM86Barrier) .
614    (eliminate SM86Barrier (lambda unrestricted current : (family SM86Barrier) . (family StdList Nat)) barrier
615      (branch SM86Barrier0 . (constructor StdList StdListCons Nat 300 sm86NoRegisters))
616      (branch SM86Barrier1 . (constructor StdList StdListCons Nat 301 sm86NoRegisters))
617      (branch SM86Barrier2 . (constructor StdList StdListCons Nat 302 sm86NoRegisters))
618      (branch SM86Barrier3 . (constructor StdList StdListCons Nat 303 sm86NoRegisters))
619      (branch SM86Barrier4 . (constructor StdList StdListCons Nat 304 sm86NoRegisters))
620      (branch SM86Barrier5 . (constructor StdList StdListCons Nat 305 sm86NoRegisters))
621      (branch SM86Barrier6 . (constructor StdList StdListCons Nat 306 sm86NoRegisters))
622      (branch SM86BarrierNone . sm86NoRegisters)))
623
624-- the barriers a control word sets
625def sm86ControlSetKeys =
626  (lambda unrestricted control : (family SM86Control) .
627    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . (family StdList Nat)) control
628      (branch SM86ControlValue stall yield write read wait reuse .
629        (stdListAppend Nat (sm86BarrierKeys write) (sm86BarrierKeys read)))))
630
631-- the barriers a control word's wait mask names (bit b: SB b)
632def sm86ControlWaitKeys =
633  (lambda unrestricted control : (family SM86Control) .
634    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . (family StdList Nat)) control
635      (branch SM86ControlValue stall yield write read wait reuse .
636        (nat-eliminate
637          (lambda unrestricted current : Nat . (family StdList Nat))
638          sm86NoRegisters
639          (lambda unrestricted bit : Nat . (lambda unrestricted induction : (family StdList Nat) .
640            (nat-eliminate
641              (lambda unrestricted current : Nat . (family StdList Nat))
642              induction
643              (lambda unrestricted set : Nat . (lambda unrestricted ignored : (family StdList Nat) .
644                (constructor StdList StdListCons Nat (naturalAdd 300 bit) induction)))
645              (nat-modulo (nat-divide (byte-to-nat wait) (naturalPowerOfTwo bit)) 2))))
646          6))))
647
648
649def sm86OpSummaryMake =
650  (lambda unrestricted reads : (family StdList Nat) .
651    (lambda unrestricted writes : (family StdList Nat) .
652      (lambda unrestricted predicateWrites : (family StdList Nat) .
653        (lambda unrestricted variable : Nat .
654          (lambda unrestricted latency : Nat .
655            (lambda unrestricted minimum : Nat .
656            (lambda unrestricted control : (family SM86Control) .
657              (constructor SM86OpSummary SM86OpSummaryValue
658                reads writes predicateWrites
659                (sm86ControlWaitKeys control) (sm86ControlSetKeys control)
660                (sm86ControlStallOf control) latency variable minimum control))))))))
661
662def sm86OpSummaryOfBody =
663  (lambda unrestricted body : (family SM86InstructionBody) .
664    (eliminate SM86InstructionBody
665      (lambda unrestricted current : (family SM86InstructionBody) . (family SM86OpSummary))
666      body
667      (branch SM86MoveConstant destination bank offset control . (sm86OpSummaryMake sm86NoRegisters (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
668      (branch SM86SpecialToRegister destination source control . (sm86OpSummaryMake sm86NoRegisters (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
669      (branch SM86MoveImmediate destination immediate control . (sm86OpSummaryMake sm86NoRegisters (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
670      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (sm86OpSummaryMake (sm86One left (sm86One addend sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
671      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (sm86OpSummaryMake (sm86One left (sm86One addend sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
672      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86Pair destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
673      (branch SM86IntegerAddThreeImmediate destination left immediate control . (sm86OpSummaryMake (sm86One left sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
674      (branch SM86IntegerAddThreeRegister destination left right control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
675      (branch SM86ShiftRightImmediate destination source amount control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
676      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
677      (branch SM86IntegerToFloat destination source control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
678      (branch SM86FloatAdd destination left right control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
679      (branch SM86FloatMultiply destination left right control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
680      -- Double arithmetic has variable latency, including late source reads.
681      -- Mesa NAK ir.rs, has_fixed_latency, revision b1fe47e94409d81924c8663f58fac97e66ab4527:
682      -- https://chromium.googlesource.com/external/gitlab.freedesktop.org/mesa/mesa/+/b1fe47e94409d81924c8663f58fac97e66ab4527/src/nouveau/compiler/nak/ir.rs
683      -- Both halves participate; waiting on the low word alone is insufficient.
684      (branch SM86Float64Binary operation destination left right control . (sm86OpSummaryMake (sm86Pair (sm86RegisterPairBase left) (sm86Pair (sm86RegisterPairBase right) sm86NoRegisters)) (sm86Pair (sm86RegisterPairBase destination) sm86NoRegisters) sm86NoRegisters 1 0 1 control))
685      (branch SM86FloatConvert conversion control . (sm86OpSummaryMake (sm86ConversionReads conversion) (sm86ConversionWrites conversion) sm86NoRegisters 1 0 1 control))
686      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (sm86OpSummaryMake (sm86One left (sm86One right (sm86One addend sm86NoRegisters))) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
687      (branch SM86MultiFunctionUnitApproximation destination source operation control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
688      (branch SM86FloatMinimumOrMaximum destination left right mode control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
689      (branch SM86FloatNegate destination source control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
690      (branch SM86FloatPairToPackedHalfPair destination high low control . (sm86OpSummaryMake (sm86One high (sm86One low sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
691      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (sm86OpSummaryMake (sm86One high (sm86One low sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
692      (branch SM86FloatPairToPackedFloat8Pair destination high low merge half format control . (sm86OpSummaryMake (sm86One high (sm86One low (sm86One merge sm86NoRegisters))) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
693      (branch SM86FloatArithmetic operation destination left right addend modifiers control . (sm86OpSummaryMake (sm86One left (sm86One right (sm86One addend sm86NoRegisters))) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
694      (branch SM86HalfToFloat destination source selector control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
695      (branch SM86BFloat16ToFloat destination source selector control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
696      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86OpSummaryMake (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))) (sm86Quad destination sm86NoRegisters) sm86NoRegisters 0 (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles) (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall) control))
697      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86OpSummaryMake (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))) (sm86Quad destination sm86NoRegisters) sm86NoRegisters 0 (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles) (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall) control))
698      (branch SM86LoadGlobal destination address offset control . (sm86OpSummaryMake (sm86Pair address sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
699      (branch SM86LoadGlobalWide destination address offset control . (sm86OpSummaryMake (sm86Pair address sm86NoRegisters) (sm86Quad destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
700      (branch SM86WarpShuffle destination source lane segment mode control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
701      (branch SM86LoadShared destination address offset control . (sm86OpSummaryMake (sm86One address sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
702      (branch SM86LoadSharedMatrix destination address offset count transpose control . (sm86OpSummaryMake (sm86One address sm86NoRegisters) (sm86RegisterRun destination (sm86SharedMatrixRegisters count) sm86NoRegisters) sm86NoRegisters 1 0 1 control))
703      (branch SM86StoreShared address value offset control . (sm86OpSummaryMake (sm86One address (sm86One value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
704      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (sm86OpSummaryMake (sm86One address (sm86Pair source sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
705      (branch SM86CommitAsyncGroup control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 1 control))
706      (branch SM86WaitAsyncGroups count control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 sm86WaitAsyncGroupsStall control))
707      (branch SM86BarrierSynchronize control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 sm86BarrierSynchronizeStall control))
708      (branch SM86BarrierSynchronizeCount barrier threads control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 sm86BarrierSynchronizeStall control))
709      (branch SM86StoreGlobal address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86One value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
710      (branch SM86StoreGlobalWide address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86Quad value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
711      (branch SM86StoreGlobal64 address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86Pair value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
712      (branch SM86ReduceGlobalAddFloat32 address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86One value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
713      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) sm86NoRegisters (sm86PredicateKeys predicate) 0 sm86FixedLatencyCycles 1 control))
714      (branch SM86Branch offset descriptor control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 1 control))
715      (branch SM86Exit control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 1 control))))