Automatic identification of assertions and invariants with small numbers of test vectors

Identifying logical relationships among internal/input/output signals is one of the key analyses for formal verification, logic synthesis, test pattern generation, and others. It is also a very important step to recognize invariant in sequential circuits which can be identified as relationships among flipflop signals. They can simplify the model checking and other sequential verification problems. In this paper, we show a method for identifying logical relationships among sets of given internal/input/output signals which are involved in assertions and invariants. The method is based on QBF (Quantified Boolean Formula) with LUT (Look Up Table)-bsaed formulation and solved by incremental SAT(non-QBF) solvers. The numbers of iterations in incremental SAT solving are small, e.g., around hundreds for thousand of gates designs. It allows extraction of logical relationships among signals that designers specify and can work for designs with hundreds of thousands of gates or more.