Multiple level transistor abstraction for dynamic circuits
View Patent ↗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.
1. A method for verifying operation of circuit modules in an integrated circuit, comprising:
(a) generating a first level of abstracted code corresponding to the pre-charge phase of a dynamic circuit, said first level of abstracted code comprising code embedded in comment logic;
(b) generating a second level of abstracted code corresponding to the evaluate phase of a dynamic circuit; and
(c) performing multi-pass processing comprising first and second processing passes of said first and second levels of abstracted code to obtain a transistor abstraction verification of the operation of said circuit with respect to said pre-charge phase and said evaluate phase;
(d) wherein said second level of abstracted code corresponding to said evaluate phase comprises code having a syntax executable in conjunction with a property checking tool and wherein said embedded code is executable in conjunction with said property checking tool.
2. The method of claim 1 , wherein said first level of abstracted code comprises executable code corresponding to a dynamic clocking scheme wherein a pre-charge net is unconditionally charged to a logical 1 or a logical 0.
3. The method of claim 2 , wherein said second level of abstracted code comprises executable code corresponding to a dynamic clocking scheme wherein a pre-charge net is conditionally discharged.
4. The method of claim 3 , wherein said second level of abstracted code corresponding to said evaluate phase comprises legal Verilog code.
5. The method of claim 4 , wherein verification of said pre-charge phase is structured in accordance with a binary decision tree corresponding to the state of said circuit module wherein a clock signal has a value of “0.”
6. The method of claim 5 , wherein said verification of said evaluate phase is structured in accordance with a binary decision tree corresponding to the state of said circuit module wherein a clock signal has a value of “1.”
7. An integrated circuit, comprising:
a plurality of circuit components for processing data signals in accordance with a timing sequence controlled by at least one clock signal;
wherein operation of said integrated circuit is verified by:
(a) generating a first level of abstracted code corresponding to the pre-charge phase of a dynamic circuit, said first level of abstracted code comprising code embedded in comment logic;
(b) generating a second level of abstracted code corresponding to the evaluate phase of a dynamic circuit; and
(c) performing multi-pass processing comprising first and second processing passes of said first and second levels of abstracted code to obtain a transistor abstraction verification of the operation of said circuit with respect to said pre-charge phase and said evaluate phase;
(d) wherein said second level of abstracted code corresponding to said evaluate phase comprises code having syntax executable in conjunction with a property checking tool and wherein said embedded code is executable in conjunction with said property checking tool.
8. The integrated circuit of claim 7 , wherein said first level of abstracted code comprises executable code corresponding to a dynamic clocking scheme wherein a pre-charge net is unconditionally charged to a logical “1” or a logical “0.”
9. The integrated circuit of claim 8 , wherein said second level of abstracted code comprises executable code corresponding to a dynamic clocking scheme wherein a pre-charge net is conditionally discharged.
10. The integrated circuit of claim 9 , wherein said second level of abstracted code corresponding to said evaluate phase comprises legal Verilog code.
11. The integrated circuit of claim 10 , wherein verification of said pre-charge phase is structured in accordance with a binary decision tree corresponding to the state of said circuit module wherein a clock signal has a value of “0.”
12. The integrated circuit of claim 11 , wherein said verification of said evaluate phase is structured in accordance with a binary decision tree corresponding to the state of said circuit module wherein a clock signal has a value of “1.”