摘要

Functional validation is widely acknowledged as a major challenge for multicore architectures. 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 article proposes a novel technique that exploits temporal, structural, and spatial symmetry in multicore designs at the same time. Our proposed technique enables the reuse of the knowledge learned from one core to the remaining cores in multicore architectures (structural symmetry), from one bound to the next for a give property (temporal symmetry), as well as from one property to other properties (spatial symmetry). The experimental results demonstrate that our approach can significantly (3-10 times) reduce overall test generation time compared to existing approaches.

  • 出版日期2012-6