Verifying Hardware at the Source: Why a User-Visible HLS Scheduling Contract Matters in an Age of AI-Generated Design

High-Level Synthesis (HLS) lets engineers design hardware in C++ and SystemC and have a tool generate the RTL. The productivity gains are real, but they expose a hard problem: verifying machine-generated RTL is at least as expensive and difficult as verifying hand-written RTL, and it may need to be redone every time the design is re-synthesized when tuning quality-of-results. This paper describes a modeling and verification approach that moves the bulk of design verification to the pre-HLS C++/SystemC model — where it is faster, cheaper, and reusable — and explains why that approach rests on a small, precise, user-visible scheduling contract that constrains what an HLS tool may do at a design's interfaces while leaving it free to optimize aggressively inside each block.

The near-term benefits are concrete: a single testbench and a common verification intent that apply across the pre- and post-HLS models; pre-HLS models that are accurate about throughput and buffering, not just function; and verification that composes block-by-block instead of requiring fresh whole-system verification after every change. These benefits do not require an all-at-once formal flow. Teams can adopt the rules first as design guidance, then add capacity-accurate modeling and progressively stronger conformance checks as their needs and tooling mature. The same contract can also organize verification for hand-written RTL and mixed HLS/RTL systems when they use compatible source or architectural models.

The paper then argues that these benefits are about to become essential rather than merely convenient. Rising design complexity and market pressure are already straining human-centric verification, and the rapid arrival of AI systems that generate and optimize both HLS models and RTL will strain it much further. A precise, machine-checkable contract is exactly the foundation an AI-driven flow needs: it gives both human and machine a single, unambiguous target to design against and to check against. Finally, the paper describes how AI can mechanize the contract's formal proofs once and for all, and can generate the per-design checks and certificates that establish that a specific — and increasingly AI-written — hardware module conforms.