Specification-Based Test Program Generation for MIPS64 Memory Management Units
https://doi.org/10.15514/ISPRAS-2016-28(4)-6
Abstract
About the Authors
A. S. KamkinRussian Federation
A. M. Kotsynyak
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