Abstract:
A system, method, computer program, and article of manufacture for generating a golden circuit including datapath components for equivalence checking of synthesized revised circuit. The method includes generating a set of static, dynamic and derived candidates for the datapath component subcircuit, evaluating the similarity degree for each candidate in relation to the revised circuits and selecting one candidate for implementation in the golden circuit. As a result, the subcircuit of datapath component in the golden circuit is replaced with the subcircuit which is more similar to the revised circuit to improve the efficiency of the equivalence checking.

Description:
CROSS-REFERENCE TO RELATED APPLICATIONS 
   The present application claims the benefit of U.S. Provisional Application Ser. No. 60/627,208, filed on Nov. 12, 2004, the content of which is hereby incorporated by reference in its entirety. 

   BACKGROUND AND SUMMARY 
   The invention is generally directed to the area of verification for IC designs. In particular, some embodiments of the invention are related to an improved approach for implementing equivalence checking functionality in EDA verification tools. 
   Today&#39;s integrated circuits (ICs) typically contain large numbers of circuit elements. Computer-aided design (CAD) and computer-aided engineering (CAE) tools are essential in assisting circuit designers to produce these complicated ICs. Circuit designs are typically represented in a user-specified hardware description language (HDL), which demonstrate the behavioral properties of the circuit. 
   Designers commonly utilize CAE software, or synthesis, to translate the behavioral representation, for example, a Register-Transfer-Level (RTL) description, into an implementation representation, for example, a gate-level representation. The synthesizer chooses the implementation architecture based on parameters such as timing, footprint, and power consumption. The result of the synthesis process, the gate-level representation, is referred to as the revised circuit, while the behavioral property of the circuit, the RTL representation, is referred to as the golden circuit. The possibility of errors in creating an implementation architecture from a golden circuit is high as the process is complex. 
   With increasing design complexity, formal verification becomes integral in the design process to ensure that the revised circuit is equivalent to the original specification, or golden circuit. In the verification of digital circuits, signals in the circuits are “compared” in some manner in order to draw a conclusion on the “correctness” of one or more properties of the circuits. For example, to determine if two circuits with identical state encoding will behave identically under some excitations, the simulated values of the corresponding state-points in the two circuits are compared when the circuits are subjected to the same excitations. 
   Alternatively, to show that the two circuits will behave identically under all possible excitations, a formal methodology is used wherein the functions of the corresponding state-points in the two circuits are proved to be functionally equivalent. This method is known as formal equivalence checking and it is in the category of verification methods known as formal verification: 
   More specifically, during equivalence checking, an implementation architecture is created for the golden circuit and is compared to a possibly synthesized revised implementation circuit to determine if they are equivalent. However, the implementation architecture in the golden circuit is not limited by considerations of power consumption, footprint, or timing, and thus, can, and often does, choose a different architecture. The likelihood of different architectures being chosen increases when datapath components are used. 
   Datapath components are sub-circuits which implement arithmetic operations like multiplication, addition, squaring, shifting and division. Typically these components operate on more than one bit of data at a time. Other examples include the adder tree or partial product generator in the multiplier. 
   There are a great number of ways to implement a datapath component while maintaining the same functionality. There are well defined methods of implementing the datapath component at bit level to achieve specific goals like power, timing, area, placement etc. Such methods generate architectures of the datapath component. Common examples of architectures for a multiplier summation tree include ripple carry, carry save and Wallace tree. Similar architectures exist for adder, subtractors, dividers, shifters. 
   As such, when a datapath component exists in the golden design, the revised design may have very different architecture than the implementation version of the golden design created during equivalence checking. If the architecture generated for golden design is dramatically different from the revised architecture, then excessive system resources/runtime may be needed to perform equivalence checking of the two designs. If the architecture generated from the RTL for equivalence checking is very close to the revised gate-level implementation, then system resources/runtime that is needed to perform equivalence checking of the two designs will be minimized. 
   A solution is needed for equivalence checking to automatically create an implementation architecture of an RTL model that is similar to the revised gate-level implementation as possible, without relying on any external auxiliary files which annotate the revised circuit information. 
   A method of subcircuit architecture selection and replacement is defined in the purpose to re-generate the golden circuit which is more similar in relation to the revised circuit. The method includes creating the candidates, evaluating the candidates, selecting the best candidate, and replacing the subcircuit with the selected candidate. 

   
     BRIEF DESCRIPTION OF THE DRAWINGS 
       FIG. 1  is a representation of process  100 , an overview of the subcircuit selection and replacement process. 
       FIG. 2  is an example of the subcircuit in the golden and revised circuit. 
       FIG. 3  is a representation of process  300 , the dynamic candidate creation process. 
       FIG. 4  is a representation of process  400 , the derived candidate creation process. 
       FIG. 5  is a representation of process  500 , the similarity evaluation and candidate refinement process. 
       FIG. 6  is a representation of process  600 , the candidate selection and replacement process. 
       FIG. 7  is a representation of system  1400 , a system where subcircuit selection and replacement can occur. 
   

   DETAILED DESCRIPTION OF INVENTION 
   According to some embodiments, the synthesis tool generates the revised circuit from the behavioral description of the circuit, or the RTL description, to achieve the logic optimization objectives. To verify that the revised circuit implements the same function as the RTL description, an equivalence checking tool generates a golden circuit by simply parsing the RTL description without logic optimizations. The outputs of golden and revised circuit are compared by the equivalence checking tool. Due to the complexity of circuit designs and the numerous methods for logic optimization, the revised circuit can be structured differently from the golden circuit. The greater the dissimilarity between the golden and revised circuit, the greater the consumption of resources during equivalence checking. This disclosure provides a method to ensure the similarity between the golden and revised circuits to minimize the required resources. 
   In one embodiment shown in  FIG. 2 , the RTL description contains several datapath components including a multiplier. The equivalence checking tool generates the golden circuit with clear boundary for each datapath component. The subcircuit of datapath component can be easily extracted in the golden circuit. On the other hand, the synthesis tool generates the revised circuit with logic optimizations. The synthesis tool chooses one of many different ways to implement the datapath subcircuit and may also merge the subcircuit boundary with other surrounding logics. Thus the corresponding datapath components can be indistinguishably embedded in the revised netlist without identifiable inputs and outputs boundaries. To generate a golden circuit that is more similar as the revised circuit for equivalence checking, multiple candidates of a subcircuit are generated and connected into the golden circuit. Each candidate is a subcircuit implementing the same function with a different structure. The candidate which serves best for equivalence checking is selected and replaced in the golden circuit. 
   An embodiment of the subcircuit selection and replacement process, overview process  100 , is shown in  FIG. 1 . One or more candidates are created in process action  102 . The set of candidates are evaluated in process action  104 . One candidate is selected in process action  106 . The selected candidate replaces a subcircuit in the golden circuit in process action  108 . Each of these actions is described in further detail below. 
   In one embodiment, there are two types of candidates, static candidates and dynamic candidates. Static candidates come from a limited set of pre-defined implementations in the static templates. The static templates include commonly used architectures in the modern VLSI design (for example, as described in Behrooz. Parhami, “Computer Arithmetic: Algorithms and Hardware Designs,” Oxford University Press, which is hereby incorporated by reference in its entirety). For example of the multiplier operator, it can be implemented with different architectures in bit-level, such as Booth or non-Booth encoder for partial product generator, ripple-carry adder or carry-save adder for summation tree. A multiplier can also be implemented with different architectures in word-level. For example, a multiplier in FPGA device can be implemented by adding the result of several smaller fixed-size multipliers, as described in Jean-Luc Beuchat and Arnaud Tisserand, “Proceeding of 12 th  International Conference on Field-Programmable Logic and Applications”, pp. 513-522, September, 2002, which is hereby incorporated by reference in its entirety. A signed multiplier can be implemented by using an unsigned multiplier with the circuitry for sign bit extension. Due to the commutative property, a multiplier can be implemented differently by swapping the input operands. The static templates are generated from various pre-defined algorithms for datapath components. The static candidate generation is independent from the implementation of the revised circuit. The static candidates can be as many as possible to match the architecture of the datapath component implemented in the revised circuit. 
   Dynamic candidates come from dynamic templates. A dynamic template is a template that is not available as part of a pre-defined implementation, but is created via a re-structure learning process. Dynamic templates can be created if the available static templates are not similar to the revised implementation. The dynamic template creation process, process  300 , is shown in  FIG. 3 . Process action  302  reads in the golden netlist and the revised netlist. Process action  304  determines the boundaries of subcircuits in the two netlists. If the boundary of a subcircuit in the revised circuit can be found, process action  306  invokes learning of the subcircuit. From this learning process, dynamic templates are created in process action  308 . Further information regarding the dynamic template creation process can be found in related U.S. Pat. No. 6,742,174, which is incorporated by reference in its entirety as if fully set forth herein. 
   The dynamic template created for one subcircuit can be used to generate a candidate for another subcircuit if they are the same datapath components. In one embodiment, the dynamic template for one subcircuit is duplicated as the candidate for another subcircuit. 
   The dynamic template can also be derived from an existing candidate. An embodiment of a process  400  for the creation of derived candidates is shown in  FIG. 4 . The non-similar portion of the candidate is identified in process action  402 . The non-similar portions of the candidate are modified in process action  404 . These modifications preserve the behavioral functionality, while creating additional candidate architectures. In different embodiments, the modification is applied based on the different optimization objectives. It includes the timing based synthesis, area based synthesis and low power based synthesis. For example, for the adder tree subcircuit, the order of full adders is permutated to change the structure of the subcircuit while keeping its output function unchanged. Each synthesis technique yields a different derived candidate. In another embodiment, these candidates that only differ from each other by a small amount, are referred to as clusters, or derived clusters. The resulting collection of derived candidates, or the cluster of derived candidates, is inserted in process action  406 . 
   It is noted there does not need to be order dependency between the creation of static templates and dynamic templates. One could create static templates followed by dynamic templates, or vice versa. In some embodiments, one could use either static templates or dynamic templates, e.g., if one is not available. 
   The group of static and dynamic candidates is evaluated to find the one which is most similar to the revised architecture in process  500 , shown in  FIG. 5 . The set of candidates is obtained in process action  502 . Process action  504  computes the local similarity of each candidate subcircuit in relation to the revised circuit. 
   Generally, the similarity degree for a candidate subcircuit in relation to the revised circuit should reflect the complexity of comparison in equivalence checking if this subcircuit is selected and replaced in the golden circuit. As shown in  FIG. 2 , in one embodiment, to compute similarity, the subcircuit boundary is known in the golden circuit and the created candidates are all connected with the input boundary. 
   To determine the similarity degree for a candidate, boolean simulation is applied to the entire golden and revised circuits based on the same primary input assignments. For each simulation run, if a wire in a revised circuit repeatedly has the equivalence or inverted-equivalence simulation result as a wire in the golden circuit, the wire in the golden netlist is noted as a potential equivalence point. The potential equivalence points can be used to calculate the similarity degree. 
   The similarity degree for a candidate in relation to the revised netlist can be measured by several factors. The ratio of potential equivalence points over all the wires in a candidate subcircuit is one factor to determine the similarity degree. 
   Another factor of similarity degree is the distribution of potential equivalence points in the candidate. If the percentage of potential equivalence points in the candidates cannot distinguish one candidate from the rest, the distribution is another deciding criterion to select the one which is expected to be easier to compare with the revised circuit. In one embodiment, the candidate whose potential equivalence points are evenly distributed in the subcircuit will be chosen. Consider another candidate that has the same percentage of potential equivalence points but the equivalence points are mainly congested in a region of the subcircuit, it is usually more difficult to compare with the revised circuit. 
   To consider the distribution of potential equivalence points in the similarity evaluation, each potential equivalence point i has a value L(i) to represent its distance to the nearest potential equivalence points in its fan-in logic cones. As shown in  FIG. 2 , L(i) is the total number of gates in the logic cones when traversing the fan-in gates from the potential equivalence point i until it reaches another potential equivalence points. The potential equivalence points also include all the outputs of candidate subcircuit. The similarity criterion is generated by normalizing the L(i) for all the potential equivalence points in the candidate subcircuit 
             (       [       ∑     i   =   0       m   -   1       ⁢         (     L   ⁡     (   i   )       )     N     m       ]       1   N       )     ,         
where m is the total number of potential equivalence points in the candidate subcircuit and N is the normalization parameter. In one embodiment, N is set to 2 and the normalization becomes root-mean-square. For the normalized result, a larger number indicates a lower similarity degree in comparison because in average it represents that the potential equivalence point is located in a longer distance from the others in the candidate sub circuit.
 
   The third factor of similarity degree focuses on particular potential equivalence points such as the outputs of full adders in the candidate subcircuit. These points are more heavily weighted during the calculation of similarity degree because they usually serve as good cutpoints in comparison. Based on these cutpoints, the structural hashing in the golden and revised circuit can be applied to analyze the circuit structural similarity as the fourth factor. 
   The calculated similarity degree has several features. First, it is a combination of several factors to predict the comparison performance as accurately as possible. Second, it focuses on each individual subcircuit instead of the whole circuit, which makes the similarity degree more sensitive to the minor changes in the local region. Third, the calculation does not require all the wires in the boundary of a golden subcircuit to have potential equivalence points in the revised circuit. Therefore, the corresponding component can be seamlessly embedded in the revised circuit without the need to locate its boundaries. This makes the process of similarity evaluation more robust. 
   In process  500 , process action  506  decides whether further evaluation of similarity degree is required. Each iteration of evaluation improves the accuracy of the similarity calculation. For example, more boolean simulation runs are invoked to get more accurate potential equivalence points for each candidate, or other factors such as distribution of potential equivalence points are considered in the similarity calculation. The evaluation process can be repeated many times to obtain an accurate result. If further evaluation is required, process  506  flows to process action  504 . In one embodiment, this decision can be based on the number of candidates which show good local similarity. If there are multiple candidates in the set which show good similarity, further evaluation is needed to determine which one of these is a better replacement. In some embodiments, a maximum limit on the number of iterations is used to ensure convergence of this process. If it is determined that no further evaluation is required, process  506  flows to process action  508 . 
   In process action  508 , a decision is made whether a satisfactory candidate has been found for replacement or if more candidates need to be created in the process for evaluation. In one embodiment this decision can be made on the basis of the similarity degree number. If at least one candidate has a similarity number above a fixed threshold, it is accepted as a satisfactory finalized candidate. If one or more satisfactory candidates are found, process action  508  flows to process action  510  where the set of candidates is finalized, else it flows to process action  512 . A maximum limit of iterations is enforced in process action  508  to ensure convergence. 
   In process action  512 , certain candidates are pruned from the set. In some embodiments, the candidates in the set that have similarity degree number below a threshold value are pruned from the set. Process action  512  flows to process action  514  which creates and inserts additional candidates. Process  514  returns to process action  504  to compute the similarity degree of the current set of candidates. Some of the candidates in the current set may be the candidates from previous iterations. In one embodiment, the computing, pruning, and inserting steps are repeated many times to provide accurate similarity calculations and generate candidates with greater similarity. 
   In process  512 , there is a number of methods that can be used for pruning candidates. In some embodiments, a threshold parameter is set. If a candidate does not meet the absolute similarity threshold, it is pruned. In another embodiment, a relative similarity threshold is used for pruning criteria. In another embodiment, the evaluation will test just one candidate from a cluster. If the similarity is high, the entire cluster can be kept. However, if the similarity is low, the entire cluster can be pruned. In process action  514 , it uses the knowledge (i.e., similarity calculations) gained from process action  504  to guide the insertion of the derived candidates which are likely to be more similar. Multiple iterations of repeatedly modifying the non-similar portions of a candidate lead to convergence of process with increasingly similar candidates. 
   An embodiment of process  600 , the selection and replacement process, is shown in  FIG. 6 . The finalized set of evaluated candidates is obtained in process action  602 . One of the candidates with the highest similarity degree is chosen in process action  604 . The percentage of the potential equivalence points as well as other factors such as the distribution of potential equivalence points can be used as the criteria to evaluate the similarity degree. In process action  606 , the selected candidate is used to replace the subcircuit of the component in the golden circuit, the other candidates are disconnected from the netlist. Equivalence checking is performed on the golden and revised circuit. 
   SYSTEM ARCHITECTURE OVERVIEW 
   The execution of the sequences of instructions required to practice the embodiments may be performed by a computer system  1400  as shown in  FIG. 7 . In an embodiment, execution of the sequences of instructions required to enact the embodiments is performed by a single computer system  1400 . According to other embodiments, two or more computer systems  1400  coupled by a communication link  1415  may perform the sequence of instructions in coordination with one another. A description of only one computer system  1400  is presented below; however, it should be understood that any number of computer systems  1400  may be employed to enact the embodiments. 
   A computer system  1400  according to an embodiment will now be described with reference to  FIG. 7 , which is a block diagram of the functional components of a computer system  1400 . As used herein, the term computer system  1400  is broadly used to describe any computing device that can store and independently run one or more programs. 
   Each computer system  1400  may include a communication interface  1414  coupled to the bus  1406 . The communication interface  1414  provides two-way communication between computer systems  1400 . The communication interface  1414  of a respective computer system  1400  transmits and receives electrical, electromagnetic or optical signals, that include data streams representing various types of signal information, e.g., instructions, messages and data. A communication link  1415  links one computer system  1400  with another computer system  1400 . For example, the communication link  1415  may be a LAN, in which case the communication interface  1414  may be a LAN card, or the communication link  1415  may be a PSTN, in which case the communication interface  1414  may be an integrated services digital network (ISDN) card or a modem, or the communication link  1415  may be the Internet, in which case the communications interface  1414  may be a analog, digital or wireless modem, or a network or Ethernet card. 
   A computer system  1400  may transmit and receive messages, data, and instructions, including program, i.e., application, code, through its respective communication link  1415  and communication interface  1414 . Received program code may be executed by the respective processor(s)  1407  as it is received, and/or stored in the storage device  1410 , or other associated non-volatile media, for later execution. 
   In an embodiment, the computer system  1400  operates in conjunction with a data storage system  1431 , e.g., a data storage system  1431  that contains a database  1432  that is readily accessible by the computer system  1400 . The computer system  1400  communicates with the data storage system  1431  through a data interface  1433 . A data interface  1433 , which is coupled to the bus  1406 , transmits and receives electrical, electromagnetic or optical signals, that include data streams representing various types of signal information, e.g., instructions, messages and data. In embodiments, the functions of the data interface  1433  may be performed by the communication interface  1414 . 
   Computer system  1400  includes a bus  1406  or other communication mechanism for communicating instructions, messages and data, collectively, information, and one or more processors  1407  coupled with the bus  1406  for processing information. Computer system  1400  also includes a main memory  1408 , such as a random access memory (RAM) or other dynamic storage device, coupled to the bus  1406  for storing dynamic data and instructions to be executed by the processor(s)  1407 . The main memory  1408  also may be used for storing temporary data, i.e., variables, or other intermediate information during execution of instructions by the processor(s)  1407 . 
   The computer system  1400  may further include a read only memory (ROM)  1409  or other static storage device coupled to the bus  1406  for storing static data and instructions for the processor(s)  1407 . A storage device  1410 , such as a magnetic disk or optical disk, may also be provided and coupled to the bus  1406  for storing data and instructions for the processor(s)  1407 . 
   A computer system  1400  may be coupled via the bus  1406  to a display device  1411 , such as, but not limited to, a cathode ray tube (CRT), for displaying information to a user. An input device  1412 , e.g., alphanumeric and other keys, is coupled to the bus  1406  for communicating information and command selections to the processor(s)  1407 . 
   According to one embodiment, an individual computer system  1400  performs specific operations by their respective processor(s)  1407  executing one or more sequences of one or more instructions contained in the main memory  1408 . Such instructions may be read into the main memory  1408  from another computer-usable medium, such as the ROM  1409  or the storage device  1410 . Execution of the sequences of instructions contained in the main memory  1408  causes the processor(s)  1407  to perform the processes described herein. In alternative embodiments, hard-wired circuitry may be used in place of or in combination with software instructions to implement the invention. Thus, embodiments are not limited to any specific combination of hardware circuitry and/or software. 
   The term “computer-usable medium,” as used herein, refers to any medium that provides information or is usable by the processor(s)  1407 . Such a medium may take many forms, including, but not limited to, non-volatile, volatile and transmission media. Non-volatile media, i.e., media that can retain information in the absence of power, includes the ROM  1409 , CD ROM, magnetic tape, and magnetic discs. Volatile media, i.e., media that can not retain information in the absence of power, includes the main memory  1408 . Transmission media includes coaxial cables, copper wire and fiber optics, including the wires that comprise the bus  1406 . Transmission media can also take the form of carrier waves; i.e., electromagnetic waves that can be modulated, as in frequency, amplitude or phase, to transmit information signals. Additionally, transmission media can take the form of acoustic or light waves, such as those generated during radio wave and infrared data communications. 
   In the foregoing specification, the embodiments have been described with reference to specific elements thereof. It will, however, be evident that various modifications and changes may be made thereto without departing from the broader spirit and scope. For example, the reader is to understand that the specific ordering and combination of process actions shown in the process flow diagrams described herein is merely illustrative, and the invention can be performed using different or additional process actions, or a different combination or ordering of process actions. The specification and drawings are, accordingly, to be regarded in an illustrative rather than restrictive sense.