| 摘要 |
A memory is encoded with data that represents a reference IC design, a retimed IC design, and logical relationships, wherein at least one logical relationship describes combinational logic without reference to structural information, such as actual cells that have been instantiated in the IC designs. The logical relationships are used to instantiate logic described therein, and to define one or more black boxes as being functionally inverse of the logic. Each instantiated logic and its functionally inverse black box are thereafter added to the reference IC design to obtain a transformed reference IC design. A transformed retimed IC design is also obtained by addition of the instantiated logic(s) and functionally inverse black box(es) to the retimed IC design. These two transformed IC designs are then supplied to an equivalence checker, for formal verification.
|
