Method for verification of combinational circuits using a filtering

Abstract

A set of filters are arranged in sequence for verification and analysis of digital circuit designs. The filters are either active filters, which are directly involved in verification of circuit designs (e.g., a Binary Decision Diagram (BDD)-based verifier or an automatic test pattern generation (ATPG)-based verifier), or passive filters, which gather information about the circuit or transform the circuit structure in order to simplify the verification problem (e.g., random pattern simulation or circuit partitioning). Given a pair of circuits to be verified, the filter approach first subjects the circuits to very simple, fast techniques having very low memory usage requirements. These steps are followed by a series of increasingly powerful methods that are more time consuming and often require more computer memory for their operation. In between the simpler active filters and the more sophisticated active filters, information about potential equivalent nodes in the circuits is collected and a decision is made as to whether to partition the circuits. The verification methodology is structured such that circuit designs that are easier to verify are never unnecessarily subjected to more expensive techniques. The method provides for a gradual increase in the sophistication of verification techniques applied, according to the difficulty of the verification problem.