An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation Mechanisms

Abstract

In this work, an approach to generate test programs for functional verification of memory management units of microprocessors is proposed. The approach is based on formal specification of memory access instructions, namely load and store instructions, and memory devices such as cache units and address translation buffers. The use of formal specifications helps automate development of test program generators and makes verification systematic due to clear definition of testing goals. In the suggested approach, test programs are constructed by using combinatorial techniques, which means that stimuli - sequences of loads and stores - are created by enumerating all feasible combinations of instructions, situations (instruction execution paths) and dependencies (sets of conflicts between instructions). It is of importance that test situations and dependencies are automatically extracted from specifications. The approach has been used in a number of industrial projects and allowed to discover critical bugs in memory management mechanisms.

Keywords

• микропроцессоры
• управление памятью
• кэширование
• трансляция адресов
• функциональная верификация
• формальные спецификации
• генерация тестовых программ
• генерация потока инструкций