QUEBS: Qualifying Event Based Search in Concolic Testing for Validation of RTL Models
Alif Ahmed, Prabhat Mishra · 2017
Input vector generation is an important step during validation and debugging of hardware designs. Validation using random and directed random tests are widely used today. However, these methods can lead to unacceptable functional coverage under tight deadlines. Concolic testing is a semi-formal method to address this issue. It combines concrete simulation guided by symbolic execution. Application of concolic testing in hardware domain is still in its infancy due to the lack of effective traversal strategies. In this paper, we present Qualifying Event Based Search (QUEBS) heuristic for concolic testing. During exhaustive concolic testing, same branch may be selected many times for traversal. Our heuristic limits the number of times a branch can be selected. By preventing repeated selection, it facilitates wider coverage within limited time. Also, whenever a previously uncovered branch is encountered, this limit is relaxed to permit thorough exploration of the newly reached area. Our experimental results demonstrate that this approach provides better branch coverage than state-of-the-art test generation methods in a given time budget. To further improve the performance of QUEBS, we provide two optimization techniques - unsolvable branch elimination and incremental solving by context reuse.