一句话：为 Vericert 实现经 Coq 验证的 hyperblock 调度器，通过翻译验证保证正确性，使生成硬件提速 2.1 倍。
高层综合（HLS）能把软件自动编译成定制硬件，但现有工具可靠性不足，难以用于安全关键场景；此前 Vericert 虽在 Coq 中验证了正确性，性能却落后于未验证工具。本文为 Vericert 设计基于 hyperblock（谓词指令基本块）的灵活操作调度器，支持操作链把相关操作压入同一时钟周期。正确性采用翻译验证：每个调度由 Coq 验证的验证器检查，并用 SAT 求解器推理谓词；为抑制指数爆炸，引入最终状态谓词与值摘要。在 PolyBench/C 上，调度使生成硬件快 2.1 倍，在启用类似优化后可与先进开源 HLS 工具竞争。
High-level synthesis (HLS) is the automatic compilation of software programs into custom hardware designs. With programmable hardware devices (such as FPGAs) now widespread, HLS is increasingly relied upon, but existing HLS tools are too unreliable for safety- and security-critical applications. Herklotz et al. partially addressed this concern by building Vericert , a prototype HLS tool that is proven correct in Coq (à la CompCert), but it cannot compete performance-wise with unverified tools. This paper reports on our efforts to close this performance gap, thus obtaining the first practical verified HLS tool. We achieve this by implementing a flexible operation scheduler based on hyperblocks (basic blocks of predicated instructions) that supports operation chaining (packing dependent operations into a single clock cycle). Correctness is proven via translation validation: each schedule is checked using a Coq-verified validator that uses a SAT solver to reason about predicates. Avoiding exponential blow-up in this validation process is a key challenge, which we address by using final-state predicates and value summaries . Experiments on the PolyBench/C suite indicate that scheduling makes Vericert-generated hardware 2.1× faster, thus bringing Vericert into competition with a state-of-the-art open-source HLS tool when a similar set of optimisations is enabled.
@article{HerklotzW24,
title = {Hyperblock Scheduling for Verified High-Level Synthesis},
author = {Yann Herklotz and John Wickerson},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656455}
}