Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2002-01-08
2004-04-27
Siek, Vuthe (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000
Reexamination Certificate
active
06728939
ABSTRACT:
FIELD OF THE INVENTION
The 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 OF THE INVENTION
Today'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.
Abstraction 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.
D. Cyrluk et al present a word-level decision procedure for the core theory of bit-vectors with extraction and concatenation in “An efficient decision procedure for the theory of fixed sized bit-vectors” (CAV-97), pages 60 to 71, 1997, using bit-vector BDDs and applying width abstraction to the core theory.
OBJECT OF THE INVENTION
The present invention seeks to provide an improved circuit verification procedure.
STATEMENT OF THE INVENTION
In accordance with a first aspect of the invention, there is provided a digital circuit design verification method wherein, prior to a property checking process for each property of a non-reduced RTL model, a reduced RTL model is determined, which reduced RTL model retains specific signal properties of a non-reduced RTL model which are to be checked.
Conveniently 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, synthesizing an RTL netlist of high level primitives, whereby the circuit is defined as an interconnection of control and data path portions, wherein signals of a width n are determined such that n &egr; N
+
, wherein bitvectors of respective length determine the signal value and N
+
represents the natural numbers (excluding 0). i.e. 1, 2, 3, . . . 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.
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.
In 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, which reduced width RTL model retains the specific signal property of a non-reduced RTL model.
Preferably 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
n &egr;
+
; 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
Dinh Paul
Siek Vuthe
Siemens Aktiengesellschaft
Staas & Halsey , LLP
LandOfFree
Method of circuit verification in digital design does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Method of circuit verification in digital design, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method of circuit verification in digital design will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3214593