High-level design verification of microprocessors via error modeling.
A design verification methodology for microprocessor hardware based on  modeling design errors and generating simulation vectors for the modeled errors via physical fault testing techniques is presented. We have systematically collected design error data from a number of microprocessor design projects. The error data is used to derive error models suitable for design verification testing. A class of basic error models is identified and shown to yield tests that provide good coverage of common error types. To improve coverage for more complex errors, a new class of conditional error models is introduced. An experiment to evaluate the effectiveness of our methodology is presented. Single actual design errors are injected into a correct design, and it is determined if the methodology  will generate a test that detects the actual errors. The experiment has been conducted for two microprocessor designs and the results indicate that very high coverage of actual design errors can be obtained with test sets that are complete for a small number of synthetic error models.
INTRODUCTION
It is well known that about a third of the cost of developing a new microprocessor is devoted
to hardware debugging and testing [25]. The inadequacy of existing hardware verification
methods is graphically illustrated by the Pentium's FDIV error, which cost its manufacturer
an estimated $500 million. The development of practical verification methodologies
for hardware verification has long been handicapped by two related problems: (1) the
A preliminary version of this paper was presented in [4] at the 1997 IEEE International High Level
Design Validation and Test Workshop, Oakland, California, November 14-15, 1997.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is
granted without fee provided that copies are not made or distributed for profit or direct commercial
advantage and that copies show this notice on the first page or initial screen of a display along with
the full citation. Copyrights for components of this work owned by others than ACM must be hon-
ored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, to
redistribute to lists, or to use any component of this work in other works, requires prior specific permission
and/or a fee. Permissions may be requested from Publications Dept., ACM Inc., 1515
Broadway, New York, NY 10036 USA, fax +1 (212) 869-0481, or permissions@acm.org. - 1998
by the Association for Computing Machinery, Inc.
Al-Asaad, J. P. Hayes, T. Mudge, and R. B. Brown
lack of published data on the nature, frequency, and severity of the design errors occurring
in large-scale design projects; and (2) the absence of a verification methodology whose effectiveness
can readily be quantified.
There are two broad approaches to hardware design verification: formal and simula-
tion-based. Formal methods try to verify the correctness of a system by using mathematical
proofs [32]. Such methods implicitly consider all possible behavior of the models
representing the system and its specification, whereas simulation-based methods can only
consider a limited range of behaviors. The accuracy and completeness of the system and
specification models is a fundamental limitation for any formal method.
Simulation-based design verification tries to uncover design errors by detecting a cir-
cuit's faulty behavior when deterministic or pseudo-random tests (simulation vectors) are
applied. Microprocessors are usually verified by simulation-based methods, but require an
extremely large number of simulation vectors whose coverage is often uncertain.
Hand-written test cases form the first line of defense against bugs, focusing on basic
functionality and important corner (exceptional) cases. These tests are very effective in the
beginning of the debug phase, but lose their usefulness later. Recently, tools have been
developed to assist in the generation of focused tests [13,20]. Although these tools can significantly
increase design productivity, they are far from being fully automated.
The most widely used method to generate verification tests automatically is random test
generation. It provides a cheap way to take advantage of the billion-cycles-a-day simulation
capacity of networked workstations available in many big design organizations.
Sophisticated systems have been developed that are biased towards corner cases, thus
improving the quality of the tests significantly [2]. Advances in simulator and emulator
technology have enabled the use of very large sets as test stimuli such as existing application
and system software. Successfully booting the operating system has become a basic
quality requirement [17,25].
Common to all the test generation techniques mentioned above is that they are not targeted
at specific design errors. This poses the problem of quantifying the effectiveness of a
test set, such as the number of errors covered. Various coverage metrics have been proposed
to address this problem. These include code coverage metrics from software testing
[2,7,11], finite state machine coverage [20,22,28], architectural event coverage [22], and
observability-based metrics [16]. A shortcoming of all these metrics is that the relationship
between the metric and the detection of classes of design errors is not well understood

A different approach is to use synthetic design error models to guide test generation.
This exploits the similarity between hardware design verification and physical fault test-
ing, as illustrated by Figure 1. For example, Al-Asaad and Hayes [3] define a class of
design error models for gate-level combinational circuits. They describe how each of these
errors can be mapped onto single-stuck line (SSL) faults that can be targeted with standard
automated test pattern generation (ATPG) tools. This provides a method to generate tests
with a provably high coverage for certain classes of modeled errors.
A second method in this class stems from the area of software testing. Mutation testing
[15] considers programs, termed mutants, that differ from the program under test by a single
small error, such as changing the operator from add to subtract. The rationale for the
approach is supported by two hypotheses: 1) programmers write programs that are close to
High-Level Design Verification of Microprocessors via Error Modeling - 3
correct ones, and 2) a test set that distinguishes a program from all its mutants is also sensitive
to more complex errors. Although considered too costly for wide-scale industrial
use, mutation testing is one of the few approaches that has yielded an automatic test generation
system for software testing, as well as a quantitative measure of error coverage
(mutation score) [24]. Recently, Al Hayek and Robach [5] have successfully applied mutation
testing to hardware design verification in the case of small VHDL modules.
This paper addresses design verification via error modeling and test generation for
complex high-level designs such as microprocessors. A block diagram summarizing our
methodology is shown in Figure 2. An implementation to be verified and its specification
are given. For microprocessors, the specification is typically the instruction set architecture
(ISA), and the implementation is a description of the new design in a hardware
description language (HDL) such as VHDL or Verilog. In this approach, synthetic error
models are used to guide test generation. The tests are applied to simulated models of both
the implementation and the specification. A discrepancy between the two simulation outcomes
indicates an error, either in the implementation or in the specification.
Section 2 describes our method for design error collection and presents some preliminary
design error statistics that we have collected. Section 3 discusses design error modeling
and illustrates test generation with these models. An experimental evaluation of our
methodology and of the error models is presented in Section 4. Section 5 discusses the
results and gives some concluding remarks.
2. DESIGN ERROR COLLECTION
Hardware design verification and physical fault testing are closely related at the conceptual
level [3]. The basic task of physical fault testing (hardware design verification) is to generate
tests that distinguish the correct circuit from faulty (erroneous) ones. The class of faulty
Prototype
system
Operational
system
Design
Manufacturing
Verification
tests
Physical
fault tests
Design errors Physical faults
Design development Field deployment
model Fault model


1. Correspondence between design verification and physical fault testing.
residual
design errors
D. Van Campenhout, H. Al-Asaad, J. P. Hayes, T. Mudge, and R. B. Brown
circuits to be considered is defined by a logical fault model. Logical fault models represent
the effect of physical faults on the behavior of the system, and free us from having to deal
with the plethora of physical fault types directly. The most widely used logical fault model,
the SSL model, combines simplicity with the fact that it forces each line in the circuit to be
exercised. Typical hardware design methodologies employ hardware description languages
as their input medium and use previously designed high-level modules. To capture the richness
of this design environment, the SSL model needs to be supplemented with additional
error models.
The lack of published data on the nature, frequency, and severity of the design errors
occurring in large-scale projects is a serious obstacle to the development of error models
for hardware design verification. Although bug reports are collected and analyzed internally
in industrial design projects the results are rarely published. Examples of user-oriented
bug lists can be found in [21,26]. Some insight into what can go wrong in a large
processor design project is provided in [14].
The above considerations have led us to implement a systematic method for collecting
design errors. Our method uses the CVS revision management tool [12] and targets ongoing
design projects at the University of Michigan, including the PUMA high-performance
microprocessor project [9] and various class projects in computer architecture and VLSI


2. Deployment of proposed design verification methodology.
Design error
models
Test
generator
Implementation
simulator
Specification
simulator
Equal?
Diagnose
Specification
Unverified
design
Verified
design
CVS
revision
database
Unknown actual error
Assisted
verification
Assisted
verification
High-Level Design Verification of Microprocessors via Error Modeling - 5
design, all of which employ Verilog as the hardware description medium. Designers are
asked to archive a new revision via CVS whenever a design error is corrected or whenever
the design process is interrupted, making it possible to isolate single design errors. We
have augmented CVS so that each time a design change is entered, the designer is
prompted to fill out a standardized multiple-choice questionnaire, which attempts to gather
four key pieces of information: (1) the motivation for revising the design; (2) the method
by which a bug was detected; (3) a generic design-error class to which the bug belongs,
and (4) a short narrative description of the bug. A uniform reporting method such as this
greatly simplifies the analysis of the errors. A sample error report using our standard questionnaire
is shown in Figure 3. The error classification shown in the report form is the
result of the analysis of error data from several earlier design projects.
Design error data has been collected so far from four VLSI design class projects that
involve implementing the DLX microprocessor [19], from the implementation of the LC-2
microprocessor [29] which is described later, and from preliminary designs of PUMA's
fixed-point and floating-point units [9]. The distributions found for the various representative
design errors are summarized in Table 1. Error types that occurred with very low frequency
are combined in the "others" category in the table.
(replace the _ with X where
MOTIVATION:
correction
_ design modification
_ design continuation
_ performance optimization
_ synthesis simplification
_ documentation
BUG DETECTED BY:
_ inspection
_ compilation
simulation
_ synthesis
Please try to identify the primary
source of the error. If in doubt,
check all categories that apply.
_ verilog syntax error
_ conceptual error
combinational logic:
wrong signal source
_ missing input(s)
_ unconnected (floating) input(s)
_ unconnected (floating)
_ conflicting outputs
_ wrong gate/module type
_ missing instance of gate/module
_ sequential logic:
_ extra latch/flipflop
_ missing latch/flipflop
_ extra state
_ missing state
_ wrong next state
_ other finite state machine error
_ statement:
_ if statement
_ case statement
_ always statement
_ declaration
_ port list of module declaration
_ expression (RHS of assignment):
_ missing term/factor
_ extra term/factor
_ missing inversion
_ extra inversion
_ wrong operator
_ wrong constant
_ completely wrong
_ buses:
_ wrong bus width
_ wrong bit order
_ new category (describe below)
Used wrong field from instruction


3. Sample error report.
6 - D. Van Campenhout, H. Al-Asaad, J. P. Hayes, T. Mudge, and R. B. Brown
3. ERROR MODELING
Standard simulation and logic synthesis tools have the side effect of detecting some design
error categories of Table 1, and hence there is no need to develop models for those particular
errors. For example a simulator such as Verilog-XL [10] flags all Verilog syntax errors
(category 9), declaration statement errors (category 12), and incorrect port lists of modules
(category 16). Also, logic synthesis tools, such as those of Synopsys, usually flag all wrong
bus width errors (category 10) and sensitivity-list errors in the always statement (category
13).
To be useful for design verification, error models should satisfy three requirements: (1)
tests (simulation vectors) that provide complete coverage of the modeled errors should
also provide very high coverage of actual design errors; (2) the modeled errors should be
amenable to automated test generation; (3) the number of modeled errors should be relatively
small. In practice, the third requirement means that error models that define a number
of error instances linear, or at most quadratic in the size of the circuit are preferred.
The error models need not mimic actual design bugs precisely, but the tests derived from
complete coverage of modeled errors should provide very good coverage of actual design
bugs.
3.1 Basic error models
A set of error models that satisfy the requirements for the restricted case of gate-level logic
circuits was developed in [3]. Several of these models appear useful for the higher-level
(RTL) designs found in Verilog descriptions as well. From the actual error data in Table 1,
we derive the following set of five basic error models:


1. Actual error distributions from three groups of design projects.
Design error category
Relative frequency [%]
1. Wrong signal source 29.9 28.4 25.0
2. Conceptual error 39.0 19.1 0.0
3. Case statement
4. Gate or module input 11.2 9.8 0.0
5. Wrong gate/module type 12.1
6. Wrong constant 0.4 5.7 10.0
7. Logical expression wrong
8. Missing input(s) 0.0 5.2 0.0
9. Verilog syntax error
10. Bit width error 0.0 2.2 15.0
11. If statement 1.1 1.6 5.0
12. Declaration statement
13. Always statement 0.4 1.4 5.0
14. FSM error 3.1
15. Wrong operator 1.7 0.3 0.0
16. Others 1.1 5.8 25.0
High-Level Design Verification of Microprocessors via Error Modeling - 7
. Bus SSL error (SSL): A bus of one or more lines is (totally) stuck-at-0 or stuck-at-
1 if all lines in the bus are stuck at logic level 0 or 1. This generalization of the
standard SSL model was introduced in [6] in the context of physical fault testing.
Many of the design errors listed in Table 1 can be modeled as SSL errors
(categories 4 and 6).
. Module substitution error (MSE): This refers to mistakenly replacing a module by
another module with the same number of inputs and outputs (category 5). This
class includes word gate substitution errors and extra/missing inversion errors.
. Bus order error (BOE): This refers to incorrectly ordering the bits in a bus
(category 16). Bus flipping appears to be the most common form of BOE.
. Bus source error (BSE): This error corresponds to connecting a module input to a
wrong source (category 1).
. Bus driver error (BDE): This refers to mistakenly driving a bus with two sources
(category 16).
Direct generation of tests for the basic error models is difficult, and is not supported by
currently available CAD tools. While the errors can be easily activated, propagation of
their effects can be difficult, especially when modules or behavioral constructs do not have
transparent operating modes. In the following we demonstrate manual test generation for
various basic error models.
3.2 Test generation examples
Because of their relative simplicity, the foregoing error models allow tests to be generated
and error coverage evaluated for RTL circuits of moderate size. We analyzed the test requirements
of two representative combinational circuits: a carry-lookahead adder and an
ALU. Since suitable RTL tools are not available, test generation was done manually, but in
a systematic manner that could readily be automated. Three basic error models are consid-
ered: BOEs, MSEs, and BSEs. Test generation for SSLs is discussed in [1,6] and no tests
are needed for BDEs, since the circuits under consideration do not have tristate buses.
Example 1: The 74283 adder
An RTL model [18] of the 74283 4-bit fast adder [30] appears in Figure 4. It consists of a
carry-lookahead generator (CLG) and a few word gates. We show how to generate tests for
some design error models in the adder and then we discuss the overall coverage of the targeted
error models.
BOE on A bus: A possible bus value that activates the error is A
an unknown value. The erroneous value of A is thus A Hence, we can represent
the error by represents the error signal which is 1 (0)
in the good circuit and 0 (1) in the erroneous circuit. One way to propagate this error
through the AND gate G 1 is to set Hence, we get G
and G Now for the module CLG we have
X. The resulting outputs are This implies that
hence the error is not detected at the primary outputs. We need to assign more input values
to propagate the error. If we set C
DXXD
DXXD
DXXD
8 - D. Van Campenhout, H. Al-Asaad, J. P. Hayes, T. Mudge, and R. B. Brown
Hence, the error is propagated to S and the complete test vector is (A, B, C
(0XX11XX10).
On generating tests for all BSEs in the adder we find that just 2 tests detect all 33
detectable BSEs, and a single BSE is redundant as shown above. We further targeted all
MSEs in the adder and we found that 3 tests detect all 27 detectable MSEs and proved that
a single MSE (G 3 /XNOR) is redundant. Finally, we found that all BOEs are detected by
the tests generated for BSEs and MSEs. Therefore, complete coverage of BOEs, BSEs,
and MSEs is achieved with only 5 tests.
Example 2: The c880 ALU
In this example, we try to generate tests for some modeled design errors in the c880 ALU,
a member of the ISCAS-85 benchmark suite [8]. A high-level model based on a Verilog
description of the ALU [23] is shown in Figure 5; it is composed of six modules: an adder,
two multiplexers, a parity unit, and two control units. The circuit has 60 inputs and 26 out-
puts. The gate-level implementation of the ALU has 383 gates.
The design error models to be considered in the c880 are again BOEs, BSEs, and MSEs
(inversion errors on 1-bit signals). We next generate tests for these error models.
BOEs: In general, we attempt to determine a minimum set of assignments needed to detect
each error. Some BOEs are redundant such as the BOE on B (PARITY), but most BOEs
are easily detectable. Consider, for example, the BOE on D. One possible way to activate
the error is to set To propagate the error to a primary output, the path
through IN-MUX and then OUT-MUX is selected. The signal values needed to activate this
path are:
Solving the gate-level logic equations for G and C we get:
All signals not mentioned in the above test have don't care values. We found that just 10
tests detect all 22 detectable BOEs in the c880 and serve to prove that another 2 BOEs are
redundant.


4. High-level model of the 74283 carry-lookahead adder [18].
A
G
High-Level Design Verification of Microprocessors via Error Modeling - 9
MSEs: Tests for BOEs detect most, but not all, inversion errors on multibit buses. In the
process of test generation for the c880 ALU, we noticed a case where a test for an inversion
error on bus A can be found even though the BOE on A is redundant. This is the case when
an n-bit bus (n odd) is fed into a parity function. Testing for inversion errors on 1-bit signals
needs to be considered explicitly, since a BOE on a 1-bit bus is not possible. Most inversion
errors on 1-bit signals in the c880 ALU are detected by the tests generated for BOEs and
BSEs. This is especially true for the control signals to the multiplexers.
3.3 Conditional error model
The preceding examples, as well as prior work on SSL error detection [1,6], show that the
basic error models can be used with RTL circuits, and that high, but not complete, error
coverage can be achieved with small test sets. These results are further reinforced by our
experiments on microprocessor verification (Section which indicate that a large fraction
of actual design errors (67% in one case and 75% in the other) is detected by complete test
sets for the basic errors. To increase coverage of actual errors to the very high levels needed
for design verification, additional error models are required to guide test generation. Many
more complex error models can be derived directly from the actual data of Table 1 to supplement
the basic error types, the following set being representative:
. Bus count error (BCE): This corresponds to defining a module with more or fewer
input buses than required (categories 4 and 8).


5. High-level model of the c880 ALU.
IN-MUX OUT-MUX
A
G
Cin
C Cont
ParA
ParB
F
Par-Hi
Par-Al
Par-Bl
Pass-B
Usel-G Cout
GEN
ADDER
Pass-H
F-add
F-and
F-xor
Al-Asaad, J. P. Hayes, T. Mudge, and R. B. Brown
. Module count error (MCE): This corresponds to incorrectly adding or removing
a module (category 16), which includes the extra/missing word gate errors and the
extra/missing registers.
. Label count error (LCE): This error corresponds to incorrectly adding or
removing the labels of a case statement (category 3).
. Expression structure error (ESE): This includes various deviations from the
correct expression (categories 3, 6, 7, 11, 15), such as extra/missing terms, extra/
missing inversions, wrong operator, and wrong constant.
. State count error (SCE): This error corresponds to an incorrect finite state
machine with an extra or missing state (category 14).
. Next state error (NSE): This error corresponds to incorrect next state function in
a finite state machine (FSM) (category 14).
Although, this extended set of error models increases the number of actual errors that
can be modeled directly, we have found them to be too complex for practical use in manual
or automated test generation. We observed that the more difficult actual errors are
often composed of multiple basic errors, and that the component basic errors interact in
such a way that a test to detect the actual error must be much more specific than a test to
detect any of the component basic errors. Modeling these difficult composite errors
directly is impractical as the number of error instances to be considered is too large and
such composite modeled errors are too complex for automated test generation. However,
as noted earlier, a good error model does not necessarily need to mimic actual errors accu-
rately. What is required is that the error model necessitates the generation of these more
specific tests. To be practical, the complexity of the new error models should be comparable
to that of the basic error models. Furthermore the (unavoidable) increase in the number
of error instances should be controlled to allow trade-offs between test generation effort
and verification confidence. We found that these requirements can be combined by augmenting
the basic error models with a condition.
A conditional error (C,E) consists of a condition C and a basic error E; its interpretation
is that E is only active when C is satisfied. In general, C is a predicate over the signals
in the circuit during some time period. To limit the number of error instances, we restrict C
to a conjunction of terms , where y i is a signal in the circuit and w i is a constant of
the same bit-width as y i and whose value is either all-0s or all-1s. The number of terms
(condition variables) appearing in C is said to be the order of (C,E). Specifically, we consider
the following conditional error types:
. Conditional single-stuck line (CSSLn) error of order n;
. Conditional bus order error (CBOEn) of order n;
. Conditional bus source error (CBSEn) of order n.
When reduces to the basic error E from which it is
derived. Higher-order conditional errors enable the generation of more specific tests, but
lead to a greater test generation cost due to the larger number of error instances. For exam-
ple, the number of CSSLn errors on a circuit with N signals is . Although the
total set of all N signals we consider for each term in the condition can possibly be
reduced, CSSLn errors where n > 2 are probably not practical.
For gate-level circuits (where all signals are 1-bit), it can be shown that CSSL1 errors
High-Level Design Verification of Microprocessors via Error Modeling - 11
cover the following basic error models: MSEs (excluding XOR and XNOR gates), missing
2-input gate errors, BSEs, single BCEs (excluding XOR and XNOR gates), and bus driver
errors. That CSSL1 errors cover missing two-input gate errors can be seen as follows.
Consider a two-input AND gate Y=AND(X1,X2) in the correct design; in the erroneous
design, this gate is missing and net Y is identical to net X1. To expose this error we have to
set X1 to 1, X2 to 0, and sensitize Y. Any test that detects the CSSL1 error, (X2=0, Y s-a-0)
in the erroneous design, will also detect the missing gate error. The proof for other gate
types is similar. Higher-order CSSLn errors improve coverage even further.
4. COVERAGE EVALUATION
To show the effectiveness of a verification methodology, one could apply it and a competing
methodology to an unverified design. The methodology that uncovers more (and hard-
er) design errors in a fixed amount of time is more effective. However, for such a comparison
to be practical, fast and efficient high-level test generation tools for our error models
appear to be necessary. Although we have demonstrated such test generation in Section 3.2,
it has yet to be automated. We therefore designed a controlled experiment that approximates
the conditions of the original experiment, while avoiding the need for automated test
generation. The experiment evaluates the effectiveness of our verification methodology
when applied to two student-designed microprocessors. A block diagram of the experimental
set-up is show in Figure 6. As design error models are used to guide test generation, the
effectiveness is closely related to the synthetic error models used.
To evaluate our methodology, a circuit is chosen for which design errors are to be systematically
recorded during its design. Let D 0 be the final, presumably correct design.
From the CVS revision database, the actual errors are extracted and converted such that
they can be injected in the final design D 0 . In the evaluation phase, the design is restored to
an (artificial) erroneous state D 1 by injecting a single actual error into the final design D 0 .
This set-up approximates a realistic on-the-fly design verification scenario. The experiment
answers the question: given D 1 , can the proposed methodology produce a test that
determines D 1 to be erroneous? This is achieved by examining the actual error in D 1 , and
determining if a modeled design error exists that is dominated by the actual error. Let D 2
be the design constructed by injecting the dominated modeled error in D 1 , and let M be the
error model which defines the dominated modeled error. Such a dominated modeled error
has the property that any test that detects the modeled error in D 2 will also detect the
actual error in D 1 . Consequently, if we were to generate a complete test set for every error
defined on D 1 by error model M, D 1 would be found erroneous by that test set. Error detection
is determined as discussed earlier (see Section 1, Figure 2). Note that the concept of
dominance in the context of design verification is slightly different than in physical fault
testing. Unlike in the testing problem, we cannot remove the actual design error from D 1
before injecting the dominated modeled error. This distinction is important because generating
a test for an error of omission, which is generally very hard, becomes easy if given
instead of D 1 .
The erroneous design D 1 considered in this experiment is somewhat artificial. In reality
the design evolves over time as bugs are introduced and eliminated. Only at the very end
of the design process, is the target circuit in a state where it differs from the final design D 0
in just a single design error. Prior to that time, the design may contain more than one
Al-Asaad, J. P. Hayes, T. Mudge, and R. B. Brown
design error. To the extent that the design errors are independent, it does not matter if we
consider a single or multiple design errors at a time. Furthermore, our results are independent
of the order in which one applies the generated tests.
We implemented the preceding coverage-evaluation experiment for two small but representative
designs: a simple microprocessor and a pipelined microprocessor. We present
our results in the remainder of this section.
4.1 A simple microprocessor
The Little Computer 2 (LC-2) [29] is a small microprocessor of conventional design used
for teaching purposes at the University of Michigan. It has a representative set of 16 instructions
which is a subset of the instruction sets of most current microprocessors. To serve as
a test case for design verification, one of us designed behavioral and RTL synthesizable
Verilog descriptions for the LC-2. The behavioral model (specification) of the LC-2 consists
of 235 lines of behavioral Verilog code. The RTL design (implementation) consists of
a datapath module described as an interconnection of library modules and a few custom
modules, and a control module described as an FSM with five states. It comprises 921 lines
of Verilog code, excluding the models for library modules such as adders, register files, etc.
A gate-level model of the LC-2 can thus be obtained using logic synthesis tools. The design
errors made during the design of the LC-2 were systematically recorded using our error collection
system (Section 2).
For each actual design error recorded, we derived the necessary conditions to detect it.
An error is detected by an instruction sequence s if the external output signals of the
behavioral and RTL models are distinguished by s. We found that some errors are undetectable
since they do not affect the functionality of the microprocessor. The detection
conditions are used to determine if a modeled error that is dominated by the actual error


6. Experiment to evaluate the proposed design verification methodology.
Simulate Simulate
Actual error
database
Debug by
Design error
collection
Test for
modeled
error
Evaluation of verification methodology
Expose
modeled error
Expose
actual error
Design and debugging process
Design
Inject
single
actual
error
Inject
modeled
error
Design error
model
designer
Actual error
Modeled error
revisions
High-Level Design Verification of Microprocessors via Error Modeling - 13
can be found. An example where we were able to do that is shown in Figure 7. The error is
a BSE on data input D 1 of the multiplexer attached to the program counter PC. Testing for
detect the BSE since the outputs of PC and its incrementer are always
different, i.e., the error is always activated, so testing for this SSL error will propagate the
signal on D 1 to a primary output of the microprocessor. A case where we were not able to
find a modeled error dominated by the actual error is shown in Figure 8. The error occurs
where a signal is assigned a value independent of any condition. However, the correct
implementation requires an if-then-else construct to control the signal assignment. To activate
this error, we need to set ir_out[15:12] == 4'b1101, ir_out[8:6] - 3'b111, and
refers to the contents of the register i in the
register file. An instruction sequence that detects this error is shown in Figure 8.
We analyzed the actual design errors in both the behavioral and RTL designs of the LC-
2, and the results are summarized in Table 2. A total of 20 design errors were made during
the design, of which four errors are easily detected by the Verilog simulator and/or logic
synthesis tools and two are undetectable. The actual design errors are grouped by cate-
gory; the numbers in parentheses refer to the corresponding category in Table 1. The columns
in the table give the type of the simplest dominated modeled error corresponding to
each actual error. For example, among the 4 remaining wrong-signal-source errors, 2 dom-

7. An example of an actual design error that is dominated by an SSL error.
design Correct design
Incrementer
Incrementer
Mux
// Instruction decoding
// Decoding of register file
inputs
// 1- Decoding of
CORRECT CODE:
if (ir_out[15:12] == 4'b1101)
else
ERRONEOUS CODE:


8. An example of an actual design error for which no dominated modeled
error was found, and an instruction sequence that detects the actual error.
// Instruction sequence
@3000
main:
JSR sub0
sub0:
// After execution of instructions
correct design
Design error Test sequence
14 - D. Van Campenhout, H. Al-Asaad, J. P. Hayes, T. Mudge, and R. B. Brown
inate an SSL error and 2 dominate a BSE error.
We can infer from Table 2 that most errors are detected by tests for SSL errors or BSEs.
About 75% of the actual errors in the LC-2 design can be detected after simulation with
tests for SSL errors and BSEs. The coverage increases to 90% if tests for CSSL1 are
added.
4.2 A pipelined microprocessor
Our second design case study considers the well-known DLX microprocessor [19], which
has more of the features found in contemporary microprocessors. The particular DLX version
considered is a student-written design that implements 44 instructions, has a five-stage
pipeline and branch prediction logic, and consists of 1552 lines of structural Verilog code,
excluding the models for library modules such as adders, registerfiles, etc. The design errors
committed by the student during the design process were systematically recorded using
our error collection system.
For each actual design error we painstakingly derived the requirements to detect it.
detection was determined with respect to one of two reference models (specifica-
tions). The first reference model is an ISA model, and as such is not cycle-accurate: only
the changes made to the ISA-visible part of the machine state, that is, to the register file
and memory, can be compared. The second reference model contains information about
the microarchitecture of the implementation and gives a cycle-accurate view of the ISA-
visible part of the machine state (including the program counter). We determined for each
actual error whether it is detectable or not with respect to each reference model. Errors
undetectable with respect to both reference models may arise from the following two rea-
sons: (1) Designers sometimes make changes to don't care features, and log them as
errors. This happens because designers can have a more detailed specification (design
in mind than that actually specified. (2) Inaccuracies can occur when fixing an error
requires multiple revisions.
We analyzed the detection requirements of each actual error and constructed a modeled


2. Actual design errors and the corresponding dominated modeled errors for LC-2.
Actual errors
Corresponding dominated
modeled errors
Category Total
Easily
detected
Undetec-
table SSL BSE CSSL1
Un-
known
Wrong signal source (1) 4
Expression error (7) 4
Bit width error
Missing assignment
Wrong constant
Unused signal
Wrong module (5) 1
Always statement
Total
High-Level Design Verification of Microprocessors via Error Modeling - 15
error dominated by the actual error, wherever possible. One actual error involved multiple
signal source errors, and is shown in Figure 9. Also shown are the truth tables for the
immediately affected signals; differing entries are shaded. Error detection via fanout Y1
requires setting sensitizing Y1. However, the combination
not achievable and thus error detection via Y1 is not possible. Detection
via fanout Y2 or Y3 requires setting sensitizing Y2 or Y3.
However, blocks error propagation via Y2 further downstream. Hence, the error
detection requirements are: sensitizing Y3.
Now consider the modeled error . Activation of E 1 in D1 requires
sensitizing Y1, Y2 or Y3. As mentioned
before, blocks error propagation via Y2. But as E 1 can be exposed via Y1
without sensitizing Y3, E 1 is not dominated by the given actual error. To ensure detection
of the actual error, we can condition S0 s-a-0 such that sensitization of Y3 is required. The
design contains a signal jump_to_reg_instr that, when set to 1, blocks sensitization of Y1,
but allows sensitization of Y3. Hence the CSSL1 error
dominated by the actual error.
The results of this experiment are summarized in Table 3. A total of 39 design errors
were recorded by the designer. The actual design errors are grouped by category; the numbers
in parentheses refer again to Table 1. The correspondence between the categories is
imprecise, because of inconsistencies in the way in which different student designers classified
their errors. Also, some errors in Table 3 are assigned to a more specific category
than in Table 1, to highlight their correlation with the errors they dominate. 'Missing mod-
ule' and `wrong signal source' errors account for more than half of all errors. The column
headed 'ISA' indicates how many errors are detectable with respect to the ISA-model;
'ISAb' lists the number of errors only detectable with respect to the micro-architectural
reference model. The sum of 'ISA' and `ISAb' does not always add up the number given


9. Example of an actual design error in our DLX implementation.
D. Van Campenhout, H. Al-Asaad, J. P. Hayes, T. Mudge, and R. B. Brown
in 'Total'; the difference corresponds to actual errors that are not undetectable with respect
to either reference model. The remaining columns give the type of the simplest dominated
modeled error corresponding to each actual error. Among the 10 detectable 'missing mod-
ule(s)' errors, 2 dominate an SSL error, 6 dominate a CSSL1 error, and one dominates a
CBOE; for the remaining one, we were not able to find a dominated modeled error.
A conservative measure of the overall effectiveness of our verification approach is
given by the coverage of actual design errors by complete test sets for modeled errors.
From

Table

3 it can be concluded that for this experiment, any complete test set for the
inverter insertion errors (INV) also detects at least 21% of the (detectable) actual design
errors; any complete test set for the INV and SSL errors covers at least 52% of the actual
design errors; if a complete test set for all INV, SSL, BSE, CSSL1 and CBOE is used, at
least 94% of the actual design errors will be detected.
5. DISCUSSION
The preceding experiments indicate that a high coverage of actual design errors can be obtained
by complete test sets for a limited number of modeled error types, such as those defined
by our basic and conditional error models. Thus our methodology can be used to construct
focused test sets aimed at detecting a broad range of actual design bugs. More impor-
tantly, perhaps, it also supports an incremental design verification process that can be
implemented as follows: First, generate tests for SSL errors. Then generate tests for other
basic error types such as BSEs. Finally, generate tests for conditional errors. As the number
of SSL errors in a circuit is linear in the number of signals, complete test sets for SSL errors
can be relatively small. In our experiments such test sets already detect at least half of the
actual errors. To improve coverage of actual design errors and hence increase the confidence
in the design, an error model with a quadratic number of error instances, such as BSE
and CSSL1, can be used to guide test generation.
The conditional error models proved to be especially useful for detecting actual errors
that involve missing logic. Most 'missing module(s)' and `missing input(s)' in Table 3


3. Actual design errors and the corresponding dominated modeled errors for DLX.
Actual errors Corresponding dominated modeled errors
Category ISA ISAb Total INV SSL BSE CSSL1 CBOE CSSL2
Un-
known
Missing module (2) 8 2 14
Wrong singal source (1) 9 2
Complex
Inversion
Missing input
Unconnected input
Missing minterm (2)
Extra input (2)
Total
High-Level Design Verification of Microprocessors via Error Modeling - 17
cannot be covered when only the basic errors are targeted. However, all but one of them is
covered when CSSL1 and CBOE errors are targeted as well. The same observation applies
to the 'missing assignment(s)' errors in Table 2.
The designs used in the experiments are small, but appear representative of real industrial
designs. An important benefit of such small-scale designs is that they allow us to analyze
each actual design error in detail. The coverage results obtained strongly demonstrate
the effectiveness of our model-based verification methodology. Furthermore the analysis
and conclusions are independent of the manner of test generation. Nevertheless, further
validation of the methodology using industrial-size designs is desirable, and will become
more practical when CAD support for design error test generation becomes available.
models of the kind introduced here can also be used to compute metrics to assess
the quality of a given verification test set. For example, full coverage of basic (uncondi-
tional) errors provides one level of confidence in the design, coverage of conditional errors
of order provides another, higher confidence level. Such metrics can also be used to
compare test sets and to direct further test generation.
We envision the proposed methodology eventually being deployed as suggested in

Figure

2. Given an unverified design and its specification, tests targeted at modeled design
errors are automatically generated and applied to the specification and the implementation.
When a discrepancy is encountered, the designer is informed and perhaps given guidance
on diagnosing and fixing the error.

ACKNOWLEDGMENTS

We thank Steve Raasch and Jonathan Hauke for their help in the design error collection
process. We further thank Matt Postiff for his helpful comments.
The research discussed in this paper is supported by DARPA under Contract No.
DABT63-96-C-0074. The results presented herein do not necessarily reflect the position
or the policy of the U.S. Government.



--R

"Logic design verification via test generation,"
"Verification of the IBM RISC System/6000 by dynamic biased pseudo-random test program generator"
"Design verification via simulation and automatic test pattern gen- eration"
"High-level design verification of microprocessors via error modeling,"
"From specification validation to hardware testing: A unified method"
"High-level test generation using bus faults,"
New York
"A neutral netlist of 10 combinational benchmark circuits and a target translator in fortran"
"Complementary GaAs technology for a GHz microprocessor"
Cadence Design Systems Inc.
"Functional verification methodology of Chameleon processor"
Version Management with CVS
"AVPGEN - a test generator for architecture verification"
"Latent design faults in the development of the Multiflow TRACE/200"
"Hints on test data selection: Help for the practicing programmer"
"Observability-based code coverage metric for functional simulation"
"Hardware emulation for functional verification of K5"
"High-level test generation using physically-induced faults"
Computer Architecture: A Quantitative Approach
"Code generation and analysis for the functional verification of microprocessors"
"Pentium Processor Specification Update,"
"I'm done simulating; Now what? Verification coverage analysis and correctness checking of the DECchip 21164 Alpha microprocessor"
high-level Verilog description"
"A Fortran language system for mutation-based software testing"
"Prototyping the M68060 for concurrent verification"
MIPS Technologies Inc.
"An experimental determination of sufficient mutant operators"
"Finite state machine trace analysis program"

The TTL Logic Data Book
"Mutation testing - its origin and evolution"
Formal Verification of Hardware Design
--TR
Computer architecture: a quantitative approach
Software testing techniques (2nd ed.)
A Fortran language system for mutation-based software testing
Verification of the IBM RISC System/6000 by a dynamic biased pseudo-random test program generator
AVPGENMYAMPERSANDmdash;a test generator for architecture verification
Design verification via simulation and automatic test pattern generation
An experimental determination of sufficient mutant operators
Code generation and analysis for the functional verification of micro processors
Hardware emulation for functional verification of K5
I''m done simulating; now what? Verification coverage analysis and correctness checking of the DEC chip 21164 Alpha microprocessor
Functional verification methodology of Chameleon processor
An observability-based code coverage metric for functional simulation
Formal Verification of Hardware Design
Prototyping the M68060 for Concurrent Verification
From Specification Validation to Hardware Testing
High-level test generation using physically-induced faults

--CTR
David Van Campenhout , Trevor Mudge , John P. Hayes, Collection and Analysis of Microprocessor Design Errors, IEEE Design & Test, v.17 n.4, p.51-60, October 2000
Katarzyna Radecka , Zeljko Zilic, Identifying Redundant Wire Replacements for Synthesis and Verification, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.517, January 07-11, 2002
Tao Lv , Jian-Ping Fan , Xiao-Wei Li , Ling-Yi Liu, Observability Statement Coverage Based on Dynamic Factored Use-Definition Chains for Functional Verification, Journal of Electronic Testing: Theory and Applications, v.22 n.3, p.273-285, June      2006
Katarzyna Radecka , Zeljko Zilic, Design Verification by Test Vectors and Arithmetic Transform Universal Test Set, IEEE Transactions on Computers, v.53 n.5, p.628-640, May 2004
Wei Lu , Xiu-Tao Yang , Tao Lv , Xiao-Wei Li, An efficient evaluation and vector generation method for observability-enhanced statement coverage, Journal of Computer Science and Technology, v.20 n.6, p.875-884, November 2005
Anand L. D'Souza , Michael S. Hsiao, Error Diagnosis of Sequential Circuits Using Region-Based Model, Journal of Electronic Testing: Theory and Applications, v.21 n.2, p.115-126, April     2005
Serdar Tasiran , Kurt Keutzer, Coverage Metrics for Functional Validation of Hardware Designs, IEEE Design & Test, v.18 n.4, p.36-45, July 2001
David Van Campenhout , Trevor Mudge , John P. Hayes, High-level test generation for design verification of pipelined microprocessors, Proceedings of the 36th ACM/IEEE conference on Design automation, p.185-188, June 21-25, 1999, New Orleans, Louisiana, United States
Jian Shen , Jacob A. Abraham, An RTL Abstraction Technique for Processor MicroarchitectureValidation and Test Generation, Journal of Electronic Testing: Theory and Applications, v.16 n.1-2, p.67-81, Feb/April 2000
Ghazanfar Asadi , Seyed Ghassem Miremadi , Alireza Ejlali, Fast co-verification of HDL models, Microelectronic Engineering, v.84 n.2, p.218-228, February, 2007
Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors, Journal of Symbolic Computation, v.35 n.2, p.73-106, February
design errors;error modeling;design verification