Scalable Concolic Testing of RTL Models

• Published in: IEEE transactions on computers 2021-07, Vol.70 (7), p.979-991
• Main Authors: Lyu, Yangdi, Mishra, Prabhat
• Format: Article
• Language: English
• Subjects: Clustering; Computational modeling; Concolic testing; Explosions; Formal method; Hardware; Model checking; Program verification (computers); RTL validation; Search problems; Searching; Test pattern generators
• ISSN: 0018-9340; 1557-9956
• DOI: 10.1109/TC.2020.2997644

Simulation is widely used for validation of Register-Transfer-Level (RTL) models. While simulating with millions of random or constrained-random tests can cover majority of the functional scenarios, the number of remaining scenarios can still be huge (hundreds or thousands) in case of today's industrial designs. Hard-to-activate branches are one of the major contributors for such remaining/untested scenarios. While directed test generation techniques using formal methods are promising in activating branches, it is infeasible to apply them on large designs due to state space explosion. In this article, we propose a fully automated and scalable approach to cover the hard-to-activate branches using concolic testing of RTL models. While application of concolic testing on hardware designs has shown some promising results in improving the overall coverage, they are not designed to activate specific targets such as uncovered corner cases and rare scenarios. In other words, existing concolic testing approaches address state space explosion problem but leads to path explosion problem while searching for the uncovered targets. Our proposed approach maps directed test generation problem to target search problem while avoiding overlapping searches involving multiple targets. This article makes two important contributions. (1) We propose a directed test generation technique to activate a target by effective utilization of concolic testing on RTL models. (2) We develop efficient learning and clustering techniques to minimize the overlapping searches across targets to drastically reduce the overall test generation effort. Experimental results demonstrate that our approach significantly outperforms the state-of-the-art methods in terms of test generation time (up to 205X, 69X on average) as well as memory requirements (up to 31X, 7X on average).