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.