Preview

Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS)

Advanced search

Specification-Based Test Program Generation for MIPS64 Memory Management Units

https://doi.org/10.15514/ISPRAS-2016-28(4)-6

Abstract

In this paper, a tool for automatically generating test programs for MIPS64 memory management units is described. The solution is based on the MicroTESK framework being developed at the Institute for System Programming of the Russian Academy of Sciences. The tool consists of two parts: an architecture-independent test program generation core and MIPS64 memory subsystem specifications. Such separation is not a new principle in the area: it is applied in a number of industrial test program generators, including IBM’s Genesys-Pro. The main distinction is in how specifications are represented, what sort of information is extracted from them, and how that information is exploited. In the suggested approach, specifications comprise descriptions of the memory access instructions, loads and stores, and definition of the memory management mechanisms such as translation lookaside buffers, page tables, table lookup units, and caches. A dedicated problem-oriented language, called mmuSL, is used for the task. The tool analyzes the mmuSL specifications and extracts all possible instruction execution paths as well as all possible inter-path dependencies. The extracted information is used to systematically enumerate test programs for a given user-defined test template and allows exhaustively exercising co-execution of the template instructions, including corner cases. Test data for a particular program are generated by using symbolic execution and constraint solving techniques.

About the Authors

A. S. Kamkin
Institute for System Programming of the Russian Academy of Sciences
Russian Federation


A. M. Kotsynyak
Institute for System Programming of the Russian Academy of Sciences
Russian Federation


References

1. MIPS64™ Architecture For Programmers. Volume 1: Introduction to the MIPS64™ Architecture. Revision 6.01. MIPS Technologies Inc. 2014. 148 p.

2. MIPS64™ Architecture For Programmers. Volume 3: MIPS64™/microMIPS64™ Privileged Resource Architecture. Revision 6.03. MIPS Technologies Inc. 2015. 368 p.

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

4. R.L. Glass. Facts and Fallacies of Software Engineering. Addison-Wesley Professional, 2002. 224 p.

5. T. Li, D. Zhu, Y. Guo, G. Liu, S. Li. MA2TG: A Functional Test Program Generator for Microprocessor Verification. Euromicro Conference on Digital System Design, 2005. pp. 176-183.

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

7. MicroTESK tool. http://forge.ispras.ru/projects/microtesk

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

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

10. D. Vorobyev, A. Kamkin. [Test program generation for memory management units of microprocesssors]. Trudy ISP RAN /Proc. ISP RAS, vol. 17, 2009. pp. 119-132 (in Russian).

11. A. Kamkin, A. Protsenko, A. Tatarnikov. An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation Mechanisms Trudy ISP RAN, 27(3), 2015. pp. 125-138.

12. Ruby programming language. http://www.ruby-lang.org

13. A. Kamkin, E. Kornykhin, D. Vorobyev. Reconfigurable Model-Based Test Program Generator for Microprocessors International Conference on Software Testing, Verification and Validation Workshops, 2011. pp. 47-54.

14. A.S. Kamkin, T.I. Sergeeva, S.A. Smolov, A.D. Tatarnikov, M.M. Chupilko. Extensible Environment for Test Program Generation for Microprocessors. Programming and Computer Software, 40(1), 2014, pp. 1-9.

15. Fortress library. http://forge.ispras.ru/projects/solver-api

16. Z3 SMT solver. http://github.com/Z3Prover/z3

17. CVC4 SMT solver. http://cvc4.cs.nyu.edu

18. MIPS64™ Architecture For Programmers. Volume 2: The MIPS64™ Instruction Set Reference Manual. Revision 6.04. MIPS Technologies Inc. 2015. 551 p.

19. Y. Naveh, M. Rimon, I. Jaeger, Y. Katz, M. Vinov, E. Marcus, G. Shurek. Constraint-Based Random Stimuli Generation for Hardware Verification AI Magazine, 28(3), 2007. pp. 13-30.


Review

For citations:


Kamkin A.S., Kotsynyak A.M. Specification-Based Test Program Generation for MIPS64 Memory Management Units. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(4):99-114. https://doi.org/10.15514/ISPRAS-2016-28(4)-6



Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)