1 Introduction↩︎

1.1 The Drive for Hardware Parallelism in HLS↩︎

High-Level Synthesis (HLS) drastically shortens the hardware development cycle by shifting design entry from structural Register Transfer Level (RTL) syntax up to high-level programming languages like C/C++ [1], [2]. Modern state-of-the-art HLS frameworks leverage compiler optimization pipelines to extract loop-level parallelism and automatically schedule operations into efficient parallel hardware architectures [3], [4]. To fully match this computational parallelism, the underlying memory system must deliver high bandwidth, which FPGAs achieve by partitioning and distributing application data across multiple isolated on-chip memory blocks or banks [5]. Loop unrolling duplicates sequential basic blocks to expose concurrent iteration traces within a single clock cycle, but its throughput gains are fundamentally bounded by the memory infrastructure’s ability to support non-interfering parallel data accesses [6].

1.2 The Bottleneck: Memory Conflicts and Affine Limitations↩︎

Concurrently scheduling these duplicated memory instructions incurs a significant risk of structural hazards when multiple parallel operations attempt to access the same single-ported memory bank during the same clock cycle. To track array coordinates within multi-dimensional iteration spaces, standard dependency solvers historically employ the polyhedral model [7]. However, these geometric techniques are bounded to static control structures where loop bounds and array access functions are affine combinations of enclosing loop variables.

In the presence of pointer arithmetic, dynamic memory allocation, or non-affine index strings—such as symbolic register multiplication, division, or modulo arithmetic—conventional analyses encounter limitations. Because legacy frameworks over-approximate systematically at the first sign of non-linear transformations, they trigger a safe but conservative fallback. This forces them to assume a dependency between all memory statements, resulting in a monolithic heap allocation that destroys potential parallelism. While conservative serialization remains a critical mathematical necessity to guarantee absolute safety when non-linear integer arithmetic cannot be resolved, executing this fallback creates an artificial bottleneck. This lack of precise spatial alias analysis ultimately forces HLS compilers to serialize operations or inject costly multiplexer-driven arbitration and stall logic that degrades target hardware efficiency.

1.3 A Spatial Resolution: Separation Logic↩︎

To overcome the non-affine bottleneck, we introduce a spatial resolution framework built upon Separation Logic [8], an extension of Hoare logic [9] designed for local reasoning about shared mutable data structures [10]. By utilizing the core separating conjunction operator (\(*\)), separation logic inherently embeds pointer non-aliasing properties directly into its algebraic structure, asserting that distinct spatial descriptions govern completely disjoint regions of the memory heap.

While prior hardware synthesis and dependency analysis methods have applied separation logic to source-level C/C++ abstract syntax trees (ASTs) [6], our framework operates directly on the LLVM Intermediate Representation (IR), utilizing symbolic execution paradigms established in software verification frameworks like Heapster [11] and llStar [12]. This low-level approach enables compositionality and allows us to intercept flat address arithmetic computed by the compiler’s getelementptr instructions [12]. By maintaining physical memory allocations and pure arithmetic states as distinct subsets, structural bank collisions evaluate to a spatial contradiction (\(P \ast P \Rightarrow \perp\)), reducing the memory conflict problem to an algebraic evaluation handled by downstream Satisfiability Modulo Theories (SMT) engines such as Z3 [13].

1.4 Contributions↩︎

In this paper, we formalize the detection of structural memory hazards in HLS scheduling loops by transforming low-level data dependency tracking into spatial logic validation properties. Our core theoretical and architectural contributions include:

• Formal Hardware Memory Model: We establish a static memory framework over the LLVM IR, mechanically abstracting multi-dimensional array index expressions via getelementptr instructions and binding them to polymorphic spatial memory bank predicates governing cyclic, block, and complete partitioning transformations.

• Conflict-Free Unrolling (CFU) Condition: We formulate a definitive spatial execution requirement, utilizing an iterated separating conjunction over target address offsets that detects physical bank hazards through automatic spatial logic collapse (\(\textsf{cfu}(E,A,N) \Rightarrow \perp\)).

• Automated SMT Translation and Fallback: We implement a mathematically sound translation function (\(\mathcal{T}\)) reducing spatial propositions into a pairwise inequality matrix across local Static Single Assignment (SSA) registers, avoiding rigid polyhedral constraints while introducing a conservative sequential fallback model to ensure absolute safety in the presence of undecidable non-linear integer arithmetic expressions.

2 Background: Arrays, Loops, and Hyperplanes↩︎

2.1 Array Partitioning and Loop Unrolling in HLS↩︎

When a High-Level Synthesis (HLS) compiler applies loop unrolling by a factor of \(U\), it performs standard basic block duplication to expose instruction-level parallelism. This optimization dictates that \(U\) concurrent memory accesses must be safely scheduled within a single hardware clock cycle to maximize throughput. However, synthesized on-chip SRAMs typically feature a limited number of access ports. To sustain the required parallel bandwidth, HLS tools employ array partitioning directives that mechanically divide a monolithic array footprint into \(N\) distinct physical memory banks. Common strategies include cyclic partitioning, where consecutive elements are interleaved round-robin across banks at offsets \(j \cdot N + k\), and block partitioning, which divides the array into contiguous chunks starting at \(\alpha + k \cdot B\). To avoid structural hazards—which occur when concurrent operations attempt to access the same single-ported memory bank simultaneously—the scheduler must mathematically guarantee that the target addresses map to strictly independent physical banks.

2.2 The Non-Affine Bottleneck in Polyhedral Analysis↩︎

To prove that duplicated memory accesses target independent banks, standard HLS compilers historically rely on the polyhedral model. This framework maps loop iteration spaces into multi-dimensional geometric hyperplanes to perform exact dependency analysis. However, polyhedral analysis strictly requires loop bounds and memory access functions to be affine—that is, linear combinations of enclosing loop variables and constants.

When array indices involve non-affine arithmetic—such as arbitrary symbolic variable multiplication, data-dependent indexing, or the modulo and division operations fundamentally required to evaluate cyclic and block bank mapping functions—the geometric model breaks down. Pioneering extensions of the polyhedral framework have successfully mitigated some of these limitations by elegantly employing parametric analysis to synthesize lightweight runtime checks and dynamic pipeline breaks, successfully parallelizing loops with uncertain or nonuniform dependencies [14]. These advanced dynamic techniques provide a robust foundation for runtime hazard resolution; however, to remain tractable within standard integer set libraries, they typically require the underlying dependence distances to retain an affine structure, and they can introduce specialized runtime controller logic to manage pipeline execution speeds dynamically [14]. To complement these runtime approaches, our framework aims to address non-linear address arithmetic statically at compile-time. By utilizing spatial logic directly over flattened intermediate expressions, we look to resolve complex bank mapping dependencies without relying on linear geometric bounds or generating additional runtime state-machine overhead.

2.3 Separation Logic in Hardware Verification↩︎

Separation Logic (SL) offers a rigorous mathematical foundation to reason about spatially distributed memory states, originally designed for shared mutable data structures [8], [10]. The fundamental unit of spatial resource isolation in SL is the separating conjunction operator (\(\ast\)). The spatial formula \(\Sigma_1 \ast \Sigma_2\) asserts that the memory heap can be partitioned into strictly disjoint hardware regions, embedding the non-aliasing property of pointers directly into the algebraic framework. A powerful consequence of this strict disjointness is that a single spatial resource cannot be exclusively owned by multiple concurrent execution entities; evaluating \(P \ast P\) instantly yields a logical contradiction (\(P \ast P \Rightarrow \perp\)) [15], [16].

Recent advancements have successfully applied SL to hardware verification and HLS parallelization [6]. Existing SL-based HLS tools focus on dynamic memory allocation, pointer-chasing, and shape analysis of recursive dynamic data structures (e.g., trees and linked lists) by inferring complex fix-point loop invariants. However, static array partitioning and flat loop unrolling still need to be studied. Our framework explicitly bridges this gap, adapting the disjointness axioms of SL down to the LLVM Intermediate Representation (IR) level [11], [12] to natively evaluate partitioned array bank mapping expressions, bypassing the polyhedral affine bottleneck.

3 HLS Memory Model in Separation Logic↩︎

3.0.0.1 Formal Syntax of the Spatial Framework

To ground the interactions between programmatic variables, symbolic non-affine expressions, and physical memory bank assets, we formally define the core language syntax via the following Backus-Naur Form (BNF) grammar. Unlike traditional software-oriented Separation Logic [8], [10], which operates over abstract syntax trees (ASTs), our framework operates directly on the LLVM Intermediate Representation (IR), following the approach of [11], [12].

Let \(\text{Reg}\) be the set of immutable LLVM virtual registers and global identifiers, \(\text{Reg}'\) be the set of auxiliary primed variables, and \(\text{Const}\) be the set of constant natural numbers. We distinguish a specific subset \(\text{ArrID} \subset \text{Reg}\) to represent the universe of synthesized array identifiers (e.g., \(@A,\)@B).

\[\begin{align} e \in \text{Expr} \quad &::= \quad c \in \text{Const} \mid x \in \text{Reg} \mid x' \in \text{Reg}' \mid e_1 + e_2 \mid e_1 - e_2 \mid e_1 \cdot e_2 \mid e_1 \pmod{e_2} \mid \lfloor e_1 / e_2 \rfloor \\ \Pi \in \text{Pure} \quad &::= \quad \text{true} \mid \text{false} \mid e_1 = e_2 \mid e_1 \neq e_2 \mid \Pi_1 \land \Pi_2 \\ \Sigma \in \text{Spatial} \quad &::= \quad \text{emp} \mid e_1 \mapsto e_2 \mid \textsf{bank}(e_1, A, e_2) \mid \textsf{arr}(A) \mid \Sigma_1 * \Sigma_2 \quad (\text{where } A \in \text{ArrID}) \end{align}\]

Where \(e_1 \cdot e_2\) natively models arbitrary symbolic variable multiplication, allowing non-affine index strings to step into the spatial heap definition before being resolved by a downstream SMT engine. The parameters within \(\textsf{bank}(e_k, A, e_N)\) follow the expression grammar rule (\(e\)), proving that bank locations are fundamentally treated as dynamic algebraic variants rather than rigid static integers.

3.0.0.2 Mechanical 1D Flattening via getelementptr

By shifting the semantic model to the LLVM IR level, our framework fundamentally bypasses the need to mathematically simulate the row-major flattening of multi-dimensional C/C++ arrays. The LLVM compiler mechanically lowers all complex array indexing into flat 1D arithmetic via the getelementptr (GEP) instruction. Consequently, the spatial framework simply extracts the resulting flat arithmetic expression \(e\) from the GEP instruction and feeds it directly into the bank mapping function, drastically simplifying the required operational semantics.

3.1 The Spatial Memory Heap and Store↩︎

To mathematically reason about High-Level Synthesis (HLS) architectures, we adapt the foundational framework of Separation Logic to model program execution and physical SRAM instances as distinct state components. Separation logic formally describes the program state using two distinct elements: the store and the heap.

3.1.0.1 The Monotonic Store (\(s\))

Because LLVM IR strictly enforces Static Single Assignment (SSA), our framework avoids the state-space explosion associated with modeling mutable C/C++ variables. Let \(\text{Reg}\) denote the set of LLVM virtual registers and \(\text{Val}\) represent the set of storable hardware values (which includes the set of physical memory addresses, \(\mathbb{L}\)). The store mathematically captures the immediate, immutable state of local registers in the synthesized hardware. It is defined as a partial function mapping registers to their currently assigned values: \[s : \text{Reg} \rightharpoonup \text{Val}\]

Due to SSA, this mapping is strictly monotonic during the symbolic execution of a basic block; virtual registers are never overwritten. For example, an evaluation of the store where \(s(\%x) = 3\) indicates that the virtual register \(\%x\) is permanently bound to the scalar value \(3\) for that execution path, eliminating the need for state-update tracking (\(s \to s'\)).

3.1.0.2 The Spatial Heap (\(h\))

While the store resolves register values, the heap models the spatially distributed on-chip memory (e.g., block RAMs). The heap, \(h\), is a finite partial function mapping physical, addressable memory locations to hardware values: \[h : \mathbb{L} \rightharpoonup \text{Val}\]

3.1.0.3 Domain and Codomain Distinction (\(\mathbb{L} \subset \text{Val}\))

It is a critical mathematical distinction of this framework that the codomain of the store (\(\text{Val}\)) and the domain of the heap (\(\mathbb{L}\)) are strictly not equivalent. In synthesized hardware, all memory addresses are values (typically unsigned bitvectors), but not all values (e.g., floating-point results, loop counters, booleans) are valid memory addresses. Therefore, the set of memory locations is a strict subset of all storable values: \[\mathbb{L} \subset \text{Val}\]

This intentional mismatch dictates the operational semantics of pointer dereferencing. When evaluating a spatial assertion such as \(\%x \mapsto v\), the state routes data through both functions sequentially: first, the store evaluates the register pointer \(s(\%x) = l\) (where \(l \in \mathbb{L}\)); second, the heap retrieves the data \(h(l) = v\) (where \(v \in \text{Val}\)). By maintaining \(\mathbb{L}\) and \(\text{Val}\) as distinct sets, the theoretical framework mathematically isolates pure arithmetic states from spatial memory allocations.

3.1.0.4 Spatial Ownership and Disjointness

The fundamental unit of spatial resource in this framework is the points-to relation. The assertion \(E \mapsto F\) strictly dictates that a physical SRAM address evaluated from expression \(E\) currently stores the value evaluated from \(F\), asserting exclusive ownership over that single physical location.

In physical hardware, structural hazards occur when concurrent parallel operations attempt to access the same single-ported memory bank simultaneously. We abstract the absence of such hazards through the strict mathematical property of heap disjointness. Two hardware memory heaps, \(h_1\) and \(h_2\), are strictly disjoint, denoted by \(h_1 \perp h_2\), if and only if their respective domains share no common physical addresses: \[h_1 \perp h_2 \iff \text{dom}(h_1) \cap \text{dom}(h_2) = \emptyset\]

3.1.0.5 The Separating Conjunction

This disjointness is elegantly encapsulated by the separating conjunction operator (\(*\)). The spatial formula \(\Sigma_1 * \Sigma_2\) asserts that the current heap can be partitioned into two strictly disjoint hardware regions (heaplets), \(h_1\) and \(h_2\), such that \(\Sigma_1\) holds for \(h_1\) and \(\Sigma_2\) holds for \(h_2\).

This operator embeds the non-aliasing property of pointers directly into the algebraic framework (e.g., \(E \mapsto F_1 * G \mapsto F_2 \implies E \neq G\)). By reducing parallel structural safety to spatial disjointness, HLS compilers can synthesize parallel memory accesses without conservative approximations of non-affine dependencies. Finally, the empty heap assertion, \(\text{emp}\), denotes a state where the active execution claims ownership of no physical memory resources.

3.2 Memory Bank Predicates↩︎

In High-Level Synthesis (HLS) flows built upon modern compiler infrastructure, source-level partitioning directives are lowered into LLVM IR metadata. This metadata explicitly instructs the backend to partition monolithic arrays into \(N\) distinct physical memory banks to increase memory bandwidth and enable parallel data access. To model this hardware transformation mathematically at the bitcode level, we introduce hardware-aware spatial predicates that encapsulate the exclusive ownership of specific partitioned memory banks.

Let array \(A\) be a finite contiguous allocation of \(M\) elements starting at physical base address \(\alpha \in \mathbb{L}\). We define the predicate \(\textsf{bank}(k, A, N)\) to assert exclusive spatial ownership over the \(k\)-th physical memory bank, where \(0 \le k < N\). The precise physical addresses governed by this predicate depend strictly on the HLS partitioning strategy employed.

3.2.0.1 The Static Hardware Environment (\(\Gamma\))

In our syntax, \(A \in \text{ArrID}\) acts purely as a symbolic identifier tied to an LLVM virtual register. To mathematically derive the physical constraints of the array—such as its base address and bounds—we introduce a fixed static hardware environment, \(\Gamma\). This environment acts as the formal equivalent of the LLVM module’s global symbol table and bitcode metadata, mapping an array identifier to its fixed hardware metadata tuple: its physical base address (\(\alpha \in \mathbb{L}\)), its total element capacity (\(M \in \mathbb{N}\)), and its partitioning scheme (\(\mathcal{P}\)).

\[\Gamma : \text{ArrID} \to \mathbb{L} \times \mathbb{N} \times \{ \text{Cyclic}, \text{Block}, \text{Complete} \}\]

For any array \(A\), its metadata is formally extracted via: \[\Gamma(A) = (\alpha, M, \mathcal{P})\]

Consequently, when the execution state evaluates a spatial predicate such as \(\textsf{bank}(k, A, N)\), the logical framework queries \(\Gamma(A)\) to anchor the abstract identifier \(A\) to the concrete physical SRAM address space defined by \(\alpha\) and bounded by \(M\).

3.2.0.2 Cyclic Partitioning

Under cyclic partitioning, consecutive array elements are interleaved across the \(N\) memory banks in a round-robin fashion. The \(k\)-th bank contains elements at offsets \(j \cdot N + k\). We formalize the spatial ownership of a cyclic bank using the iterated separating conjunction (\(\scalebox{1.5}{\ast}\)): \[\textsf{bank}_{cyc}(k, A, N) \triangleq \scalebox{1.5}{\ast}_{j=0}^{\lfloor (M-1-k)/N \rfloor} (\alpha + j \cdot N + k \mapsto v_{j,k})\] where \(v_{j,k} \in \text{Val}\) represents the value stored at that specific 1D SRAM address offset.

3.2.0.3 Block Partitioning

Under block partitioning, the array is divided into \(N\) contiguous chunks. Let \(B = \lceil M / N \rceil\) denote the block size. The \(k\)-th bank owns a contiguous sequence of addresses starting at \(\alpha + k \cdot B\). The spatial ownership for a block bank is formalized as: \[\textsf{bank}_{blk}(k, A, N) \triangleq \scalebox{1.5}{\ast}_{j=0}^{\min(B-1, M - 1 - k \cdot B)} (\alpha + k \cdot B + j \mapsto v_{j,k})\]

3.2.0.4 Complete Partitioning (The Boundary Case)

The third standard HLS directive is complete partitioning, which dissolves the SRAM entirely into discrete, independent hardware registers. Mathematically, this is modeled as a strict boundary case of either block or cyclic partitioning where the number of partitioned banks equals the total number of array elements (\(N = M\)). Consequently, the bank size is exactly 1, and the iterated conjunction collapses into a singular spatial points-to assertion for each physical index: \[\textsf{bank}_{comp}(k, A, M) \triangleq \alpha + k \mapsto v_k\] This demonstrates that our spatial framework universally captures all HLS memory architectures, scaling seamlessly from monolithic SRAMs (\(N=1\)) down to fully unrolled register files (\(N=M\)).

3.2.0.5 The Polymorphic Bank Predicate

To maintain the universality of our theoretical framework across diverse hardware generation strategies, we define the generic spatial predicate \(\textsf{bank}(k, A, N)\) as a polymorphic interface. During the static symbolic execution of an LLVM basic block, this abstract predicate is dynamically instantiated into a concrete spatial representation based on the specific HLS partitioning metadata attached to the array’s allocation instruction in the IR.

Let \(\mathcal{P} \in \{\text{Cyclic}, \text{Block}, \text{Complete}\}\) denote the specific partitioning scheme applied to array \(A\). The abstract bank predicate is formally defined as a piecewise mapping: \[\textsf{bank}(k, A, N) \triangleq \begin{cases} \textsf{bank}_{cyc}(k, A, N) & \text{if } \mathcal{P} = \text{Cyclic} \\ \textsf{bank}_{blk}(k, A, N) & \text{if } \mathcal{P} = \text{Block} \\ \textsf{bank}_{comp}(k, A, N) & \text{if } \mathcal{P} = \text{Complete} \end{cases}\]

Crucially, the parameters \(k\) and \(N\) are not restricted to compile-time natural constants; they are treated as symbolic expressions evaluated under the SSA store \(s\) and path condition \(\pi\), thereby natively accommodating non-affine variable terms (e.g., \(k = (x \cdot Y + y) \pmod N\)) whose functional disjointness is deferred to algebraic evaluation.

This mathematical abstraction is critical for the robustness of the framework. It guarantees that our core theorems remain universally valid for any partitioned array. Furthermore, it explicitly links the high-level Separation Logic axioms directly to the LLVM IR, allowing the Entailment Engine to apply the exact algebraic mapping function (e.g., modulo for cyclic, division for block) required by the SMT solver to verify physical disjointness.

3.2.0.6 The Array Composition Rule

Regardless of the partitioning strategy, the fundamental physical reality of the synthesized hardware is that the complete array is merely the disjoint spatial union of its constituent banks. We prove this mathematically via the array composition rule.

A complete array predicate, \(\textsf{arr}(A)\), is strictly equivalent to the iterated separating conjunction of all \(N\) disjoint bank predicates: \[\textsf{arr}(A) \triangleq \scalebox{1.5}{\ast}_{k=0}^{N-1} \textsf{bank}(k, A, N)\]

This formulation is mathematically powerful because it inherently guarantees structural non-interference. By the fundamental axioms of Separation Logic, the iterated separating conjunction strictly enforces that for any two distinct banks \(k_1 \neq k_2\), their physical address domains are completely disjoint (\(\text{dom}(\textsf{bank}_{k_1}) \cap \text{dom}(\textsf{bank}_{k_2}) = \emptyset\)).

During the symbolic execution of a duplicated LLVM basic block (resulting from a loop unroll pass), getelementptr instructions compute flat 1D address offsets. If two concurrent load or store instructions subsequently attempt to claim ownership of the same physical bank \(k\) using these offsets, the execution state will attempt to evaluate \(\textsf{bank}(k) * \textsf{bank}(k)\). According to the core properties of the separating conjunction, \(P * P \implies \bot\) (a logical contradiction). This logical contradiction mathematically flags the exact presence of a structural memory conflict, entirely bypassing the need for affine constraint resolution.

4 Catching Memory Conflicts in Loop Unrolling↩︎

4.1 The Conflict-Free Unrolling (CFU) Condition↩︎

When a High-Level Synthesis (HLS) compiler applies loop unrolling by a factor of \(U\), it does not fundamentally execute a source-level C/C++ AST transformation. Instead, it performs standard LLVM basic block duplication. Each unrolled iteration generates a fresh, immutable set of Static Single Assignment (SSA) virtual registers (e.g., %idx.1, %idx.2). This makes the symbolic execution completely linear across the unroll factor \(U\). To parallelize these duplicated basic blocks safely within a single hardware clock cycle, the compiler must guarantee that the concurrent execution does not induce structural memory hazards. We formalize the absence of these hazards through the Conflict-Free Unrolling (CFU) condition.

4.1.0.1 Extraction of Concurrent Memory Accesses

During the symbolic execution of these unrolled basic blocks, spatial ownership is not triggered by C language level array indexing. Instead, it is natively asserted when the framework intercepts concurrent LLVM load or store instructions targeting a partitioned array \(A\). These memory instructions consume flat 1D address offsets computed natively by preceding getelementptr (GEP) instructions. The scheduler extracts this target set of \(U\) algebraic GEP expressions. We denote this set of concurrent memory accesses as \(E\): \[E = \{expr_1, expr_2, \dots, expr_U\}\] where each \(expr_i\) represents the pure algebraic evaluation of the flat array offset for the \(i\)-th parallel iteration.

To determine the physical hardware routing of these expressions, we define a bank mapping function, \(\mathcal{B}(expr_i, N)\), which maps an evaluated GEP arithmetic offset (\(expr_i\)) to its corresponding physical bank given a partition factor \(N\). This mapping is mathematically bound to the array’s partitioning scheme \(\mathcal{P}\), extracted from the static hardware environment \(\Gamma(A) = (\alpha, M, \mathcal{P})\): \[\mathcal{B}(expr_i, N) \triangleq \begin{cases} expr_i \pmod N & \text{if } \mathcal{P} = \text{Cyclic} \\ \lfloor expr_i / B \rfloor & \text{if } \mathcal{P} = \text{Block} \quad (\text{where } B = \lceil M/N \rceil) \\ expr_i & \text{if } \mathcal{P} = \text{Complete} \end{cases}\]

4.1.0.2 Formulation of the CFU Condition

For the HLS scheduler to safely synthesize these \(U\) accesses in parallel, the compile-time symbolic state must demonstrate concurrent and exclusive spatial ownership over the target memory banks in the spatial heap \(H\). We model this simultaneous scheduling requirement by demanding that \(H\) can satisfy the iterated separating conjunction (\(\scalebox{1.5}{\ast}\)) of the required bank predicates.

We formally define the Conflict-Free Unrolling condition for the target set \(E\) as follows. \[\textsf{cfu}(E, A, N) \triangleq \scalebox{1.5}{\ast}_{i=1}^{U} \textsf{bank}(\mathcal{B}(expr_i, N), A, N)\]

The iterated separating conjunction requires the existence of \(U\) strictly disjoint heaplets, each satisfying the exclusive spatial ownership of a required physical bank. Because the path condition \(\pi\) handles pure LLVM IR algebra—natively accommodating non-affine operations like modulo or division evaluated by the bank mapping function—the framework completely bypasses strict polyhedral geometric models.

The detection of a memory conflict is thus reduced to an SMT algebraic equivalence query over the SSA variables. If iteration \(i\) claims ownership of \(\textsf{bank}(k_1)\) and iteration \(j\) claims \(\textsf{bank}(k_2)\), the spatial logic strictly requires \(\textsf{bank}(k_1) * \textsf{bank}(k_2)\). To enforce spatial disjointness, the framework can mechanically generate the Verification Condition (VC): \[\pi \implies k_1 \neq k_2\]

If the SMT oracle evaluates this VC to false or unknown—meaning it cannot mathematically prove the physical indices are distinct—the system explicitly flags a structural memory hazard. Consequently, if \(\textsf{cfu}(E, A, N)\) evaluates to a satisfiable spatial state rather than \(\bot\), it serves as proof that the synthesized parallel Verilog execution trace is free of memory bank collisions.

4.2 Spatial Collapse as Conflict Detection↩︎

At the core of Separation Logic lies the principle of exclusive spatial ownership. The separating conjunction, \(P * Q\), strictly dictates that the spatial propositions \(P\) and \(Q\) must hold over disjoint regions of the memory heap. A direct consequence of this foundational axiom is that a single spatial resource cannot be disjointly owned by multiple execution entities simultaneously. For any non-empty spatial predicate \(P\), attempting to separate it from itself yields a logical contradiction: \[P * P \implies \bot\]

We leverage this inherent spatial disjointness as a mathematical mechanism to natively detect structural memory hazards in HLS scheduling. When the Conflict-Free Unrolling (CFU) condition is evaluated, a memory conflict manifests mathematically as a spatial collapse triggered by the Entailment Engine and SMT oracle.

Consider two concurrent LLVM memory instructions (e.g., load or store) from distinct unrolled basic blocks, \(i\) and \(j\) (where \(1 \le i < j \le U\)). Their respective getelementptr instructions compute flat 1D offsets that map to physical memory banks \(k_i = \mathcal{B}(expr_i, N)\) and \(k_j = \mathcal{B}(expr_j, N)\). To safely schedule these instructions simultaneously, the spatial logic strictly requires \(\textsf{bank}(k_i, A, N) * \textsf{bank}(k_j, A, N)\).

To mathematically prove this spatial disjointness, the framework generates a Verification Condition (VC) bounded by the pure algebraic path condition \(\pi\): \[\pi \implies k_i \neq k_j\]

If the SMT oracle cannot prove this VC—either evaluating it to “false” or returning “Unknown” due to the undecidability of non-linear arithmetic embedded in the SSA variables—the framework safely assumes a hazard exists where both accesses target the same physical bank \(k\). When constructing the CFU condition for this parallel execution state, the iterated separating conjunction forcefully expands to demand concurrent ownership of bank \(k\) twice: \[\textsf{cfu}(E, A, N) = \textsf{bank}(k, A, N) * \textsf{bank}(k, A, N) * \scalebox{1.5}{\ast}_{\substack{m=1 \\ m \neq i,j}}^{U} \textsf{bank}(\mathcal{B}(expr_m, N), A, N)\]

Applying the disjointness axiom, the conflicting term \(\textsf{bank}(k, A, N) * \textsf{bank}(k, A, N)\) immediately collapses to \(\bot\). Because the separating conjunction distributes over logical false (\(\bot * \Sigma \implies \bot\)), the entire spatial state evaluates to a contradiction: \[\textsf{cfu}(E, A, N) \implies \bot\]

This unsatisfiable state explicitly and automatically catches the structural hazard. By reducing the detection of non-affine memory collisions to an SMT algebraic equivalence query that triggers a fundamental collapse in spatial logic, the framework definitively halts the synthesis of unsafe parallel Verilog without requiring strict polyhedral or affine geometric approximations.

5 Translating Spatial Disjointness to SMT↩︎

5.1 Algebraic Entailment Rules↩︎

Standard Satisfiability Modulo Theories (SMT) solvers operate over decidable first-order theories (such as bitvectors and integer arithmetic). They do not natively understand the spatial heap \(H\) or Separation Logic constructs like the separating conjunction (\(\ast\)). To bridge this gap, the spatial requirements of the hardware layout must be mechanically reduced into pure boolean algebra. We define a formal translation function, \(\mathcal{T}\), which maps a spatial assertion into a pure first-order logic formula digestible by an SMT oracle, evaluated strictly over the Static Single Assignment (SSA) virtual registers accumulated in the path condition \(\pi\).

The translation function acts upon the Conflict-Free Unrolling (\(\textsf{cfu}\)) condition. When the execution of duplicated LLVM basic blocks attempts to union multiple bank predicates into \(H\) (triggered by load and store instructions), the framework extracts the target bank indices. Given a path condition \(\pi\), an array \(A\) mapped in the static environment \(\Gamma\), and a set of \(U\) concurrent symbolic bank indices \(K = \{k_1, k_2, \dots, k_U\}\), the spatial safety requirement \(\pi \vdash \textsf{cfu}(K, A, N)\) is translated as follows:

\[\mathcal{T}(\pi \vdash \textsf{cfu}(K, A, N)) \triangleq \pi \implies \bigwedge_{1 \le i < j \le U} (k_i \neq k_j)\]

This translation reduces the high-level spatial disjointness requirement to an equivalent matrix of pairwise inequality constraints over the symbolic SSA variables representing the bank indices.

5.1.0.1 Mechanization of the Verification Condition (VC)

The output of \(\mathcal{T}\) yields the formal Verification Condition (VC) for the HLS scheduler. For example, under a cyclic partitioning directive, the bank index is derived from the flat 1D address offset computed by an LLVM getelementptr (GEP) instruction, such that \(k = \text{offset} \bmod N\). A loop unrolled by a factor of \(U = 3\) generating virtual registers for indices \(\{k_1, k_2, k_3\}\) expands to the following algebraic constraint:

\[\pi \implies \Big( (k_1 \neq k_2) \;\land\; (k_1 \neq k_3) \;\land\; (k_2 \neq k_3) \Big)\]

By embedding the path condition \(\pi\) as the antecedent, the SMT solver evaluates these inequalities exclusively within the valid algebraic boundaries, branching constraints, and SSA assignments of the active execution trace. If the SMT solver proves that this VC is valid (\(\text{Sat}\)), it implies that no two SSA registers can map to the same physical bank identifier under the current path constraints. This algebraically preserves the core spatial invariant:

\[\text{Valid}\left(\mathcal{T}(\pi \vdash \textsf{cfu}(K, A, N))\right) \iff \langle \pi, H \rangle \not\models \bot\]

Consequently, because \(\pi\) handles the pure LLVM IR algebra—including non-affine arithmetic such as modulo and division inherent to the bank mapping functions—the framework bypasses polyhedral geometry. Structural conflict detection is cleanly reduced to an SMT algebraic equivalence query over immutable SSA variables.

5.2 Conservative Fallback for Undecidability↩︎

A fundamental challenge in bypassing geometric polyhedral constraints via algebraic translation is that LLVM IR getelementptr (GEP) offset calculations and bank mapping functions (such as modulo or division) frequently generate non-linear integer arithmetic within the path condition \(\pi\). Because first-order theories containing non-linear integer arithmetic are fundamentally undecidable, an automated SMT solver cannot be guaranteed to resolve the generated Verification Conditions within finite bounds. Consequently, the SMT oracle may return an Unknown status or trigger a deterministic synthesis timeout (\(\mathcal{T}_{out}\)).

While our spatial framework tries to resolve a subset of non-affine constraints that polyhedral models blindly serialize, non-linear integer arithmetic remains undecidable in first-order logic. To bridge this mathematical boundary and guarantee structural safety in the physical hardware, our framework implements a deterministic sequential fallback mechanism. We mathematically formalize this operational boundary by augmenting the verification decision space. Let \(\mathcal{S}\) be the verification status returned by the SMT oracle for a given translation \(\mathcal{T}(\pi \vdash \textsf{cfu}(K, A, N))\). The synthesized scheduler’s permission mapping, \(\mathcal{M}(\mathcal{S}) \in \{\text{Parallel}, \text{Sequential}\}\), is formally defined as:

\[\mathcal{M}(\mathcal{S}) \triangleq \begin{cases} \text{Parallel} & \text{if } \mathcal{S} = \text{Sat} \\ \text{Sequential} & \text{if } \mathcal{S} = \text{Unsat} \lor \mathcal{S} = \text{Unknown} \lor \mathcal{S} = \mathcal{T}_{out} \end{cases}\]

By conservatively treating an Unknown or timed-out result identically to an Unsat result, the framework establishes a sound theoretical ceiling. It mechanically maps unresolvable non-linear algebra to a potential spatial hazard, explicitly triggering the Separation Logic contradiction (\(P \ast P \implies \bot\)).

5.2.0.1 Preserving the Soundness Invariant

This mapping ensures that the framework does not under-approximates a structural hazard. From a hardware reality perspective, if the algebraic entailment engine cannot definitively prove the absolute mutual exclusion of the evaluated SSA bank indices (\(k_i \neq k_j\)), the framework assumes a worst-case scenario: that a physical memory conflict exists.

The HLS scheduler reacts to \(\text{Sequential}\) by immediately halting parallel synthesis for those duplicated basic blocks. It falls back to generating standard sequential execution states, inserting appropriate multiplexer-driven stall logic or pipeline registers to serialize the conflicting memory accesses over subsequent clock cycles. While this fallback occasionally yields a false positive (halting parallelization for an otherwise safe but undecidable non-linear GEP offset), it guarantees that the core Theorem of Soundness is not violated, ensuring the synthesized RTL is structurally immune to actual physical hardware collisions.

6 Theorem of Soundness↩︎

6.1 Hardware Safety Guarantee↩︎

To establish the structural safety of the synthesized hardware, we bridge the algebraic verification performed by the SMT oracle with the physical reality of the Register Transfer Level (RTL) execution trace. The core guarantee of our framework relies on the mathematical translation of spatial disjointness into pure first-order logic, proving that symbolic safety implies physical hardware safety.

Theorem 1 (Hardware Safety via Spatial Soundness). Let \(E\) be a set of \(U\) concurrent memory accesses targeting an array \(A\) partitioned into \(N\) banks, evaluated under a pure LLVM IR path condition \(\pi\). Let \(K = \{k_1, k_2, \dots, k_U\}\) be the set of symbolic bank indices extracted via the hardware mapping function \(\mathcal{B}(expr_i, N)\). If the algebraic Verification Condition (VC) is validated by the SMT solver, then the spatial Separation Logic requirement strictly holds, guaranteeing that the synthesized RTL is free of structural memory bank collisions under all valid execution traces.

6.2 Proof of Theorem 1↩︎

7 Conclusion↩︎

7.1 Summary of Contributions↩︎

High-Level Synthesis (HLS) relies on loop unrolling and array partitioning to maximize parallel hardware throughput. However, traditional dependency solvers based on the geometric polyhedral model over-approximate when scheduling concurrent memory accesses governed by non-affine array indices. To overcome this bottleneck, this paper presented a theoretical framework that repurposes Separation Logic (SL) to statically model physical hardware memory banks as distinct spatial resources directly over the LLVM Intermediate Representation (IR). By defining the Conflict-Free Unrolling (CFU) condition utilizing the iterated separating conjunction, we reduced the detection of structural memory hazards to an algebraic, SMT-solvable constraint matrix. This approach translates spatial disjointness into pairwise inequalities across immutable Static Single Assignment (SSA) registers, bypassing the affine limitations of HLS compilers and guaranteeing the structural safety of the synthesized RTL.

7.2 Future Work↩︎

Looking forward, we aim to extend this theoretical foundation in both formal and practical directions. Theoretically, we plan to rigorously define Separation Logic loop invariants to effectively manage the spatial state-space of partially unrolled loops and pipelined memory architectures, expanding the framework’s applicability to a broader class of complex scheduling scenarios. Furthermore, we intend to refine the spatial heap model by incorporating fractional permissions in Concurrent Separation Logic [16], [17] to differentiate between concurrent LLVM load and store instructions. While the current framework enforces strict exclusive ownership for all memory operations to safely model single-ported SRAM constraints, adopting fractional permissions will allow shared spatial ownership for read-only accesses. This theoretical extension will prevent artificial spatial collapses during safe concurrent reads, optimizing throughput for multi-ported memory or ROM broadcast architectures.

Practically, the next step is the software realization of this framework as a custom LLVM analysis pass, integrated natively with an automated SMT oracle such as Z3 [13]. This implementation will allow us to empirically benchmark the framework’s conflict detection accuracy, compilation time overhead, and resulting hardware resource efficiency against standard industry HLS tools, bridging the gap between formal programming language theory and physical hardware generation.

References↩︎