Repository navigation

Formal on NVIDIA GPUs: integrated --gpu=cuda stack + hardware runbook - #10

Draft

certik wants to merge 29 commits into

formal-cuda-nvidia-basefrom

test/formal-cuda-nvidia

Draft

Formal on NVIDIA GPUs: integrated --gpu=cuda stack + hardware runbook#10
certik wants to merge 29 commits into
formal-cuda-nvidia-basefrom
test/formal-cuda-nvidia

Commits on Oct 18, 2026
- fix: regenerate CUDA sources per translation unit
  certik
  committed
  e4bb7dc
- fix: frame CUDA archive metadata
  certik
  committed
  91ae734
- fix: keep native CUDA registrar local
  certik
  committed
  161e7a2
- fix: resolve CUDA archive libraries before source collection
  certik
  committed
  ac9c757
Commits on Oct 19, 2026
- fix: cover CUDA library selection helpers
  certik
  committed
  fe16b8a
- fix: compile CUDA device code for the target GPU architecture
  certik
  committed
  b2f389b
- fix: make formal CUDA fixtures portable
  certik
  committed
  33ce46e
- fix: give each CUDA translation unit a uniquely named kernel registrar
  certik
  committed
  5430573
- fix: skip a GPU launch with no threads in the CUDA runtime
  certik
  committed
  6a5d5a1
- test: run the GPU tests that pass on an NVIDIA GPU with the cuda backend
  certik
  committed
  24efaca
- fix: give each GPU thread its own copy of per-iteration arrays
  certik
  committed
  f1bbb3a
- Merge branch 'pr-15546' into test/formal-cuda-nvidia
  certik
  committed
  5033cd4
- Merge branch 'pr-15559' into test/formal-cuda-nvidia
  certik
  committed
  a1cc5c7
- Merge branch 'pr-15560' into test/formal-cuda-nvidia
  certik
  committed
  4f1f3fb
- Merge branch 'pr-15562' into test/formal-cuda-nvidia
  certik
  committed
  09a1155
- Merge branch 'pr-15563' into test/formal-cuda-nvidia
  certik
  committed
  2c09997
- test: restore cuda labels from #15562/#15563 dropped while merging
  certik
  committed
  e569d5a
- Merge branch 'pr-15569' into test/formal-cuda-nvidia
  certik
  committed
  386048e
- fix: declare only the variables a GPU kernel scope refers to
  certik
  committed
  8d5b1ed
- fix: evaluate each operand of a defined operator once
  certik
  committed
  0dadf0c
- fix: forget tracked counters across calls in GPU array privatization
  certik
  committed
  f13ef24
- Merge branch 'pr-15569' into test/formal-cuda-nvidia
  certik
  committed
  d5c48f1
- Merge branch 'pr-15570' into test/formal-cuda-nvidia
  certik
  committed
  e51d12a
- Merge branch 'pr-15578' into test/formal-cuda-nvidia
  certik
  committed
  b69450c
- perf(gpu): reuse CUDA scratch buffers across launches
  certik
  committed
  9021c8b
- Merge branch 'pr-15580' into test/formal-cuda-nvidia
  certik
  committed
  65b945d
- test: regenerate gpu_metal_474 CUDA reference for the combined stack
  certik
  committed
  97301a0
- ci: document and script validating --gpu=cuda on NVIDIA hardware with Formal
  certik
  committed
  3ba8e18
- ci: check that every do concurrent in Formal is offloaded
  certik
  committed
  93826d8

Commits

Commits on Oct 18, 2026

Commits on Oct 19, 2026