Platform.DGXSpark.Profile

1module Platform.DGXSpark.Profile
2
3import Accelerator.SM86.Capability
4import Model.Parameter
5import Model.Word64
6import Platform.AArch64.HostCapability
7import Std.Natural
8import Std.Physical
9import Std.Word
10
11-- The one measured DGX Spark (NVIDIA GB10, product GX10) profile.  Every value
12-- here was read on 2026-09-18 from the host recorded in
13-- evidence/hardware/dgx-spark-20260918/ (lscpu, /proc/cpuinfo, /proc/meminfo,
14-- getconf PAGESIZE, nvidia-smi -q).  Hostname, kernel, driver and product
15-- strings live in Platform.DGXSpark.PhysicalInventory as evidence only.
16def dgxSparkProfileIdentity : Bytes =
17  b"dgx-spark-bringup-v1"
18
19-- MIDR_EL1 implementer 0x41 (Arm Ltd); parts 0xd85 (Cortex-X925) and 0xd87
20-- (Cortex-A725), ten cores each, one NUMA node.
21def dgxSparkArmImplementer : Nat =
22  65
23
24def dgxSparkPerformanceCorePart : Nat =
25  3461
26
27def dgxSparkPerformanceCoreCount : Nat =
28  10
29
30def dgxSparkEfficiencyCorePart : Nat =
31  3463
32
33def dgxSparkEfficiencyCoreCount : Nat =
34  10
35
36-- /proc/meminfo MemTotal 127,535,204 kB = 130,596,048,896 bytes of unified
37-- CPU/GPU memory; there is no dedicated video memory (nvidia-smi reports N/A).
38def dgxSparkTotalMemory : ByteCount =
39  (stdByteCount 0x0000_001E_6821_9000)
40
41def dgxSparkPageSize : Nat =
42  4096
43
44def dgxSparkLevel2Cache : ByteCount =
45  (stdByteCount 0x0000_0000_0190_0000)
46
47def dgxSparkLevel3Cache : ByteCount =
48  (stdByteCount 0x0000_0000_0180_0000)
49
50def dgxSparkHostObservation : (family AArch64HostCapabilities) =
51  (constructor
52    AArch64HostCapabilities
53    AArch64HostCapabilitiesValue
54    dgxSparkArmImplementer
55    dgxSparkPerformanceCorePart
56    dgxSparkPerformanceCoreCount
57    dgxSparkEfficiencyCorePart
58    dgxSparkEfficiencyCoreCount
59    (stdByteCountValue dgxSparkTotalMemory)
60    dgxSparkPageSize
61    (stdByteCountValue dgxSparkLevel2Cache)
62    (stdByteCountValue dgxSparkLevel3Cache)
63    1
64    0)
65
66-- What the Alpha Stage-0 tree needs from an AArch64 build host: Arm cores, at
67-- least sixteen of them, at least 64 GiB (the release build of the Coppelius
68-- host emitter peaked at 7.9 GB RSS), 4 KiB pages, and no host fallback.
69def dgxSparkBuildHostMinimumMemory : ByteCount =
70  (stdByteCount 0x0000_0010_0000_0000)
71
72def dgxSparkBuildHostRequirements : (family AArch64HostRequirements) =
73  (constructor
74    AArch64HostRequirements
75    AArch64HostRequirementsValue
76    dgxSparkArmImplementer
77    16
78    (stdByteCountValue dgxSparkBuildHostMinimumMemory)
79    dgxSparkPageSize
80    1)
81
82def dgxSparkBuildHostAdmit =
83  (lambda unrestricted observed : (family AArch64HostCapabilities) .
84    (aarch64HostAdmit dgxSparkBuildHostRequirements observed))
85
86-- The GB10 seen through the SM86 capability lens.  Compute capability 12.1
87-- (Blackwell); no dedicated video memory; QMD, pushbuffer and GPFIFO support
88-- are recorded as zero because no Alpha owner has demonstrated them on this
89-- architecture.  Any SM86 requirement must reject this observation: the
90-- accepted SM86 artifacts do not run here, and that is a fact of the profile,
91-- not a fallback.
92def dgxSparkDeviceComputeMajor : Nat =
93  12
94
95def dgxSparkDeviceComputeMinor : Nat =
96  1
97
98def dgxSparkDeviceObservationSM86 : (family SM86DeviceCapabilities) =
99  (constructor
100    SM86DeviceCapabilities
101    SM86DeviceCapabilitiesValue
102    dgxSparkDeviceComputeMajor
103    dgxSparkDeviceComputeMinor
104    modelWord64Zero
105    modelWord64Zero
106    modelWord64Zero
107    1024
108    1
109    1
110    0
111    0
112    0
113    1
114    0)