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:

Table 1: MIPS64 sample - groups of instructions
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).

Table 2: MIPS64 sample - generator description
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:

Table 3: DSP sample - groups of instructions
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).

Table 4: DSP sample - generator description
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:

Table 5: CP1 sample - groups of instructions
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:

Table 6: CP2 sample - groups of instructions
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).

Table 7: CP1 sample - generator description
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%
Table 8: CP2 sample - generator description
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).