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.RTM. is generated for the evaluate phase of a dynamic circuit. Second, "comment-logic" in Verilog.RTM. 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.RTM. 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.RTM. with pre-charge for verification against RTL with detailed pre-charge information.