MIPS64
Overview
MIPS64 is a 64-bit instruction set architecture. It is referenced in the literature as a target for specification-based test program generation and functional verification of microprocessors.
Verification and Test Program Generation
MIPS64 has been the subject of industrial-scale functional verification efforts. The MicroTESK (Microprocessor TEsting and Specification Kit) framework, developed by ISP RAS, has been successfully applied in industrial projects for the verification of MIPS64 microprocessors. MicroTESK uses formal specifications as a source of knowledge about the configuration of the microprocessor under verification and generates assembly-language test programs that exercise verification goals expressed as test situations derived from those specifications.
A dedicated publication, Specification-based test program generation for MIPS64 memory management units by A. S. Kamkin and A. M. Kotsynyak (Proceedings of the Institute for System Programming of the RAS, 2016, vol. 28, issue 4, pp. 99–114), specifically targets the memory management unit (MMU) component of MIPS64 processors using the specification-based approach.
Related Tools
- MicroTESK — A test program generation framework that targets MIPS64 among other ISAs. The framework generates assembly test programs from formal specifications written in a Ruby-based description language, allowing verification goals to be expressed in terms of test situations derived from those specifications.
References
- 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, 2016, 28(4): 99–114. doi:10.15514/ISPRAS-2016-28(4)-6
- ISP RAS project page: MicroTESK — a test program generator.