Mining-guided state justification with partitioned navigation tracks

This work introduces a new guidance strategy to justify hard-to-reach target states in sequential circuits, which also applies to reaching corner-case states in design validation. We propose data-mining methods to extract several partition sets of state variables directly from the gate-level netlist of the design, such that they enable the search to reach the target state. The partition sets are used to compute partitioned navigation tracks (PNTs). PNTs capture the behavior of expanded portions of the state space as they relate to a target state of interest, thus providing a more accurate distance metric than traditional abstract guideposts. Moreover, the computation and storage costs of the PNTs are small, making our approach scalable to large circuits. With the proposed PNTs, we also need not refine the abstract models. Experiments showed that we are able to reach many more hard-to-reach states compared to state-of-the-art methods.