IChecker: An Efficient Checker for Inductive Invariants

Invariants in sequential circuits could be very useful for sequential optimizations and for speeding up functional verification tasks. However, the lack of efficient and scalable invariant identification tools limits their usage. In this paper, we present a new tool, IChecker, for efficient identification of true invariants for any given initial set of invariant candidates. ICheker uses new circuit simplification techniques to iteratively minimize constrained circuit models, along with a number of heuristics for efficient computation of invariants. Experimental results demonstrate the high efficiency and effectiveness of the proposed approach for identifying sequential invariants