AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs

TL;DR

AutoINV is a framework that uses high-level design features to generate helper assertions, significantly speeding up formal verification of HLS-generated RTL designs by guiding model checking more efficiently.

Contribution

It introduces a method to construct helper assertions from high-level features and a proving mechanism to select the most effective helpers, improving verification speed.

Findings

Achieves up to 6.05x speedup in model checking.

Average speedup of 2.23x over vanilla model checking.

Effectively guides model checker to handle large RTL designs.

Abstract

High-level synthesis (HLS) transforms an algorithmic description of hardware from a higher abstraction (e.g., C/C++) into a register-transfer level (RTL) design, offering reduced development time and greater flexibility in design space exploration. However, such machine-generated RTL designs may contain major functional bugs or security vulnerabilities due to limitations or errors in the HLS tools. One of the most reliable methods to identify these vulnerabilities is formal verification, particularly model checking. Nevertheless, the large size of the generated RTL often causes model checking to struggle to conclude within reasonable time or resource limits. In this study, we propose utilizing the high-level design features from the HLS flow to construct a set of helper assertions aimed at guiding the model checker and accelerating the verification process. To identify the most effective set of helpers to assist the model checker, we develop a proving mechanism that iteratively reuses proving information to select the potentially most useful set of helpers. We evaluate the proposed framework on a set of HLS design benchmarks. Experimental results demonstrate that, when compared to vanilla model checking, our approach achieves a speedup of up to 6.05x, and 2.23x on average.