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 (sm86Pair 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 SM86HalfToFloat destination source selector control . (sm86One source sm86NoRegisters))
154      (branch SM86BFloat16ToFloat destination source selector control . (sm86One source sm86NoRegisters))
155      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
156        (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))))
157      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
158        (sm86Quad a (sm86Pair b (sm86Quad accumulator sm86NoRegisters))))
159      (branch SM86LoadGlobal destination address offset control . (sm86Pair address sm86NoRegisters))
160      (branch SM86LoadGlobalWide destination address offset control . (sm86Pair address sm86NoRegisters))
161      (branch SM86WarpShuffle destination source lane segment mode control . (sm86One source sm86NoRegisters))
162      (branch SM86LoadShared destination address offset control . (sm86One address sm86NoRegisters))
163      (branch SM86LoadSharedMatrix destination address offset count transpose control . (sm86One address sm86NoRegisters))
164      (branch SM86StoreShared address value offset control . (sm86One address (sm86One value sm86NoRegisters)))
165      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (sm86One address (sm86Pair source sm86NoRegisters)))
166      (branch SM86CommitAsyncGroup control . sm86NoRegisters)
167      (branch SM86WaitAsyncGroups count control . sm86NoRegisters)
168      (branch SM86BarrierSynchronize control . sm86NoRegisters)
169      (branch SM86BarrierSynchronizeCount barrier threads control . sm86NoRegisters)
170      (branch SM86StoreGlobal address value offset control . (sm86Pair address (sm86One value sm86NoRegisters)))
171      (branch SM86StoreGlobalWide address value offset control . (sm86Pair address (sm86Quad value sm86NoRegisters)))
172      (branch SM86StoreGlobal64 address value offset control . (sm86Pair address (sm86Pair value sm86NoRegisters)))
173      (branch SM86ReduceGlobalAddFloat32 address value offset control . (sm86Pair address (sm86One value sm86NoRegisters)))
174      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (sm86One source sm86NoRegisters))
175      (branch SM86Branch offset descriptor control . sm86NoRegisters)
176      (branch SM86Exit control . sm86NoRegisters)))
177
178def sm86WriteRegisters =
179  (lambda unrestricted body : (family SM86InstructionBody) .
180    (eliminate SM86InstructionBody
181      (lambda unrestricted current : (family SM86InstructionBody) . (family StdList Nat))
182      body
183      (branch SM86MoveConstant destination bank offset control . (sm86One destination sm86NoRegisters))
184      (branch SM86SpecialToRegister destination source control . (sm86One destination sm86NoRegisters))
185      (branch SM86MoveImmediate destination immediate control . (sm86One destination sm86NoRegisters))
186      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (sm86One destination sm86NoRegisters))
187      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (sm86One destination sm86NoRegisters))
188      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (sm86Pair destination sm86NoRegisters))
189      (branch SM86IntegerAddThreeImmediate destination left immediate control . (sm86One destination sm86NoRegisters))
190      (branch SM86IntegerAddThreeRegister destination left right control . (sm86One destination sm86NoRegisters))
191      (branch SM86ShiftRightImmediate destination source amount control . (sm86One destination sm86NoRegisters))
192      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (sm86One destination sm86NoRegisters))
193      (branch SM86IntegerToFloat destination source control . (sm86One destination sm86NoRegisters))
194      (branch SM86FloatAdd destination left right control . (sm86One destination sm86NoRegisters))
195      (branch SM86FloatMultiply destination left right control . (sm86One destination sm86NoRegisters))
196      (branch SM86Float64Binary operation destination left right control . (sm86Pair (sm86RegisterPairBase destination) sm86NoRegisters))
197      (branch SM86FloatConvert conversion control . (sm86ConversionWrites conversion))
198      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (sm86One destination sm86NoRegisters))
199      (branch SM86MultiFunctionUnitApproximation destination source operation control . (sm86One destination sm86NoRegisters))
200      (branch SM86FloatMinimumOrMaximum destination left right mode control . (sm86One destination sm86NoRegisters))
201      (branch SM86FloatNegate destination source control . (sm86One destination sm86NoRegisters))
202      (branch SM86FloatPairToPackedHalfPair destination high low control . (sm86One destination sm86NoRegisters))
203      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (sm86One destination sm86NoRegisters))
204      (branch SM86HalfToFloat destination source selector control . (sm86One destination sm86NoRegisters))
205      (branch SM86BFloat16ToFloat destination source selector control . (sm86One destination sm86NoRegisters))
206      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86Quad destination sm86NoRegisters))
207      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (sm86Quad destination sm86NoRegisters))
208      (branch SM86LoadGlobal destination address offset control . (sm86One destination sm86NoRegisters))
209      (branch SM86LoadGlobalWide destination address offset control . (sm86Quad destination sm86NoRegisters))
210      (branch SM86WarpShuffle destination source lane segment mode control . (sm86One destination sm86NoRegisters))
211      (branch SM86LoadShared destination address offset control . (sm86One destination sm86NoRegisters))
212      (branch SM86LoadSharedMatrix destination address offset count transpose control .
213        (sm86RegisterRun destination (sm86SharedMatrixRegisters count) sm86NoRegisters))
214      (branch SM86StoreShared address value offset control . sm86NoRegisters)
215      (branch SM86LoadGlobalToShared address offset source sourceOffset control . sm86NoRegisters)
216      (branch SM86CommitAsyncGroup control . sm86NoRegisters)
217      (branch SM86WaitAsyncGroups count control . sm86NoRegisters)
218      (branch SM86BarrierSynchronize control . sm86NoRegisters)
219      (branch SM86BarrierSynchronizeCount barrier threads control . sm86NoRegisters)
220      (branch SM86StoreGlobal address value offset control . sm86NoRegisters)
221      (branch SM86StoreGlobalWide address value offset control . sm86NoRegisters)
222      (branch SM86StoreGlobal64 address value offset control . sm86NoRegisters)
223      (branch SM86ReduceGlobalAddFloat32 address value offset control . sm86NoRegisters)
224      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . sm86NoRegisters)
225      (branch SM86Branch offset descriptor control . sm86NoRegisters)
226      (branch SM86Exit control . sm86NoRegisters)))
227
228def sm86InstructionBodyOf =
229  (lambda unrestricted instruction : (family SM86Instruction) .
230    (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . (family SM86InstructionBody)) instruction
231      (branch SM86InstructionValue guard body . body)))
232
233-- one past the highest of the values, or start if that is higher
234def sm86SpanOf =
235  (lambda unrestricted values : (family StdList Nat) . (lambda unrestricted start : Nat .
236    (eliminate StdList (lambda unrestricted current : (family StdList Nat) . Nat) values
237      (branch StdListEmpty . start)
238      (branch StdListCons head tail induction . (naturalSelect (naturalLess induction (succ head)) (succ head) induction)))))
239
240-- one past the highest register the program names (0 for none)
241def sm86RegisterSpan =
242  (lambda unrestricted program : (family SM86Program) .
243    (eliminate SM86Program (lambda unrestricted current : (family SM86Program) . Nat) program
244      (branch SM86ProgramEnd . 0)
245      (branch SM86ProgramNext head tail induction .
246        (sm86SpanOf (sm86ReadRegisters (sm86InstructionBodyOf head))
247          (sm86SpanOf (sm86WriteRegisters (sm86InstructionBodyOf head)) induction)))))
248
249-- the register count a launch of the program declares: the registers it
250-- names (the QMD encoder adds the reserved two and rounds to the granule)
251def sm86RegisterDemand =
252  (lambda unrestricted program : (family SM86Program) . (sm86RegisterSpan program))
253-- the registers a thread of a launch declaring `demand` is allocated
254def sm86RegisterAllocation =
255  (lambda unrestricted demand : Nat .
256    (naturalMultiply sm86RegisterGranule
257      (naturalDivideUnchecked
258        (naturalAdd (naturalAdd demand sm86ReservedRegisters) (naturalSaturatingSubtract sm86RegisterGranule 1))
259        sm86RegisterGranule)))
260
261-- ---- control words, predicates as hazard keys, fixed latency ----
262
263-- an instruction body's control word
264def sm86BodyControlOf =
265  (lambda unrestricted body : (family SM86InstructionBody) .
266    (eliminate SM86InstructionBody
267      (lambda unrestricted current : (family SM86InstructionBody) . (family SM86Control))
268      body
269      (branch SM86MoveConstant destination bank offset control . control)
270      (branch SM86SpecialToRegister destination source control . control)
271      (branch SM86MoveImmediate destination immediate control . control)
272      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . control)
273      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . control)
274      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . control)
275      (branch SM86IntegerAddThreeImmediate destination left immediate control . control)
276      (branch SM86IntegerAddThreeRegister destination left right control . control)
277      (branch SM86ShiftRightImmediate destination source amount control . control)
278      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . control)
279      (branch SM86IntegerToFloat destination source control . control)
280      (branch SM86FloatAdd destination left right control . control)
281      (branch SM86FloatMultiply destination left right control . control)
282      (branch SM86Float64Binary operation destination left right control . control)
283      (branch SM86FloatConvert conversion control . control)
284      (branch SM86FloatFusedMultiplyAdd destination left right addend control . control)
285      (branch SM86MultiFunctionUnitApproximation destination source operation control . control)
286      (branch SM86FloatMinimumOrMaximum destination left right mode control . control)
287      (branch SM86FloatNegate destination source control . control)
288      (branch SM86FloatPairToPackedHalfPair destination high low control . control)
289      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . control)
290      (branch SM86HalfToFloat destination source selector control . control)
291      (branch SM86BFloat16ToFloat destination source selector control . control)
292      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . control)
293      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . control)
294      (branch SM86LoadGlobal destination address offset control . control)
295      (branch SM86LoadGlobalWide destination address offset control . control)
296      (branch SM86WarpShuffle destination source lane segment mode control . control)
297      (branch SM86LoadShared destination address offset control . control)
298      (branch SM86LoadSharedMatrix destination address offset count transpose control . control)
299      (branch SM86StoreShared address value offset control . control)
300      (branch SM86LoadGlobalToShared address offset source sourceOffset control . control)
301      (branch SM86CommitAsyncGroup control . control)
302      (branch SM86WaitAsyncGroups count control . control)
303      (branch SM86BarrierSynchronize control . control)
304      (branch SM86BarrierSynchronizeCount barrier threads control . control)
305      (branch SM86StoreGlobal address value offset control . control)
306      (branch SM86StoreGlobalWide address value offset control . control)
307      (branch SM86StoreGlobal64 address value offset control . control)
308      (branch SM86ReduceGlobalAddFloat32 address value offset control . control)
309      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . control)
310      (branch SM86Branch offset descriptor control . control)
311      (branch SM86Exit control . control)))
312
313-- the body with another control word
314def sm86BodyWithControl =
315  (lambda unrestricted body : (family SM86InstructionBody) .
316    (lambda unrestricted replacement : (family SM86Control) .
317      (eliminate SM86InstructionBody
318        (lambda unrestricted current : (family SM86InstructionBody) . (family SM86InstructionBody))
319        body
320      (branch SM86MoveConstant destination bank offset control . (constructor SM86InstructionBody SM86MoveConstant destination bank offset replacement))
321      (branch SM86SpecialToRegister destination source control . (constructor SM86InstructionBody SM86SpecialToRegister destination source replacement))
322      (branch SM86MoveImmediate destination immediate control . (constructor SM86InstructionBody SM86MoveImmediate destination immediate replacement))
323      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddConstant destination left bank offset addend replacement))
324      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (constructor SM86InstructionBody SM86IntegerMultiplyAddImmediate destination left immediate addend replacement))
325      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (constructor SM86InstructionBody SM86IntegerMultiplyAddWideConstant destination left right bank offset replacement))
326      (branch SM86IntegerAddThreeImmediate destination left immediate control . (constructor SM86InstructionBody SM86IntegerAddThreeImmediate destination left immediate replacement))
327      (branch SM86IntegerAddThreeRegister destination left right control . (constructor SM86InstructionBody SM86IntegerAddThreeRegister destination left right replacement))
328      (branch SM86ShiftRightImmediate destination source amount control . (constructor SM86InstructionBody SM86ShiftRightImmediate destination source amount replacement))
329      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (constructor SM86InstructionBody SM86LogicThreeInputTruthTable destination left right truthTable replacement))
330      (branch SM86IntegerToFloat destination source control . (constructor SM86InstructionBody SM86IntegerToFloat destination source replacement))
331      (branch SM86FloatAdd destination left right control . (constructor SM86InstructionBody SM86FloatAdd destination left right replacement))
332      (branch SM86FloatMultiply destination left right control . (constructor SM86InstructionBody SM86FloatMultiply destination left right replacement))
333      (branch SM86Float64Binary operation destination left right control . (constructor SM86InstructionBody SM86Float64Binary operation destination left right replacement))
334      (branch SM86FloatConvert conversion control . (constructor SM86InstructionBody SM86FloatConvert conversion replacement))
335      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (constructor SM86InstructionBody SM86FloatFusedMultiplyAdd destination left right addend replacement))
336      (branch SM86MultiFunctionUnitApproximation destination source operation control . (constructor SM86InstructionBody SM86MultiFunctionUnitApproximation destination source operation replacement))
337      (branch SM86FloatMinimumOrMaximum destination left right mode control . (constructor SM86InstructionBody SM86FloatMinimumOrMaximum destination left right mode replacement))
338      (branch SM86FloatNegate destination source control . (constructor SM86InstructionBody SM86FloatNegate destination source replacement))
339      (branch SM86FloatPairToPackedHalfPair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedHalfPair destination high low replacement))
340      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (constructor SM86InstructionBody SM86FloatPairToPackedBFloat16Pair destination high low replacement))
341      (branch SM86HalfToFloat destination source selector control . (constructor SM86InstructionBody SM86HalfToFloat destination source selector replacement))
342      (branch SM86BFloat16ToFloat destination source selector control . (constructor SM86InstructionBody SM86BFloat16ToFloat destination source selector replacement))
343      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator replacement))
344      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . (constructor SM86InstructionBody SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator replacement))
345      (branch SM86LoadGlobal destination address offset control . (constructor SM86InstructionBody SM86LoadGlobal destination address offset replacement))
346      (branch SM86LoadGlobalWide destination address offset control . (constructor SM86InstructionBody SM86LoadGlobalWide destination address offset replacement))
347      (branch SM86WarpShuffle destination source lane segment mode control . (constructor SM86InstructionBody SM86WarpShuffle destination source lane segment mode replacement))
348      (branch SM86LoadShared destination address offset control . (constructor SM86InstructionBody SM86LoadShared destination address offset replacement))
349      (branch SM86LoadSharedMatrix destination address offset count transpose control . (constructor SM86InstructionBody SM86LoadSharedMatrix destination address offset count transpose replacement))
350      (branch SM86StoreShared address value offset control . (constructor SM86InstructionBody SM86StoreShared address value offset replacement))
351      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (constructor SM86InstructionBody SM86LoadGlobalToShared address offset source sourceOffset replacement))
352      (branch SM86CommitAsyncGroup control . (constructor SM86InstructionBody SM86CommitAsyncGroup replacement))
353      (branch SM86WaitAsyncGroups count control . (constructor SM86InstructionBody SM86WaitAsyncGroups count replacement))
354      (branch SM86BarrierSynchronize control . (constructor SM86InstructionBody SM86BarrierSynchronize replacement))
355      (branch SM86BarrierSynchronizeCount barrier threads control . (constructor SM86InstructionBody SM86BarrierSynchronizeCount barrier threads replacement))
356      (branch SM86StoreGlobal address value offset control . (constructor SM86InstructionBody SM86StoreGlobal address value offset replacement))
357      (branch SM86StoreGlobalWide address value offset control . (constructor SM86InstructionBody SM86StoreGlobalWide address value offset replacement))
358      (branch SM86StoreGlobal64 address value offset control . (constructor SM86InstructionBody SM86StoreGlobal64 address value offset replacement))
359      (branch SM86ReduceGlobalAddFloat32 address value offset control . (constructor SM86InstructionBody SM86ReduceGlobalAddFloat32 address value offset replacement))
360      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate predicate source immediate replacement))
361      (branch SM86Branch offset descriptor control . (constructor SM86InstructionBody SM86Branch offset descriptor replacement))
362      (branch SM86Exit control . (constructor SM86InstructionBody SM86Exit replacement)))))
363
364def sm86ControlStallOf =
365  (lambda unrestricted control : (family SM86Control) .
366    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . Nat) control
367      (branch SM86ControlValue stall yield write read wait reuse . (byte-to-nat stall))))
368
369def sm86ControlWithStall =
370  (lambda unrestricted control : (family SM86Control) . (lambda unrestricted stall : Nat .
371    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . (family SM86Control)) control
372      (branch SM86ControlValue old yield write read wait reuse .
373        (constructor SM86Control SM86ControlValue (nat-to-byte stall) yield write read wait reuse)))))
374
375-- A predicate as a hazard key beside the registers: 256 + its index (P0 ..
376-- P6; PT, which reads true and absorbs writes, is none).
377def sm86PredicateKeys =
378  (lambda unrestricted predicate : (family SM86Predicate) .
379    (eliminate SM86Predicate (lambda unrestricted current : (family SM86Predicate) . (family StdList Nat)) predicate
380      (branch SM86Predicate0 . (constructor StdList StdListCons Nat 256 sm86NoRegisters))
381      (branch SM86Predicate1 . (constructor StdList StdListCons Nat 257 sm86NoRegisters))
382      (branch SM86Predicate2 . (constructor StdList StdListCons Nat 258 sm86NoRegisters))
383      (branch SM86Predicate3 . (constructor StdList StdListCons Nat 259 sm86NoRegisters))
384      (branch SM86Predicate4 . (constructor StdList StdListCons Nat 260 sm86NoRegisters))
385      (branch SM86Predicate5 . (constructor StdList StdListCons Nat 261 sm86NoRegisters))
386      (branch SM86Predicate6 . (constructor StdList StdListCons Nat 262 sm86NoRegisters))
387      (branch SM86PredicateTrue . sm86NoRegisters)))
388
389-- the predicate an instruction's guard reads
390def sm86GuardKeys =
391  (lambda unrestricted instruction : (family SM86Instruction) .
392    (eliminate SM86Instruction (lambda unrestricted current : (family SM86Instruction) . (family StdList Nat)) instruction
393      (branch SM86InstructionValue guard body .
394        (eliminate SM86InstructionGuard (lambda unrestricted current : (family SM86InstructionGuard) . (family StdList Nat)) guard
395          (branch SM86InstructionAlways . sm86NoRegisters)
396          (branch SM86InstructionWhen predicate . (sm86PredicateKeys predicate))
397          (branch SM86InstructionWhenNot predicate . (sm86PredicateKeys predicate))))))
398
399-- the predicate a body writes
400def sm86PredicateWriteKeys =
401  (lambda unrestricted body : (family SM86InstructionBody) .
402    (eliminate SM86InstructionBody (lambda unrestricted current : (family SM86InstructionBody) . (family StdList Nat)) body
403      (branch SM86MoveConstant destination bank offset control . sm86NoRegisters)
404      (branch SM86SpecialToRegister destination source control . sm86NoRegisters)
405      (branch SM86MoveImmediate destination immediate control . sm86NoRegisters)
406      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . sm86NoRegisters)
407      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . sm86NoRegisters)
408      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . sm86NoRegisters)
409      (branch SM86IntegerAddThreeImmediate destination left immediate control . sm86NoRegisters)
410      (branch SM86IntegerAddThreeRegister destination left right control . sm86NoRegisters)
411      (branch SM86ShiftRightImmediate destination source amount control . sm86NoRegisters)
412      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . sm86NoRegisters)
413      (branch SM86IntegerToFloat destination source control . sm86NoRegisters)
414      (branch SM86FloatAdd destination left right control . sm86NoRegisters)
415      (branch SM86FloatMultiply destination left right control . sm86NoRegisters)
416      (branch SM86Float64Binary operation destination left right control . sm86NoRegisters)
417      (branch SM86FloatConvert conversion control . sm86NoRegisters)
418      (branch SM86FloatFusedMultiplyAdd destination left right addend control . sm86NoRegisters)
419      (branch SM86MultiFunctionUnitApproximation destination source operation control . sm86NoRegisters)
420      (branch SM86FloatMinimumOrMaximum destination left right mode control . sm86NoRegisters)
421      (branch SM86FloatNegate destination source control . sm86NoRegisters)
422      (branch SM86FloatPairToPackedHalfPair destination high low control . sm86NoRegisters)
423      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . sm86NoRegisters)
424      (branch SM86HalfToFloat destination source selector control . sm86NoRegisters)
425      (branch SM86BFloat16ToFloat destination source selector control . sm86NoRegisters)
426      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . sm86NoRegisters)
427      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control . sm86NoRegisters)
428      (branch SM86LoadGlobal destination address offset control . sm86NoRegisters)
429      (branch SM86LoadGlobalWide destination address offset control . sm86NoRegisters)
430      (branch SM86WarpShuffle destination source lane segment mode control . sm86NoRegisters)
431      (branch SM86LoadShared destination address offset control . sm86NoRegisters)
432      (branch SM86LoadSharedMatrix destination address offset count transpose control . sm86NoRegisters)
433      (branch SM86StoreShared address value offset control . sm86NoRegisters)
434      (branch SM86LoadGlobalToShared address offset source sourceOffset control . sm86NoRegisters)
435      (branch SM86CommitAsyncGroup control . sm86NoRegisters)
436      (branch SM86WaitAsyncGroups count control . sm86NoRegisters)
437      (branch SM86BarrierSynchronize control . sm86NoRegisters)
438      (branch SM86BarrierSynchronizeCount barrier threads control . sm86NoRegisters)
439      (branch SM86StoreGlobal address value offset control . sm86NoRegisters)
440      (branch SM86StoreGlobalWide address value offset control . sm86NoRegisters)
441      (branch SM86StoreGlobal64 address value offset control . sm86NoRegisters)
442      (branch SM86ReduceGlobalAddFloat32 address value offset control . sm86NoRegisters)
443      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (sm86PredicateKeys predicate))
444      (branch SM86Branch offset descriptor control . sm86NoRegisters)
445      (branch SM86Exit control . sm86NoRegisters)))
446
447-- ASSUMED, and stated as an assumption: the cycles after issue before a
448-- fixed-latency form's destination (register or predicate) may be read --
449-- 6 for every such form, above the 4 published for Ampere's FP32 and
450-- integer pipes.  Variable-latency forms (loads, S2R, SHFL, MUFU, HMMA)
451-- deliver through a scoreboard barrier instead, and forms with no
452-- destination deliver nothing (0).  A program accepted under this table
453-- that a card computes wrongly refutes it: silicon runs of stall-compacted
454-- programs are its evidence.
455def sm86FixedLatencyCycles : Nat = 6
456
457-- HMMA.16816.F32: a fixed-latency result, as ptxas schedules it for sm_86
458-- (no scoreboard; a dependent HMMA 24 cycles after its producer, a store
459-- of the result 23 -- nvdisasm -hex of a dependent mma.sync chain on the
460-- DGX Spark, 2026-09-26; sm_121's is 29, Accelerator.SM121.Lowering's
461-- tensor class).  Its sources are read at issue.  An HMMA that declares a
462-- write barrier is ordered by it instead (the older products do).
463def sm86TensorLatencyCycles : Nat = 24
464
465-- 1 when a control word declares a write barrier
466def sm86ControlWritesBarrier =
467  (lambda unrestricted control : (family SM86Control) .
468    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . Nat) control
469      (branch SM86ControlValue stall yield write read wait reuse .
470        (eliminate SM86Barrier (lambda unrestricted current : (family SM86Barrier) . Nat) write
471          (branch SM86Barrier0 . 1) (branch SM86Barrier1 . 1) (branch SM86Barrier2 . 1) (branch SM86Barrier3 . 1)
472          (branch SM86Barrier4 . 1) (branch SM86Barrier5 . 1) (branch SM86Barrier6 . 1) (branch SM86BarrierNone . 0)))))
473
474def sm86FixedLatency =
475  (lambda unrestricted body : (family SM86InstructionBody) .
476    (eliminate SM86InstructionBody (lambda unrestricted current : (family SM86InstructionBody) . Nat) body
477      (branch SM86MoveConstant destination bank offset control . sm86FixedLatencyCycles)
478      (branch SM86SpecialToRegister destination source control . 0)
479      (branch SM86MoveImmediate destination immediate control . sm86FixedLatencyCycles)
480      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . sm86FixedLatencyCycles)
481      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . sm86FixedLatencyCycles)
482      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . sm86FixedLatencyCycles)
483      (branch SM86IntegerAddThreeImmediate destination left immediate control . sm86FixedLatencyCycles)
484      (branch SM86IntegerAddThreeRegister destination left right control . sm86FixedLatencyCycles)
485      (branch SM86ShiftRightImmediate destination source amount control . sm86FixedLatencyCycles)
486      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . sm86FixedLatencyCycles)
487      (branch SM86IntegerToFloat destination source control . sm86FixedLatencyCycles)
488      (branch SM86FloatAdd destination left right control . sm86FixedLatencyCycles)
489      (branch SM86FloatMultiply destination left right control . sm86FixedLatencyCycles)
490      (branch SM86Float64Binary operation destination left right control . 0)
491      (branch SM86FloatConvert conversion control . 0)
492      (branch SM86FloatFusedMultiplyAdd destination left right addend control . sm86FixedLatencyCycles)
493      (branch SM86MultiFunctionUnitApproximation destination source operation control . 0)
494      (branch SM86FloatMinimumOrMaximum destination left right mode control . sm86FixedLatencyCycles)
495      (branch SM86FloatNegate destination source control . sm86FixedLatencyCycles)
496      (branch SM86FloatPairToPackedHalfPair destination high low control . sm86FixedLatencyCycles)
497      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . sm86FixedLatencyCycles)
498      (branch SM86HalfToFloat destination source selector control . sm86FixedLatencyCycles)
499      (branch SM86BFloat16ToFloat destination source selector control . sm86FixedLatencyCycles)
500      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
501        (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles))
502      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
503        (naturalSelect (sm86ControlWritesBarrier control) 0 sm86TensorLatencyCycles))
504      (branch SM86LoadGlobal destination address offset control . 0)
505      (branch SM86LoadGlobalWide destination address offset control . 0)
506      (branch SM86WarpShuffle destination source lane segment mode control . 0)
507      (branch SM86LoadShared destination address offset control . 0)
508      (branch SM86LoadSharedMatrix destination address offset count transpose control . 0)
509      (branch SM86StoreShared address value offset control . 0)
510      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 0)
511      (branch SM86CommitAsyncGroup control . 0)
512      (branch SM86WaitAsyncGroups count control . 0)
513      (branch SM86BarrierSynchronize control . 0)
514      (branch SM86BarrierSynchronizeCount barrier threads control . 0)
515      (branch SM86StoreGlobal address value offset control . 0)
516      (branch SM86StoreGlobalWide address value offset control . 0)
517      (branch SM86StoreGlobal64 address value offset control . 0)
518      (branch SM86ReduceGlobalAddFloat32 address value offset control . 0)
519      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . sm86FixedLatencyCycles)
520      (branch SM86Branch offset descriptor control . 0)
521      (branch SM86Exit control . 0)))
522
523-- The fewest cycles an instruction must stall before the next issues, from
524-- its own issue rather than a result: 1, except BAR.SYNC.DEFER_BLOCKING
525-- (6) and an HMMA ordered by its fixed latency (8).  ptxas always gives
526-- the barrier 6 (sm_86 and sm_121, every bar.sync read off nvdisasm -hex on
527-- the DGX Spark, 2026-09-26).  With 1 the GB10 let a warp's
528-- shared-matrix load right after the barrier read, now and then, what
529-- another warp had stored before it: the tiled product's last k-step (its
530-- loads follow the barrier directly) read the buffer's previous tile.
531def sm86BarrierSynchronizeStall : Nat = 6
532-- ptxas gives DEPBAR.LE SB0, n (cp.async.wait_group) 4 on sm_86 and sm_121
533-- (every wait read off nvdisasm -hex on the DGX Spark, 2026-09-26, research
534-- p4-hmma/cp_async*.cu); the realization keeps it.
535def sm86WaitAsyncGroupsStall : Nat = 4
536-- ptxas never issues an HMMA.16816 within 8 cycles of the one before on
537-- sm_86 (16 on sm_121: the tensor pipe's rate); the model asks every
538-- instruction after an HMMA to wait 8, which is stricter (ptxas fills the gap
539-- with other work) and puts a product's dependent, however few products
540-- apart, past sm86TensorLatencyCycles.
541def sm86TensorIssueStall : Nat = 8
542def sm86MinimumStall =
543  (lambda unrestricted body : (family SM86InstructionBody) .
544    (eliminate SM86InstructionBody (lambda unrestricted current : (family SM86InstructionBody) . Nat) body
545      (branch SM86MoveConstant destination bank offset control . 1)
546      (branch SM86SpecialToRegister destination source control . 1)
547      (branch SM86MoveImmediate destination immediate control . 1)
548      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . 1)
549      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . 1)
550      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . 1)
551      (branch SM86IntegerAddThreeImmediate destination left immediate control . 1)
552      (branch SM86IntegerAddThreeRegister destination left right control . 1)
553      (branch SM86ShiftRightImmediate destination source amount control . 1)
554      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . 1)
555      (branch SM86IntegerToFloat destination source control . 1)
556      (branch SM86FloatAdd destination left right control . 1)
557      (branch SM86FloatMultiply destination left right control . 1)
558      (branch SM86Float64Binary operation destination left right control . 1)
559      (branch SM86FloatConvert conversion control . 1)
560      (branch SM86FloatFusedMultiplyAdd destination left right addend control . 1)
561      (branch SM86MultiFunctionUnitApproximation destination source operation control . 1)
562      (branch SM86FloatMinimumOrMaximum destination left right mode control . 1)
563      (branch SM86FloatNegate destination source control . 1)
564      (branch SM86FloatPairToPackedHalfPair destination high low control . 1)
565      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . 1)
566      (branch SM86HalfToFloat destination source selector control . 1)
567      (branch SM86BFloat16ToFloat destination source selector control . 1)
568      (branch SM86TensorCoreHalfMatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
569        (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall))
570      (branch SM86TensorCoreBFloat16MatrixMultiplyAccumulate16x8x16Float32 destination a b accumulator control .
571        (naturalSelect (sm86ControlWritesBarrier control) 1 sm86TensorIssueStall))
572      (branch SM86LoadGlobal destination address offset control . 1)
573      (branch SM86LoadGlobalWide destination address offset control . 1)
574      (branch SM86WarpShuffle destination source lane segment mode control . 1)
575      (branch SM86LoadShared destination address offset control . 1)
576      (branch SM86LoadSharedMatrix destination address offset count transpose control . 1)
577      (branch SM86StoreShared address value offset control . 1)
578      (branch SM86LoadGlobalToShared address offset source sourceOffset control . 1)
579      (branch SM86CommitAsyncGroup control . 1)
580      (branch SM86WaitAsyncGroups count control . sm86WaitAsyncGroupsStall)
581      (branch SM86BarrierSynchronize control . sm86BarrierSynchronizeStall)
582      (branch SM86BarrierSynchronizeCount barrier threads control . sm86BarrierSynchronizeStall)
583      (branch SM86StoreGlobal address value offset control . 1)
584      (branch SM86StoreGlobalWide address value offset control . 1)
585      (branch SM86StoreGlobal64 address value offset control . 1)
586      (branch SM86ReduceGlobalAddFloat32 address value offset control . 1)
587      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . 1)
588      (branch SM86Branch offset descriptor control . 1)
589      (branch SM86Exit control . 1)))
590
591-- A scoreboard barrier as a hazard key: 300 + its number (SB0 .. SB5).  An
592-- instruction that sets one (write or read barrier) makes it pending
593-- sm86BarrierSetCycles after issue -- ASSUMED, like the table above: a
594-- waiter issued sooner could miss it -- and an instruction whose wait mask
595-- names it reads it.
596def sm86BarrierSetCycles : Nat = 2
597
598def sm86BarrierKeys =
599  (lambda unrestricted barrier : (family SM86Barrier) .
600    (eliminate SM86Barrier (lambda unrestricted current : (family SM86Barrier) . (family StdList Nat)) barrier
601      (branch SM86Barrier0 . (constructor StdList StdListCons Nat 300 sm86NoRegisters))
602      (branch SM86Barrier1 . (constructor StdList StdListCons Nat 301 sm86NoRegisters))
603      (branch SM86Barrier2 . (constructor StdList StdListCons Nat 302 sm86NoRegisters))
604      (branch SM86Barrier3 . (constructor StdList StdListCons Nat 303 sm86NoRegisters))
605      (branch SM86Barrier4 . (constructor StdList StdListCons Nat 304 sm86NoRegisters))
606      (branch SM86Barrier5 . (constructor StdList StdListCons Nat 305 sm86NoRegisters))
607      (branch SM86Barrier6 . (constructor StdList StdListCons Nat 306 sm86NoRegisters))
608      (branch SM86BarrierNone . sm86NoRegisters)))
609
610-- the barriers a control word sets
611def sm86ControlSetKeys =
612  (lambda unrestricted control : (family SM86Control) .
613    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . (family StdList Nat)) control
614      (branch SM86ControlValue stall yield write read wait reuse .
615        (stdListAppend Nat (sm86BarrierKeys write) (sm86BarrierKeys read)))))
616
617-- the barriers a control word's wait mask names (bit b: SB b)
618def sm86ControlWaitKeys =
619  (lambda unrestricted control : (family SM86Control) .
620    (eliminate SM86Control (lambda unrestricted current : (family SM86Control) . (family StdList Nat)) control
621      (branch SM86ControlValue stall yield write read wait reuse .
622        (nat-eliminate
623          (lambda unrestricted current : Nat . (family StdList Nat))
624          sm86NoRegisters
625          (lambda unrestricted bit : Nat . (lambda unrestricted induction : (family StdList Nat) .
626            (nat-eliminate
627              (lambda unrestricted current : Nat . (family StdList Nat))
628              induction
629              (lambda unrestricted set : Nat . (lambda unrestricted ignored : (family StdList Nat) .
630                (constructor StdList StdListCons Nat (naturalAdd 300 bit) induction)))
631              (nat-modulo (nat-divide (byte-to-nat wait) (naturalPowerOfTwo bit)) 2))))
632          6))))
633
634
635def sm86OpSummaryMake =
636  (lambda unrestricted reads : (family StdList Nat) .
637    (lambda unrestricted writes : (family StdList Nat) .
638      (lambda unrestricted predicateWrites : (family StdList Nat) .
639        (lambda unrestricted variable : Nat .
640          (lambda unrestricted latency : Nat .
641            (lambda unrestricted minimum : Nat .
642            (lambda unrestricted control : (family SM86Control) .
643              (constructor SM86OpSummary SM86OpSummaryValue
644                reads writes predicateWrites
645                (sm86ControlWaitKeys control) (sm86ControlSetKeys control)
646                (sm86ControlStallOf control) latency variable minimum control))))))))
647
648def sm86OpSummaryOfBody =
649  (lambda unrestricted body : (family SM86InstructionBody) .
650    (eliminate SM86InstructionBody
651      (lambda unrestricted current : (family SM86InstructionBody) . (family SM86OpSummary))
652      body
653      (branch SM86MoveConstant destination bank offset control . (sm86OpSummaryMake sm86NoRegisters (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
654      (branch SM86SpecialToRegister destination source control . (sm86OpSummaryMake sm86NoRegisters (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
655      (branch SM86MoveImmediate destination immediate control . (sm86OpSummaryMake sm86NoRegisters (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
656      (branch SM86IntegerMultiplyAddConstant destination left bank offset addend control . (sm86OpSummaryMake (sm86One left (sm86One addend sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
657      (branch SM86IntegerMultiplyAddImmediate destination left immediate addend control . (sm86OpSummaryMake (sm86One left (sm86One addend sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
658      (branch SM86IntegerMultiplyAddWideConstant destination left right bank offset control . (sm86OpSummaryMake (sm86One left (sm86Pair right sm86NoRegisters)) (sm86Pair destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
659      (branch SM86IntegerAddThreeImmediate destination left immediate control . (sm86OpSummaryMake (sm86One left sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
660      (branch SM86IntegerAddThreeRegister destination left right control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
661      (branch SM86ShiftRightImmediate destination source amount control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
662      (branch SM86LogicThreeInputTruthTable destination left right truthTable control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
663      (branch SM86IntegerToFloat destination source control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
664      (branch SM86FloatAdd destination left right control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
665      (branch SM86FloatMultiply destination left right control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
666      -- Double arithmetic has variable latency, including late source reads.
667      -- Mesa NAK ir.rs, has_fixed_latency, revision b1fe47e94409d81924c8663f58fac97e66ab4527:
668      -- https://chromium.googlesource.com/external/gitlab.freedesktop.org/mesa/mesa/+/b1fe47e94409d81924c8663f58fac97e66ab4527/src/nouveau/compiler/nak/ir.rs
669      -- Both halves participate; waiting on the low word alone is insufficient.
670      (branch SM86Float64Binary operation destination left right control . (sm86OpSummaryMake (sm86Pair (sm86RegisterPairBase left) (sm86Pair (sm86RegisterPairBase right) sm86NoRegisters)) (sm86Pair (sm86RegisterPairBase destination) sm86NoRegisters) sm86NoRegisters 1 0 1 control))
671      (branch SM86FloatConvert conversion control . (sm86OpSummaryMake (sm86ConversionReads conversion) (sm86ConversionWrites conversion) sm86NoRegisters 1 0 1 control))
672      (branch SM86FloatFusedMultiplyAdd destination left right addend control . (sm86OpSummaryMake (sm86One left (sm86One right (sm86One addend sm86NoRegisters))) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
673      (branch SM86MultiFunctionUnitApproximation destination source operation control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
674      (branch SM86FloatMinimumOrMaximum destination left right mode control . (sm86OpSummaryMake (sm86One left (sm86One right sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
675      (branch SM86FloatNegate destination source control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
676      (branch SM86FloatPairToPackedHalfPair destination high low control . (sm86OpSummaryMake (sm86One high (sm86One low sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
677      (branch SM86FloatPairToPackedBFloat16Pair destination high low control . (sm86OpSummaryMake (sm86One high (sm86One low sm86NoRegisters)) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
678      (branch SM86HalfToFloat destination source selector control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
679      (branch SM86BFloat16ToFloat destination source selector control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 0 sm86FixedLatencyCycles 1 control))
680      (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))
681      (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))
682      (branch SM86LoadGlobal destination address offset control . (sm86OpSummaryMake (sm86Pair address sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
683      (branch SM86LoadGlobalWide destination address offset control . (sm86OpSummaryMake (sm86Pair address sm86NoRegisters) (sm86Quad destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
684      (branch SM86WarpShuffle destination source lane segment mode control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
685      (branch SM86LoadShared destination address offset control . (sm86OpSummaryMake (sm86One address sm86NoRegisters) (sm86One destination sm86NoRegisters) sm86NoRegisters 1 0 1 control))
686      (branch SM86LoadSharedMatrix destination address offset count transpose control . (sm86OpSummaryMake (sm86One address sm86NoRegisters) (sm86RegisterRun destination (sm86SharedMatrixRegisters count) sm86NoRegisters) sm86NoRegisters 1 0 1 control))
687      (branch SM86StoreShared address value offset control . (sm86OpSummaryMake (sm86One address (sm86One value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
688      (branch SM86LoadGlobalToShared address offset source sourceOffset control . (sm86OpSummaryMake (sm86One address (sm86Pair source sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
689      (branch SM86CommitAsyncGroup control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 1 control))
690      (branch SM86WaitAsyncGroups count control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 sm86WaitAsyncGroupsStall control))
691      (branch SM86BarrierSynchronize control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 sm86BarrierSynchronizeStall control))
692      (branch SM86BarrierSynchronizeCount barrier threads control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 sm86BarrierSynchronizeStall control))
693      (branch SM86StoreGlobal address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86One value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
694      (branch SM86StoreGlobalWide address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86Quad value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
695      (branch SM86StoreGlobal64 address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86Pair value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
696      (branch SM86ReduceGlobalAddFloat32 address value offset control . (sm86OpSummaryMake (sm86Pair address (sm86One value sm86NoRegisters)) sm86NoRegisters sm86NoRegisters 0 0 1 control))
697      (branch SM86PredicateGreaterThanImmediate predicate source immediate control . (sm86OpSummaryMake (sm86One source sm86NoRegisters) sm86NoRegisters (sm86PredicateKeys predicate) 0 sm86FixedLatencyCycles 1 control))
698      (branch SM86Branch offset descriptor control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 1 control))
699      (branch SM86Exit control . (sm86OpSummaryMake sm86NoRegisters sm86NoRegisters sm86NoRegisters 0 0 1 control))))