Interrupt behaviors, particularly the external ones, are difficult to verify in a microprocessor. Because the external interrupt arrival time and the microprocessor response time must be precise, verification requires sophisticated hardware and software design. This paper proposes a computer-aided design tool, called processor exception verification tool (PEVT), to verify the external interrupt behaviors of microprocessors, including individual, multiple, and nested interrupts. An architecture description language extension, called Exception Description Language (EXPDL), is developed for the designer to capture the external interrupt behaviors for the microprocessor under verification. PEVT is responsible for generating the verification cases, consisting of both the hardware and software modules, which are then used to trigger the expected behaviors. A monitor is also generated from the EXPDL description to verify these cases. PEVT has been applied to the verification of an academic implementation of the ARM7 microprocessor core and a public domain scalable processor architecture (SPARC) microprocessor core. The ARM7 has had a system-on-a-chip test chip and software porting including multimedia applications (MP3/JPEG/ ...) and a real time operating system muC-OSII. PEVT successfully identified several sophisticated remaining bugs with 527 lines of EXPDL description and took only 4 204 961 cycles of register transfer language simulation with execution time of 4.5 h in a SUN Blade2000 workstation. The experiment shows that PEVT could generate highly focused verification cases, less than 98 cycles per case on the average, which identify potential bugs with much less simulation cycles at the early verification stage, compared with traditional manual-based approaches.

Interrupt behaviors, especially the external ones, are difficult to verify in a microprocessor design project in that they involve both interacting hardware and software. This paper proposes a CAD tool, called PEVT, to verify the external interrupt behaviors of microprocessors. An architecture description language extension, called EXPDL, is developed for the designer to capture the external interrupt behaviors for the microprocessor. PEVT is responsible to generate the verification cases, consisting of both the hardware and software modules, which are then used to trigger the expected behaviors. A monitor is also generated from the EXPDL description to verify these cases. PEVT has been applied to the verification of an academic implementation of ARM7 microprocessor core, which has had a SoC test chip and software porting including MP3 decoder and uC-OSII. PEVT successfully identified several sophisticated remaining bugs with only less than 88,000 cycles of RTL simulation with execution time of 424 seconds in a SUN Blade2000 workstation. The experiment shows that PEVT could generate highly focused verification cases, less than 21 cycles per case on the average, which identify potential bugs with much less simulation cycles, compared with traditional regression tests which consume huge amount of simulation cycles.