Digital circuit verification

Details Digital circuit verification Digital circuit verification

1999-09-23

2003-04-22

Beausoliel, Robert (Department: 2184)

Error detection/correction and fault detection/recovery

Data processing system error or fault handling

Reliability and availability

C714S033000, C714S724000, C714S741000, C703S013000, C703S014000, C703S015000, C703S016000, C716S030000, C716S030000

Reexamination Certificate

active

06553514

ABSTRACT:

BACKGROUND
1. Field of the Present Invention
The present invention relates to the field of logic design verification and more particularly to a method for extending the verification coverage achieved with traditional non-formal verification techniques such as simulation.
2. History of Related Art
Verification of digital hardware is generally accomplished by a simulation technique in which a given set of input test vectors is applied to a model of the circuit to be verified. Traditional simulation, however, is significantly limited in its ability to completely verify complex hardware. The number of states, state transitions, and state transition sequences associated with any particular digital circuit all increase exponentially as the model size, calculated in terms of the number of latches comprising the model, increases linearly. Referring to
FIG. 1
, a state transition diagram
100
representing various states and transition paths between the various states for a given logic design is presented where a transition path is defined as a sequence of one or more transitions and a transition is defined as a single step from a present state to a next state under control of the present input. State transition diagram
100
includes an initial state
102
a
and multiple transition paths
104
a
,
104
b
, and
104
c
, leading from initial transition state
102
a
to next transition states
102
b
,
102
c
, and
102
d
. Each of the states
102
b
,
102
c
, and
102
d
can transition to other states indicated in transition table
100
through the various transition paths. It will be appreciated by those skilled in the field of digital hardware design that state transition diagram
100
of
FIG. 1
is a grossly simplified representation of the state machines contemplated by complex digital circuitry. It will be further appreciated that the number of transition states
102
and, correspondingly, the number of transition paths
104
increases exponentially with the number of latches, such that even a moderately complex circuit comprised of, for example, 1000 latches can assume 2
1000
or roughly 10
300
states. Traditionally, conventional simulation techniques verify a given digital circuit in a depth-first fashion. As an example, a simulation technique might attempt to verify the digital circuit represented by state diagram
100
by applying a sequence of inputs to a model of the digital circuit and recording the transition paths that the model follows. Thus, for example, a given simulation trace may follow the digital circuit from an initial state
102
a
through intermediate states
102
c
and
102
e
to a final state
102
f
via transition paths
104
b
,
104
d
and
104
e
. If any rules or specifications with which the digital circuit must comply are violated along the transition path indicated from initial state
102
a
to final state
102
f
, the simulation trace indicated will identify the violation. As the number of states and transition paths increases exponentially with the number of latches in the circuit, achieving any significant coverage of the total number of available transition paths quickly becomes exceedingly difficult using conventional simulation techniques because each simulation run exposes only a single transition path. Circuit simulation is commonly referred to as a non-formal verification technique to emphasize the limited coverage achieved using such a technique. At the other end of the verification spectrum, formal verification tools and techniques are used to rigorously verify that an implantation satisfies a given specification or set of rules. Typically, a formal verification technique utilizes a breadth-first approach in which each possible transition path from a given transition state is verified before proceeding to another state (or set of states) in the machine. In the depiction of
FIG. 1
, for example, a formal verification technique might begin by verifying transition paths
104
a
,
104
b
, and
104
c
with respect to state
102
a
before proceeding to the second “tier” of states including states
102
b
,
102
c
, and
102
d
. After verifying each transition path
104
leading from the second tier of states, a formal verification tool might verify each transition path extending from the second tier of states to the third tier, and so forth. In this manner, a formal verification technique verifies essentially every permitted combination of transitions in state diagram
100
. While formal verification tools and techniques obviously enjoy the advantage of the greatest possible coverage of the digital circuit being verified, it will be readily appreciated that the computational load contemplated by a full formal verification of a digital circuit with any significant complexity can quickly become overwhelming. Typically, therefore, formal verification tools are utilized in conjunction with an environment that is associated with the design to be verified. A model, such as an HDL model is imported into a formal verification tool such as a model checker. A verification engineer then constructs an environment around the design consisting of a variety of input constraints associated with the circuit. In addition, a set of properties or rules to be verified is supplied to the formal verification tool. The verification tool will then extract the full state transition table for the design limited by the environmental constraints. While this type of formal verification provides the desirable level of verification coverage, the construction of the environment around the design is a manually intensive, arduous, and time consuming process. It is therefore highly desirable to implement a verification technique striking a reasonable compromise between the limited coverage afforded by conventional simulation techniques and the expense and time consumed by formal verification methods.
SUMMARY OF THE INVENTION
The problems identified above are in large part addressed by a verification method according to the present invention in which a conventional non-formal verification tool is utilized to generate information from which a partial state transition diagram of the circuit to be verified can be extracted. A formal verification tool such as a model checker is then used to achieve formal verification of the portion of the circuit represented by the extracted state transition information. By combining non-formal with formal verification techniques, the invention is able to achieve additional verification coverage over the coverage provided by traditional simulation with only an incremental increase in the amount of time and expense required to generate the simulation.
Broadly speaking, the present invention contemplates the use of a two stage verification process in which the second stage augments verification coverage obtained by the first stage in an automatic fashion. In the first stage, state transition information is extracted from the output of a non-formal verification technique. A formal verification tool is then applied to the extracted state transition information to extend the verification coverage of the digital circuit beyond the coverage that is achieved using the first verification technique. In one embodiment, the method includes the initial step of applying a first verification technique such as a simulation technique to a model of the digital circuit. In one embodiment, the information from which the state transition information is extracted includes an all events trace that is produced by executing a set or plurality of simulation runs using the simulation tool or technique. In the preferred embodiment, the application of the formal verification tool comprises applying a model checker to the extracted state transition data to achieve a formal verification of the state machine represented by the state transition diagram. In one embodiment, the extracted state transition information includes a set of data points each representing a present state, a present input, and a next state. Preferably, the state transition information is sorted by the present state

Affiliated with

Also associated with

Rating

Digital circuit verification does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Digital circuit verification, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Digital circuit verification will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-3010247