Efficient Reachability Analysis Based on Inductive Invariant Using X-value Based Flipflop Selection

For sequential circuits, it is well known that the sets of reachable states may be much smaller than the entire state space, and computing the supersets of reachable states is practically useful due to the less computational complexity than the exact set of the reachable states. Inductive invariant is the one of the methods to compute such supersets. We first show a way to prove the property of the sequential circuits with inductive invariants. For inductive invariants, it is important to select the subset of flipflops in order to find a small and/or useful superset of reachable states or prove the property. Unknown value X based analysis is used to find the subset of flipflops. In some HWMCC2017 benchmark circuits, the proposed method can find the subset of flipflops to prove the correctness of the property. The calculation of inductive invariants is formulated with Quantified Boolean Formula. The QBF problem can be solved by repeatedly applying SAT solvers. We also show a way to reduce the number of variables in QBF problems. In the method, we start with smaller inputs LUT and gradually increase the number of inputs in order to reduce variables. This method has reduced calculation time by up to around 80% when solving large QBF problem.