Abstract:
A method for preparing an IC design that has been modified to be formally verified with a reference IC design. Because some formal verification tools cannot handle the complexity often associated with sequential equivalence checking at the top level of a circuit, the modified IC design may be instantiated into a number of different design versions, each having different levels of modification complexity. In addition, the reference IC design and the modified versions may be decomposed into a datapath and control path. The reference IC design and each of the modified IC design versions may also use wrappers to encapsulate various levels of hierarchy of the logic. Lastly, rather than having to verify each of the modified versions back to the reference IC design, the equivalence checking may be performed between each modified IC design version and a next modified IC design version having a greater modification computational complexity.

Description:
[0001]    This patent application claims the benefit of Provisional Patent Application Ser. No. 61/484,997, filed May 11, 2011, which is herein incorporated by reference in its entirety. This patent application is also a continuation-in-part of U.S. patent application Ser. No. 13/128,153, filed May 6, 2011, which is a National Stage application of International Patent Application No. PCT/US2009/062337, filed Oct. 28, 2009, which claims the benefit of U.S. Provisional Application Ser. No. 61/112,537, filed Nov. 7, 2008, each of which is herein incorporated by reference in its entirety. 
     
    
     BACKGROUND 
       [0002]    1. Technical Field 
         [0003]    This disclosure relates to integrated circuit (IC) design, and more particularly to formal verification of integrated circuit logic designs. 
         [0004]    2. Description of the Related Art 
         [0005]    In IC design, formal verification refers to a type of functional validation (verification) method that uses mathematical models of the circuits to prove a property of interest rather than relying upon simulations of individual test cases. An advantage of a formal verification is that it may be equivalent to doing an exhaustive simulation of every possible test case. Exhaustive simulation by itself is not practical for any but the most trivial of circuits because of the size of the state space. 
         [0006]    One type of formal verification is referred to as equivalence checking. Equivalence checking is used to verify that two circuits perform the same function, where one circuit is considered to be the reference model, and the other circuit is a design model. For two circuits to be the same, each must have the same number of primary inputs (PIs) and the same number of primary outputs (POs), and there must be some way to identify corresponding inputs/outputs. Many commercial combinatorial equivalence tools may require a complete correspondence between internal sequential elements (e.g., latches or flops) of the two designs. However, because it is often necessary to modify the boundaries of modules and/or change the signal timing on the inter-module boundaries, which may break the correspondence of circuits between sequential elements, this view of equivalence may be too restrictive. 
         [0007]    Accordingly, when the matching of sequential elements cannot be assumed, the equivalence checking is referred to as sequential equivalence checking. The sequential equivalence checking problem space may be much larger and harder than that of combinatorial equivalence checking, so application of any algorithms for proving sequential equivalence may fail due to computational complexity. If it were possible to run equivalence checking on the top-level design, nothing else would be necessary. However, because of issues with some sequential equivalence checking tools, it is often difficult to prove sequential equivalence without many iterations and trials. 
       SUMMARY OF THE EMBODIMENTS 
       [0008]    Various embodiments of a method for formally verifying a modified IC design are disclosed. Broadly speaking, a method for preparing an IC design that has been modified to be formally verified with a reference IC design is contemplated. Because many verification tools cannot handle the complexity often associated with sequential verification at the top level of a circuit, the modified IC design may be instantiated into a number of different design versions, each having different levels of modification complexity. In addition, the reference IC design and the modified versions may be decomposed into a datapath and control path. The reference IC design and each of the modified IC design versions may also use wrappers to encapsulate various levels of hierarchy of the logic. Lastly, rather than having to verify each of the modified versions back to the reference IC design, the sequential equivalence checking may be performed between each modified IC design version and a next modified IC design version having a greater modification computational complexity. 
         [0009]    In one embodiment, the method includes providing a reference IC design version including a reference logic block. The method may also include creating a plurality of modified IC design versions, each including a modified logic block that corresponds to the reference logic block. The modified logic block may also include one or more modifications relative to the reference logic block. The modifications may increase in computational complexity from one version to a next version. The method may also include decomposing the reference logic block and each of the modified logic blocks into a datapath logic and a control logic. The method may further include verifying sequential equivalence of logic between each modified IC design version and a next modified IC design version having a greater modification computational complexity, beginning with the reference IC design version and a modified IC design version having a least modification computational complexity. 
     
    
     
       BRIEF DESCRIPTION OF THE DRAWINGS 
         [0010]      FIG. 1  is a conceptual diagram depicting one embodiment of a process for preparing and formally verifying a modified integrated circuit (IC) design. 
           [0011]      FIG. 2  is a flow diagram describing a method for preparing and formally verifying a modified IC design. 
           [0012]      FIG. 3  is a block diagram of one embodiment of a system for implementing a tool for preparation and formal verification of a modified IC design. 
       
    
    
       [0013]    Specific embodiments are shown by way of example in the drawings and will herein be described in detail. It should be understood, however, that the drawings and detailed description are not intended to limit the claims to the particular embodiments disclosed, even where only a single embodiment is described with respect to a particular feature. On the contrary, the intention is to cover all modifications, equivalents and alternatives that would be apparent to a person skilled in the art having the benefit of this disclosure. Examples of features provided in the disclosure are intended to be illustrative rather than restrictive unless stated otherwise. 
         [0014]    As used throughout this application, the word “may” is used in a permissive sense (i.e., meaning having the potential to), rather than the mandatory sense (i.e., meaning must). Similarly, the words “include,” “including,” and “includes” mean including, but not limited to. 
         [0015]    Various units, circuits, or other components may be described as “configured to” perform a task or tasks. In such contexts, “configured to” is a broad recitation of structure generally meaning “having circuitry that” performs the task or tasks during operation. As such, the unit/circuit/component can be configured to perform the task even when the unit/circuit/component is not currently on. In general, the circuitry that forms the structure corresponding to “configured to” may include hardware circuits. Similarly, various units/circuits/components may be described as performing a task or tasks, for convenience in the description. Such descriptions should be interpreted as including the phrase “configured to.” Reciting a unit/circuit/component that is configured to perform one or more tasks is expressly intended not to invoke 35 U.S.C. §112, paragraph six, interpretation for that unit/circuit/component. 
         [0016]    The scope of the present disclosure includes any feature or combination of features disclosed herein (either explicitly or implicitly), or any generalization thereof, whether or not it mitigates any or all of the problems addressed herein. Accordingly, new claims may be formulated during prosecution of this application (or an application claiming priority thereto) to any such combination of features. In particular, with reference to the appended claims, features from dependent claims may be combined with those of the independent claims and features from respective independent claims may be combined in any appropriate manner and not merely in the specific combinations enumerated in the appended claims. 
       DETAILED DESCRIPTION 
       [0017]    As mentioned above, sequential equivalence checking of IC designs can be difficult when a modified design includes many modifications and logic edits and/or the state space is large. More particularly, the issue may be described in terms of computational complexity of the computational problem to be solved. In other words, the computational complexity refers to the level of difficulty of the problem being solved by a computer. A problem may be regarded as difficult if solving it requires many resources irrespective of what type of computational algorithm is used. For example, the computational complexity may be considered to increase as the amount of time and/or the amount of memory that is needed to solve the problem increases. In addition, in the issue at hand, the number of gates in the circuit may be a measure of complexity. 
         [0018]    In the following example, an original IC design includes a logic block (e.g., the barrel shifter  101  of  FIG. 1 ) that is replaced by another block of logic (e.g., the funnel shifter  109  of  FIG. 1 ). The issue is trying to formally verify that the resultant top-level design that includes the new funnel shifter logic is sequentially equivalent to the top-level design with the barrel shifter. However, the state space for that type of verification becomes intractable for sequential equivalence checking tools. Accordingly, the following discussion describes a way to break the modified design into pieces that can be handled by the tools, using wrapper logic to accommodate changes in connectivity of inputs and outputs at different hierarchies, and separating the datapath logic from the control path. In one embodiment, wrapper logic may be logic that encapsulates a particular group or portion of a logic. The wrapper logic may isolate that portion of the circuit from the rest of the circuit, and provide inputs and outputs that may be connected to the rest of the circuit. In addition, within a wrapper a new level of circuit hierarchy may be created. It is noted that although the exemplary circuit uses a barrel shifter and a funnel shifter, in other embodiments the method and process described below may be used for any type of circuit. 
         [0019]    Turning now to  FIG. 1 , a conceptual diagram depicting one embodiment of a process for preparing and formally verifying a modified integrated circuit (IC) design is shown. In block  10 , the original IC design includes other logic  100  and barrel shifter logic  101 . In one embodiment, other logic  100  may be representative of logic that surrounds the barrel shifter  101 . For example, the other logic  100  may be part of a processor and the barrel shifter logic  101  may be part of the arithmetic logic unit. In this example, the other logic  100  and the barrel shifter  101  may be a hardware definition language (HDL) representation of the circuit such as register transfer level (RTL), for example. As shown in block  20  of  FIG. 1 , the other logic block  100  is instantiated and a new level of hierarchy is created in the module  102 . This is depicted by the arrow number  1 . In one embodiment, the control and datapath of the barrel shifter are separated. Datapath logic associated with various shifter functions (e.g.  103 ) is encapsulated by the new module  102 , while the control external to that functionality is outside of the module  102  so that the output of the module  102  may be consumed correctly. 
         [0020]    Once the block  20  has been created, the changes made to the hierarchy can be formally verified against the original design, as indicated by arrow number  2  using a sequential equivalence tool. Thus, block  20  is checked against block  10 . After these two blocks are verified by the tool, the block  20  is modified to create block  30  where the barrel shifter datapath logic  103  is replaced by funnel shifter datapath logic  109  and additional funnel shifter control logic  107  that is used to convert barrel shifter control signals to funnel shifter control signals. Arrow  3  depicts such a transformation. As shown, block  30  includes a module  105  that is at the same level of hierarchy as module  102  of block  20  and includes the funnel shifter datapath logic  109  and additional funnel shifter control logic  107 . In one embodiment, there may be input/output constraints that may be required by certain functions (e.g., one or more reverse shifting functions) of the funnel shifter applied to module  105 . 
         [0021]    Once block  30  has been created, the changes can be formally verified against the design of block  20 , as indicated by arrow number  4  using a sequential equivalence tool. After these two blocks are verified by the tool, the block  30  is modified to create block  40 , as indicated by arrow  5 . 
         [0022]    In block  40 , the module  105  is replaced by a wrapper module  120 . As shown the wrapper module  120  encapsulates the funnel shifter datapath logic and the funnel shifter control logic. In addition, within the wrapper  120 , a new level of hierarchy is created in that an n-ary dynamic logic (NDL) behavioral model of the funnel shifter datapath is instantiated as a new module  131 . The control logic block  111  is outside of the module  131  and includes additional flip-flops. In one embodiment, the NDL behavioral model may be an HDL implementation such as Verilog or VHDL, for example. The NDL behavioral model also includes conversion logic to convert the signals coming into the funnel shifter datapath logic from standard binary signals to a 1-of-4 encoding. In addition, a number of flip-flops may be added to the control logic  111  at cycle boundaries to more accurately reflect equivalence of the NDL behavioral model with the actual NDL circuit on a cycle-by-cycle basis. 
         [0023]    Once the block  40  has been created, the changes can be formally verified against the design of block  30 , as indicated by arrow number  6  using a sequential equivalence tool. After these two blocks are verified by the tool, the block  40  is modified to create block  50 , as indicated by arrow  7 . 
         [0024]    In block  50 , the NDL behavioral model of the funnel shifter datapath module  131  is replaced with a new module  151  that includes an NDL representation, which is an actual logic representation of the circuit and is substantially identically functionally equivalent to the NDL behavioral. Thus, the wrapper  120  of block  50  includes the funnel shifter control logic  111 , and the new funnel shifter datapath NDL module  151 . In one embodiment, clock-gating logic may be placed in the logic. However, to simplify the verification, the clock enables may be tied (constrained), to keep all clock-gating disabled. 
         [0025]    Once block  50  has been created, the changes can be formally verified against the design of block  40 , as indicated by arrow number  8  using a sequential equivalence tool. In embodiments that include the clock-gating, as a next step the clock-gating may be enabled within the wrapper  120 , and the appropriate constraints applied to the wrapper  120 . For example, block  60  is created by transforming block  50  as shown by arrow  9  to apply the appropriate clock-gating enable signals to the wrapper  120 . An additional sequential equivalence check may be performed between the block  50  with clock-gating disabled, and block  60  with the clock-gating enabled and proper constraints applied. 
         [0026]    Accordingly, each new instantiation is only checked for equivalence with the previous version/iteration of the design, thereby reducing the complexity of the state space that the sequential equivalence tool must negotiate. In addition, because with each new hierarchy there may be inputs and outputs that may be different, the wrapper may be wired up to the new module to preserve the correct input and output relationships. 
         [0027]    Referring to  FIG. 2 , a flow diagram describing a method for preparing and formally verifying a modified IC design is shown. Beginning in block  300 , the original reference design block is instantiated. A new copy of the block is modified such that the datapath and control logic is separated, and the reference datapath logic block is encapsulated within a new level of hierarchy or module. The outputs of the new module are wired up and connected to the appropriate connections in the surrounding logic. The new modular reference block is verified against the original reference block using a sequential equivalence checking tool (block  305 ). 
         [0028]    If the tool verifies the equivalence, the new modular design is copied and modified. More particularly, the module in the new reference design is replaced with a new module that includes a new/modified logic block (block  310 ). For example, as shown in  FIG. 1 , the module  102  and the barrel shifter datapath logic  103  is replaced with the module  105 , which includes the funnel shifter datapath logic  109  and the funnel shifter control logic  107 . The new modular funnel shifter block is verified against the previous reference block using a sequential equivalence checking tool (block  315 ). 
         [0029]    If the tool verifies the equivalence, the new modular shifter design is copied and modified. More particularly, the module in the new shifter design that includes the shifter datapath and control logic is replaced with a new wrapper that encapsulates the shifter control logic and a new module that includes a behavioral model of the new shifter (block  320 ). For example, as shown in  FIG. 1 , the module  105  which includes the funnel shifter datapath logic  109  and the funnel shifter control logic  107  is replaced with a wrapper  120  which encapsulates a new funnel shifter control logic  111  and the module  131 , which includes the funnel shifter datapath logic behavioral model. The new wrapper funnel shifter block is verified against the previous modular funnel shifter block using a sequential equivalence checking tool (block  325 ). 
         [0030]    If the tool verifies the equivalence, the new wrapper shifter design is copied and modified. More particularly, the module that includes the shifter datapath behavioral model is replaced with a new module that that includes the actual NDL of the new shifter (block  330 ). For example, as shown in  FIG. 1 , the module  131  which includes the funnel shifter datapath NDL behavioral is replaced with a new module that includes the actual funnel shifter datapath logic NDL  151 . The new wrapper funnel shifter block with actual NDL is verified against the previous funnel shifter block with the NDL behavioral using a sequential equivalence checking tool (block  335 ). If the tool verifies the equivalence, the process is essentially complete. 
         [0031]    As described in the above embodiments, the logic block datapath and the control paths were separated to facilitate ease of the verification flow. Accordingly, this type of verification flow may be used on any type of logic that includes a datapath and control logic. For example, in addition to shifter logic, adders, multipliers, and the like may be verified using a flow like the flow described above. 
         [0032]    In one embodiment, the steps of the formal verification preparation and subsequent sequential equivalence checking may be performed manually on a computer by a user. In other embodiments however, one or more of the steps of the formal verification preparation and subsequent sequential equivalence checking may be performed in a more automated fashion. More particularly, some of the various steps may be performed on a computer by executing instructions that cause one or more electronic design automation (EDA) tools to run. For example, a script or other software routine may prepare files for execution, or make calls to cause a tool to run, and the like. In  FIG. 3 , one embodiment of a system that may be used to perform various ones of the above steps is shown. 
         [0033]    Turning to  FIG. 3 , a block diagram of one embodiment of a system for implementing a tool for preparation and formal verification of a modified IC design is shown. Computer system  300  includes a plurality of workstations designated  312 A through  312 C. The workstations are coupled together through a network  316  and to a plurality of storages designated  318 A through  318 C. In one embodiment, each of workstations  312 A- 312 C may be representative of any standalone computing platform that may include, for example, one or more processors, local system memory including any type of random access memory (RAM) device, monitor, input output (I/O) means such as a network connection, mouse, keyboard, monitor, and the like (many of which are not shown for simplicity). 
         [0034]    In one embodiment, storages  318 A- 318 C may be representative of any type of non-transitory computer readable storage device such as hard disk systems, optical media drives, tape drives, ram disk storage, and the like. As such, the program instructions comprising the design tools may be stored within any of storages  318 A- 318 C and loaded into the local system memory of any of the workstations during execution. As an example, as shown in  FIG. 3 , the compiler/synthesis tool  311  and the verification preparation tool  313  are shown stored within storage  318 A, while the netlist  315  is stored within storage  318 C. Further, the sequential equivalence checking tool  317  is stored within storage  318 B. Additionally, the program instructions may be stored on a portable/removable storage media. The program instructions may be executed directly from the removable media or transferred to the local system memory of a given workstation  312  or mass storages  318  for subsequent execution. As such, the portable storage media, the local system memory, and the mass storages may be referred to as non-transitory computer readable storage mediums. The program instructions may be executed by the one or more processors on a given workstation or they may be executed in a distributed fashion among the workstations, as desired. 
         [0035]    In one embodiment, the formal verification preparation tool  313  may be used to prepare an IC design for sequential equivalence checking by the sequential equivalence checking tool  317  as described above. In one embodiment, the formal verification preparation tool  313  may include program instructions written in any of a variety of programming languages or scripting languages, and which may be executable by a processor to perform the above tasks. More particularly, in one embodiment the formal verification preparation tool  313  may receive information that corresponds to the decomposition of the datapath and the control path, and the formal verification preparation tool  313  may encapsulate the datapath into a different module as described above. 
         [0036]    It is noted that although the computer system shown in  FIG. 3  is a networked computer system, it is contemplated that in other embodiments, each workstation may also include local mass storage. In such embodiments, the program instructions and the results of the design tools may be stored locally. Further, it is contemplated that the program instructions may be executed on a standalone computer such as a personal computer that includes local mass storage and a system memory. 
         [0037]    Although the embodiments above have been described in considerable detail, numerous variations and modifications will become apparent to those skilled in the art once the above disclosure is fully appreciated. It is intended that the following claims be interpreted to embrace all such variations and modifications.