Decision ordering based property decomposition for functional test generation

SAT-based BMC is promising for directed test generation since it can locate the reason of an error within a small bound. However, due to the state space explosion problem, BMC cannot handle complex designs and properties. Although various optimization methods are proposed to address a single complex property, the test generation process cannot be fully automated. This paper presents an efficient automated approach that can scale down the falsification complexity using property decomposition and learning techniques. Our experimental results using both software and hardware benchmarks demonstrate that our approach can drastically reduce the overall test generation effort.