Efficient directed test generation for validation of multicore architectures

Functional verification of multicore architectures is widely acknowledged as a major challenge. Directed tests are promising since a significantly smaller number of directed tests can achieve the same coverage goal compared to constrained-random tests. SAT-based bounded model checking is effective for automated generation of directed tests (counterexamples). While existing approaches focus on clause forwarding between different bounds to reduce the test generation time, this paper proposes a novel technique that exploits the structural similarity within the same bound as well as between different bounds. Our proposed technique enables the reuse of the knowledge learned from one core to the remaining cores in multicore architectures. The experimental results demonstrate that our approach can significantly (2-10 times) reduce overall test generation time compared to existing approaches.