Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
Abstract elided by the publisher.
Related papers
- A Refinement Calculus for the Synthesis of Verified Hardware Descriptions in VHDL TOPLAS 1997
- A Unified Memory Dependency Framework for Speculative High-Level Synthesis CC 2024
- Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic OOPSLA 2025
- Synthesizing Specialized Sparse Tensor Accelerators for FPGAs via High-Level Functional Abstractions CGO 2026
- Designing scalable FPGA architectures using high-level synthesis PPoPP 2018
- Formal verification of high-level synthesis OOPSLA 2021
- Selene: Cross-Level Barrier-Free Pipelining for Irregular Nested Loops in High-Level Synthesis CGO 2026
- Predictable accelerator design with time-sensitive affine types PLDI 2020