Functional verification of power gated designs by compositional reasoning

A novel and useful method of functional verification of power gated designs by compositional reasoning. The method of the present invention performs a sequential equivalence check between the power gated design and a version of itself in which power gating is disabled. A compositional approach is first used to look for conditional equivalence of each functional block of the circuit (and its corresponding functional block with power gating disabled) under a suitable set of assumptions, guaranteed by the neighboring functional blocks. Circular reasoning rules are then employed to compose the conditional equivalences proved on the individual functional blocks back into total equivalence on the whole circuit.

FIELD OF THE INVENTION

The present invention relates to the field of integrated circuit design tools and more particularly relates to a method of verifying power gated circuit designs via sequential and compositional conditional equivalency.

SUMMARY OF THE INVENTION

There is thus provided in accordance with the invention, a method of verifying a circuit comprising a power gated design, the method comprising the steps of creating a version of said circuit, wherein power gating is disabled, defining one or more valid inputs for said circuit comprising a power gated design, performing a sequential equivalence check between said circuit comprising a power gated design and said version comprising a non power gated design utilizing said one or more valid inputs and comparing the outputs of said circuit comprising a power gated design and said circuit wherein power gating is disabled.

There is also provided in accordance of the invention, a method of verifying a circuit comprising a power gated design, the method comprising the steps of partitioning said circuit into a plurality of original functional blocks, wherein power gating is enabled in each said original functional block, creating a corresponding functional block for each original functional block, wherein said corresponding functional block comprises said original functional block in which power gating is disabled, defining one or more valid inputs for each said original functional block, defining one or more valid conditions for each original functional block and its associated corresponding functional block, performing a conditional equivalence check between each said original functional block and each said corresponding functional block utilizing said one or more valid inputs and said one or more valid conditions, thereby determining conditional equivalency and composing said conditional equivalencies to define a compositional conditional equivalency.

There is further provided a computer program product for verifying a circuit comprising a power gated design, the computer program product comprising a computer usable medium having computer usable code embodied therewith, the computer program product comprising computer usable code configured for creating a version of said circuit, wherein power gating is disabled, computer usable code configured for defining one or more valid inputs for said circuit comprising a power gated design, computer usable code configured for performing a sequential equivalence check between said circuit comprising a power gated design and said version comprising a non power gated design utilizing said one or more valid inputs and computer usable code configured for comparing the outputs of said circuit comprising a power gated design and said circuit wherein power gating is disabled.

There is also provided a computer program product for verifying a circuit comprising a power gated design, the computer program product comprising a computer usable medium having computer usable code embodied therewith, the computer program product comprising computer usable code configured for partitioning said circuit into a plurality of original functional blocks, wherein power gating is enabled in each said original functional block, computer usable code configured for creating a corresponding functional block for each original functional block, wherein said corresponding functional block comprises said original functional block in which power gating is disabled, computer usable code configured for defining one or more valid inputs for each said original functional block, computer usable code configured for defining one or more valid conditions for each original functional block and its associated corresponding functional block, computer usable code configured for performing a conditional equivalence check between each said original functional block and each said corresponding functional block utilizing said one or more valid inputs and said one or more valid conditions, thereby determining conditional equivalency and computer usable code configured for composing said conditional equivalencies to define a compositional conditional equivalency.

DETAILED DESCRIPTION OF THE INVENTION

Notation Used Throughout

The following notation is used throughout this document:

Detailed Description of the Invention

The present invention is a method of performing a sequential equivalence check between the power gated design and a version of itself in which power gating is disabled. A compositional approach is first used to look for conditional equivalence of each functional block of the circuit (and its corresponding functional block with power gating disabled) under a suitable set of assumptions, guaranteed by neighboring functional blocks. Circular reasoning rules are then employed to compose the conditional equivalences proved on the individual functional blocks back into total equivalence on the whole circuit.

The method of present invention employs a methodology that addresses functional verification of a circuit design implementing power gating, where the verification task is segmented into two steps. First, correct functionality of the design is checked when power gating is disabled, using the usual techniques (formal and/or dynamic). Second, a sequential equivalence check is performed between a version of the design with power gating enabled and one with it disabled.

Due to the increasing complexity of power gated circuit designs, the circuit is partitioned into functional blocks and a sequential equivalence check is performed on each block. Conditions are identified where the interface between a power gated functional block and its neighbors (i.e. functional blocks) is “active”, and therefore preserving power gating unit functionality at that point. The next step is to prove that the neighboring functional blocks are not affected by a difference in behavior when the interface is not active. Finally, after establishing conditional equivalence of each functional block, circular reasoning rules enable composition of the functional blocks and their respective conditional equivalences into a total equivalence for the entire circuit.

A block diagram illustrating an example computer processing system adapted to implement the functional verification of power gated design method of the present invention is shown inFIG. 1. The computer system, generally referenced10, comprises a processor12which may comprise a digital signal processor (DSP), central processing unit (CPU), microcontroller, microprocessor, microcomputer, ASIC or FPGA core. The system also comprises static read only memory18and dynamic main memory20all in communication with the processor. The processor is also in communication, via bus14, with a number of peripheral devices that are also included in the computer system. Peripheral devices coupled to the bus include a display device24(e.g., monitor), alpha-numeric input device25(e.g., keyboard) and pointing device26(e.g., mouse, tablet, etc.)

The computer system is connected to one or more external networks such as a LAN or WAN23via communication lines connected to the system via data I/O communications interface22(e.g., network interface card or NIC). The network adapters22coupled to the system enable the data processing system to become coupled to other data processing systems or remote printers or storage devices through intervening private or public networks. Modems, cable modem and Ethernet cards are just a few of the currently available types of network adapters. The system also comprises magnetic or semiconductor based storage device52for storing application programs and data. The system comprises computer readable storage medium that may include any suitable memory means, including but not limited to, magnetic storage, optical storage, semiconductor volatile or non-volatile memory, biological memory devices, or any other memory storage device.

Software adapted to implement the functional verification of power gated design method of the present invention is adapted to reside on a computer readable medium, such as a magnetic disk within a disk drive unit. Alternatively, the computer readable medium may comprise a floppy disk, removable hard disk, Flash memory16, EEROM based memory, bubble memory storage, ROM storage, distribution media, intermediate storage media, execution memory of a computer, and any other medium or device capable of storing for later reading by a computer a computer program implementing the method of this invention. The software adapted to implement the functional verification of power gated design method of the present invention may also reside, in whole or in part, in the static or dynamic main memories or in firmware within the processor of the computer system (i.e. within microcontroller, microprocessor or microcomputer internal memory).

Other digital computer system configurations can also be employed to implement the complex event processing system rule generation mechanism of the present invention, and to the extent that a particular system configuration is capable of implementing the system and methods of this invention, it is equivalent to the representative digital computer system ofFIG. 1and within the spirit and scope of this invention.

Once they are programmed to perform particular functions pursuant to instructions from program software that implements the system and methods of this invention, such digital computer systems in effect become special purpose computers particular to the method of this invention. The techniques necessary for this are well-known to those skilled in the art of computer systems.

It is noted that computer programs implementing the system and methods of this invention will commonly be distributed to users on a distribution medium such as floppy disk or CD-ROM or may be downloaded over a network such as the Internet using FTP, HTTP, or other suitable protocols. From there, they will often be copied to a hard disk or a similar intermediate storage medium. When the programs are to be run, they will be loaded either from their distribution medium or their intermediate storage medium into the execution memory of the computer, configuring the computer to act in accordance with the method of this invention. All these operations are well-known to those skilled in the art of computer systems.

Functional Verification of Power Gated Designs

In a first embodiment of the present invention, a corresponding version of the power gated circuit is created with power gating disabled. A sequential equivalence check is performed for the power gated circuit and its corresponding version with power gating disabled using known valid inputs.

In a second embodiment of the present invention, the power gated circuit is partitioned into functional blocks B1. . . Bn(i.e. power gating enabled in each Bi). Corresponding functional blocks B′1. . . B′nare then defined where power gating functionality is disabled in each B′i. A sequential equivalence check is then performed for each Biand its corresponding B′i. A compositional approach is first used to look for conditional equivalence of each functional block of the circuit under a suitable set of assumptions, guaranteed by the neighboring functional blocks. Circular reasoning rules are then employed to compose the conditional equivalences proved on the individual functional blocks back into total equivalence on the whole circuit.

Note that there are instances where the power gated circuit to be verified comprises both functional blocks that are power gated and functional blocks that are not power gated. In this instance, the effects of power gating may be evident even in the non-power gated blocks by virtue of the inputs passed to them by the power gated blocks. For reasons of explication only, B (comprising the blocks B1. . . Bn) is divided into two groups, G and U. Group G consists of the power management unit, all power gated units and all non-power gated units in which the effects of power gating are evident and group U consists of all other blocks.

An example partitioning step of the present invention for this type of circuit is shown inFIG. 2. The block diagram, generally referenced30, comprises section G32, consisting of functional blocks which are all power gated and section U34, consisting of functional blocks in the circuit not implementing power gating logic. Section G is further comprised of power manager (PM)36and functional blocks G138, G240through Gm42. Section U is further comprised of functional blocks U144through Un46.

Note that G has no interface other than with U. That is, if G receives inputs directly from the chip interface or drives outputs directly to it, we assume for simplicity that they are buffered (with possibly zero delay) through U.

The method of the present invention is to show that the design G∥U is equivalent to the design G′∥U′, where the only difference between the primed and unprimed versions is that pg_enable=1 in G∥U whereas pg_enable=0 in G′∥U′. This shows that power gating does not affect the functionality of the design as a whole.

The goal of the method of the present invention is to show that G∥U is equivalent to G′∥U′. Due to size problems (i.e. of the circuit) this is performed compositionally, by comparing each Gi with G′i and each Ui with U′i. For simplicity of the explication, the problem is first broken down to comparing G with G′ and U with U′, and only afterwards how to break the problem down further.

When G is powered off, its outputs are not necessarily equivalent to those of G′, therefore precluding full equivalence. Although U and U′ will surely behave the same if they receive the same inputs (because there is no difference between them), in the method of the present invention, U will get its inputs from G and U′ from G′, thus showing equivalence between them is not trivial. Furthermore, care must be taken when comparing G with G′. If the inputs of the power management unit power manager “misbehave”, it might shut off some Gi at an inappropriate time, for example, when it is in the middle of processing a transaction. Therefore some minimal guaranteed assumptions are needed for the inputs that influence the power manager.

In order to ensure guaranteed assumptions, a simple observer (i.e. a piece of code) is supplied that monitors the interface between G and U and outputs flags that indicate properties of the interface. Each flag is used as an assumption by one of G∥G′ or U∥U′ and is guaranteed by the other, and the apparent circularity is broken by induction over time.

An example of using an observer with functional blocks to implement the method of the present invention is shown inFIG. 3. The block diagram, generally referenced50, comprises observers56,58and functional blocks52,5460and62. Observer Obs56is associated with functional blocks G52and U60. Observer Obs'58is associated with functional blocks G′54and62U′.

The setup of the methodology of the present invention is as shown in block diagram50(where the flags are signals partitioned into sets GoodU, GoodG and V) is as follows:GoodU: Each flag in this set has the value “1” as long as some assumption about the behavior of U is preserved. These assumptions do not specify the exact correct behavior of U on this interface, only the minimal needed restrictions. As soon as a violation of these assumptions is detected the flag goes to “0” and stays so forever.GoodG: This set is similar to GoodU, but over G.V: Conceptually, this set contains a single flag v, which is a “valid” signal that indicates whether the interface between G and U is active. When v=1 the outputs of G and G′ are expected to be equivalent, and when v=0 that are not expected to be equivalent. For example, v could be readytransmitting, where ready is an output of U signifying that U is ready to receive data and transmitting is an output of G signifying that G has data ready on the bus. In fact, V is not a single flag but a set of flags, because each Ui may have its own interface with each Gj, and even across a single interface not all signals necessarily follow the same protocol.

The sets GoodU and GoodG are typically initialized as empty sets, with constraints gradually added to refine them as needed. In the general case of assume-guarantee reasoning for functional correctness, this refinement process is complex since it requires a semantic understanding of how the design is intended to work. In the simplified setting described supra, these conditions will typically be simple translations from the English specification of the interface (e.g., “there are no requests during reset”). Moreover, assumptions weaker than those necessary to check functional correctness are used, since it is acceptable for the designs misbehave as long as the two copies (mis)behave in exactly the same way.

Note that it is possible to code a correct design in which the interface between G and U is always active (despite the fact that G can be powered down), and that this does not break the methodology. In such a case the fences and the state retention logic of G will be such that the valid signal has the constant value “1”, and the equivalence between U and U′ is trivial.

An example of a power gated circuit partitioned into functional blocks is shown inFIG. 4. The block diagram, generally referenced70comprises power gated functional block G72, non power gated functional block U74, shifter76, input ports78,80,82,84and output ports86,88,90,92. Functional; block G is further comprised of power manager94and adder96. Functional block U is further comprised of dispatch unit98, registers100and arbiter102.

In the circuit, commands are injected into the unit through the four input ports, and are held in the dispatch queue until they are sent by the dispatch unit to either the adder or the shifter, depending on their type. The results pass to an arbiter, which distributes them to the four output ports. The adder is responsible for all add/subtract and branch commands, while the shifter executes shift and load/store commands. In this implementation the functional block comprising the adder is power gated. The power manager receives commands from the dispatch unit to either turn the adder on or off (via power gating), depending on the instruction type being processed by the dispatch unit.

A flow diagram illustrating the power gated circuit verification via sequential equivalency method of the present invention is shown inFIG. 5. First, the power gated circuit to be verified is loaded (step110). A corresponding version of the circuit is created with power gating (step112). Reasonable valid inputs are then defined for the circuit (step114). A sequential check is then performed on the original and corresponding circuits using the defined inputs (step116). If the outputs from the two circuits are equivalent (step118) then the circuit passes verification (step122). Otherwise the circuit fails verification (step120). Finally the results are presented to the user (step124)

A flow diagram illustrating the power gated circuit verification via compositional conditional equivalency method of the present invention is shown inFIG. 6. First, the circuit to be verified is loaded (step130). The circuit is then partitioned into functional blocks, with power gating enabled in each functional block (step132). A corresponding version of each functional block is then created, with power gating disabled in each corresponding functional block (step134). Valid inputs are defined for each functional block (step136), where the inputs comprise either inputs to the loaded circuit or outputs from other functional blocks. For each functional block conditions (i.e. signals) are defined where the outputs from each pair of functional blocks (i.e. one with power gating enabled and one with power gating disabled) are expected to be equivalent (step138). Using the defined inputs and conditions, a conditional equivalence check is performed on each pair of functional blocks (step140). If the outputs from each pair of functional blocks (i.e. each conditional equivalence check) are equivalent (step142) then the loaded power gated circuit passes verification via compositional conditional equivalency (step146). Otherwise the loaded power gated circuit fails verification (step144). Finally, the results are presented to the user (step148).

Proving Sequential Equivalence

The approach described supra is based on the compositional reasoning rule presented by McMillan in K. L. McMillan, “Verification of an implementation of Tomasulo's algorithm by compositional model checking”, CAV '98, pp. 110-121, 1998, and borrows notation therefrom. Following McMillan, the notation is modified by using Q to denote the conjunction of all predicates in the set Q.

Let P be a set of predicates describing the design and let S be a set of predicates defining the specification. For each predicate sεS, let εs⊂P∪S be the environment of s. Intuitively, this is the set of predicates needed in order to show that s holds. We assume a well-founded orderon S that defines for each predicate s which other predicates will be assumed up to time i when proving s at time i (this is Zs), and which will be assumed only up to time i−1 (this isZs, the complement of Zs). Then by McMillan we can use Theorem 1 below:Theorem 1: Let P and S be sets of predicates, for each sεS, let εs⊂P∪S and letbe a well-founded order on S. Let Zs=P∪{s1εS:s1s}, and for a predicate p let p↑τstand fort≦Tp(t). Then, if for all sεS,
(εS∩ZS)↑τ(εS∩ZS)↑τ−1s(τ)  (1)is valid, then (∀t.P(t))∀t.S(t) is valid.

The goal is to use Theorem 1 to prove sequential equivalence between G∥U and G′∥U′. Since we have assumed that all outputs of G∥U are outputs of U it is sufficient to show that the predicate

EqU⁡(t)⁢=def⁢{o⁡(t)↔o′⁡(t)⁢:⁢⁢o⁢⁢is⁢⁢an⁢⁢output⁢⁢of⁢⁢U}(2)
holds at all times t. The following auxiliary sets of predicates are needed:

Let G, G′, U, U′, Ob and Ob′ be the sets of predicates describing the respective designs ofFIG. 3. Let Ĝ=G∪G′∪Ob∪Ob′ and Û=U∪U′∪Ob∪OB′. Let P=Ĝ∪Û S=PV∪PGoodU∪PGoodG∪EqU∪EqG.

To begin, it is assumed that the relationis empty, thus for every element s of S, we have Zs=P andZs=S. Therefore proving the following
Ĝ↑τ(EqU∪PGoodU)↑τ−1(EqG∪PGoodG∪PV)(τ)  (7)
Û↑τ(EqG∪PGoodG∪PV)↑τ−1(EqU∪PGoodU)(τ)  (8)
enables us to conclude that (∀t.P(t)∀t.S(t), and in particular that (∀t.P(t)∀t.EqU(t), which is the goal.

In practice, there will usually be some combinational paths from inputs to outputs in one or more of G, U and Ob, in which case we will need stronger assumptions for some of the proof obligations. That is, we will need s↑τas opposed to s↑τ−1for some element sεS used on the left-hand side of Obligation (1) or (2). Thus we will need to set an order, easily determined from the topology of the design, between the elements of S. As noted by McMillan cited supra, such an order is guaranteed to exist when there are no combinatorial loops in the design. Since a combinatorial loop is a basic structural design error, we are guaranteed the existence of a well-founded order. Using the well-founded order, each of the Obligations (1) and (2) will be split into a number of proof obligations, one for each predicate in the conjunction on the right hand side. For example, let one such predicate be s(t)=(υo→(o(t)o′(t)))εEqG, and let A={s′(t)|s′s and s′εEqU∪PGoodU} and B=(EqU∪PGoodU)\A. The corresponding proof obligation for s is then
(Ĝ∪A)↑τB↑τ−1(υo→(o(τ)o′(τ)))  (9)

Conceptually, it has been convenient up till now to view G and U as monolithic units. However, in reality each will typically consist of a number of smaller units, as shown inFIG. 2. Thus we would like to decompose the verification problem further by considering each Giand Uiseparately. For an output o of some Ui, we would like to use only Uirather than all of U on the left hand side of its proof obligation. To do so, we must add the following predicates to S:

The situation for a single Giis slightly more complicated: we must include the power management unit PM together with each Gi, and the predicates that we add for the outputs of Giwill be conditional, thus we might need to add some new valid signals. Denote the new valid signals by Vnew. Then we add the following additional predicates to S:

The orderis easily extended to the new predicates by a topological analysis of the design. For each output o of some Gior Ui, we verify its proof obligation using Ĝior Ûiin place of Ĝ or Û, where Ĝi=PM∥Gi∥Gi′ and Ûi=Ui∥Ui′.

Note that the theory supports multiply clocked designs as well as singly clocked ones. In the case of a singly clocked design, each time t is simply a tick of the clock. In the case of a multiply clocked design, each time t is a tick of the smallest granularity of time as seen by the verification tool (this is exactly the same as in model checking or equivalence checking of multiply clocked designs).

It is intended that the appended claims cover all such features and advantages of the invention that fall within the spirit and scope of the present invention. As numerous modifications and changes will readily occur to those skilled in the art, it is intended that the invention not be limited to the limited number of embodiments described herein. Accordingly, it will be appreciated that all suitable variations, modifications and equivalents may be resorted to, falling within the spirit and scope of the present invention.