PaperlayerView exact revision on arXiv

Source-linked AI summary

Verification of Compiler-to-Accelerator Mappings for Machine Learning Accelerators

Akash Gaonkar, Mike He, Yi Li, Bo-Yuan Huang, Andrew Cheung, Vishal Canumalla, Gus Henry Smith, Zachary Tatlock, Grigory Fedyukovich, Sharad Malik, Aarti Gupta

arXiv:2609.30651v1cs.PL

TL;DR

ML compiler mappings to specialized accelerators are often not checked against formal hardware semantics, leaving their functional equivalence unverified. BOLT aligns software and hardware loops, relates their tensor layouts, and verifies product programs; it successfully verifies complex mappings for open-source accelerators, with best-effort alignment as a scope caveat.

  • Problem

    Most ML compiler frameworks do not verify compiler-to-accelerator mappings against formal hardware semantics, despite correctness requiring equivalent outputs for the same inputs.

    Source: §1 · p. 1, §1.1 · p. 3

  • Method

    BOLT uses product programs, a sync-skeleton to guide loop alignment, and a layout-sketch to specify data-layout relationships without compiler-internal mapping information.

    Source: §1.2 · p. 3, Summary of Contributions · p. 6

  • Results

    BOLT successfully verified complex mappings across two open-source ML accelerators, including mappings with deeply nested loops and dynamic data layouts.

    Source: §7.3 · p. 21, §9 · p. 23

  • Takeaways & Limitations

    The results demonstrate that program-equivalence verification can handle several complex coarse-grained accelerator mappings, including four verified with actual hardware parameter values.

    Source: §7.3 · p. 21, §9 · p. 23

    Best-effort alignment may leave loops unmatched, requiring additional invariants and potentially increasing solver time or causing verification to fail, without affecting soundness.

    Source: §4.3 · p. 15

Abstract

from arXiv · show

To meet the performance needs of modern machine learning (ML) applications, ML compiler frameworks support compiler-to-accelerator mappings that offload parts of application code to operations in specialized hardware accelerators. However, most of these frameworks do not verify these mappings down to the hardware level, potentially resulting in functional mismatches. In this paper we propose BOLT, the first framework for formally verifying the correctness of compiler-to-accelerator mappings for coarse-grained intrinsics in ML accelerators, with respect to a formal hardware semantics. BOLT does not require additional information from the compiler, and verifies the functional equivalence of the application code and the code for the mapped hardware accelerator intrinsic, including handling of complex loop nests and tensor data layouts in hardware. It effectively utilizes a pattern of *aligning* software loops with the hardware, followed by *relating* corresponding data layouts, to enable verification using well-aligned product programs. To support these steps, we propose two custom templates --- the sync-skeleton and the layout-sketch --- to guide users in aligning loops and specifying data layout relationships, respectively. We have developed a proof-of-concept prototype for BOLT and use it to successfully verify the correctness of several complex mappings for two recent open-source ML accelerators.

1 Introduction

ML compilers map software tensor operations to specialized hardware, but these mappings often lack verification against hardware semantics. BOLT checks their functional equivalence by aligning software and hardware loops, relating their data layouts, and verifying a product program.

1 Introduction

  • Specialized accelerators use parallel loops and customized tensor storage to improve performance, motivating compiler mappings from application code to coarse-grained hardware operations.ML frameworks including BYOC [9], Exo, MLIR, Halide, and 3LA support this approach.Source: §1 · pp. 1–2

1.1 Motivation: Verifying correctness of compiler-to-accelerator mappings

  • Most ML compilers do not verify mappings against formal hardware semantics, although correctness requires the mapped code to preserve the original program's outputs.BOLT frames this as equivalence for the same input tensors, including the general case where no internal compiler correspondences are available.Source: §1.1 · p. 2

1.2 Proposed framework: Bolt

  • BOLT formally verifies coarse-grained accelerator mappings without requiring compiler-internal mapping information, using Hex to represent MMIO code with hardware semantics.Hex models MMIO code as a stateful program, with hardware behavior specified by an Instruction Level Abstraction model.Source: §1.2 · p. 3, §1.4 · p. 4

1.3 Verification Challenges

  • Verification is difficult because hardware semantics must be related to software, while deeply nested loops and optimized buffer layouts obscure tensor correspondences.Parallelism, partitioning, rearrangement, duplication, and complex address arithmetic make these correspondences challenging to reason about.Source: §1.1 · p. 3, §1.3 · p. 4

1.4 Bolt: Key Ideas and Contributions

  • BOLT first aligns software loops with hardware compute loops, then relates tensor layouts in corresponding updates to decompose the equivalence check.The sync-skeleton guides alignment; the layout-sketch captures output correspondences and helps construct relational invariants.Source: §1.4 · pp. 4–5

Summary of Contributions

  • BOLT combines product programs and user-guided templates, and successfully verifies complex mappings from two open-source accelerators, including a 29-loop product program of depth seven.The sync-skeleton and layout-sketch guide loop alignment and data-layout relationships, respectively.Source: Summary of Contributions · p. 6

2 Overview of the Bolt framework

The overview follows a FlexASR linear-layer mapping from functional IR and MMIO code through BOLT's alignment, layout-relation, and verification steps. The example shows how its templates support a product program while retaining checks for invalid rewrites.

2.1 Running Example

  • The FlexASR example maps a functional IR linear-layer operation to MMIO commands, whose final command triggers the accelerator computation.The example's Hex code represents each hardware call and the computation it triggers.Source: §2.1 · p. 6, §2.2 · p. 7

2.2 Bolt in action

  • Hex represents accelerator code as stateful loops and buffer updates, including parallel hardware loops and address arithmetic for tensor layouts.The FlexASR linear-layer implementation has 28 hardware loops, including loops for processing-element and SIMD parallelism.Source: §2.2 · p. 7
  • The sync-skeleton extracts hardware tensor-computation loops while abstracting data-movement loops, then guides best-effort rewriting of IR to align those loops.In the example, the skeleton contains 10 loops, and 29 rewriting steps align the IR with them.Source: §2.2 · pp. 8–9
  • For each aligned loop, a layout-sketch specifies correspondence between updated IR tensor elements and hardware buffer elements, from which relational invariants are constructed.For the example, s[j] corresponds to macAcc[p, j]; invalid invariants cause verification to fail with a counterexample.Source: §2.2 · p. 9
  • BOLT checks the annotated product program by generating verification conditions for Z3; the reduced running example verified in 104 seconds.Only IR rewriting can introduce unsoundness through incorrect rewrite rules; the other steps are sound or checked during verification.Source: §2.2 · pp. 9–10

3 Hex: A Verification Language for Hardware Explication

Hex provides a structured-program view of accelerator hardware semantics for proving equivalence between IR and MMIO code. Its loops and multidimensional buffers support aligning software computation with hardware execution and relating tensor layouts.

3 Hex: A Verification Language for Hardware Explication

  • Hex also represents the verification product program and supports annotations for relational loop invariants.Hex is a structured-program view of transition-system hardware semantics; the authors note that an existing verification language could be extended to provide these features.Source: §3 · p. 10
  • Hex parameters describe application and hardware bounds or dimensions, and derived parameters combine both; verification substitutes concrete values and does not prove parametric models.Parameters are symbolic during Align and Relate, but concrete values are used during Verify to address solver limitations with nonlinear arithmetic.Source: §3 · pp. 10–11
  • Hex translates hierarchical ILA state updates into hw_call statements and makes implicit parallelism and counter-driven iteration explicit as loops.Parallel state updates and control-flow back-edges are represented with par-for and for loops, respectively.Source: §3 · p. 11
  • Hex for and par-for loops model tensor map/reduce and data movement, while where-by clauses relate software counters to hardware counters.Loops also capture whether hardware uses SIMD or counter-based iteration.Source: §3 · pp. 11–12
  • Hex multidimensional buffers represent related hardware registers or buffers holding tensor data, with atomic, globally visible updates; Bolt assumes the code is data-race-free.For example, macAcc[p, j] denotes the jth accumulator of the pth PE.Source: §3 · p. 12
  • Hex treats accelerator custom numerical operations as uninterpreted functions and introduces corresponding IR-side operations through rewrite rules, checking equivalence modulo those functions.Source: §3 · p. 12

4 Align step: Aligning the IR code with loop nests in hardware

The Align step rewrites IR loop nests to match accelerator tensor-computation loops, using a sync-skeleton extracted from hardware Hex code. Heuristics omit data-movement loops, while best-effort rewriting can leave loops unaligned.

4.1 Sync-Skeleton

  • The sync-skeleton abstracts tensor computations into a functional template, omitting data buffers and data-movement loops so standard tensor-program rewrites can align IR loops.It represents control flow and tensor-computing loops with patterns matched during rewriting.Source: §4.1 · p. 12

4.2 Heuristic procedure for loops in the sync-skeleton

  • Heuristics include loops that operate on tensor state and classify computation loops as map, reduce, or unknown; parallel loops are treated as maps to prevent data races.Loops without accumulator state can be classified as maps; accumulator state is detected through cross-iteration read-write conflicts.Source: §4.2 · p. 13
  • The inclusion heuristic is less effective when unrelated tensor computations co-occur, while complex reductions with overwriting are categorized as unknown loops.The paper reports that unrelated co-occurring tensor computations were rare and absent from its evaluations.Source: §4.2 · pp. 13–14

4.3 Rewriting the IR code

  • Rewriting combines structural rules with parameter substitution, arithmetic, custom numeric, and type-casting rules to match IR loops to the sync-skeleton.The rule categories are summarized in Table 2.Source: §4.3 · p. 14, Table 2 · p. 14
  • In the running example, 29 rewrites fully matched all 10 sync-skeleton loops; incomplete rewriting may leave loops unaligned, affecting solver performance but not soundness.Parameter substitution with structural and arithmetic rewrites matched 7 of 10 loops; adding custom numeric and type-casting rules completed the match.Source: §4.3 · pp. 14–15, Table 3 · p. 14

5 Relate step: Relating the tensor data layouts

The Relate step captures tensor-data correspondences between IR and accelerator Hex code as relational loop invariants. Layout-sketches specify those relationships for aligned loops and guide invariant construction.

5.1 Layout-Sketch

  • A layout-sketch relates an IR tensor assignment to a hardware buffer assignment, including the input correspondences on which they depend.Its tuple records the quantified loop range, IR access, hardware access, and input correspondences.Source: §5.1 · p. 15

5.2 Tactics for developing a layout-sketch

  • Layout-sketches work most directly when aligned loops compute the same outputs from the same inputs in lockstep; mismatches may require extra invariants during verification.IR loops identify tensor results and their inputs, while nearby aligned loops can often supply reusable correspondence patterns.Source: §5.2 · p. 16
  • For data movement and zero-initialization without an aligned loop, users relate source and destination accesses or specify the order in which elements are zeroed.Data movement uses address arithmetic to relate accesses; zero-initialization quantifies over surrounding loop counters.Source: §5.2 · pp. 16–17

5.3 Procedure for specifying data layout invariants from a layout-sketch

  • The procedure turns each layout-sketch correspondence into an invariant equating tensor and buffer elements over a range expressed with shared loop counters.Aligning loop nests supplies the shared counters needed to identify corresponding elements.Source: §5.3 · p. 17
  • Guards track which elements correspond during execution: map outputs cover iterations up to the current counter, while reduce accumulators need no guard.For overwritten hardware inputs, a guard instead preserves correspondence for the remaining iterations.Source: §5.3 · p. 17

6 Verify step: Verifying the product program

BOLT verifies equivalence by turning the aligned software and accelerator programs into a product program, then checking its verification conditions with an SMT solver. The Verify step relies on loop and hardware-state invariants, including relational data-layout invariants.

6 Verify step: Verifying the product program

  • BOLT builds a product program from transformed IR and accelerator Hex code, then checks loop-boundary verification conditions with Z3.The conditions use bitvectors, uninterpreted functions, arrays, and linear integer arithmetic.Source: §6 · p. 17
  • The verifier cuts the product program at loops, annotates the resulting cut-point graph, and checks a verification condition for each loop-free segment.Validity of every condition establishes equivalence; an invalid condition can indicate weak or strong annotations, or a program bug.Source: §6 · p. 17, Figure 7 · p. 18
  • The verifier substitutes concrete parameter values to avoid nonlinear address arithmetic, so it does not yet prove equivalence for all parameterized sizes and dimensions.The authors identify parametric verification using improved SMT solvers or interactive theorem provers as future work.Source: §6 · p. 18
  • For layout-invariant assumptions, BOLT removes universal quantifiers through bounded flattening using bounds from the concrete parameters.This addresses SMT solvers' difficulty reasoning about quantified assumptions and assertions.Source: §6 · p. 18

6.1 Categories of useful invariants

  • BOLT uses loop-bound, hardware-counter, WORM, and data-layout invariants; static analyses derive many, but not all, required invariants.WORM captures a register value written once and read later, including across loops.Source: §6.1 · p. 18

7 Case Studies and Evaluation

BOLT was evaluated on complex mappings for FlexASR and HLSCNN, with successful verification on real hardware parameters for four mappings and downscaled parameters for two. The case studies also expose how loop structure, layout invariants, and user effort affect verification.

7.1 Case studies: Compiler-to-Accelerator Mappings

  • The case studies cover FlexASR linear-layer and pooling, plus HLSCNN 2D convolution and an accumulative variant with a hardware flag enabled.The accumulative mapping was created and verified because its flag changes data-layout correspondences.Source: §7.1 · p. 19

7.2 Bolt by the numbers

  • Although the mappings can look loop-light in MMIO, FLL's Hex code has 28 hardware loops and maximum nesting depth 7.Its mapping also includes significant hardware data-parallelism and data movement.Source: §7.2 · pp. 19–20
  • Align matches the IR loops to sync-skeleton loops, while Relate uses layout-sketches to specify relational data-layout invariants.The evaluation reports rewriting steps for alignment and invariant counts for the Relate step; FLL requires many invariants.Source: §7.2 · pp. 20–21

7.3 Results for the Verify step

  • Four mappings were verified with actual hardware parameters, and two more with downscaled parameters retaining key hardware features.The verified mappings cover varied coarse-grained ML operations across two accelerators.Source: §7.3 · p. 21
  • With loop nests held constant, C2D and C2D+ take longer to verify when more data-layout invariants are required; mappings with more or deeper loops also generally take longer.These cases indicate that both loop structure and data-layout invariants affect verification time.Source: §7.3 · pp. 21–22
  • Providing sync-skeletons and manual invariants for unaligned loops reduced FLL verification time by up to 52%, but produced similar or longer times in other cases.BOLT therefore unrolls unaligned loops by default to minimize user burden.Source: §7.3 · p. 22
  • Z3/Spacer did not finish the smallest case within one day without invariants, and SMT-based bounded model checking failed even on the smallest cases.The authors attribute the BMC difficulty to extensive unrolling of nested loops.Source: §7.3 · p. 22

8 Related Work

Related work verifies compiler transformations, hardware, or program equivalence in narrower settings, but does not cover BOLT's target of black-box mappings against formal accelerator semantics. BOLT draws on product-program verification while addressing complex hardware loop nests and data layouts.

8 Related Work

  • Verified compiler systems target high-level IR-to-C compilation or certified C compilation, but do not verify coarse-grained ML accelerator intrinsics against hardware semantics.Liu et al. and Courant and Leroy use Rocq; CompCert targets conventional processor architectures.Source: §8 · p. 22
  • CGRA translation validation uses compiler information, while Exo and Mosaic verify transformations or tensor properties rather than black-box mappings against formal hardware semantics.BOLT addresses the stated mapping-verification gap for these compilers.Source: §8 · p. 22
  • HLS equivalence checking relies on statically interpretable branches and bounds and loop unrolling, while affine dataflow verification requires nearly identical operations on both sides.BOLT instead uses loop invariants and considers formal hardware semantics.Source: §8 · p. 22
  • Prior product-program work informs BOLT's Align and Relate steps, but the authors report no prior work addressing case studies with comparable loop and dynamic-layout complexity.BOLT introduces the sync-skeleton and layout-sketch to guide loop alignment and relational-invariant annotation.Source: §8 · p. 23

9 Conclusions and Future Directions

BOLT introduces a framework for verifying coarse-grained ML compiler-to-accelerator mappings against formal hardware semantics. Its evaluation verifies complex mappings, and its future work targets invariant synthesis and broader rewriting support.

9 Conclusions and Future Directions

  • BOLT verifies coarse-grained ML accelerator mappings against formal hardware semantics using program equivalence.The framework addresses mappings without compiler-provided construction information.Source: §9 · p. 23
  • The evaluation successfully verifies complex mappings for open-source ML accelerators, including deeply nested loops and dynamic data layouts.Source: §9 · p. 23
  • Future work targets automatic generation of key invariants and a comprehensive set of rewriting transformations using equality saturation.Source: §9 · p. 23

Related papers

Loading 2609.30651v1…