Towards the Functional Verification of Large Sequential Circuits

Verifying the equivalence of sequential circuits is computationally expensive. Therefore it is interesting to investigate whether a divide-and-conquer strategy can be used to manage the complexity of this problem. This approach requires a verification method which combines an effective decomposition technique with a powerful base verification algorithm. In this paper, we discuss how functional dependencies can be used to find a good decomposition and to improve the performance of the base verification algorithm. 1. Introduction Formal verification methods are clearly gaining acceptance in industry. Especially for combinational equivalence checking, automated tools are being developed which are sufficiently powerful to verify the functional correctness of circuits generated by a logic synthesis tool or manually by a designer. The underlying verification methods combine a powerful base verification algorithm with techniques to exploit the similarities between the circuits beingcompared..