APE-FV: Concolic Testing for RTL Functional Verification Using Adaptive Path Exploration

The validation of Register-Transfer Level (RTL) models requires achieving sufficient branch coverage. However, automatically activating all branches in RTL models is challenging, considering the complexity of modern designs. While traditional methods, such as model checkers, can achieve high coverage, they typically demand substantial computational resources to solve formal equations. In contrast, constraint-random approaches have better scalability but suffer from inefficiency due to poor heuristics. This paper introduces APE-FV, a Concolic testing framework designed for RTL functional verification to effectively cover rare branches. APE-FV dynamically modifies the path exploration strategy by considering structural information, simulated paths, and states. Additionally, our framework incorporates an incremental exploration technique, which reduces the burden on solvers and enhances efficiency. Experimental results demonstrate that our approach accelerates the verification process and maintains high coverage, outperforming state-of-the-art techniques.