Incremental Verification for Sequential Circuits

In this chapter we address the problem of verifying the equivalence of two sequential circuits. In an attempt to handle larger circuits, we modify the test pattern generation technique for verification. The suggested approach utilizes the efficient backward justification technique popularly used in most sequential ATPG programs. We present several techniques to enhance the efficiency of this approach: (1) identifying equivalent flip-flop pairs using an induction-based algorithm, and (2) generalizing the idea of exploring the structural similarity between circuits to perform verification in stages. This ATPG-based framework is suitable for verifying circuits either with or without a reset state. Experimental results on verifying the correctness of circuits after sequential redundancy removal with up to several hundred flip-flops are presented.