Method and system for verifying the equivalence of digital circuits
View Patent ↗The automatic verification of designs of digital circuits for their equivalence, wherein logic designs implemented in different hardware description languages (HDLs) and different design methodologies are compared. The designs (Code A, Code B) are modified by adding special wrappers (Wrapper A, Wrapper B), and used to equalize the timing of pairs of selected input signals and selected output signals of the logic designs. The wrappers drive certain signals of the designs that are not relevant for actual comparison, such signals including clock signals, clock control signals, scan-path signals, scan-path control signals, and reset signals. In a preferred embodiment, HDL descriptions of logic designs are analyzed. Based on this analysis, the wrappers are implemented as changes to the HDL descriptions. In another embodiment, RTL and/or gate-level netlists are analyzed and modified.
1. A method for verifying equivalent logic circuits respectively having different clocking configurations, different types of storage elements, and different descriptive languages, the method comprising:
a) comparing with a computer a first logic circuit having a first clocking configuration and a first descriptive language against a second logic circuit having a second clocking configuration and a second descriptive language, the first and second logic circuit each having different descriptive languages from each other, and the first and second logic circuit each having different clocking configurations from each other;
b) based on results of said comparison, creating first and second wrappers respective to said first and second logic circuits, matching said first clocking configuration to said second clocking configuration; and
c) equalizing said first and second wrappers of said first and second logic circuits, said equalization being performed without affecting the respective storage elements.
2. The method of claim 1 , wherein in step a), said clocking configurations are determined by analyzing the first and second clocking configurations of said respective storage elements, wherein said storage elements is determined by selected inputs or selected outputs.
3. The method of claim 1 , wherein in step b), said first and second clocking configurations are equalized based on said storage elements ef attached to said clocking configurations.
4. The method of claim 1 , wherein in step c) said equalization results in an equivalent offset to timing axes of said inputs and outputs.
5. The method of claim 2 , wherein added logic elements are inserted in said logic configurations that are connected to unselected input and outputs.
6. The method of claim 1 , wherein in step b), added storage elements are inserted in said first and second logic configurations connected to a subset of said selected inputs and said selected outputs.
7. The method of claim 1 , wherein said first and second descriptive languages respectively comprise Verilog and VHDL, or vice versa.
8. The method of claim 1 , wherein step c) is performed using a functional formal verification tool.
9. The method of claim 8 , wherein said first and second logic configurations are specified in hardware description languages, and wherein the analyzing step is performed in a lexical analysis tool.
10. The method of claim 9 , wherein said lexical analysis tool is based on coding conventions.
11. The method of claim 8 , wherein said first and second logic configurations are RTL or a gate-level netlist representation of the logic configurations.
12. The method of claim 1 , wherein said clocking configurations include clock staging and controls resulting in differences at the inputs and outputs between models of said first and second logic configurations being compared to each other.
13. The method of claim 12 , wherein said inputs are selected from a group consisting of clocking control signals, scan-path and scan-path control signals, and reset signals.
14. A non-transitory program storage device readable by a machine, tangibly embodying a program of instructions executable by the machine to perform method steps for verifying equivalent logic circuits having different clocking configurations, different types of storage elements, and different descriptive languages, the program of instructions executable comprising:
a) comparing with a computer a first logic circuit having a first clocking configuration and a first descriptive language against a second logic circuit having a second clocking configuration and a second descriptive language, the first and second logic circuit each having different descriptive languages from each other, and the first and second logic circuit each having different clocking configurations from each other;
b) based on results of said comparison, creating first and second customized wrappers to said respective first and second logic circuits to match said first clocking configuration to said second clocking configuration; and
c) equalizing said customized wrappers of said first and second logic circuits, said equalization being performed without affecting the respective storage elements.
15. The non-transitory program storage device of claim 14 , wherein the comparing step is performed by a tool selected from a group consisting of a checker, a semiformal verification tool, a simulation tool, and any combination thereof.