Functional Test Generation at the RTL Using Swarm Intelligence and Bounded Model Checking
Kelson Gent, Michael S. Hsiao · 2013
Although stochastic search techniques have shown promise in test generation and design validation, they often fail when there is a specific, random-resistant sequence of vectors required to exercise a target. In order to combat this, deterministic techniques are added, resulting in a hybrid solution to maintain high speed of execution while improving metric performance. This paper presents a formal hybridization that combines a Register Transfer Level (RTL) stochastic swarm intelligence based test vector generation with the Verilator Verilog-to-C++ source-to-source compiler. Verilator generates a fast cycle accurate C++ simulation unit for Verilog descriptions and provides instrumentation for branch and toggle coverage metrics. This RTL model can also be used to generate a bounded model checking (BMC) instance. During the stochastic search, the bounded model checker is launched to expand the unexplored search frontier and aid in the navigation of narrow paths. Additionally, an inductive reach ability test is applied in order to eliminate unreachable branches from our search space. These additions have significantly improved branch coverage, reaching 100% in several ITC99 benchmarks. Additionally, compared to previous functional test generation methods, we achieve substantial speedup achieved with purely stochastic methods.