A method of circuit verification in digital design

Field of the invention

0001The present invention relates to a method of circuit verification in digital design and in particular relates to a method of register transfer level property checking to enable the same.

Background to the invention

0002Today's electrical circuit designs frequently contain up to several million transistors and circuit designs need to be checked to ensure that circuits operate correctly. Formal methods for verification are becoming increasingly attractive since they confirm design behaviour without exhaustively simulating a design. Over the past years, bounded model checking and bounded property checking have increased in significance in electronic design automation (EDA). When checking large industrial circuits, long run times, ranging between hours and several days, are quite common. With designs continually increasing in size and complexity the test for correct behaviour becomes more important and a major economic issue, but at the same time becomes more complex, time consuming and expensive. Automated abstraction techniques have been developed to enhance capabilities of formal verification methods.

0003Abstraction techniques are used as a pre-process in high-level property checking of digital circuits. The majority of today's industrial hardware verification tools use bit-level decision procedures, like decision procedures for the Boolean satisfiability problem (SAT) or decision procedures based on binary decision diagrams (BDDs). In electronic design automation, SAT procedures have many direct applications, including test pattern generation, timing analysis, logic verification, functional testing, etc. SAT belongs to the class of NP-complete problems, with algorithmic solutions having exponential worst case complexity. This problem has been widely investigated and continues to be so because efficient SAT techniques can greatly affect the operation of many EDA tools. For example in VLSI CAD, SAT formulations start from an abstract circuit description, for which a required output value needs to be validated. The resulting formulation is then mapped on to an instance of SAT. Conjunctive Normal Form (CNF) formulae can be used and several versions of this procedure incorporate a chronological backtrack-determination: at each node in the search tree, an assignment is selected and a subsequent search procedure is controlled by iterative application of "unit clauses" and "pure literal rules". Non-chronological backtrack determinations are also known. An alternative to SAT are BDDs: a set of BDD's can be constructed representing output value constraints. The conjunction of all the constraints expressed as a Boolean product of the corresponding BDD (termed as a product BDD) represents the set of all satisfying solutions. Any element of the resulting constraint set gives a feasible SAT solution. However a major limitation of this approach is that there is a corresponding exponential increase in memory requirement for the operating system and in run times of the verification tools. The CNF-based SAT solvers can be directly applied to circuits, which are broken down into bit-level Boolean logic, by transforming the entire circuit into CNF formulae. However, since practical gate-level circuit descriptions can be quite large, dealing with substantially large CNF formulae results in unacceptable CPU run times. However, circuit designs are usually defined in terms of Register-Transfer-Level (RTL) specifications, for example, coded in hardware description languages (HDL's) like VHDL or Verilog. RTL specifications of digital circuits contain explicit structural information which is lost in bit-level descriptions. At the bit-level, for example in gate lists, all signals are of 1-bit width and all available functional units are Boolean gates. In contrast, with RTL, word-level data structures, for example bit-vectors and buses, as well as high-level operators, for example adders, multipliers and shifters, are still visible. Several approaches to formal circuit verification have been proposed which make use of such high level information.

0004D. Cyrluk et al present a word-level decision procedure for the core theory of bit-vectors with extraction and concatenation in "<nplcit id="ncit0001" npl-type="s"><text>An efficient decision procedure for the theory of fixed sized bit-vectors" (CAV-97), pages 60 to 71, 1997</text></nplcit>, using bit-vector BDDs and applying width abstraction to the core theory.

0005Document <patcit id="pcit0001" dnum="US5946481A"><text>US 5,946,481</text></patcit> describes a method and a device for forming a restricted model from a system model for formally verifying the system and design. The method of <patcit id="pcit0002" dnum="US59464811B"><text>US 5,946,481 1</text></patcit> its based on eliminating system model variables and system model inputs that are not used for a function of the system model state. In this case, a restricted model is a system model which is restricted to certain state transitions, limited by restricting the variables of the system model.

0006Document <patcit id="pcit0003" dnum="US5465216A"><text>US 5,465,216</text></patcit> discloses a method and an apparatus for formal verification. A state transition system with corresponding specifications is reduced and subsequently verified by formal verification such as simple model verification. <patcit id="pcit0004" dnum="US5465216A"><text>US 5,465,216</text></patcit> describes the parameterization of values within the full model for reducing the number of states and thereby the model of the circuit. Subsequently, an HDL description may be generated.

0007Document <patcit id="pcit0005" dnum="US5926622A"><text>US 5,926,622</text></patcit> discloses a method and an apparatus for verifying the behaviour of properties or functions of a system for running a simulation on a reduced model for verifying the behaviour of properties of the system. The concept of <patcit id="pcit0006" dnum="US5926622A"><text>US 5,926,622</text></patcit> is based on running a simulation of the system.

Object of the invention

0008The present invention seeks to provide an improved circuit verification procedure.

Statement of the invention

0009In accordance with a first aspect of the invention, there is provided a digital circuit design verification method comprising: automatically determining for each property of a non reduced RTL model a reduced RTL model with reduced signal width for a design specification, which reduced RTL model retains the signal property of the non-reduced RTL model, wherein the RTL model includes word-level signals comprising bit-vectors and, for each bit-vector variable, the method of reducing the RTL model is separated into two sequential steps; the first step comprising the computation of the coarsest granularity of each word-level signal whereby to separate each signal into several contiguous chunks which indicate the basic groups of bits with respect to structural data dependencies, the second step comprising the computation of the minimum width with respect to dynamic data dependencies; and subjecting the reduced RTL model to a property checking process. The design verification process comprises, in a step prior to the determination of a reduced width RTL model, of determining the design specification of the digital circuit design and the specification of the properties to be investigated, synthesising an RTL netlist of high level primitives whereby the circuit is defined as an interconnection of control and data path portions, wherein in signals of a width <i>n</i> are determined such that: <maths id="math0001"><math display="block"><mi mathvariant="normal">n</mi><mo>∈</mo><msub><mi mathvariant="normal">ℕ</mi><mo>+</mo></msub><mo>;</mo></math><img file="EP1221663B1_D0001.tif" /></maths> wherein bitvectors of respective length determine the signal value. Conveniently, in the property checking process, an internal bit level representation contains a bit level variable for each bit of each word signal. This bit-level representation is passed to a verification engine and then to a property test unit which operates to provide a positive result if the investigated property holds true for the circuit and which operates to provide a counter-example if the property does not hold. In the event that a counter-example is produced for the reduced RTL design, signal width enhancement is performed to create a counter-example for the original RTL.

0010In accordance with a further aspect of the present invention there is provided a digital circuit design verification tool wherein a pre-property checking unit is operable to reduce the widths of the signals occurring in an RTL model of an input design specification and an input property specification to determine a reduced width RTL model, wherein the RTL model includes word-level signals comprising bit-vectors and, for each bit-vector variable, the tool is operable to reduce the RTL model width of a signal in two sequential steps; wherein, a first step, a coarse granularisation of each word-level signal is determined whereby to separate each signal into several contiguous chunks which indicate the basic groups of bits with respect to structural data dependencies; and, in a second step, a minimum width with respect to dynamic data dependencies is determined;, which reduced width RTL model retains the specific signal property of a non-reduced RTL model. The tool further comprises a front end unit operable to receive input data relating to a design specification and the property characteristics of a design to be verified and is operable to provide an RTL netlist of the circuit design and property whereby the circuit can be defined as an interconnection of control and data path portions, wherein in signals of a width n are determined such that <maths id="math0002"><math display="inline"><mi>n</mi><mo>∈</mo><msub><mi mathvariant="normal">ℕ</mi><mo>+</mo></msub><mo>;</mo></math><img file="EP1221663B1_D0002.tif" /></maths>and bitvectors of a respective length determine the signal value. Conveniently a property checking unit is operable to create an internal bit level representation having received a reduced RTL representation. This representation is sequentially passed to a verification engine and to a property test unit. The property test unit being operable to provide a positive result if the circuit property holds true and which is operable to provide a counter-example in the case of the property does not hold. Conveniently the signal width enhancement unit is operable to receive counter-examples for reduced RTL data and to expand the signal width to provide a counter example for the original RTL.

0011A linear signal width reduction causes an exponential reduction of the induced state space. Reducing state space sizes in general goes hand in hand with reduced verification runtimes. Thus the technique holds a high potential for speeding up verification tasks. Tests have shown that the present invention can significantly reduce the runtimes of existing prover tools. Furthermore, the present invention will be able to process design sizes which have, hitherto, exceeded the capacities of existing verification tools and which could not be taken into account before due to resource limitations. FIFO's, queues, stacks, bridges and interface protocols comprise part of a class of digital hardware designs to which the present invention is particularly well suited to processing.

0012A further advantage of the present invention is that, if the analysis yields that no reduction at all is possible for a given design and a given property, then reduced model and original design are identical. The verification task itself cannot be impaired by using the proposed method as a pre-process, and in all case studies pre-processing runtimes were negligible Furthermore, the technique can be applied in high-level equivalence checking and high-level simulation. High-level equivalence checking, for example, can be considered a special case of high-level property checking. The design specification can include two different implementations of the same circuit and the property can require functional equivalence, or the property itself can be written in a hardware description language representing a functional specification of the circuit.

Brief description of the figures

0013The invention may be understood more readily, and various other aspects and features of the invention may become apparent, from consideration of the following description and the figures as shown in the accompanying drawing sheets, wherein: <ul id="ul0001" list-style="none" compact="compact"><li><figref idref="f0001">Figures 1a</figref> and <figref idref="f0002">1b</figref> show property checking flow diagrams;</li><li><figref idref="f0003">Figure 2</figref> shows the basic steps involved in the abstraction technique of this invention;</li><li><figref idref="f0004">Figure 3</figref> is a table detailing the syntax of various bit-vector operators supported in the reduction technique of this invention;</li><li><figref idref="f0003">Figure 4</figref> is a flow chart detailing the generation of the reduced RTL model;</li><li><figref idref="f0005">Figure 5</figref> shows the effect of slicing equivalence classes;</li><li><figref idref="f0005">Figure 6</figref> illustrates a granularity analysis in terms of bit-vectors, dependency classes of bit-vector chunks and granularities; and</li><li><figref idref="f0006">Figure 6a</figref> details a process for determining the granularity analysis of bit-vector equations;</li><li><figref idref="f0007">Figure 7</figref> illustrates a minimum width computation for a dependency class;</li><li><figref idref="f0008">Figure 7a</figref> details a process for reduced model generation;</li><li><figref idref="f0009">Figure 8</figref> shows a block diagram of an Asynchronous Transfer Mode (ATM) switching element operable in accordance with the invention;</li><li><figref idref="f0010">Figure 9</figref> comprises tabulated results of the address management unit shown in <figref idref="f0009">Figure 8</figref>;</li><li><figref idref="f0011">Figure 10</figref> shows a granularity analysis flow chart together with a first example;</li><li><figref idref="f0012">Figure 11</figref> shows a granularity analysis flow chart together with a second example;</li><li><figref idref="f0013">Figure 12</figref> shows a granularity analysis flow chart together with a third example;</li><li><figref idref="f0014">Figure 13</figref> shows a minimal width abstraction flow chart together with a first example;</li><li><figref idref="f0015">Figure 14</figref> shows a minimal width abstraction flow chart together with a second example;</li><li><figref idref="f0016">Figure 15</figref> shows a minimal width abstraction flow chart together with a third example;</li><li><figref idref="f0017">Figure 16</figref> shows a model generation flow chart together with a first example;</li><li><figref idref="f0018">Figure 17</figref> shows a model generation flow chart together with a second example; and</li><li><figref idref="f0019">Figure 18</figref> shows a model generation flow chart together with a third example.</li></ul>

Detailed description of invention

0014There will now be described by way of example, the best mode contemplated by the inventor for carrying out the invention. In the following description numerous specific details are set out in order to provide a complete understanding of the invention. It will be apparent however, to those skilled in the art, that the present invention may be put in to practice with variations of the specific.

0015Referring to <figref idref="f0001">Figure 1a</figref> there is shown a prior-art property checking flow diagram. A property specification, 112, and a design specification, 114, is presented to a bounded property checker, 120. The property and design specifications, 112, 114, are input to a front end processor which converts the specifications to Register Transfer Level (RTL) specifications. A decision relating to the property is made at decision point 122: if the property holds then the design feature is confirmed 124; if the property does not hold, then a counterexample 126 is determined. A counterexample, as is known, is an indication that a circuit does not function in the way intended by the designer; a counterexample is given in terms of assignments of values to the circuit inputs such that a violation of the desired behaviour which is described by the property specification can be observed when looking a the values of the circuit outputs resulting from the circuit inputs. A design modification would be made to eliminate the occurrence of the counterexample and, indeed, further counterexamples which may consequentially arise.

0016The present invention employs the use of properties described in a linear time logic over finite bounded intervals of time. Properties consist of an assumption part which implies a commitment part: <maths id="math0003"><math display="block"><mi mathvariant="italic">Property</mi><mo mathvariant="italic">≡</mo><mi mathvariant="italic">Assumptions</mi><mo mathvariant="italic">⇒</mo><mi mathvariant="italic">Commitment</mi></math><img file="EP1221663B1_D0003.tif" /></maths>

0017Properties specify the intended behaviour of the design within a finite interval of time and consist of temporal operators and state expressions, involving relationships among data words. As an example consider: <ul id="ul0002" list-style="none" compact="compact"><li>assume (during [t+0, t+4]: reset = 0) and (at t+0: request = 1);</li><li>prove (at t+3: acknowledge = 1) and (at t+4: data = 11111111);</li></ul>

0018Referring now to <figref idref="f0002">Figure 1b</figref>, there is shown a property-checking flow in accordance with the invention. As a first step, design and property are synthesized into a flattened netlist of high-level primitives, called an RTL netlist, as is known. These netlists include word-level signals, word-level gates, arithmetic units, comparators (data to control), multiplexors (control to data) and memory elements Each signal <b><i>x</i></b> has a fixed given width <maths id="math0004"><math display="inline"><mi mathvariant="normal">n</mi><mo>∈</mo><msub><mi mathvariant="normal">ℕ</mi><mo>+</mo></msub></math><img file="EP1221663B1_D0004.tif" /></maths>and takes bitvectors of respective length as values. The RTL representation of the design is handed to a property checker which translates the netlist into a bit-level representation and either proves that the property holds for the given design, or returns a counterexample.

0019In a pre-processing step prior to the invocation of the property checker, the RTL netlist is obtained, 118, and a scaled down RTL model 130 is computed by signal-width reduction processor, 128, in which signal widths are reduced, while guaranteeing that: <maths id="math0005"><math display="block"><mi>The property holds for the original RTL</mi><mo>⇔</mo><mi>The property holds for the reduced RTL</mi></math><img file="EP1221663B1_D0005.tif" /></maths>

0020The reduced RTL, 130, is given to the property checker, 132, instead of the original RTL. The internal bit-level representation, 138, used by the property checker contains a bit-level variable for each bit of each word-level signal of the RTL representation, and, depending on the degree of reduction of the signal widths, now can contain significantly less variables for the reduced RTL. The property checker, 132 includes a verification engine (SAT, BDD...), 140. If the property does not hold, the property checker returns a counterexample in terms of an assignment of values to all inputs of the reduced RTL, 134. The method provides a technique which takes such counterexample and generates an assignment of values to the inputs of the original design in a signal width enhancement step by signal width enhancement processor, 136, such that the property does not hold when these input values are applied to the circuit, and provides a counterexample, 126.

0021The invention conveniently uses structural data-path dependency analyses for minimum width abstractions. The basic idea is illustrated by the following introductory examples.

0022In a first example, example 1, we assume we want to check if the conjunction of two word-level signals of width 8, denoted by <i>x</i>[8] and <i>y</i>[8] can evaluate to the 8-bit zero vector. Let 'and' denote bitwise Boolean conjunction. In RTL, we have to check if the equation <maths id="math0006" num="(1)"><math display="block"><msub><mi>x</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mspace width="1em" /><mi>and</mi><mspace width="1em" /><msub><mi>y</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mo>=</mo><mn>00000000</mn></math><img file="EP1221663B1_D0006.tif" /></maths> is satisfiable. A corresponding bit-level representation of the same problem involves 16 variables and 8 equations. It is not necessary to solve all 8 equations because bit positions 0-7 are treated uniformly. Let <i>x</i>'_[1] and <i>y</i>_[1] denote signals of width 1. It is sufficient to check if: <maths id="math0007" num="(2)"><math display="block"><msub><mi mathvariant="italic">xʹ</mi><mfenced open="[" close="]"><mn>1</mn></mfenced></msub><mspace width="1em" /><mi>and</mi><mspace width="1em" /><msub><mi mathvariant="italic">yʹ</mi><mfenced open="[" close="]"><mn>1</mn></mfenced></msub><mo>=</mo><mn>0</mn></math><img file="EP1221663B1_D0007.tif" /></maths> is satisfiable, because (1) is satisfiable if and only if (2) is satisfiable. Furthermore, a satisfying solution for (1) can be obtained from a satisfying solution of (2) by copying the values of <i>x'</i>_[1] 1 and <i>y'</i>_[1] into all bit positions of the corresponding signals of (1). For example, <i>x'</i>_[1] = 1, yields <i>x</i>_[8] = 00000000 and <i>y</i>_[8]= 11111111.

0023In the example above, signals <i>x</i>_[8] and <i>y</i>_[8] both could be reduced to a width of one bit. In general, reduction depends on the structural data dependencies occurring in the cone of influence of a signal in a given design.

0024In a second example, given the assumptions of Example 1, we let <i>z</i>_[4] be an additional word-level signal of width 4 and assume that <i>z</i>_[4] is assigned to the 4 most significant bits of <i>x</i>_[8]. That is to say we have to check if the following system of equations is satisfiable: <maths id="math0008" num="(3)"><math display="block"><mtable columnalign="left"><mtr><mtd><msub><mi>x</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mfenced open="[" close="]"><mn>7</mn><mn>4</mn></mfenced></mtd><mtd><mo>=</mo><msub><mi>z</mi><mfenced open="[" close="]"><mn>4</mn></mfenced></msub></mtd></mtr><mtr><mtd><msub><mi>x</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mspace width="1em" /><mi>and</mi><mspace width="1em" /><msub><mi>y</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub></mtd><mtd><mo>=</mo><mn>00000000</mn></mtd></mtr></mtable></math><img file="EP1221663B1_D0008.tif" /></maths> Bit positions 0-3 as well as 4-7 are treated uniformly, though both cases in a different way. Signals <i>x</i>_[8] and <i>y</i>_[8] have to be split. Let <i>x</i>¹_[2], <i>y</i>¹_[2] and <i>z</i>¹_[1] denote signals of width 2 and 1 respectively, and consider: <maths id="math0009" num="(4)"><math display="block"><mtable columnalign="left"><mtr><mtd><msub><msup><mi>x</mi><mn>1</mn></msup><mfenced open="[" close="]"><mn>2</mn></mfenced></msub><mfenced open="[" close="]"><mn>1</mn><mn>1</mn></mfenced></mtd><mtd><mo>=</mo><msub><msup><mi>z</mi><mn>1</mn></msup><mfenced open="[" close="]"><mn>1</mn></mfenced></msub></mtd></mtr><mtr><mtd><msub><msup><mi>x</mi><mn>1</mn></msup><mfenced open="[" close="]"><mn>2</mn></mfenced></msub><mspace width="1em" /><mi>and</mi><mspace width="1em" /><msub><mi>y</mi><mfenced open="[" close="]"><mn>2</mn></mfenced></msub></mtd><mtd><mo>=</mo><mn>00</mn></mtd></mtr></mtable></math><img file="EP1221663B1_D0009.tif" /></maths>

0025System (3) is satisfiable if and only if (4) is satisfiable. To obtain a solution of (3), we copy <i>x'</i>_[2][1, 1] into all positions of <i>x</i>_[8] [7, 4] and <i>x</i>'_[2] [0, 0] into all positions of <i>x</i>_[8] [3, 0]. The same is done for <i>y</i>'_[2] and <i>y</i>_[8], and <b><i>z</i></b>'_[1] is copied into all positions of <i>z</i>_[4]. For example, <i>x'</i>_[2] = 10, <i>y'</i>_[2] = 01, <i>z'</i>_[1] = 1, yields <i>x</i>_[8] = 11110000, <i>y</i>_[8] = 00001111 and <i>z</i>_[4] = 1111.

0026Signals <i>x</i>_[8] and <i>y</i>_[8] are both split into two parts, and each part can be reduced to a width of one bit, resulting in an overall width of 2 bits for <i>x</i>'_[2] and <i>y</i>'_[2]. In general, it is not always possible to reduce a chunk of bits processed in exactly the same manner to only one bit. Equations containing dynamic data dependencies, e.g. if-then-else operators, require an analysis of all possible inequalities between signals, as shown in the following example.

0027In a third example, we let <i>x</i>_[8], <i>y</i>_[8] and <i>z</i>_[8] be data signals of width 8, and let <b>a</b>_[1], <b>b</b>_[1] and <b>c</b>_[1] be control signals. The satisfiability of the following system of equations can be characterised as: <img file="EP1221663B1_D0010.tif" /> Obviously, <i>x</i>_[8], <i>y</i>_[8] and <i>z</i>_[8] cannot be reduced to a width of only one bit, because <i>x</i>_[8] ≠ <i>y</i>_[8] ∧ <i>y</i>_[8]<i>≠ z</i>_[8] ∧ <i>z</i>_[8] ≠ <i>x</i>_[8] is satisfiable, while <i>x'</i>_[1] # <i>y'</i>_[1] ∧ <i>y'</i>_[1] ≠ <i>z'</i>_[1] ∧ <i>z'</i>_[1] ≠ <i>x'</i>_[1] is not. Insted the following holds: <ul id="ul0003" list-style="none"><li>Instead, the following holds: <i>x</i>_[m] ≠ <i>y</i>_[m] ∧ <i>y</i>_[m] ≠ <i>z</i>_[m] ∧ <i>z</i>_[m] ≠ <i>x</i>_[m] is satisfiable for all <i>m</i> ≥ 2. Therefore, 2 is the minimum value for <i>m</i> which <img file="EP1221663B1_D0011.tif" /> is true, and thus the original system of equations can be replaced by <b>a'</b>_[1] = ite(<i><b>x</b>'</i>_[2]=<i><b>y</b>'</i>_[2], 0_[1], 1_[1]) <b>b'</b>_[1] = ite(<i><b>y</b>'</i>_[2]= <b><i>z</i></b>'_[2], 0_[1], 1_[1]) <b>c'</b>_[1] = ite(<b><i>z</i></b>'_[2]=<i><b>x</b>'</i>_[2], 0_[1], 1_[1]) l_[1]= a'_[1] and b'_[1] and c'_[1]</li><li>Without changing satisfiability.</li></ul> A satisfying solution for the original system can be obtained from a solution of (5) by a sign extension of the values of the reduced variables, e.gof the reduced variables, e.g., <b><i>x</i></b>'_[2] = 00, <i><b>y</b>'</i>_[2] =01, <b><i>z</i></b>'_[2] = 10, yields <b><i>x</i></b>_[8] = 00000000, <b><i>y</i></b>_[8] = 00000001 and <b><i>z</i></b>_[4] = 11111110.

0028The process of scaling down signal widths is separated into two sequential phases.

0029The basic idea of this abstraction technique is shown in the flow chart, 200, of <figref idref="f0003">Figure 2</figref>, as will be described below. First, the coarsest granularity of each word-level signal <i>x</i>_[16] is computed, as determined by the structural data dependencies in a granularity analysis step, 210. A granularity is a separation of a signal into several contiguous chunks, 218, which indicate the coarsest possible subsumptions of individual bits of the signal, which are treated in the exact same manner with respect to structural data dependencies. Then, for each chunk, the necessary minimum width, 220, is computed, as required by dynamical data dependencies in a minimum width abstraction step, 212. According to these computed minimum chunk widths, the reduced width for the corresponding variable is reassembled, in a reduced model generation step, 214, to be provide a reduced signal, 222.

0030The present invention provides an equational theory BV_ext of fixed-size bitvectors, derived from the core theory of bitvectors. Let B = {0, 1} denote the set of bit values 0 and 1. A bitvector of width <maths id="math0010"><math display="inline"><mi mathvariant="normal">n</mi><mo mathvariant="normal">∈</mo><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub></math><img file="EP1221663B1_D0012.tif" /></maths> is a vector element of B<i>ⁿ</i>, consisting of <i>n</i> individual bits which are indexed from right to left, starting with index 0. Bitvectors are written as binary bitstrings, and, accordingly, the set B<i>ⁿ</i> of bitvectors of length <i>n</i> is denoted by B_[n]. The invention provides a bitvector variable definition wherein, for <maths id="math0011"><math display="inline"><mi>n</mi><mo>∈</mo></math><img file="EP1221663B1_D0013.tif" /></maths><maths id="math0012"><math display="inline"><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub><mo>,</mo></math><img file="EP1221663B1_D0014.tif" /></maths> a bitvector variable <b><i>x</i></b>_[n] of width n is a typed variable, representing fixed-size bitvectors v ∈ <b>B</b>_[n] of width n.

0031Fixed-size in this context means that for each bitvector variable the width _n is a fixed (but arbitrary) positive natural number. We write <b><i>x</i></b>_[n][<i>i</i>] to refer to the <i>i</i>^th bit of <b><i>x</i></b>_[n]. <i>BV</i>_ext includes bitvector variables and bitvector constants <i>c</i>_[n], <maths id="math0013"><math display="inline"><mi mathvariant="normal">n</mi><mo>∈</mo><mo mathvariant="normal" /><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub></math><img file="EP1221663B1_D0015.tif" /></maths> and <b>c</b> ∈ B_[n]. The present invention, compared to the core theory of bitvectors, provides additional high-level operators as tabulated in <figref idref="f0004">Figure 3</figref>. Further operators, like shifts, rotations or further comparisons, are conveniently expressed within this theory. The Boolean predicates = and &lt; occurring in the guards of <b>ite</b> (if-then-else) expressions, are defined on two bitvector arguments of equal width. Equality is defined bitwise, whereas &lt; is defined according to the lexicographical order of bitstrings.

0032The set of terms is defined over a set of free bitvector variables and the operators shown in <figref idref="f0004">Figure 3</figref>. If the terms are "well-formed" then the terms require variable widths to comply with operator demands, and index expressions must not exceed the widths of argument terms. A valuation is an assignment of values to the bitvector variables occurring in the terms. A system <i>E</i> of equations over such terms is satisfiable if there exists a valuation of the variables such that all equations of <i>E</i> hold simultaneously. Correspondingly, we define the term "valid" such that <i>E</i> is universally valid if all possible valuations satisfy <i>E</i>.

0033In a fourth example, <b><i>x</i></b>_[16]<i><b>y</b></i>_[4] and <b><i>z</i></b>_[4] are bitvector variables. Consider: <ul id="ul0004" list-style="none" compact="compact"><li>1. <i>x</i>[16] [15,8] ⊗ <i>x</i>_[16] [7,0] = <i>x</i>_[16]</li><li>2. <i>x</i>_[16] = neg (<i>x</i>_16])</li><li>3. <i>y</i>_[4] and 1100_[4] = <i>z</i>_[4]</li></ul> Equation 1 is universally valid and Equation 2 is unsatisfiable. Equation 3 is satisfiable, e.g. by <b><i>y</i></b>_[4] := 0111_[4] and <b><i>z</i></b>_[4] :=0100_[4], but not universally valid.

0034In a fifth example <i>x</i>_[8] and <i>y</i>_[4] are bitvector variables. <maths id="math0014"><math display="block"><msub><mi>x</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mo>=</mo><msub><mi>y</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mo>⊗</mo><msub><mi>y</mi><mfenced open="[" close="]"><mn>4</mn></mfenced></msub></math><img file="EP1221663B1_D0016.tif" /></maths><maths id="math0015"><math display="block"><mtable><mtr><mtd><msub><mi>x</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mfenced open="[" close="]"><mn>4</mn><mn>4</mn></mfenced></mtd></mtr></mtable><mo>=</mo><mi>neg</mi><mfenced><mtable><mtr><mtd><msub><mi>x</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mfenced open="[" close="]"><mn>0</mn><mn>0</mn></mfenced></mtd></mtr></mtable></mfenced></math><img file="EP1221663B1_D0017.tif" /></maths>

0035Consider the system of equations given above. Taken separately, the first and second equations are satisfiable. However, the system of equations, as a whole, is unsatisfiable.

0036Referring now to <figref idref="f0003">Figure 4</figref>, there is illustrated the steps of the proposed abstraction technique in accordance with the present invention. As a first step, the RTL representation of design, 410, and property is translated into a system <i>E</i>, <i>412,</i> of equations of bitvector terms over BV_ext, such that: <maths id="math0016" num="(5)"><math display="block"><mi mathvariant="italic">E is satisfiable</mi><mo mathvariant="italic">⇔</mo><mi mathvariant="italic">Property does not hold for the Design</mi></math><img file="EP1221663B1_D0018.tif" /></maths>

0037A possible solution of <i>E</i>, if existent, would be a counterexample which would give value assignments to all circuit signals, such that the property does not hold for these assignments.

0038The data dependencies within the bitvector equations ofE are analysed, 414, and a second system <i>E'</i>, 416, of bitvector equations is computed, in which the type (i.e. the width) of each bitvector variable is reduced to a smallest number of bits that is possible with respect to the abstraction technique, such that: <maths id="math0017" num="(6)"><math display="block"><mi mathvariant="italic">Eʹ is satisfiable</mi><mo mathvariant="italic">⇔</mo><mi mathvariant="italic">E is satisfiable</mi></math><img file="EP1221663B1_D0019.tif" /></maths> From (5) and (6) it follows that: <maths id="math0018" num="(7)"><math display="block"><mi mathvariant="italic">Eʹ is satisfiable</mi><mo mathvariant="italic">⇔</mo><mi mathvariant="italic">Property does not hold for the Design</mi></math><img file="EP1221663B1_D0020.tif" /></maths>

0039<i>E'</i> is translated back to an RTL netlist, 418, representing a scaled down version of the original design. According to (7), the property checking task can be completely carried out on the reduced model.

0040Given a system <i>E</i> of bitvector equations over <i>BV</i>_ext, structural and functional dependencies are imposed on the bitvector variables by the high-level operators occurring in the equations. Dependencies may be found between complete variables or only between certain parts. For each variable, the present invention analyses such dependencies and determines the contiguous parts in which all bits are treated uniformly with respect to data dependencies.

0041Further definitions are now provided for 'Chunk' and 'Granularity': A chunk <b><i>x</i></b>_[-_n]<<i>j,i</i>>, o ≤ <i>i</i> ≤ <i>j</i> < <i>n</i>, of a bitvector variable <b><i>x</i></b>_[n] is a syntactical representation for a contiguous part of <i>x</i>_[n], i.e. <i>x</i>_[n] <<i>j,i</i>> := <i>x</i>_[n] [<i>j,i</i>].

0042Chunks are used to describe the above-mentioned contiguous parts of bitvector variables.

0043A granularity of a bitvector variable <b><i>x</i></b>_[n] is any ordered decomposition of <i>x_[n]</i> into chunks {<b><i>x</i></b>_[<i>n</i>]<<i>j₂</i>,i₁>, <b><i>x</i></b>_[n] <<i>j_q</i>,<i>i_q</i>>} 0 = <i>i₁</i><<i>j₁</i> = <i>1</i> = i₂ < <i>j</i>₂ +1 = ... = <i>i</i>_q < <i>j</i>_q + 1 = <i>n</i>, such that <maths id="math0019"><math display="block"><msub><mi>x</mi><mfenced open="[" close="]"><mi>n</mi></mfenced></msub><mfenced open="[" close="]"><msub><mi>j</mi><mi>q</mi></msub><msub><mi>i</mi><mi>q</mi></msub></mfenced><mo>⊗</mo><mo>…</mo><mo>⊗</mo><msub><mi>x</mi><mfenced open="[" close="]"><mi>n</mi></mfenced></msub><mfenced open="[" close="]"><msub><mi>j</mi><mn>2</mn></msub><msub><mi>i</mi><mn>2</mn></msub></mfenced><mo>⊗</mo><msub><mi>x</mi><mfenced open="[" close="]"><mi>n</mi></mfenced></msub><mfenced open="[" close="]"><msub><mi>j</mi><mn>1</mn></msub><msub><mi>i</mi><mn>1</mn></msub></mfenced><mo>=</mo><msub><mi>x</mi><mfenced open="[" close="]"><mi>n</mi></mfenced></msub><mn>.</mn></math><img file="EP1221663B1_D0021.tif" /></maths> is a tautology

0044In a sixth example, <i>x</i>_[16] is a bitvector variable. {<i>x</i>_[16]<15,18>, <i>x</i>_[16]<7,4>, <b><i>x</i></b>_[16]<3,0>} is a granularity of <b><i>x</i></b>_[16], whereas {<b><i>x</i></b>_[16]<15, 10>, <b><i>x</i></b>_[16]<5,0>} and { <b><i>x</i></b>_[16]<15,5>, <b><i>x</i></b>_[16]<10,0>} is not.

0045Granularities are used to describe how different data dependencies exist for different chunks of a bitvector variable. Non-uniform structural dependencies occur whenever a variable (or a term) is not treated as a whole, but separated into parts upon which different operations are performed, e.g. by extractions or concatenations.

0046The relation between granularities and structural dependencies is shown in a further example: consider the following bitvector equation: <maths id="math0020"><math display="block"><msub><mi>x</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mo>=</mo><msub><mi>y</mi><mfenced open="[" close="]"><mn>4</mn></mfenced></msub><mo>⊗</mo><msub><mi>z</mi><mfenced open="[" close="]"><mn>4</mn></mfenced></msub></math><img file="EP1221663B1_D0022.tif" /></maths>

0047The concatenation on the right hand side of the equation imposes different dependencies on the upper and lower part of <i>x</i>_[8], the first depending on <i>y</i>_[4], the latter on <i>z</i>_[4]. This is described by the granularity {<i>x</i>_[8](7,4), <i>x</i>_[8] (3,0)}.

0048For each bitvector variable <i>x</i>_[n], the method in accordance with one aspect of the invention computes the coarsest possible granularity which describes the splitting of data dependencies for <i>x</i>_[n], as imposed by the equations of <i>E</i>. Slicing is performed only if necessary. For example, the equation <i>x</i>_[16] =<i>y</i>_[16] [15,12] ⊗ <i>y</i>_[16][11,0] is equivalent to <b><i>x</i></b>_[16] = <i><b>y</b></i>_[16] and does not require slicing of <b><i>x</i></b>_[16]. Hence, initially a normalization of all bitvector terms is performed. The computation of the coarsest granularities is carried out using an equivalence class structure which groups chunks between which functional dependencies are detected.

0049Granularity analysis and functional dependencies are shown in another example. The equation given in the fourth example imposes functional dependencies between <i>x</i>_[8][7,4] and <i>y</i>_[4][3,0] and between <i>x</i>_[8][3,0] and <i>z</i>_[4][3,0]. The resulting equivalence classes are {<i>x</i>_[8]<7,4>, <i>y</i>_[4]<3,0>} and {<i>x</i>_[8]<3,0>, <i>z</i>_[4]<3,0>}. As a second example consider <i>x</i>_[16] = <i>y</i>_[16] or <i>z</i>_[16]. Here, <i>x</i>_[16], <i>y</i>_[16] and <i>z</i>_[16] are related to each other by a bitwise Boolean operator, requiring that all three go into the same equivalence class {<i>x</i>_[16]<15,0>,<i>y</i>_[16]<15,0>, <i>z</i>[16]<15,0>}.

0050The equivalence class computation works incrementally and can efficiently be performed by employing a union-find algorithm, which, besides the known <b>union</b> () and <b>find</b>() operations, defines a new procedure <b>slice</b>(). Initially, in each bitvector group of classes, 510, variable <i>x</i>_[n] resides in its own singleton equivalence class: {<b><i>x</i></b>_[n]<n - 1,0>}. Find (<i>x</i>_[n],<i>i</i>) yields the (non ambiguous) equivalence class, which includes a chunk of <i>x</i>_[n] which contains bit position <i>i</i>, union() performs the usual set union of two classes, and <b>slice</b>(<i>x</i>[n],<i>j,i</i>) calls <b>find</b>(<i>x</i>_[n],<i>i</i>) and <b>find</b>(<i>x</i>_[n],<i>j</i>) and splits all chunks of the respective classes at the bit positions corresponding to <i>i</i> and <i>j</i> and groups the originating parts in two new equivalence classes, as illustrated in <figref idref="f0005">Figure 5</figref>, with a second group of classes, 512.

0051<figref idref="f0005">Figure 6</figref> exemplifies a granularity analysis in terms of bitvectors, dependency classes of bitvectors chunks and granularities. Each bitvector equation <i>e</i> is processed sequentially by the analyser and the next state of the equivalence class structure is computed by means of the procedure gran(e), which is outlined in process 1 as shown in <figref idref="f0006">Figure 6a</figref>. Once all bitvector equations have been processed, for each bitvector variable the coarsest possible granularity is given by the state of the equivalence classes.

0052The granularity analysis decomposes the initial satisfiability problem for <i>E</i> into a number of independent satisfiability problems, characterized by the computed equivalence classes. The solutions of these problems can be characterized by bitwise bitvector functions, as will be defined as follows:

0053Let <maths id="math0021"><math display="inline"><mi mathvariant="normal">n</mi><mo mathvariant="normal">∈</mo><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub></math><img file="EP1221663B1_D0023.tif" /></maths>: and <maths id="math0022"><math display="inline"><mi mathvariant="normal">k</mi><mo mathvariant="normal">∈</mo><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub><mo>,</mo></math><img file="EP1221663B1_D0024.tif" /></maths> a k-ary bitvector function on bitvectors of width n is a function. <img file="EP1221663B1_D0025.tif" />

0054Bitvector functions <i>G</i>_[1] : B x ... x B → B on bitvectors of width 1 are called Boolean functions.

0055Let <maths id="math0023"><math display="inline"><mi mathvariant="normal">n</mi><mo mathvariant="normal">∈</mo><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub><mo>,</mo></math><img file="EP1221663B1_D0026.tif" /></maths><maths id="math0024"><math display="inline"><mi mathvariant="normal">k</mi><mo mathvariant="normal">∈</mo><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub><mo>,</mo></math><img file="EP1221663B1_D0027.tif" /></maths> and <i>F</i>_[n] be a k-ary bitvector function on bitvectors of width n. <i>F</i>_[n] is a bitwise bitvector function if there exists a k-ary Boolean function <i>G</i>_[1] such that: <maths id="math0025"><math display="block"><msub><mi>F</mi><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub><mo>≡</mo><mfenced><msub><mi>G</mi><mfenced open="[" close="]"><mn>1</mn></mfenced></msub><mo>,</mo><msub><mi>G</mi><mfenced open="[" close="]"><mn>1</mn></mfenced></msub><mo>,</mo><mo>…</mo><msub><mi>G</mi><mfenced open="[" close="]"><mn>1</mn></mfenced></msub></mfenced><mspace width="1em" /><mi>i</mi><mn>.</mn><mi mathvariant="normal">e</mi><mn>.</mn><mspace width="1em" /><mo>∀</mo><mi>i</mi><mo>∈</mo><mfenced open="{" close="}"><mn>0</mn><mo>,</mo><mo>…</mo><mo>,</mo><mi mathvariant="normal">n</mi><mo>-</mo><mn>1</mn></mfenced><mo>:</mo><msub><mi>F</mi><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub><mfenced><msub><msup><mi>x</mi><mn>1</mn></msup><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub><mo>…</mo><msub><msup><mi>x</mi><mi mathvariant="normal">k</mi></msup><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub></mfenced><mo>⁢</mo><mfenced open="[" close="]"><mi>i</mi></mfenced><mo>=</mo><msub><mi>G</mi><mfenced open="[" close="]"><mn>1</mn></mfenced></msub><mfenced><msub><msup><mi>x</mi><mn>1</mn></msup><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub><mfenced open="[" close="]"><mi>i</mi></mfenced><mo>,</mo><mo>…</mo><mo>,</mo><msub><msup><mi>x</mi><mi>k</mi></msup><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub><mfenced open="[" close="]"><mi>i</mi></mfenced></mfenced></math><img file="EP1221663B1_D0028.tif" /></maths>

0056<i>F</i>_[n] operates uniformly on all bit positions of its arguments according to <i>G</i>_[1]. If two k-ary bitwise Boolean functions <i>F</i>¹_[n] and <i>F</i>²_[m], one taking bitvectors of width <i>n</i> as arguments and the other bitvectors of width <i>m</i>, operate according to the same Boolean function <i>G</i>_[1], then this correspondence is denoted by <i>F</i>¹_[n] ≃ <i>F</i>²_[m]. in a ninth example <b><i>x</i></b>_[8] , <b><i>y</i></b>_[8], <b><i>z</i></b>_[8] are bit-vector variables of width 8 and let <i><b>x</b>'</i>_[4]<i><b>y</b>'</i>_[4] , <i>z'</i>_[4] , be bit-vector variables of width 4. Let <i>F</i>¹_[8] (<b><i>x</i></b>_[8] , <b><i>y</i></b>_[8], <b><i>z</i></b>_[8] ):= <b><i>x</i></b>[8] and (neg (<b><i>y</i></b>_[8]) <b><i>or z</i></b>_[8]); and <i>F</i>²_[4] (<b><i>x</i></b>'_[4], , <i><b>y</b>'</i>_[4]<i>, <b>z</b></i>'_[4]): = <b><i>x</i></b>'_[4] and (neg (<i><b>y</b>'</i>[4])) <i><b>or z</b>'</i>_[4]); and <i>F</i>¹_[8] and <i>F</i>²_[4] are bit-wise bit-vector functions with <i>F</i>¹_[8] ≃ <i>F</i>²_[4]. Furthermore, consider: <img file="EP1221663B1_D0029.tif" /><i>F</i>³_[8] (<b><i>x</i></b>_[8] , <b><i>y</i></b>_[8] , <b><i>z</i></b>_[8] ):= (<b><i>x</i></b>_[8] [7,4] and <b><i>y</i></b>_[8][7,4]) ⊗ <b><i>z</i></b>_[8][3,0]; <i>F</i>³_[8] is a bitvector function, but not bit-wise.

0057Let <i>C</i> be one of the equivalence classes computed by the granularity analysis. The set of all satisfying solutions of <i>E</i>, projected to the chunks contained in <i>C</i>, can be characterized by a first theorem with respect to satisfiability: <maths id="math0026"><math display="block"><mi>If C</mi><mo>=</mo><mfenced open="{" close="}"><msub><msup><mi>x</mi><mi>l</mi></msup><mfenced open="[" close="]"><mi mathvariant="normal">n</mi><mo>⁢</mo><mn>1</mn></mfenced></msub><mo><</mo><msub><mi>j</mi><mn>1</mn></msub><mo>,</mo><msub><mi>i</mi><mn>1</mn></msub><mo>></mo><mo>,</mo><mo>…</mo><mo>,</mo><msub><msup><mi>x</mi><mi>k</mi></msup><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub><mo><</mo><msub><mi>j</mi><mi>k</mi></msub><mo>,</mo><msub><mi>i</mi><mi>k</mi></msub><mo>></mo></mfenced><mo>,</mo></math><img file="EP1221663B1_D0030.tif" /></maths> with <i>j</i>₁ - <i>i</i>₁ = ...=<i>j_k</i> - <i>i_k</i> = n, then there exists a k-ary bit-wise bit-vector function: <i>F</i>_[n](<b><i>x</i></b>¹_[n] <<i>j</i>₁<i>, i</i>₁<i>></i>,...,<b><i>x</i></b>^k_[n]<<i>j_k, i_k</i>>) such that the set of satisfying solutions of the equation <img file="EP1221663B1_D0031.tif" /> describes the set of solutions of <b>E</b>, projected to <b><i>x</i></b>¹_[n] <<i>j</i>₁, <i>i</i>₁ >,...,<b><i>x</i></b>^k_[n] <<i>j_k, i_k</i>>.

0058Referring now to <figref idref="f0007">Figure 7</figref>, there is shown an equivalence class <i>C_i</i> containing chunks of width <i>n_i</i>. For each such class <i>C_i</i>, a ϕ(<i>C_i</i>) ≤ <i>n_i</i> is computed, ϕ (<i>C_i</i>) depending on the number of chunks residing in <i>C_i</i> and on the number of possible inequalities between these chunks, as determined by the guards of if-then-else expressions in the bitvector equations.

0059The satisfiability problem <i><b>B</b>_[ni],</i> which is related to <i>C_i</i> according to method 1, is satisfiable if and only if the modified satisfiability problem <i><b>B</b></i>_{<i>[</i>ϕ<i>(Ci)]</i>}, in which each chunk of <i>C_i</i> is replaced by a corresponding chunk of width ϕ<i>(C_i)</i>, i.e. we have <i><b>B</b>_[ni] ≃<b>B</b>[</i>ϕ<i>(Ci)],</i> is satisfiable. We will now consider the reduction of bitvector widths with a second method: Let <i>V</i>_[<i>n</i>] = {<i>x</i>¹_[<i>n</i>], <i>x</i>²_[<i>n</i>], <i>x^k</i>_[<i>n</i>]} be a finite set of <i>k</i> bitvector variables of width <maths id="math0027"><math display="inline"><mi mathvariant="normal">n</mi><mo mathvariant="normal">∈</mo><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub><mn>.</mn></math><img file="EP1221663B1_D0032.tif" /></maths> Let <i>F</i>_[n](<i><b>x</b>¹</i>_[n], <b><i>x</i></b>²_[n],...,<b><i>x</i></b>^k[n]) be a k-ary bitwise bitvector function on V_[n], and let <b>I</b> ⊆ V_[n] × V_[n] be a set of pairs of elements of V_[n], such that P₁,..., P_q are the connected components of the corresponding undirected graph (V_[n], I). Let <maths id="math0028"><math display="block"><mi mathvariant="normal">ϕ</mi><mfenced><msub><mi mathvariant="normal">V</mi><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub><mi mathvariant="normal">E</mi></mfenced><mspace width="1em" /><mo mathvariant="normal">:</mo><mo mathvariant="normal">=</mo><mfenced open="|" close="|"><msub><mi mathvariant="normal">V</mi><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub></mfenced><mo mathvariant="normal">-</mo><mfenced open="|" close="|"><mfenced open="{" close="}"><msub><mi mathvariant="normal">P</mi><mn mathvariant="normal">1</mn></msub><mo mathvariant="normal">…</mo><msub><mi mathvariant="normal">P</mi><mi mathvariant="normal">q</mi></msub></mfenced></mfenced><mo mathvariant="normal">=</mo><mi mathvariant="normal">k</mi><mo mathvariant="normal">-</mo><mi mathvariant="normal">q</mi></math><img file="EP1221663B1_D0033.tif" /></maths> and let m := max {ϕ(V_[n],E),1}. Then the following equivalence holds:

0060There exists a valuation <i>v</i> of <i>x</i>¹_[n],... ,<i>x^k</i>_[n] There exists a valuation <i>v</i> of <i>x'¹</i>_[m],..., <i>x'</i>^k_[m] such that <i>F</i>_[n](<i>v</i>(<i>x</i>¹_[n]), ...,<i>v</i>(<i>x^k</i>_[n]<i>))</i> = 0_[n] ⇔ of such that <i>F</i>_[m](<i>v</i>(<i>x'¹</i>_[m]),...,<i>v</i>(<i>x'</i>^k_[m])) =0_[m] EINBETTEN <i>and for all</i> (<i>xⁱ_[n]</i>,<i>xⁱ_[n]</i>)∈ <i>I</i> : <i>v</i>(<i>xⁱ_[n]</i>) ≠ <i>v(x^j_[n]) and for all</i> (<i>xⁱ_[m],x^j_[m]</i>) ∈ <i>I</i> : <i>v</i>(<i>x^,i_[m]</i>) ≠ <i>v</i>(<i>x</i>^<i>,</i>j<i>_[m]</i>) where <i>F</i>_[m](<i>x</i>'¹_[m],<i>x</i>'²_[m],...,<i>x'</i>^k_[m]) is the corresponding bitwise bitvector function with <i>F</i>_[m] ≃ <i>F</i>_[n] on bitvectors <i>x'</i>¹_[m],<i>x'</i>²_[m],...,<i>x'</i>^k_[m] of width m.

0061The information about possible inequalities is obtained during the Granularity Analysis and annotated within the equivalence classes. For each equivalence class <i>C</i> we define ϕ<i>(C)</i>:= max{ϕ(<i>V_[n]</i>,<i>I</i>),1}, where V<i>_[n]</i> is the set of chunks in <i>C</i>, and <b><i>I</i></b> is the set of possible inequalities annotated to <i>C</i>. The reduced system <i>E'</i> of bitvectors equations is constructed according to process 2.

0062<b>Example 10.</b> Let <i>x</i>_[8], <i>y</i>_[16], <i>z</i>_[16] be bitvector variables and assume that <i>E</i> contains the following equation: <maths id="math0029" num="(8)"><math display="block"><msub><mi>x</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mo>=</mo><mfenced><msub><mi>y</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub><mspace width="1em" /><mi>and</mi><mspace width="1em" /><msub><mi>z</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub></mfenced><mo>⁢</mo><mfenced open="[" close="]"><mn>15</mn><mn>8</mn></mfenced></math><img file="EP1221663B1_D0034.tif" /></maths> Assume that granularity analysis and minimum width abstraction yield the following results: <maths id="math0030"><math display="block"><msub><mi>C</mi><mi>i</mi></msub><mo>=</mo><mfenced open="{" close="}"><mo>…</mo><mo>,</mo><msub><mi>x</mi><mfenced open="[" close="]"><mn>8</mn></mfenced></msub><mo><</mo><mn>7</mn><mo>,</mo><mn>0</mn><mo>></mo><mo>,</mo><msub><mi>y</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub><mo><</mo><mn>15</mn><mo>,</mo><mn>8</mn><mo>></mo><mo>,</mo><msub><mi>z</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub><mo><</mo><mn>15</mn><mo>,</mo><mn>8</mn><mo>></mo><mo>,</mo><mo>…</mo></mfenced><mo>;</mo><mi mathvariant="italic">ϕ</mi><mfenced><msub><mi mathvariant="italic">C</mi><mi mathvariant="italic">i</mi></msub></mfenced><mo>=</mo><mn>2</mn></math><img file="EP1221663B1_D0035.tif" /></maths><maths id="math0031"><math display="block"><msub><mi>C</mi><mrow><mi>i</mi><mo>+</mo><mn mathvariant="italic">1</mn></mrow></msub><mo>=</mo><mfenced open="{" close="}"><mo>…</mo><mo>,</mo><msub><mi>y</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub><mo><</mo><mn>7</mn><mo>,</mo><mn>0</mn><mo>></mo><mo>,</mo><msub><mi>z</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub><mo><</mo><mn>7</mn><mo>,</mo><mn>0</mn><mo>></mo><mo>,</mo><mo>…</mo></mfenced><mo>;</mo><mspace width="7em" /><mi mathvariant="italic">ϕ</mi><mo>⁢</mo><mfenced><msub><mi mathvariant="italic">C</mi><mrow><mi mathvariant="italic">i</mi><mo>+</mo><mn>1</mn></mrow></msub></mfenced><mo>=</mo><mn>3</mn></math><img file="EP1221663B1_D0036.tif" /></maths>

0063<i>The granularity of y_[16] for example, is given by:</i><maths id="math0032"><math display="block"><mfenced open="{" close="}"><msub><mi>y</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub><mo><</mo><mn>15</mn><mo>,</mo><mn>8</mn><mo>></mo><mo>,</mo><msub><mi>y</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub><mo><</mo><mn>7</mn><mo>,</mo><mn>0</mn><mo>></mo></mfenced><mo>,</mo><mspace width="2em" /><mi mathvariant="italic">i</mi><mn mathvariant="italic">.</mn><mi mathvariant="italic">e</mi><mspace width="4em" /><msub><mi>y</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub><mfenced open="[" close="]"><mn>15</mn><mn>8</mn></mfenced><mo>⊗</mo><msub><mi>y</mi><mfenced open="[" close="]"><mn>16</mn></mfenced></msub><mfenced open="[" close="]"><mn>7</mn><mn>0</mn></mfenced></math><img file="EP1221663B1_D0037.tif" /></maths>

0064According to the minimum chunk widths, the corresponding reduced variable is assembled as follows: <maths id="math0033"><math display="block"><mfenced open="{" close="}"><msub><mi mathvariant="italic">yʹ</mi><mfenced open="[" close="]"><mn>5</mn></mfenced></msub><mfenced><mn>4</mn><mn>3</mn></mfenced><mo>,</mo><msub><mi mathvariant="italic">yʹ</mi><mfenced open="[" close="]"><mn>5</mn></mfenced></msub><mo><</mo><mn>2</mn><mo>,</mo><mn>0</mn><mo>></mo></mfenced><mo>,</mo><mi mathvariant="italic">i</mi><mn mathvariant="italic">.</mn><mi mathvariant="italic">e</mi><mspace width="4em" /><msub><mi mathvariant="italic">yʹ</mi><mfenced open="[" close="]"><mn>5</mn></mfenced></msub><mo>=</mo><msub><mi mathvariant="italic">yʹ</mi><mfenced open="[" close="]"><mn>5</mn></mfenced></msub><mfenced open="[" close="]"><mn>4</mn><mn>3</mn></mfenced><mo>⊗</mo><msub><mi mathvariant="italic">yʹ</mi><mfenced open="[" close="]"><mn>5</mn></mfenced></msub><mfenced open="[" close="]"><mn>2</mn><mn>0</mn></mfenced></math><img file="EP1221663B1_D0038.tif" /></maths>

0065Hence, the reduced equation of E', which corresponds to (8) of E is: <maths id="math0034" num="(9)"><math display="block"><msub><mi mathvariant="italic">xʹ</mi><mfenced open="[" close="]"><mn>2</mn></mfenced></msub><mo>=</mo><mfenced><msub><mi mathvariant="italic">yʹ</mi><mfenced open="[" close="]"><mn>5</mn></mfenced></msub><mspace width="1em" /><mi>and</mi><mspace width="1em" /><msub><mi mathvariant="italic">zʹ</mi><mfenced open="[" close="]"><mn>5</mn></mfenced></msub></mfenced><mo>⁢</mo><mfenced open="[" close="]"><mn>4</mn><mn>3</mn></mfenced></math><img file="EP1221663B1_D0039.tif" /></maths>

0066Indices of extraction expressions are modified according to the new chunk widths.

0067Method 1 and method 2 yield that the original system <i>E</i> of bitvector equations is satisfiable if and only if the reduced system <i>E'</i>, where all chunks of each class <i>C_i</i> are reduced to a width, ϕ<i>(C_i)</i>, is satisfiable.

0068Accordingly a third method is applied: The reduced system E' of bitvector equations which results from the proposed abstraction technique is satisfiable if and only if the original equational system E is satisfiable. For each solution of the reduced system a solution of the original system can be computed.

0069It is to be understood that ϕ(<i>C</i>) depends only on the sizes and number of the connected components of the corresponding undirected graph of <i>C</i> and <i>I</i>. The computation of the number of connected graph components for each class can efficiently be done by using a union-find algorithm, and, moreover, can be embedded within the computation of the equivalence classes during the granularity analysis.

0070Let <i>V_[n]</i>= {<i>x</i>¹<i>_[n]</i>,...,<i>_x^k_[n]</i>} be a set of bitvector variables, <i><b>B</b>[n]</i>(<i>x¹_[n]</i>,...,<i>x^k_[n]</i>) be a bitwise bitvector function and <i><b>I</b></i> ⊆ <i>V_[n]</i> × <i>V_[n]</i>. For <maths id="math0035"><math display="inline"><mi>m</mi><mo mathvariant="normal">∈</mo><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub><mo>,</mo></math><img file="EP1221663B1_D0040.tif" /></maths> let <i><b>B</b>_[m]</i> denote the corresponding bitwise bitvector function with <i><b>B</b>_[m] ≃ <b>B</b>_[n]</i> on bitvector variables <i>x</i>'¹_[m],...,<i>x'^k_[m]</i> of width <i>m,</i> and let <i>P</i>(<i><b>B</b>_[m],<b>I</b></i>) denote the following satisfiability problem:

0071There exists a valuation <i>v</i> of <i>x</i>¹_[m],...,<i>x</i>^k_[m] such that: <maths id="math0036"><math display="block"><mi>P</mi><mfenced><msub><mi mathvariant="bold-italic">B</mi><mfenced open="[" close="]"><mi mathvariant="italic">m</mi></mfenced></msub><mi mathvariant="bold-italic">I</mi></mfenced><mo>⇔</mo><msub><mi mathvariant="bold-italic">B</mi><mfenced open="[" close="]"><mi mathvariant="normal">m</mi></mfenced></msub><mo>,</mo><mfenced><mi>v</mi><mfenced><msub><msup><mi>x</mi><mn>1</mn></msup><mfenced open="[" close="]"><mi mathvariant="normal">m</mi></mfenced></msub></mfenced><mo>,</mo><mo>…</mo><mo>,</mo><mi>v</mi><mfenced><msub><msup><mi>x</mi><mi mathvariant="normal">k</mi></msup><mfenced open="[" close="]"><mi mathvariant="normal">m</mi></mfenced></msub></mfenced></mfenced><mo>=</mo><msub><mn>0</mn><mfenced open="[" close="]"><mi mathvariant="normal">m</mi></mfenced></msub><mspace width="1em" /><mi>and for all</mi><mspace width="1em" /><mfenced><msub><msup><mi>x</mi><mi mathvariant="normal">i</mi></msup><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub><msub><msup><mi>x</mi><mi mathvariant="normal">j</mi></msup><mfenced open="[" close="]"><mi mathvariant="normal">n</mi></mfenced></msub></mfenced><mo>∈</mo><mi mathvariant="bold-italic">I</mi><mo>:</mo><mi>v</mi><mfenced><msub><msup><mi>x</mi><mi mathvariant="normal">i</mi></msup><mfenced open="[" close="]"><mi mathvariant="italic">m</mi></mfenced></msub></mfenced><mo>≠</mo><mi>v</mi><mfenced><msub><msup><mi>x</mi><mi>j</mi></msup><mfenced open="[" close="]"><mi mathvariant="italic">m</mi></mfenced></msub></mfenced></math><img file="EP1221663B1_D0041.tif" /></maths>

0072According to Theorem 1, each satisfiability problem belonging to an equivalence class C can be described by a bitwise bitvector function <i><b>B</b>_[n]</i> and a set of inequalities <i><b>I</b>.</i> The reduced chunk width <i>m</i> := ϕ(<i>C</i>) computed in Theorem 2 is independent of any further mathematical property of <i><b>B</b>_[n],</i> i.e. we purposely abstract from the concrete aspects of <i><b>B</b>_[n]</i> except for bitwise operation. <i>m</i> is minimal with respect to this abstraction, which leads to a fourth theorem, relating to minimality:.

0073Let V_[n] = {<i>x</i>¹_[n],... ,<i>x</i>^k_[n]} be a finite set of k bitvector variables of width <maths id="math0037"><math display="inline"><mi mathvariant="normal">n</mi><mo mathvariant="normal">∈</mo><msub><mi mathvariant="normal">N</mi><mo mathvariant="normal">+</mo></msub><mn>.</mn></math><img file="EP1221663B1_D0042.tif" /></maths> Let <b><i>I</i></b> ⊆ V_[n], and let m := max{ ϕ(V_[n], <b>I</b>), 1}. Then there exists a k-ary bitwise bitvector function <b><i>B</i></b>_[n](<i>x</i>¹_[n],...,<i>_x</i>^k_[n]) such that <maths id="math0038"><math display="block"><mi>P</mi><mfenced><msub><mi mathvariant="bold-italic">B</mi><mfenced open="[" close="]"><mi mathvariant="italic">m</mi></mfenced></msub><mi mathvariant="bold-italic">I</mi></mfenced><mo>⇔</mo><mi>P</mi><mfenced><msub><mi mathvariant="bold-italic">B</mi><mfenced open="[" close="]"><mi mathvariant="italic">n</mi></mfenced></msub><mi mathvariant="bold-italic">I</mi></mfenced><mspace width="2em" /><mi mathvariant="italic">and not</mi><mspace width="2em" /><mfenced><mi>P</mi><mo>⁢</mo><mfenced><msub><mi mathvariant="bold-italic">B</mi><mfenced open="[" close="]"><mi mathvariant="italic">m</mi><mo mathvariant="italic">-</mo><mn>1</mn></mfenced></msub><mi mathvariant="bold-italic">I</mi></mfenced><mo>⇔</mo><mi>P</mi><mfenced><msub><mi mathvariant="bold-italic">B</mi><mfenced open="[" close="]"><mi mathvariant="italic">n</mi></mfenced></msub><mi mathvariant="bold-italic">I</mi></mfenced></mfenced></math><img file="EP1221663B1_D0043.tif" /></maths> i.e. m is the minimum width for which <i>P</i>(<b><i>B</i></b>_[m],<b><i>I</i></b>) is satisfiable if and only if <i>P</i>(<b><i>B</i></b>_[n],<b><i>I</i></b>) is satisfiable.

0074A prototype system was implemented in C++ and tested in several case studies at the Design Automation department of Siemens Corporation in Munich and at the Computer Network Peripherals department of Infineon Technologies in San Jose, CA. All test cases were run on an Intel Pentium II PC with a 450 MHz CPU, 128 MB main memory and a Linux operating system. Referring to <figref idref="f0009">Figure 8</figref>, which shows a block diagram of an ATM switching element 800, a case study of an address management unit of an ATM switching element will now be discussed. Results are tabulated in <figref idref="f0010">Figure 9</figref>. The design comprised of approximately 3000 lines of Verilog code, the netlist synthesis comprised of approximately 24.000 gates and 35.000 RAM cells. Signals input to cell inputs 802, which are multiplexed by multiplexer, 804, to a central RAM, 814, or via a target decoder 806 to an RTL unit 808, which provides signals to the central RAM. The RTL unit incorporates 16 FIFO queue buffers, 810, and complex control logic, 812. Memory addresses are fed to 33 input channels to the multiplexer unit, 804, stored in FIFO's and, upon request, output from one of 17 output channels, 816, while the cell sequence is preserved and no addresses are allowed to be dropped from the management unit.

0075The prototype was used as preprocessor to a collection of known property checking tools. Three different properties, nop, read and write were required to be verified, which specified the intended behaviour within a range of 4 timesteps (nop, write), respectively 6 timesteps (read). It transpired that the write property did not hold due to a design bug in the Verilog code. A counterexample for the reduced model was found by the property checkers and recomputed by the prototype into a counterexample for the original design, whereupon the bug was fixed by the designers and the property was again checked on the corrected design (write fail, write hold). All runtimes on the reduced models were compared to those achieved on the original design without preprocessing. The results are given in CPU seconds (respectively minutes) and are shown in <figref idref="f0010">Figure 9</figref>.

0076The present invention provides a significant reduction in the different sizes of the design models and a tremendous drop in the runtimes of the property checkers. Design sizes could be reduced to approximately 30% of the original sizes, and runtimes dropped from between half and three quarters of an hour to minutes or even seconds. Note, in particular, that the computation times the prototype took to analyse the designs and generate the reduced models, ranging between 3 and 7 seconds, are negligible compared to the runtimes of the property checkers.

0077<figref idref="f0011 f0012 f0013 f0014 f0015 f0016 f0017 f0018 f0019">Figures 10-18</figref> show flow charts for granularity analysis, minimal width abstraction, model generation, together with three corresponding examples.

0078Reduced runtimes and a reduced requirement for memory needed in computations is one requirement to match today's sizes of designs in hardware verification. The present invention provides an abstraction technique which, given a high-level circuit and a property specification, scales down the design by reducing the widths of input, output and internal signals. The method provides a one-to-one abstraction, which yields minimal models with respect to the minimality statement we have given. If a property fails, counterexamples for the original design can be computed from counterexamples for the reduced model. Pre- and post-processing of design and counterexample and the property checking process itself are strictly separated. The proposed method is independent of the system realization of the property checker and can be combined with a variety of existing verification techniques which take RTL netlists as input, no matter if the underlying prover engines operate on bit-level (like SAT or BDD-based approaches), or use high-level techniques (e.g. Integer Linear Programming, Arithmetic Constraint Solving). The approach is particularly well suited to SAT and BDD-based hardware verification, since the complexity of those techniques depends on the number of variables such provers have to deal with.

0079In known SAT and BDD-based circuit verification such variables are created (at least) for each single bit of each signal of the circuit. In Bounded Property Checking even multiple instances of each variable and each signal have to be created for each step of the considered interval of time. In practice, design sizes range from several thousands up to 2 - 5 million gates and typical bounded properties incorporate 2 - 30 timesteps depending on the field of application.

Appendix

Algorithm 2

Reduced Model Generation

0080<ul id="ul0005" list-style="none" compact="compact"><li>1 for each bitvector variable <i>x_[n]</i> {</li><li>2 <i>m</i> :=0;</li><li>3 for each chunk <i>x_[n]</i>(<i>j,i</i>) of the computed granulartiy of <i>x_[n]</i> {</li><li>4 <i>C := find</i> (<i>x_[n]</i>(<i>j,i</i>)); // equivalence class containing <i>x_[n]</i>(<i>j,I</i>)</li><li>5 <i>m</i> := <i>m</i> + ϕ(<i>C</i>);</li><li>6 }</li><li>7 if (<i>m</i>≥<i>n</i>) <b>then</b><i>m</i> := <i>n</i>;</li><li>8 replace all occurrences of <i>x_[n]</i> of bitvector equations by <i>x'_[m]</i></li><li>9 and adjust all extraction expressions affected by <i>x_[n]</i>;</li><li>10}</li></ul>