Abstract
The paper presents MicroTESK, a tool for test program generation for functional verification of microprocessors. It generates test programs from templates which describe generation tasks in terms of constraints that must be satisfied in order to reach certain coverage goals. The tool uses formal specifications of the instruction set as a source of knowledge about the microprocessor under verification. This gives several advantages. First, the tool is easily adapted to new architectures by providing corresponding specifications. Second, constraints that constitute coverage model are automatically extracted from specifications. Third, a reference model used to track the microprocessor state during test generation is constructed on the basis of specifications. Such an approach helps to reduce the effort required to create test programs and increase the quality of testing. The tool has been successfully applied in industrial projects for verification of ARMv8 and MIPS64 microprocessors.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
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. Des. Test Comput. 21, 84–93 (2004)
MicroTESK page. http://forge.ispras.ru/projects/microtesk
RAVEN test program generator. http://www.slideshare.net/DVClub/introducing-obsidian-software-andravengcs-for-powerpc
Mishra, P., Dutt, N. (eds.): Processor Description Languages. Systems on Silicon. Morgan Kaufmann, San Francisco (2008). 432 pages
Freericks, M.: The nML machine description formalism. Technical report TR SM-IMP/DIST/08, TU Berlin CS Department (1993)
Chupilko, M., Kamkin, A., Kotsynyak, A., Protsenko, A., Smolov, S., Tatarnikov, A.: Specification-based test program generation for ARM VMSAv8-64 memory management units. In: Workshop on Microprocessor Test and Verification, pp. 1–6 (2015). https://doi.org/10.1109/MTV.2015.13
Kamkin, A., Kotsynyak, A.: Specification-based test program generation for MIPS64 memory management units. In: Trudy ISP RAN [Proceedings of ISP RAS], vol. 28, part 4, pp. 99–114 (2016)
Tatarnikov, A.: Language for describing templates for test program generation for microprocessors. In: Trudy ISP RAN [Proceedings of ISP RAS], vol. 28, part 4, pp. 81–102 (2016)
MicroTESK for MIPS64 page. http://forge.ispras.ru/projects/microtesk-mips64
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Kamkin, A., Tatarnikov, A. (2018). MicroTESK: A Tool for Constrained Random Test Program Generation for Microprocessors. In: Petrenko, A., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2017. Lecture Notes in Computer Science(), vol 10742. Springer, Cham. https://doi.org/10.1007/978-3-319-74313-4_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-74313-4_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-74312-7
Online ISBN: 978-3-319-74313-4
eBook Packages: Computer ScienceComputer Science (R0)