Test environment for verification of multi-processor interrupt system with virtualization support

Interrupt system is an important part of microprocessors. Interrupts are widely used for interaction with hardware and responding to stimuli. Modern microprocessor interrupt systems include hardware support of virtualization. Hardware support helps to increase the performance of virtual machines. However, including additional functionality may lead to potential errors. The paper presents an overview of approaches used for multi-core microprocessors interrupt system with virtualization support verification. Some definitions and characteristics of interrupt systems that needed to be taken into account in the process of verification are described. Stand-alone verification environment general scheme is presented. Universal Verification Methodology was applied to construct test system. To simplify development of checking module discrete-event with time accounting reference model was used. Sequences of primary requests and automatically generated secondary requests in the special modules named auto-handlers were used for test system behavior randomization. We describe some difficulties discovered in the verification process and corresponding solving methods. Generalized test algorithm stages are presented. Some other techniques for checking the correctness of interrupt system have been reviewed. In conclusion, we provide the case study of applying the suggested approaches for interrupt system verification of microprocessors with “Elbrus” and “SPARC-V9” architectures developed by MCST. The results and further plan of the test system development are presented.