We are pleased to announce the first build of MicroTESK for RISC-V. The build has the following properties: nML specifications of 201 instructions (including pseudo ones); no MMU specification; sample test templates. Here is a link to the project: http://forge.ispras.ru/projects/microtesk-riscv
MicroTESK was presented at the tool demo session of the Haifa Verification Conference (HVC) held in Haifa, Israel on November 13-15, 2017. HVC 2017 is the 13th in the series of annual conferences dedicated to advancing the state-of the art and state-of-the-practice in verification and testing. The conference provides a forum for researchers and practitioners from academia and industry to share their work, exchange ideas, and discuss the future directions of testing and verification for hardware, software, and complex hybrid systems. The common underlying goal of these techniques is to ensure the correct functionality and performance of complex systems. HVC is the only conference that brings together researchers and practitioners from all verification and testing sub-fields, thereby encouraging the migration of methods and ideas among domains.
Trying to keep up with the times, we started MicroTESK for RISC-V, an open test program generator for the open instruction set architecture (ISA). Here is a link to the project: http://forge.ispras.ru/projects/microtesk-riscv. The first build is expected on the beginning of December. RISC-V is an open, free ISA enabling a new era of processor innovation through open standard collaboration. Born in academia and research, RISC-V ISA delivers a new level of free, extensible software and hardware freedom on architecture, paving the way for the next 50 years of computing design and innovation (http://riscv.org).
We are pleased to inform you that MicroTESK has general support for ARMv8.2-A. The formal specifications have been updated: enhanced memory model with wider virtual and physical addresses (52 bits); 16-bit SIMD instructions and FP instructions; Reliability, Availability, and Serviceability (RAS); Statistical Profiling Extension (SPE). It required 70 new instructions, modification of some older ones, and update of the MMU description. The overall specifications include 1000+ instructions; their volume is almost 20 KLOC. ARMv8.2-A is a 64/32-bit architecture developed by ARM Holdings (arm.com).