Property learning techniques for efficient generation of directed tests

Property falsification in model checking is widely used for automated generation of directed tests. Due to state space explosion problem, traditional model checking techniques cannot handle large scale designs. SAT-based bounded model checking is promising to address the prohibitively large time and resource requirements during the property falsification. This article presents several efficient learning techniques that can improve the overall test generation time for a single property as well as a cluster of similar properties. The goal is to exploit both variable assignments and common conflict clauses of the prechecked partial or similar SAT instances for property falsification. Our method makes three novel contributions: 1) investigates the decision ordering-based learnings for a single SAT instance; 2) applies the decision ordering learnings between similar SAT instances; and 3) exploits the relation between the decision ordering-based learning and conflict clauses-based learning. Our experimental results using both software and hardware benchmarks demonstrate that our approach can drastically reduce the overall test generation time.