Apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs

RELATED APPLICATIONS

[0001] The present application is directed to similar subject matter as co-pending and commonly assigned U.S. patent application Ser. No. ______ (Attorney Docket No. AUS920020074US1) entitled “Apparatus and Method for Representing Gated-Clock Latches for Phase Abstraction” and U.S. patent application Ser. No. ______ (Attorney Docket No. AUS920020075US1) entitled “Apparatus and Method for Removing Effects of Phase Abstraction from a Phase Abstracted Trace,” both filed concurrently herewith and incorporated by reference.

BACKGROUND OF THE INVENTION

[0002] 1. Technical Field

[0003] The present invention is directed to an apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs.

[0004] 2. Description of Related Art

[0005] Functional hardware verification is the process of demonstrating the correct behavior of a hardware design. Typically, the verification is performed on a “software” model of the design, e.g., the hardware description language (HDL), or a netlist representation derived through compilation of the HDL or custom design (or some other “compiled” format), which is executed on a computer or downloaded onto a hardware emulator. A trace of the “software” model is generated by a verification tool and may be used to expose any problems in the software model or provide an output to a human user that may use the trace to evaluate the correctness of the design during operation.

[0006] A trace may be, for example, an “all events trace” that illustrates 0, 1 valuations to each gate of a software model over time. Such traces can be created by simulation tools evaluating the software model in response to a test case, e.g., sequences of 0, 1 values of the input to the software model over time, or by formal verification algorithms which are commonly referred to as “counterexample traces.”

[0007] The size of the design under test represents a significant bottleneck for the necessary verification resources. For simulation and emulation test-based techniques, the required resources are nearly linear with respect to design size. The drawback of such test-based techniques is that they are incomplete, and cannot prove the absence of design flaws, only their presence. Consequently there has been a peak of interest in formal verification techniques, which can prove the absence as well as presence of design flaws. However, such techniques consume exponential verification resources with respect to design size. In particular, verification resources typically run exponential with respect to the number of sequential elements (e.g., latches or registers) in the design. Combinational optimization techniques, prevalent in both test-based and formal verification paradigms, are capable of significantly reducing design size, but are limited in applicability to only the logic between sequential element boundaries. Thus sequential elements limit the ability of combinational model reduction techniques to simplify designs for verification regardless of the verification paradigm.

[0008] One technique, known as phase abstraction, has been developed to help minimize the number of sequential elements in a design under test. The use of phase abstraction for enhanced verification has been noted in several publications including “Efficient Equivalence Checking of Multi-Phase Designs Using Phase Abstraction and Retiming,” G. Hasteer, A. Mathur, and P. Banerjee, in Proceedings of the High-Level Design Validation and Test Symposium 1997 (which focusses on sequential hardware equivalence checking) and “Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists,” J. Baumgartner, T. Heyman, V. Singhal, and A. Aziz, in Proceedings of the Conference on Computer-Aided Verification 1999 (which focusses on functional verification), which are hereby incorporated by reference. In addition, a specific technique for performing phase abstraction is described in commonly assigned U.S. Pat. No. 6,321,184, which is also hereby incorporated by reference. In particular, for a design composed of level-sensitive latches, phase abstraction converts all but one “class” of latches to wires based on the fact that the latches are transparent when they are clocked. The remaining class of latches is converted to registers, thereby significantly reducing the number of sequential elements by at least a factor of “k” for a “k”-phase design.

[0009] The impact of this technique on increasing the power of combinational optimization techniques, and on increasing the speed with which verification algorithms operate (basically linear for test-based techniques, and exponential for formal verification techniques), has been previously noted above. However, this technique has several complications and unpleasant side effects.

[0010] First, one must provide the glue to partition the latches into various classes. In other words, the user of the phase abstraction technique must identify which latches are of a particular type in order for the phase abstraction to work. Thus, an additional burden is placed on the user of the phase abstraction technique. Moreover, if the determination of latch type is incorrect, verification of the phase abstracted netlist becomes unsound, i.e. the verification results obtained on the phase abstracted netlist may not imply anything about correctness of the original netlist.

[0011] Second, design techniques such as gated-clock latches provide complications for these techniques. During phase abstraction, if a gated clock latch is replaced by a wire, the resulting trace includes errors due to the fact that the latch is not always transparent during the latch's clocking at which it is normally transparent. This is because a gate signal may be used to alter the operation of the latch during this clocking. In particular, the global clock of the netlist can be selectively stopped for gated-clock latches by ANDing this global clock with a gate signal before driving it to these latches. As a result, if phase abstraction eliminates such latches, their gated behavior is destroyed, i.e. when their gates “close” they will still appear to behave as if their gates were “open.” Thus, phase abstraction in the presence of gated-clock latches also risks making the transformation unsound for verification purposes.

[0012] Third, any simulation-style of traces obtained on a phase abstracted design will be in terms of the phase-abstracted model itself, which may be unattractive to those who expect a trace in terms of the original model. It may be difficult and time consuming for the human user of the phase abstraction technique to convert the trace obtained through phase abstraction into a corresponding trace that would have been obtained without the phase abstraction.

[0013] Thus, it would be beneficial to have an apparatus and method for eliminating these three unattractive side-effects and/or complications of phase abstraction and thereby, provide a truly seamless or “invisible” automatic use of phase abstraction for enhanced verification.

SUMMARY OF THE INVENTION

[0014] The present invention provides an apparatus and method for automated use of phase abstraction for enhanced verification of circuit designs. With the apparatus and method of the present invention latches are “colored,” i.e. classified into different types, based on information obtained from a clock tree of the circuit design. In the clock tree, clock tree primitives drive all clock signals to the latches. These clock tree primitives contain sufficient information to taxonomize the clocks into their respective phases. This information may further be used to identify which latches are gated latches.

[0015] In coloring the latches, in a preferred embodiment, gated latches are replaced in the circuit design with a free running clock, a multiplexor, and a sequence of L1 to Ln latches to provide a feedback path via the data path. This allows the gated latch to be phase abstracted without losing the “gated” functionality of the gated latch in the resulting trace.

[0016] Once the latches are colored in this way, phase abstraction is performed on the colored circuit design. The phase abstracted netlist is then subjected to verification, e.g., simulation, or formal verification. As a result of the verification, a trace may be produced. This trace will be in terms of the phase abstracted circuit, since verification was performed upon the phase abstracted circuit. The coloring information of the original circuit, plus information as to the exact nature of the phase abstraction performed, is then used to transform the phase abstracted trace to one which resembles a trace of the circuit without phase abstraction.

[0017] To undo the effects of phase abstraction in the trace, a list of all signal names of each “color” is generated. In other words, all nets are colored such that all nets combinationally driven by latches of color “i” also have color “i”; all nets combinationally driving data_in of latches of color “i” have color “(i−1) mod k”; all nets in combinational cones of color “i” also have color “i”; and all non-clock nets not colored by the above are defaulted to color “0”. Having colored the nets and generated a listing of all signals, the effects of the phase abstraction are removed from the phase-abstracted trace by propagating only signals appearing in the “color_i” list, i.e. clock tree signals are eliminated; and for a color “j” signal, the value present in the phase-abstracted trace at time “i” will be replicated at times “k*i−j” through “k*(i+1)−j−1.” Note that “j” ranges from 0 to k−1.

[0018] These and other features and advantages of the present invention will be described in, or will become apparent to those of ordinary skill in the art in view of, the following detailed description of the preferred embodiments.

BRIEF DESCRIPTION OF THE DRAWINGS

[0019] The novel features believed characteristic of the invention are set forth in the appended claims. The invention itself, however, as well as a preferred mode of use, further objectives and advantages thereof, will best be understood by reference to the following detailed description of an illustrative embodiment when read in conjunction with the accompanying drawings, wherein:

[0020]FIG. 1 is an exemplary block diagram of a computing apparatus according to the present invention;

[0021]FIG. 2 is an exemplary diagram illustrating a process of verification of a circuit design;

[0022]FIG. 3 is an exemplary diagram illustrating a clock tree from the level of a hierarchical design;

[0023]FIG. 4 is an exemplary diagram illustrating a “terminal” design at the logic blocks of FIG. 3;

[0024]FIG. 5 is a diagram illustrating the operation of a gated-clock latch;

[0025]FIG. 6A is an exemplary diagram illustrating the manner by which a two phase gated-clock latch is represented in accordance with one embodiment of the present invention;

[0026]FIG. 6B is an exemplary diagram illustrating the manner by which a three phase gated-clock latch is modeled in accordance with one embodiment of the present invention;

[0027]FIG. 7 is an exemplary diagram of a two-phase circuit design for illustrating the manner by which the present invention removes effects of phase abstraction from a phase-abstracted trace;

[0028]FIG. 8A illustrates the circuit design of FIG. 7 following phase abstraction in which latches of a first color are preserved;

[0029]FIG. 8B illustrates the circuit design of FIG. 7 following phase abstraction in which latches of a second color are preserved;

[0030]FIG. 9 is a flowchart outlining an exemplary operation of the present invention when coloring latches in a circuit design;

[0031]FIG. 10 is a flowchart outlining an exemplary operation of the present invention to explicitly represent gated latches;

[0032]FIG. 11 is a flowchart outlining an exemplary operation of the present invention for removing the effects of phase abstraction for a phase-abstracted trace;

[0033]FIG. 12 is a flowchart outlining an exemplary operation of the present invention for automatically performing coloring of latches in a circuit design, performing phase abstraction, and generating a trace in which phase abstraction effects are removed; and

[0034]FIG. 13 is an exemplary block diagram of an apparatus for performing the functions of the present invention.

DETAILED DESCRIPTION OF THE PREFERRED EMBODIMENT

[0035] With reference now to the figures, and in particular FIG. 1, a block diagram illustrating a data processing system is depicted in which the present invention may be implemented. Data processing system <b>100</b> is an example of a client computer. Data processing system <b>100</b> employs a peripheral component interconnect (PCI) local bus architecture. Although the depicted example employs a PCI bus, other bus architectures such as Accelerated Graphics Port (AGP) and Industry Standard Architecture (ISA) may be used. Processor <b>102</b> and main memory <b>104</b> are connected to PCI local bus <b>106</b> through PCI bridge <b>108</b>. PCI bridge <b>108</b> also may include an integrated memory controller and cache memory for processor <b>102</b>. Additional connections to PCI local bus <b>106</b> may be made through direct component interconnection or through add-in boards. In the depicted example, local area network (LAN) adapter <b>110</b>, SCSI host bus adapter <b>112</b>, and expansion bus interface <b>114</b> are connected to PCI local bus <b>106</b> by direct component connection. In contrast, audio adapter <b>116</b>, graphics adapter <b>118</b>, and audio/video adapter <b>119</b> are connected to PCI local bus <b>106</b> by add-in boards inserted into expansion slots. Expansion bus interface <b>114</b> provides a connection for a keyboard and mouse adapter <b>120</b>, modem <b>122</b>, and additional memory <b>124</b>. Small computer system interface (SCSI) host bus adapter <b>112</b> provides a connection for hard disk drive <b>126</b>, tape drive <b>128</b>, and CD-ROM drive <b>130</b>. Typical PCI local bus implementations will support three or four PCI expansion slots or add-in connectors.

[0036] An operating system runs on processor <b>102</b> and is used to coordinate and provide control of various components within data processing system <b>100</b> in FIG. 1. The operating system may be a commercially available operating system, such as Windows 2000, which is available from Microsoft Corporation. An object oriented programming system such as Java may run in conjunction with the operating system and provide calls to the operating system from Java programs or applications executing on data processing system <b>100</b>. “Java” is a trademark of Sun Microsystems, Inc. Instructions for the operating system, the object-oriented operating system, and applications or programs are located on storage devices, such as hard disk drive <b>126</b>, and may be loaded into main memory <b>104</b> for execution by processor <b>102</b>.

[0037] Those of ordinary skill in the art will appreciate that the hardware in FIG. 1 may vary depending on the implementation. Other internal hardware or peripheral devices, such as flash ROM (or equivalent nonvolatile memory) or optical disk drives and the like, may be used in addition to or in place of the hardware depicted in FIG. 1. Also, the processes of the present invention may be applied to a multiprocessor data processing system.

[0038] As another example, data processing system <b>100</b> may be a stand-alone system configured to be bootable without relying on some type of network communication interface, whether or not data processing system <b>100</b> comprises some type of network communication interface. As a further example, data processing system <b>100</b> may be a personal digital assistant (PDA) device, which is configured with ROM and/or flash ROM in order to provide nonvolatile memory for storing operating system files and/or user-generated data.

[0039] The depicted example in FIG. 1 and above-described examples are not meant to imply architectural limitations. For example, data processing system <b>100</b> also may be a notebook computer or hand held computer in addition to taking the form of a PDA. Data processing system <b>100</b> also may be a kiosk or a Web appliance.

[0040]FIG. 2 illustrates the process involved in generating and verifying a hardware circuit design. As shown in FIG. 2, the process starts with a hardware designer generating a hardware description of the circuit design. This hardware description may be written, for example, using a hardware description language (HDL). High-level synthesis and register-transfer-level (RTL) synthesis are then performed on the HDL description to thereby generate a description of a network of nets, gates, busses, multi-bit boxes (e.g., adders, registers) corresponding to the HDL description, in a particular format. Logic synthesis takes this network description, optimizes it, and produces a technology mapped netlist of the circuit design which is then used to fabricate the circuit.

[0041] Verification is the process of verifying the operation of the circuit model. Verification may be performed on the HDL description of the circuit design or on the network description. Verification may produce a trace illustrating the operation of the circuit design. This trace may be manually or automatically parsed to assess if the circuit behaved properly or improperly along that trace. Phase abstraction may be performed to reduce the workload in performing the verification.

[0042] The present invention provides an apparatus and method for improving the operation of phase abstraction. The present invention improves phase abstraction by providing automated apparatus and methods for coloring latches in a circuit design, handling gated latches, and removing the effects of phase abstraction on resulting traces. As a result, an accurate trace of the circuit design is obtained in which the use of phase abstraction is not perceivable in the resulting trace.

[0043] In explaining how the present invention operates to improve the operation of phase abstraction, consider a k-phase level-sensitive latch-based design that is composed of combinational logic and level-sensitive latches. A level-sensitive latch is a device which has 2 inputs, data and clock, and one data output. A level-sensitive latch acts as a wire when its clock is active (i.e., when it is “transparent”), and holds its last-output value when the clock is inactive. For purposes of the present description, it will be assumed, without loss of generality, that the clock is active when it is a logical one.

[0044] An initial value is defined for the latches in the circuit design to define their output values at time 0 if their clocks are inactive. A correct level-sensitive latch-based design is one whose latches can be classified into k classes as follows: latches of class “c” can only transitively (i.e., without passing through another latch) fan out to latches of class “(c+1) mod k”; the clock to each latch is active every k′th time-step; the clocks to latch class <b>0</b> are active at time 0; and if clocks to latch class “c” are active at time “i”, then clocks to class “(c+1) mod k” are active at time “i+1”. Note that in such designs, functional signals only “toggle” at most every k time-steps due to the clocking.

[0045] Phase abstraction consists of making all but one class of latches into wires, and transforming the remaining class into registers which implicitly update values at each time-step, i.e. they become unconditional one-cycle delay elements. By doing such, time is folded modulo k when verifying this design (ordinarily k time-steps would be necessary for a logical value to propagate through all k classes of latches, but after phase abstraction only one time-step is necessary). Logic in the clock tree itself is eliminated because it is no longer necessary, and its semantics are destroyed by phase abstraction.

[0046] As discussed above, phase abstraction can significantly reduce the number of latches in a design (by at least a factor of k, for a k-phase design) which in itself can provide a linear increase in the speed by which test-based techniques operate and an exponential increase in speed of formal verification techniques. Phase abstraction can further enable combinational optimizations which can arbitrarily further reduce model size.

[0047] There are several complications relating to the use of phase abstraction on real designs. First, the latches must be partitioned into classes, denoting in which “phase” of the clock they are transparent. Second, gated-clock latches pose a complication for phase abstraction because they cannot safely be transformed into wires without violating the semantics of the abstraction (i.e., a wire cannot hold values). Third, traces obtained from verification of phase-abstracted designs reflect the process of phase abstraction, e.g., the inputs and outputs of eliminated latches become simultaneous copies of each other, which can make viewing sequential traces difficult by the designer of the corresponding logic who expects traces to be in terms of the original design, not the phase abstracted variant. None of these topics are addressed by prior art phase abstraction techniques.

[0048] The present invention alleviates these three complications that come as a by-product of the use of phase abstraction by providing an automated mechanism for coloring latches in the circuit design, handling gated latches, and removing the effects of phase abstraction from the resulting trace of the phase abstraction. Each of these aspects of the present invention may be used with known phase abstraction techniques independently of the other aspects. For example, the automated mechanism for coloring latches may be used independently of the automated mechanism for handling gated latches and the automated mechanism for removing the effects of phase abstraction from a phase-abstracted trace.

[0049] In coloring latches in a circuit design, a clock tree is utilized to obtain information about the latches in the circuit design. A clock tree is a representation of the manner by which clock signals are distributed throughout the circuit logic in a circuit design. Clock trees and the manner by which clock trees are generated and described are generally known in the art and thus, a detailed explanation is not included herein.

[0050]FIG. 3 is an exemplary diagram illustrating a clock tree for a hierarchical circuit design. As shown in FIG. 3, the hierarchical design <b>300</b> includes a plurality of inputs <b>310</b> and outputs <b>350</b>. One of the many inputs is a clock signal <b>315</b>. The clock signal <b>315</b> passes through clock buffer/redistribution logic <b>320</b> to recreate many “balanced” copies of the clock signal. This is done to minimize circuit noise, delay and clock skew. This clock buffer/redistribution logic <b>320</b> may contain a numerous elements, of which only a few are depicted. The cloud <b>330</b> is depicted to illustrate other elements of the clock buffer/redistribution logic <b>320</b> which are explicitly shown.

[0051] Ultimately, the outputs of the clock buffer/redistribution logic <b>320</b> pass to logic blocks <b>340</b> at a lower level of the hierarchy. It is at this lower level of the hierarchy that the mechanisms of the present invention are applied for high-performance circuit designs. The same mechanisms of the present invention may be applied to the clock tree depicted in FIG. 3 for lower performance circuit designs without departing from the spirit and scope of the present invention.

[0052] It should be appreciated that the hierarchical view of a circuit design may be for an entire integrated circuit chip or any component thereof. In other words, each “child” of the chip level view may also be represented as a hierarchical design similar to that shown in FIG. 3. Thus, the present invention may be applied to any level of the circuit design.

[0053]FIG. 4 is an exemplary diagram illustrating a “terminal” design entity corresponding to logic blocks <b>340</b> in FIG. 3. While FIG. 4 is illustrated for a lower level of the hierarchical design in FIG. 3, the present invention is not limited to such. Rather, the “terminal” design is intended to merely represent the particular design on which the present invention is operating. This design may be at a level of the entire circuit, a terminal part of the circuit, or any portion or level in-between. In a preferred embodiment, the present invention operates on a terminal part of the circuit design and thus, the design shown in FIG. 4 is termed a “terminal” design entity.

[0054] As shown in FIG. 4, the terminal design <b>400</b> includes a plurality of inputs <b>410</b> and outputs <b>450</b> in a similar manner as with the hierarchical design shown in FIG. 3. Also similar to FIG. 3, the terminal design <b>400</b> has one clock input <b>415</b>. Pre-defined clock tree primitives <b>420</b> drive all clock signals received on clock input <b>415</b> to the latches <b>430</b> and <b>440</b> themselves. These primitives <b>420</b> contain sufficient information to taxonomize the clocks into their respective phases (i.e., no logic is allowed between the clock tree primitives and the latches in these design styles). From this information, a simple combinational fanout sweep from the clock tree primitives <b>420</b> can be used to “color” latches into their respective classes.

[0055] In the terminal design, the clock tree passes through more complex clock buffers <b>422</b> that have two (or for k-phase designs “k”) outputs. These outputs represent clock signals to the respective latches <b>430</b> and <b>440</b> themselves. Thus, for a two phase circuit design, there are two types of clock outputs from these clock buffers—L1 clock signals (illustrated as solid lines) and L2 clock signals (illustrated as dashed lines). An L1 clock signal can only drive an L1 latch (latches <b>430</b>), and an L2 clock signal can only drive an L2 latch (latches <b>440</b>). Thus, it is possible to infer a latch type or classification from the clock signals sent to that latch. In this way, the clock buffers <b>422</b> ensure that the clock signals to the latches themselves are correct, i.e. that the clocks to the latches are active, hence the respective latches are transparent at the proper time (i.e. clock phase) with respect to the global clock <b>415</b>.

[0056] With the high performance designs discussed above, the clock tree is distributed in a balanced manner through the logic. For example, in higher performance designs, the clock buffers of FIG. 4 are very tightly regulated for synthesis purposes to minimize skew, and the like. Only a specific set of clock buffers are developed for use within the design. All functional latches must be clocked directly by outputs of these clock buffers. It is illegal for functional latches to be clocked by the global clock, i.e. not by the output of a clock buffer. It is also illegal for any logic to be placed between the outputs of a clock buffer and the latches that it clocks. This set of clock buffers is developed for a specific set of purposes: their outputs represent L1 clocks versus L2 clocks (up to arbitrary Lk clocks), they are further attributed as to whether they are functional clocks versus “scan clocks” (the latter used only during scanning of the netlist, not during its functional operation), and whether they are free running versus gated clocks. Such buffers are also specially marked (or readily can be) so that synthesis and verification tools can easily locate them.

[0057] In lower performance designs, however, the clock tree is not distributed throughout the logic. Rather, clocks are driven from a central point. In lower performance designs, the global clocks may be distributed directly to latches without passing through clock buffers (in reality, the “terminal block” may not have buffers but one of its ancestors will—lower performance netlists just worry less about skew and thus, do not redistribute the clock logic to as large of a degree). There are separate global clocks of functional versus scan, but inverters or AND gates may be used to differentiate L1 versus L2 latches and free running versus gated clocks. For such designs, coloring can be performed by a counting of inversions along the clock logic (lower performance designs can be assumed to be two phase while higher phases are used only to improve performance beyond that possible with two phase netlists). Clock gates can be found by identifying AND gates along this path. Thus, the same mechanisms may be used but instead, the presence of clock buffers is inferred from the logic along the clock tree.

[0058] Thus, by obtaining the clock tree information regarding the terminal design, the clock signals sent to the latches may be identified. Based on this identification, the latches may be colored, i.e. categorized, into various classes based on their clock signals. This may be done in an automated fashion such that the burden is taken off of the circuit designer to identify which latches in the design are of which type. As a result, the possible sources of error are reduced and the speed with which design verification can be performed is increased. Utilizing such a clocking convention further makes connectivity failures, i.e. a L1 latch transitively fanning out to another L1 latch or “coloring errors” such as improper clock connectivity, significantly easier to identify. Errors detected with the present invention will not be time-consuming user errors, but instead actual errors in the design.

[0059] As shown in FIG. 4, a global clock is redistributed to each of the individual latches via clock buffers. For normal latches, the clock appearing at every latch of color “i” will be a logical one at the same time. The clock appearing at every latch of color “i+1 mod k” will be a logical one at the next time-step. Note that each latch itself is of an identical type in a level-sensitive latch-based netlist, i.e. removed from the circuit, there is nothing differentiating a L1 latch from a L2 latch. By redistributing the “global” clock to each individual latch, this clock distribution logic enforces the above rule as to when the distributed clock appearing at the individual latches will be a logical one.

[0060] As previously mentioned above, not all latches may be simply categorized into L1 or L2 latches. Some latches may be gated, i.e. may have gated clocks, and thus, do not always operate strictly on an L1 or L2 latch basis depending on whether they receive a gate signal or not. Hereafter, the terms “gated-clock latch” and “gated latch” will be used interchangeably to refer to a latch that has a gated-clock input. FIG. 5 is an exemplary diagram of a gated latch to illustrate how the gated latch operates differently from a regular non-gated latch.

[0061] A gated latch may be an identical structure as a normal L1 or L2 latch. However, unlike normal latches where the clock buffers ensure that each clock will be active every k time steps, a “gate” signal is utilized, as depicted in FIG. 5, to be able to “stop the clock,” i.e. to prevent the clock seen at a given gated-clock latch from being a 1 when the clock buffer of a non-gated variant of the same “color” would otherwise drive a 1 to the latch. For example, as shown in FIG. 5, an AND gate <b>510</b> exists before the latch <b>520</b>. Thus, the AND gate <b>510</b> outputs a logical one on the clock signal <b>530</b> to the latch <b>520</b> only when both the clock signal <b>530</b> and the gate signal <b>540</b> are a logical 1. If only the clock signal <b>530</b> is a 1 but the gate is a logical 0, the AND gate <b>510</b> generates a “0” clock output and thus, the latch <b>520</b> holds its value since it is not transparent at the time that it ordinarily would be (i.e. during its “phase” of the clock period).

[0062] Since phase abstraction involves replacing latches with wires, which assumes that latch clocks are free-running, i.e. not gated, the functionality of the clock gate must be made explicit in order for the phase abstraction to be able to be performed accurately without introducing errors into the resulting trace output. The present invention provides an automated mechanism for identifying gated latches from the information obtained from clock tree primitives and then converting these gated latches into an explicit representation of the gated latch using only non-gated latches. This conversion is performed accurately without performing and “unsound” transformation which violates the correctness of phase abstraction, thereby invalidating any verification results obtained from the phase abstracted netlist. It should be appreciated, however, that with some embodiments of the present invention, other mechanisms, such as manual enumeration, for identifying gated-clock latches may be used without departing from the spirit and scope of the present invention.

[0063]FIG. 6A is an exemplary diagram of a representation of a two-phase gated-clock latch using non-gated-clock latches in accordance with one embodiment of the present invention. As shown in FIG. 6A, this representation of the gated latch includes a first latch <b>610</b> of a same type as the gated latch and a second latch <b>620</b> of an opposite type from that of the gated latch. The second latch <b>620</b> is present in a feedback path from the first latch <b>610</b>. The feedback path passes through a multiplexor <b>630</b>.

[0064] With the multiplexor <b>630</b>, if the gate signal is “0”, then the clock to the first latch <b>610</b> is stopped so that the feedback path output is passed through the multiplexor. Otherwise, if the gate signal is not “0”, then the data input <b>635</b> is passed through the multiplexor. In this way, the first latch <b>610</b>, which corresponds to the gated latch, and the added second latch <b>620</b> may be driven with appropriate phase ungated clocks. Thus, traditional phase abstraction may be used on this representation of the gated latch without introducing errors into the resulting trace, e.g. circuit amnesia—the latch is unable to hold a value when its gate is shut because phase abstraction will eliminate the latch.

[0065]FIG. 6B extends the representation of a gated latches from the two-phase gated latch illustrated in FIG. 6A, to a three phase gated latch. As shown in FIG. 6B, the difference between the representation of a two phase and a three phase gated latch is in the sequence of latches included in the feedback loop to the multiplexor. In both cases, a sequence of opposite type latches from that of the gated latch are included in the feedback loop. Assuming that the gated latch is of type L1, in a two phase gated latch, the latch in the feedback loop is of type L2. In a three phase gated latch, the latches in the feedback loop include a L2 and L3 type latch.

[0066] Of course this extension of the representation of a gated latch may be further extended to “k” phase gated latches. It should further be recognized that gated latches may be combined in any number of different ways and thus, the representations discussed above may also be combined. Thus, for example, if the original circuit involved a gated L1 latch coupled to a gated L2 latch, the resulting representation under the present invention would involve a representation as show in FIG. 6A coupled to a representation of a gated L2 latch.

[0067] Gated latches may be identified from the clock tree primitives, e.g., clock buffers. The clock tree primitives include information identifying whether the output of the clock buffer, for example, is gated and, if so, what the “gate” signal is. Thus, by parsing the clock tree primitive information, a determination may be made as to which latches in the circuit design are gated. Once the gated latches are identified, their functionality may be explicitly represented using non-gated latches, as described in greater detail hereafter.

[0068] In one embodiment of the present invention, an algorithm is provided for performing the conversion of a gated latch to the representation shown in FIG. 6A. The pseudocode for the algorithm that performs this conversion is as follows: <tables id="TABLE-US-00001" num="1"><table frame="none" colsep="0" rowsep="0"><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="14PT" align="left" /><colspec colname="1" colwidth="203PT" align="left" /><thead><row><entry /><entry /></row><row><entry /><entry namest="OFFSET" nameend="1" align="center" rowsep="1" /></row></thead><tbody valign="top"><row><entry /><entry>Determine “k” for the circuit via clock/coloring</entry></row><row><entry /><entry>info</entry></row><row><entry /><entry>for each latch L</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="28PT" align="left" /><colspec colname="1" colwidth="189PT" align="left" /><tbody valign="top"><row><entry /><entry>if L has a gated-clock</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="42PT" align="left" /><colspec colname="1" colwidth="175PT" align="left" /><tbody valign="top"><row><entry /><entry>make_gate_explicit(L, k)</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="14PT" align="left" /><colspec colname="1" colwidth="203PT" align="left" /><tbody valign="top"><row><entry /><entry>algorithm make_gate_explicit(latch_i, k) {</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="28PT" align="left" /><colspec colname="1" colwidth="189PT" align="left" /><tbody valign="top"><row><entry /><entry>// latch_i is the gated-clock register</entry></row><row><entry /><entry>// k is the number of phases of the design</entry></row><row><entry /><entry>cur_color = (color(latch_i) + 1) mod k;</entry></row><row><entry /><entry>cur_latch = latch_i;</entry></row><row><entry /><entry>while(cur_color != color(latch_i)) {</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="42PT" align="left" /><colspec colname="1" colwidth="175PT" align="left" /><tbody valign="top"><row><entry /><entry>next_latch = get_or_create_latch(cur_color,</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="14PT" align="left" /><colspec colname="1" colwidth="203PT" align="left" /><tbody valign="top"><row><entry /><entry>cur_latch, initial_value(cur_latch));</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="42PT" align="left" /><colspec colname="1" colwidth="175PT" align="left" /><tbody valign="top"><row><entry /><entry>cur_latch = next_latch;</entry></row><row><entry /><entry>cur_color = (cur_color + 1) mod k;</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="28PT" align="left" /><colspec colname="1" colwidth="189PT" align="left" /><tbody valign="top"><row><entry /><entry>}</entry></row><row><entry /><entry>cur_mux = create_mux();</entry></row><row><entry /><entry>Connect_mux_select(cur_mux, clock_gate(latch_i));</entry></row><row><entry /><entry>connect_mux_port_p(cur_mux, data_out(next_latch));</entry></row><row><entry /><entry>connect_mux_port_1(cur_mux, data_in(latch_i));</entry></row><row><entry /><entry>data_in(latch_i) = data_out(cur_mux);</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="2"><colspec colname="OFFSET" colwidth="14PT" align="left" /><colspec colname="1" colwidth="203PT" align="left" /><tbody valign="top"><row><entry /><entry>}</entry></row><row><entry /><entry namest="OFFSET" nameend="1" align="center" rowsep="1" /></row></tbody></tgroup></table></tables>

[0069] The procedure get_or_create_latch attempts to locate a latch of color “(cur_color+1) mod k” in the direct fanout of cur_latch (i.e. passing through no logic other than simple buffering), with the same initial_value as that of cur_latch. If no such latch exists, then this procedure creates such a latch with an ungated clock, driven directly by cur_latch. This process is iterated to create (or find) a topologically-correct feedback path to the current latch. The process then creates a multiplexor in front of latch_i. This multiplexor is selected by the clock gate. If the clock gate is inactive, then this created (or discovered) feedback path is sensitized. If the clock gate is active, then the data_in of latch_i is sensitized. The output of the multiplexor is then connected to the data_in of latch_i. This procedure makes the clock gate explicit. That is, after being applied to all gated clocks, simple phase abstraction can be applied and semantics will not be violated as they would otherwise in presence of gated-clock latches.

[0070] Thus, the present invention provides mechanisms for automatically coloring latches in a circuit design such that the burden of specifying which latches are of which type is shifted from the human designer to the automated mechanisms. These mechanisms further include an automated methodology for identifying and representing gated latches such that the phase abstraction applied to the gated latches will not result in erroneous information in the resulting trace. These mechanisms may be used in conjunction with one another or separate from one another with known phase abstraction tools.

[0071] Once the latches in a circuit design are colored into their respective categories, phase abstraction may be applied to them. As previously mentioned, phase abstraction involves replacing all but one class of latches with wires and replacing the remaining class with an edge sensitive element, e.g., a register. Once this replacement is done, verification of the modified circuit design is performed to identify whether there are any operational inconsistencies between the designer's intention for the circuit and its actual behavior.

[0072] Typically, however, when a trace is obtained after having performed phase abstraction, the resulting phase-abstracted trace does not resemble a trace of the circuit design that would be obtained without phase abstraction. That is, the resulting trace includes effects from the phase abstraction that make it difficult and/or time consuming for a human designer to convert into a trace of a non-phase abstracted circuit design. The present invention provides a mechanism by which the effects of phase abstraction may be removed from a phase abstracted trace to thereby, automatically generate a non-phase abstracted trace for use by circuit designers in verifying the operation of their circuit designs.

[0073]FIG. 7 is an exemplary diagram of a circuit design for illustrating the manner by which the present invention removes the effects of phase abstraction from the phase abstracted trace. As shown in FIG. 7, the two-phase circuit design includes combinational logic elements <b>710</b>, <b>720</b> and <b>730</b>. The combinational logic element <b>710</b> performs a function “f1” on received data signals to generate an output signal. Similarly, combinational logic elements <b>720</b> and <b>730</b> perform functions “f2” and “f3”, respectively, on their input data signals to generate output signals.

[0074] Between combinational logic elements <b>710</b> and <b>720</b> is a first latch L₁having a color 0. Between combinational logic elements <b>720</b> and <b>730</b> is a second latch L₂having a color 1. The signals along the wires between elements are denoted A, B, C, D, E and F. A feedback loop from the output of latch L₂to an input of combinational logic <b>710</b> is also provided.

[0075] An un-phase-abstracted trace of the circuit design shown in FIG. 7 is shown in Table 1 below: <tables id="TABLE-US-00002" num="2"><table frame="none" colsep="0" rowsep="0"><tgroup align="left" colsep="0" rowsep="0" cols="1"><colspec colname="1" colwidth="217PT" align="center" /><thead><row><entry namest="1" nameend="1" align="center">TABLE 1</entry></row></thead><tbody valign="top"><row><entry /></row><row><entry namest="1" nameend="1" align="center" rowsep="1" /></row><row><entry>Unabstracted Trace of FIG. 7</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="5"><colspec colname="1" colwidth="28PT" align="left" /><colspec colname="2" colwidth="42PT" align="left" /><colspec colname="3" colwidth="49PT" align="left" /><colspec colname="4" colwidth="42PT" align="left" /><colspec colname="5" colwidth="56PT" align="left" /><tbody valign="top"><row><entry>Clock</entry><entry>L1</entry><entry>L2</entry><entry>L1</entry><entry>L2</entry></row><row><entry namest="1" nameend="5" align="center" rowsep="1" /></row><row><entry>A</entry><entry>a</entry><entry>a′</entry><entry>b</entry><entry>b′</entry></row><row><entry>B</entry><entry>f1(a,L2₀)</entry><entry>f1(a′,a)</entry><entry>f1(b,a)</entry><entry>f1(b′,f2(f1(b,a)))</entry></row><row><entry>C</entry><entry>f1(a,L2₀)</entry><entry>f1(b,L2₀)</entry><entry>f1(b,a)</entry><entry>f1(b,a)</entry></row><row><entry>D</entry><entry>a</entry><entry>a</entry><entry>f2(f1(b,a))</entry><entry>f2(f1(b,a))</entry></row><row><entry>E</entry><entry>L2₀</entry><entry>a</entry><entry>a</entry><entry>f2(f1(b,a))</entry></row><row><entry>F</entry><entry>f3(L2₀)</entry><entry>f3(a)</entry><entry>f3(a)</entry><entry>f3(f2(f1(b,a)))</entry></row><row><entry namest="1" nameend="5" align="center" rowsep="1" /></row></tbody></tgroup></table></tables>

[0076] In the above table, a, a′, b and b′ are arbitrarily defined input values to the circuit design at the various clock timings. In addition, α is defined as f2(f1(a,L2₀)) where L2₀is the initial value of latch L2. While the above table illustrates the various data values input/output along lines A-F as symbolic values over arbitrary input values a, a′, b, b′ . . . , in actuality the trace would be a plurality of 0's and 1's indicating the data values at different times during the trace when filling in a 0 or a 1 value for each input value a, a′, etc.

[0077] In one exemplary embodiment, in order to remove the effects of phase abstraction in a phase abstracted trace, a linear-time algorithm may be used to perform this transformation from phase abstracted trace to non-phase abstracted trace.

[0078] During phase abstraction, a list of all signal names of each color is generated. In other words, the nets of the circuit are colored as follows:

[0079] (1) all nets combinationally driven by latches of color “i” also have color “i”;

[0080] (2) all nets combinationally driving data_in of latches of color “i” have color “(i−1) mod k”;

[0081] (3) all nets in combinational cones of color “i” also have color “i”; and

[0082] (4) all non-clock nets (see below) not colored by the above can default to color 0.

[0083] In addition clock nets (which are in the fanin of ungated latch clocks) are specially colored since these will be eliminated from the trace. The coloring algorithm used for clock nets sweeps fanin-wise through combinational and sequential logic, beginning from all clock inputs of latches (since clock logic may contain sequential elements).

[0084] In deciding which signals to add into the un-phase-abstracted trace, it is important to preserve the values of the functional logic in the trace but to strip out the clock tree logic since phase abstraction will destroy its semantics. Verification of the clock logic is a much simpler process than functional verification in general. Therefore, partitioning the overall verification tasks is quite worthwhile. In other words, it may be assumed that the clock logic is correct when verifying functionality, and the clock logic may be verified separately. It should be noted that the functional gate of gated-clock latches will be propagated.

[0085] In a two-phase circuit design, phase abstraction may be performed in two different ways. That is, elements of color 0 may be preserved or elements of color 1 may be preserved. FIGS. 8A and 8B illustrate these two methods of phase abstraction. Of course, in higher phase circuits, i.e. three phase circuits and higher, additional ways to perform the phase abstraction are possible. The methodology of the present invention may be extended to any k-phase circuit design.

[0086]FIG. 8A illustrates the circuit design of FIG. 7 when phase abstraction is performed such that color 1 elements are preserved. As shown in FIG. 8A, since color 1 elements are preserved, the latch L₁, is replaced by a wire, i.e. is made transparent. A phase-abstracted trace of the resulting circuit design shown in FIG. 8A is provided in Table 2 below: <tables id="TABLE-US-00003" num="3"><table frame="none" colsep="0" rowsep="0"><tgroup align="left" colsep="0" rowsep="0" cols="1"><colspec colname="1" colwidth="217PT" align="center" /><thead><row><entry namest="1" nameend="1" align="center">TABLE 2</entry></row></thead><tbody valign="top"><row><entry /></row><row><entry namest="1" nameend="1" align="center" rowsep="1" /></row><row><entry>Phase Abstraction 1 (FIG. 8A)</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="6"><colspec colname="OFFSET" colwidth="14PT" align="left" /><colspec colname="1" colwidth="35PT" align="left" /><colspec colname="2" colwidth="49PT" align="left" /><colspec colname="3" colwidth="56PT" align="left" /><colspec colname="4" colwidth="21PT" align="center" /><colspec colname="5" colwidth="42PT" align="center" /><tbody valign="top"><row><entry /><entry>Clock</entry><entry>T</entry><entry>T</entry><entry>color</entry><entry>δ</entry></row><row><entry /><entry namest="OFFSET" nameend="5" align="center" rowsep="1" /></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="5"><colspec colname="1" colwidth="49PT" align="left" /><colspec colname="2" colwidth="49PT" align="left" /><colspec colname="3" colwidth="56PT" align="left" /><colspec colname="4" colwidth="21PT" align="center" /><colspec colname="5" colwidth="42PT" align="center" /><tbody valign="top"><row><entry>A</entry><entry>a</entry><entry>b</entry><entry>1</entry><entry>0</entry></row><row><entry>B</entry><entry>f1(a,L2₀)</entry><entry>f1(b,a)</entry><entry>1</entry><entry>0</entry></row><row><entry>C</entry><entry>f1(a,L2₀)</entry><entry>f1(b,a)</entry><entry>0</entry><entry>2</entry></row><row><entry>D</entry><entry>a</entry><entry>f2(f1(b,a))</entry><entry>0</entry><entry>2</entry></row><row><entry>E</entry><entry>L2₀</entry><entry>a</entry><entry>1</entry><entry>0</entry></row><row><entry>F</entry><entry>f3(L2₀)</entry><entry>f3(a)</entry><entry>1</entry><entry>0</entry></row><row><entry namest="1" nameend="5" align="center" rowsep="1" /></row></tbody></tgroup></table></tables>

[0087] In the above table, each column of the trace represents an entire clock period T, a and b are arbitrarily defined input values to the circuit design and α is defined as f2(f1(a,L2₀)) where L2₀is the initial value of latch L2.

[0088] The “color” column identifies the color of the data signal, as identified by the color of the combinational logic elements and preserved latches. The mechanisms for coloring elements of a circuit design, and thus the data signals in the circuit design, have been discussed previously.

[0089] The δ column represents a delay in the trace data. In other words, the δ value represents the amount of shifting in the trace data that is necessary to remove the effects of the phase abstraction in the resulting trace. For nets v, the δ value is defined as k (for a two phase circuit design, k is 2) only if the color of the data signal, i.e. color(v), is less than the color of the latches preserved by the phase abstraction; otherwise the value for δ is 0. Presented a different way, the δ value is 0 if color(v) is k−1 or if latches of color 0 to color(v) are preserved; otherwise, the value of δ is k.

[0090]FIG. 8B illustrates the circuit design of FIG. 7 when phase abstraction is performed such that color 0 elements are preserved. As shown in FIG. 8B, since color 0 elements are preserved, the latch L₂, is replaced by a multiplexor. A phase-abstracted trace of the resulting circuit design shown in FIG. 8A is provided in Table 3 below: <tables id="TABLE-US-00004" num="4"><table frame="none" colsep="0" rowsep="0"><tgroup align="left" colsep="0" rowsep="0" cols="1"><colspec colname="1" colwidth="217PT" align="center" /><thead><row><entry namest="1" nameend="1" align="center">TABLE 3</entry></row></thead><tbody valign="top"><row><entry /></row><row><entry namest="1" nameend="1" align="center" rowsep="1" /></row><row><entry>Phase Abstraction 2 (FIG. 8B)</entry></row></tbody></tgroup><tgroup align="left" colsep="0" rowsep="0" cols="6"><colspec colname="OFFSET" colwidth="14PT" align="left" /><colspec colname="1" colwidth="35PT" align="left" /><colspec colname="2" colwidth="49PT" align="left" /><colspec colname="3" colwidth="56PT" align="left" /><colspec colname="4" colwidth="21PT" align="center" /><colspec colname="5" colwidth="42PT" align="center" /><tbody valign="top"><row><entry /><entry>Clock</entry><entry>T</entry><entry>T</entry><entry>color</entry><entry>δ</entry></row><row><entry /><entry namest="OFFSET" nameend="5" align="center" rowsep="1" /></row><row><entry /><entry>A</entry><entry>a</entry><entry>b</entry><entry>1</entry><entry>0</entry></row><row><entry /><entry>B</entry><entry>f1(a,L2₀)</entry><entry>f1(b,a)</entry><entry>1</entry><entry>0</entry></row><row><entry /><entry>C</entry><entry>L1₀</entry><entry>F1(a,L2₀)</entry><entry>0</entry><entry>0</entry></row><row><entry /><entry>D</entry><entry>f2(L1₀)</entry><entry>a</entry><entry>0</entry><entry>0</entry></row><row><entry /><entry>E</entry><entry>L2₀</entry><entry>a</entry><entry>1</entry><entry>0</entry></row><row><entry /><entry>F</entry><entry>f3(L2₀)</entry><entry>f3(a)</entry><entry>1</entry><entry>0</entry></row><row><entry /><entry namest="OFFSET" nameend="5" align="center" rowsep="1" /></row></tbody></tgroup></table></tables>

[0091] Whether the phase abstraction from FIG. 8A or FIG. 8B is utilized, the present invention performs functions designed to remove the effects of the phase abstraction. Because phase abstraction essentially collapses the time periods in the trace, in order to remove the effects of phase abstraction, the time periods must be expanded. In order to do this, the data signal values at various timings during the trace must be recreated from the phase abstracted trace.

[0092] The present invention recreates these data signal values by replicating the data signal values shown in the phase abstracted trace at determined time intervals in the un-phase-abstracted trace. In other words, the values of net v at time i from the phase abstracted trace are applied to chosen time steps i′ of the un-phase-abstracted trace. These time steps i′ are chosen based on the following relationship:

times <i>i′=[k*</i>(<i>i−</i>1)+color(<i>v</i>)+δ(<i>v</i>), . . . , <i>k*</i>(<i>i</i>)+color(<i>v</i>)−1+δ(<i>v</i>)]

[0093] as long as: i′≧0 (no negative time steps); and

[0094] [color(v)=k−1 or i′≧color(v)] (used to prevent replication of initial values of an “artifact latch.”

[0095] An “artifact latch” is any latch of color &lt;k−1. They are referred to as “artifacts” since they will cause the phase-abstracted trace to illustrate initial values that do not appear in the un-phase-abstracted trace.

[0096] Thus, the present invention generates an un-phase-abstracted trace from a phase-abstracted trace by replicating the data signal values at times defined by the relationship above. In so doing, a trace similar to that shown in Table 1 is generated. This allows a user of the present invention who expects to see a trace in terms of the actual circuit design, rather than a phase-abstracted circuit, to receive an un-phase-abstracted trace even though phase abstraction was used during the verification of the circuit design. Thus, the benefits of phase abstraction are obtained while eliminating the negative effects of having the user interpret the phase abstracted trace in terms of an un-phase-abstracted trace.

[0097]FIG. 9 is a flowchart outlining an exemplary operation for coloring latches in a circuit design in accordance with the present invention. As shown in FIG. 9, the operation starts with receiving a circuit design (step <b>910</b>). The terminal points at the output of the clock buffers in the clock tree corresponding to the circuit design are identified (step <b>920</b>). Since a list of all types of clock buffers is available from the circuit design, e.g., from the netlist, the important portions of the clock tree can be identified.

[0098] From the clock tree, the clock signals that activate the various latches in the circuit design are identified (step <b>930</b>). The corresponding latches are then colored based on the type of clock signal that activates the latch (step <b>940</b>). A listing of latches and their corresponding colors is then generated (step <b>950</b>) and the operation ends.

[0099]FIG. 10 is a flowchart outlining an exemplary operation of the present invention when converting a gated-clock latch into an explicit representation of the gated latch using non-gated latches. As shown in FIG. 10, the operation starts with the identification of a gated latch from clock tree information for the circuit design (step <b>1010</b>). The latch type, e.g., L1 or L2, for the gated latch is identified (step <b>1020</b>). The gate is removed and a multiplexor having the gate signal and a data_in signal as inputs is created before the gated latch (step <b>1030</b>). The gate signal acts a selector signal wherein the data_in signal is selected in a “gate open” state and the feedback path is selected in a “gate closed” state. A sequence of latches of opposite type from that of the gated latch are generated along the feedback loop (step <b>1040</b>). The resulting modified circuit design is then stored for use in the phase abstraction (step <b>1050</b>) and the operation ends. This process may be repeated for each gated latch identified in the clock tree.

[0100]FIG. 11 is a flowchart outlining an exemplary operation of the present invention when removing the effects of phase abstraction from a phase abstracted trace. As shown in FIG. 11, the operation starts with receiving a phase abstracted trace (step <b>1110</b>). Coloring information for the original circuit is received (step <b>1120</b>). Information as to which type of latches were made into wires by phase abstraction is also received (step <b>1130</b>). The effects of the phase abstraction in the trace are then undone (step <b>1140</b>) and the un-phase-abstracted trace is stored for later output (step <b>1150</b>).

[0101] The mechanisms described in FIGS. <b>9</b>-<b>11</b> may be employed separately or in any combination to obtain the various benefits indicated above with regard to each mechanism. That is, the automated coloring of latches, representation of gated latches as non-gated latches, and removal of phase abstraction effects from a phase-abstracted trace, may each be used individually or with one or more of the other mechanisms. In a preferred embodiment, to obtain maximum benefit from the above mechanisms, all three are combined into an overall automated method of verification of a circuit design using phase abstraction.

[0102]FIG. 12 if a flowchart illustrating a combined methodology for verification of a circuit design using phase abstraction in accordance with a preferred embodiment of the present invention. As shown in FIG. 12, the operation starts with the receipt of a circuit design (step <b>1210</b>). Then, the latch clocks are taxonomized (step <b>1220</b>). Gated latches in the circuit design are identified and explicitly represented as non-gated latches (step <b>1230</b>). The latches in the modified circuit design are colored based on the information obtained from the clock tree (step <b>1240</b>).

[0103] Phase abstraction is then performed on the colored circuit design (step <b>1250</b>). For example, for a k-phase netlist, the netlist can be phase abstracted to k different “preserve-color-i-latches.” If color “k−1” latches are preserved, the remaining latches are replaced by wires. If color “j!=k−1” is preserved, color “k−1” latches are eliminated (and maybe others if k!=2), so that another mulitplexor is introduced to preserve the initial values of the color k−1 latches. This multiplexor is selected by a new signal “f” that is created such that it is 1 at time 0, and thereafter it is a 0 for any time i&gt;0. The “selector is 0” input is the original L2 input (or L “k−1” input). The “selector is 1” input is connected to the initial value of the removed L “k−1” latch. Note that which phase was preserved is now part of the un-phase-abstracting of trace code.

[0104] The phase abstracted circuit design is then verified, e.g., using a verification tool (step <b>1260</b>). Pass/Fail information and the resulting trace are received from the verification tool (step <b>1270</b>). The phase abstracted trace is then processed to remove the effects of the phase abstraction (step <b>1280</b>).

[0105]FIG. 13 is an exemplary block diagram of the primary elements of an automated design verification apparatus according to the present invention. The elements shown in FIG. 13 may be implemented in hardware, software, or any combination of hardware and software without departing from the spirit and scope of the present invention. In a preferred embodiment, the elements shown in FIG. 13 are implemented as software instructions implemented in one or more hardware devices.

[0106] As shown in FIG. 13, the automated design verification apparatus includes a controller <b>1310</b>, a user interface <b>1320</b>, a design storage device <b>1330</b>, a circuit element coloring module <b>1340</b>, a phase abstraction module <b>1350</b>, a phase-abstracted trace conversion module <b>1360</b>, and a trace output device <b>1370</b>. The elements <b>1310</b>-<b>1370</b> are coupled to one another via the control/data signal bus <b>1380</b>. Although a bus architecture is shown in FIG. 13, the present invention is not limited to such and any architecture that facilitates the communication of control/data signals between the elements <b>1310</b>-<b>1370</b> may be used without departing from the spirit and scope of the present invention.

[0107] Furthermore, while FIG. 13 depicts the elements <b>1310</b>-<b>1370</b> as being integrated into the same physical device, the present invention is not limited to such an embodiment. Rather, one or more of the elements <b>1310</b>-<b>1370</b> may be remotely located from one or more of the other elements such that a distributed processing environment is obtained. In such an embodiment, the elements <b>1310</b>-<b>1370</b> that are remotely located may be in communication with the other elements <b>1310</b>-<b>1370</b> via one or more networks or other communication links.

[0108] The controller <b>1310</b> is responsible for controlling the overall operation of the automated design verification apparatus and for orchestrating the operation of the other elements <b>1320</b>-<b>1370</b>. The controller <b>1310</b> receives input from a human designer via the user interface <b>1320</b>. The user may enter a circuit design or the like, and store this circuit design in the design storage device <b>1330</b>. In response to commands from the user, the controller <b>1310</b> may instruct the element coloring module <b>1340</b>, phase abstraction module <b>1350</b>, and phase-abstracted trace conversion module <b>1360</b>, to operate in order to perform a verification of the circuit design stored in the design storage device <b>1330</b>.

[0109] In response to instructions from the controller <b>1310</b>, the element coloring module <b>1340</b> performs analysis on a clock tree of the circuit design to thereby color the various latches in the circuit design, as previously described above. This coloring of the latches may include representing gated latches as non-gated latches. The colored circuit design may then be input to the phase abstraction module <b>1350</b> which performs phase abstraction on the colored circuit design and performs a trace of the circuit operation. The resulting phase-abstracted trace is then input to the phase-abstracted trace conversion module <b>1360</b> which processes the phase-abstracted trace to remove the effects of phase abstraction.

[0110] Thus, the present invention provides an apparatus and method for automatically coloring latches, both gated and non-gated latches, in a circuit design based on clock tree information. The present invention further provides an apparatus and method for verifying a circuit design using phase abstraction in which the phase abstracted trace is processed to remove the effects of the phase abstraction. In this way, the burden of performing the circuit verification on the human designer is lessened, the speed with which the verification can be performed is increased, and the accuracy of the trace is increased.

[0111] It is important to note that while the present invention has been described in the context of a fully functioning data processing system, those of ordinary skill in the art will appreciate that the processes of the present invention are capable of being distributed in the form of a computer readable medium of instructions and a variety of forms and that the present invention applies equally regardless of the particular type of signal bearing media actually used to carry out the distribution. Examples of computer readable media include recordable-type media, such as a floppy disk, a hard disk drive, a RAM, CD-ROMs, DVD-ROMs, and transmission-type media, such as digital and analog communications links, wired or wireless communications links using transmission forms, such as, for example, radio frequency and light wave transmissions. The computer readable media may take the form of coded formats that are decoded for actual use in a particular data processing system.

[0112] The description of the present invention has been presented for purposes of illustration and description, and is not intended to be exhaustive or limited to the invention in the form disclosed. Many modifications and variations will be apparent to those of ordinary skill in the art. The embodiment was chosen and described in order to best explain the principles of the invention, the practical application, and to enable others of ordinary skill in the art to understand the invention for various embodiments with various modifications as are suited to the particular use contemplated.