Spatial Logic Solutions for High-Performance Hardware Synthesis

The Challenge: Non-Linear Memory Bottlenecks in HLS

High-Level Synthesis (HLS) accelerates hardware development by converting high-level software code (C/C++) directly into parallel Register Transfer Level (RTL) hardware architectures, such as FPGAs. To improve performance, HLS tools unroll loops and partition arrays across isolated physical memory banks to enable concurrent data access within a single clock cycle.

• Structural Memory Hazards: When multiple concurrent operations attempt to access the same single-ported memory bank during the same clock cycle, hardware memory collisions occur.
• Polyhedral Analysis Limitations: Traditional dependency solvers rely on geometric polyhedral models that require linear (affine) address calculations. When index formulas contain non-linear operations—such as modulo, division, dynamic pointer arithmetic, or symbolic register multiplication—these methods often struggle to verify memory independence.
• Performance Bottlenecks: To ensure safety, conventional tools over-approximate dependencies and conservatively serialize memory operations. This can restrict parallel performance and introduce multiplexer-driven stall logic into the synthesized hardware.

Our Solution: Spatial Verification via Separation Logic

Our framework addresses non-affine memory conflicts at the LLVM Intermediate Representation (IR) level by applying Separation Logic—a mathematical formalism designed for reasoning about disjoint physical resources.

Instead of treating memory addresses purely as geometric integers, our approach models hardware memory banks as distinct spatial regions. This enables memory conflict detection without relying strictly on linear geometric constraints.

Core Technologies & Intellectual Property (IP)

Our solutions are based on original research and patent-pending architectures:

• Separation Logic-Based Non-Linear Memory Hazard Verification
  • The Tech: Analyzes non-affine hardware memory conflicts at the LLVM IR level by applying Separation Logic to evaluate concurrent memory bank disjointness.
  • Status: Korean Patent Application Filed (Provisional Specification)
  • Publication: “Separation Logic for Memory Conflict Detection in High-Level Synthesis” (Preprint DOI: 10.48550/arXiv.2607.07126)