Patent attributes
A method and apparatus for improved formal equivalence checking to verify the operation of components in a VLSI integrated circuit. The present invention enhances previous techniques for dynamic circuits by generating a multi-level transistor abstraction for dynamic circuits. Two-levels of abstracted code are generated. First, an abstracted legal Verilog® is generated for the evaluate phase of a dynamic circuit. Second, “comment-logic” in Verilog® syntax is generated for the pre-charge phase of the dynamic circuit. Using the method and apparatus of the present invention, it is possible to obtain a multi-level transistor abstraction for both the “clk=0” and the “clk=1” conditions. The binary decision diagram property of the circuit being analyzed is used to generate multi-level representations for both the pre-charge (clk=0) and the evaluate phases (clk=1). The multi-level abstracted model of the present invention has several advantages over the prior art. The legal Verilog® can be used for traditional simulation and equivalency verification, ATPG. The “comment logic” can be used with a property checking tool to verify that the clock connectivity is correct. In addition, the present invention has the advantage of being able to generate legal Verilog® with pre-charge for verification against RTL with detailed pre-charge information.
