Hot-FV: A Semi-Formal Test Generation Framework for RTL Functional Coverage Using Warm Starting States

Abstract

Functional verification is critical in ensuring the correctness of register transfer level (RTL) models. Formal methods, such as model checkers, are powerful tools that help achieve high coverage in functional validation by transforming the coverage problem into property verification tasks. However, these methods typically demand significant memory usage and long verification times. One major issue is that the satisfiability problem for each unsolved property always starts from the reset state of a design, leading to repeated solving of the same subset of clauses across different properties. In this paper, we propose an open-source semi-formal framework based on model checkers that accelerates test stimulus generation through two techniques: assertion ordering and strategic selection of starting states. These techniques enable model checkers to intelligently select starting states that are much closer to the final state, thereby reducing unnecessary computations. Through comprehensive experiments on ITC'99 benchmarks and modern complex processor designs, including OpenCores 1200 and Rocket-Chip, we demonstrate that our proposed techniques can achieve higher coverage with less than half of the test generation time.

Guangyu (Gary) Hu

Researcher at Huawei Hong Kong Research Center, Fermat Lab

My research interests include LLM + formal verification reasoning and hardware formal verification.