Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
2000-10-02
2003-07-08
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
C716S030000, C716S030000
Reexamination Certificate
active
06591403
ABSTRACT:
FIELD OF THE INVENTION
The presented invention relates generally to the use of hardware description languages to specify circuit logic design in a format that is acceptable to logic synthesis tools, and, more particularly, to a system and method for unifying the specification of design constraints and properties using a hardware description language (HDL) independent assertion format.
BACKGROUND OF THE INVENTION
Hardware logic design is preferably tested prior to manufacture. The objective of design verification is to ensure that a design's implementation satisfies the requirements of its specification. Design analysis enables the design engineer to uncover errors at a point of the design phase where they will still be relatively inexpensive to fix. In order to make verification and analysis of logic design economically feasible, it is desirable to dramatically reduce the cost of design specification and automate the analysis process.
Design engineers traditionally verify their design using a black-box testing approach in which the engineer will first create a model of the design written in a hardware description language (HDL), such as Verilog [IEEE 1364-1995] or VHDL [IEEE 1076-1993]; the design model is often referred to as the device-under-test (DUT) in a verification process. The engineer will then create a model of the design environment, referred to as a testbench, which will include or instantiate a copy of the DUT. The testbench is responsible for driving stimulus, i.e., logical one and zero values, into the DUT. In addition, the testbench provides the means for observing and validating the output response values from the DUT. The specification defines the values or sequences of values permitted by the DUT.
One problem with using a black-box testing approach to validate proper design behavior is that it is limited to observing output ports of the DUT. The DUT might exhibit improper internal behavior, such as if a state machine violates its one-hot property (meaning that only one bit is actively high after a reset), but still have proper output response values because the design error is not directly observable on the output ports. This might be due to the current set of input stimulus, when applied to the DUT, impeding the internal problem from propagating to an output port. Given a different set of input stimulus the internal error might be observable. Hence, validating all internal properties of a design using black-box testing techniques is often impractical, particularly as design size increases.
White-box testing is an alternative technique for validating properties of a design. This technique creates test monitors and checkers on internal points within the DUT, resulting in an increase in observable behavior during testing. The previous assertion that a state machine within the DUT is always one-hot can be validated by adding an internal checker to directly monitor each register bit of the state machine. Thus, if the one-hot property is violated, the error is instantly isolated to the problem. This overcomes the problem of black-box testing possibly missing an internal error (for a given input stimuli) by only observing DUT output responses.
There currently exist several types of design verification and analysis tools for validating correct functional design intent. This set of tools includes logic simulation tools, testbench generation tools, formal verification tools, and semi-formal verification tools. Logic simulation tools are used to model and validate design behavior responses for a given set of input stimuli or test vectors; of course, the results obtained using logic simulation tools are only as good as the quality of the set of input stimuli used. Testbench generation tools are used to generate design input stimuli and specify events and assertions for validation in their proprietary languages. So-called formal tools include state-space exploration, static property checker and model checker tools that validate user-specified properties using static and formal techniques without test vectors. Formal tools are heavily proof driven and mathematical in approach. Semi-formal verification tools, such as amplification tools, combine traditional simulation techniques with formal state-space exploration and model checking techniques. The mathematical proofs of the formal tool approach are employed with a limited or bounded search at certain times during the verification process.
One way of specifying a design's functional intent, expressed by the properties of the design, is to create a set of design assertions representative of the logic design. As an example, consider that a possible design assertion is that a state machine's encoding is always “one-hot” after a reset, meaning that only one bit of a collection of bits is actively high at a time. If the state machine violates the one-hot assertion following a reset, then the logic design is flawed in some way.
In discussing design assertions, it is helpful to understand both verification events and design assertions. A verification event may be defined as an HDL expression, which evaluates to a TRUE value. For example, if the expression (c_ready==1 && c_reset!=1) evaluates TRUE, then an event has occurred in the verification environment. An assertion is defined as a property of a design, and may be classified as either static or temporal A static assertion is an event that must be TRUE for all time. A temporal assertion has a time relationship of events associated with it, whose correct sequence must be TRUE. For example, a temporal assertion can be viewed as an event-triggered window, bounding a specific property, i.e., an event.
The following examples illustrate aspects of both temporal and static assertions, and combinations thereof.
FIG. 1
illustrates an assertion for an invariant property. The property (i.e., event P) in this example is always valid after Event 1 occurs, and continues to be to be TRUE until Event 2 occurs.
FIG. 2
illustrates an assertion for a liveness property. The event P, in this example, must eventually be valid after the first event-trigger occurs and before the second event-trigger occurs. In this example, a property of the design is invalid if event P does not occur within the specified event-triggered window.
In addition to static and temporal, an assertion can also be classified as either a constraint or a property, depending upon where the assertion is made. A constraint may be thought of as a range of allowable values. An assertion made on an input port of the design model being verified, referred to as the DUT, is an example of a constraint because it bounds the input stimulus to permissible operating values for that particular input port. The DUT cannot be guaranteed to operate correctly if its input stimulus violates a specified constraint. A property may be thought of as expected behavior in response to defined stimuli (constraints). An assertion made on an output port of a DUT, or an internal point in the design, is an example of a property. For any permissible sequence of input values applied to the DUT, the properties of the design will not be violated if the design is functionally correct. It is noted that the term “property”, as used herein, may be used to refer to a property assertion as well as a constraint assertion.
There are several techniques currently available for specifying the assertions, or properties, of a logic design. VHDL [IEEE 1076-1993] provides a language construct for specifying a static invariant assertion. For example:
assert event
report message
severity level
The assert statement can be used as an internal checker during the course of simulation; this is an example of white-box testing.
Unfortunately, VHDL does not provide any constructs for specifying temporal assertion or fiveness properties. In addition, with the exception of logic simulators, commercial verification tools such as property checkers, model checkers and semiformal verification tools will not use the VHDL
Bass Bradley Forrest
Foster Harry David
Hewlett--Packard Development Company, L.P.
Smith Matthew
Thompson A. M.
LandOfFree
System and method for specifying hardware description... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with System and method for specifying hardware description..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and System and method for specifying hardware description... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3058378