Case Study on Core-Level Verification
The core-level approach to hardware verification has been applied to several RISC microprocessors, arithmetical coprocessors, and particular CPU subsystems. This page contains three case studies:
- verification of MIPS64 microprocessor (PDF file);
- verification of DSP coprocessor (PDF file).
- verification of arithmetical coprocessors (PDF file).
Verification of MIPS64 Microprocessor
The approach was used for verification of MIPS64-compatible microprocessor. The microprocessor implements 221 instructions. All instructions can be clustered into 13 groups:
Group of instructions | Number of instructions |
arithmetic | 33 |
logic | 8 |
move | 8 |
shift | 15 |
branch | 20 |
nop | 2 |
memory | 26 |
interrupt | 14 |
system | 13 |
fpu.arithmetic | 24 |
fpu.move | 26 |
fpu.convert | 26 |
fpu.branch | 6 |
We used triples of instructions as test actions. Test situations and dependencies used for load/store instructions were focused on address spaces, TLB/cache hits/misses, etc. Test data for all kinds of arithmetic instructions were directed to exceptional cases and boundary values. Branch instructions were described by condition value (for conditional jumps) and jump direction (forward or backward).
The table below shows size of test descriptions in lines of code without comments (LOCWC).
Generator Component | Code Volume, LOCWC | Code Volume, Percentage |
Specification of subsystems | 4450 | 10.5% |
Specification of instructions | 16650 | 39% |
Test situations | 20550 | 48% |
Dependencies | 1050 | 2.5% |
Total | 42700 | 100% |
We have found 9 errors in the RTL model of the microprocessor and 6 errors in the microprocessor simulator (reference model).
Verification of DSP Coprocessor
The technology was applied to verification of DSP coprocessor. The coprocessor implements 109 instructions. All instructions can be clustered into 8 groups:
Group of instructions | Number of instructions |
complex arithmetic | 12 |
floating-point SIMD arithmetic | 12 |
type conversion | 11 |
integer arithmetic | 21 |
comparison | 4 |
move | 6 |
memory | 22 |
control | 21 |
We used triples of instructions as test actions. Test situations were directed to exceptions, boundary values, and hard-to-round cases.
The table below shows size of test descriptions in lines of code without comments (LOCWC).
Generator Component | Code Volume, LOCWC | Code Volume, Percentage |
Specification of subsystems | 1650 | 8.5% |
Specification of instructions | 6250 | 32.5% |
Test situations | 11400 | 59% |
Dependencies | 0 | 0% |
Total | 19300 | 100% |
We have found about 5 errors in the RTL model of the DSP coprocessor and more than 10 errors in the coprocessor simulator (reference model).
Verification of Arithmetical Coprocessors
MicroTESK technology was applied to verification of floating-point arithmetic coprocessors (CP1 and CP2).
The CP1 coprocessor implements 114 instructions. All instructions can be clustered into 5 groups:
Group of instructions | Number of instructions |
floating-point SIMD arithmetic | 38 |
branches | 6 |
type conversion | 33 |
memory | 19 |
move | 18 |
The CP2 coprocessor implements 75 instructions. All instructions can be clustered into 6 groups:
Group of instructions | Number of instructions |
complex arithmetic | 33 |
branches | 4 |
comparison | 16 |
memory | 12 |
move | 8 |
control operations | 2 |
We used quadruples of instructions as test cases. Test situations were directed to the dependency resolution mechanisms of the coprocessors.
The tables below show volume of test descriptions in lines of code without comments (LOCWC).
Generator Component | Code Volume, LOCWC | Code Volume, Percentage |
Specification of subsystems | 1650 | 25.5% |
Specification of instructions | 3000 | 46.5% |
Test situations | 1800 | 28.0% |
Total | 6450 | 100% |
Generator Component | Code Volume, LOCWC | Code Volume, Percentage |
Specification of subsystems | 2350 | 20.5% |
Specification of instructions | 5600 | 48.5% |
Test situations | 3600 | 31.0% |
Total | 11550 | 100% |
We have found more then 10 errors in the RTL models of the coprocessors and more than 10 errors in the coprocessors’ simulators (reference models).