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

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.

microprocessors, memory management, caching, address translation, functional verification, formal specifications, test program generation, instruction stream generation

1. Bryant R.E., O’Hallaron D.R. Computer Systems: A Programmer’s Perspective. Pearson, 2010. 1080 p.

2. Adir A., Almog E., Fournier L, Marcus E., Rimon M., Vinov M., Ziv A. Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification. Design & Test of Computers, 2004. pp. 84-93.

3. Sorin D.J., Hill M.D., Wood D.A. A Primer on Memory Consistency and Cache Coherence. Morgan and Claypool, 2011. 195 p.

4. Adir A., Fournier L., Katz Y., Koyfman A. DeepTrans - Extending the Model-based Approach to Functional Verification of Address Translation Mechanisms. High-Level Design Validation and Test Workshop, 2006. pp. 102-110.

5. Vorobyev D., Kamkin A. Generatsiya testovykh programm dlya podsistemy upravleniya pamyat'yu mikroprotsessora [Test Program Generation for Memory Management Units of Microprocessors]. Trudy ISP RAN [The Proceedings of ISP RAS], 2009, vol. 17. pp. 119-132 (in Russian).

6. Kamkin A., Tatarnikov A. MicroTESK: An ADL-Based Reconfigurable Test Program Generator for Microprocessors. Spring/Summer Young Researchers’ Colloquium on Software Engineering, 2012, pp. 64-69.

7. MicroTESK page - http://forge.ispras.ru/projects/microtesk

8. Freericks M. The nML Machine Description Formalism. Technical Report TR SM-IMP/DIST/08, TU Berlin CS Department, 1993.

9. MIPS64™ Architecture For Programmers. MIPS Technologies Inc.

10. Fortress page - http://forge.ispras.ru/projects/solver-api