Генератор тестовых программ для архитектуры RISC-V на основе инструмента MicroTESK

Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС). 2018. № 2. С. 2–8.

Tatarnikov A., Kamkin A., Проценко А. С., Смолов С. А.

In this paper, a specification-based test program generator for functional verification of RISC-V microprocessors is presented. The tool is based on the MicroTESK framework and consists of two main parts: (1) the formal specifications of the RISC-V ISA and (2) the ISA-independent generation core. Test programs are generated on the basis of the ISA specifications and test templates that are high-level descriptions of test scenarios. The RISC-V ISA specifications are written in nML language. They describe the syntax and semantics of the instructions. The information extracted from the specifications is used in multiple ways: to get instruction signatures to be used in test templates; to build the test coverage model that holds constraints describing execution paths of the instructions; to construct the instruction set simulator that serves as a reference model. Test templates are created using a Ruby-based domain-specific language and describe how instruction sequences are composed and what constraints and generation methods are applied. The generation core provides random, combinatorial, and constraint-based test generation methods. The built-in instruction set simulator allows executing instructions in the process of test program generation. This allows predicting the microprocessor state to ensure the validity of the tests, to create self-checks, and to solve constraints that use state information. MicroTESK for RISC-V supports the following instruction subsets: RV32I, RV64I, RV32M, RV64M, RV32A, RV64A, RV32F, RV64F, RV32D, RV64D, RV32C, and RV64C. In total, the specifications cover 262 instructions. The effort required to develop the specifications constituted about 4 man-months. The specifications can be easily modified to support more instructions. MicroTESK for RISC-V includes a set of test templates that provide basic ISA coverage and demonstrate the generator facilities.

Keywords: верификация, formal specifications, система команд, микропроцессоры, формальная спецификация, генерация тестовых программ, functional verification, test program generation, microprocessors, instruction set architecture, RISC-V, nML, MicroTESK, RISC-V, nML, MicroTESK