ИСТИНА

In this talk, we present an open-source specification-based test program generator (TPG) for functional verification of RISC-V microprocessors [1]. The TPG is based on the MicroTESK (Microprocessor TEsting and Specification Kit) framework [2][3] and consists of two main parts: (1) the formal specifications of the RISC-V instruction set architecture (ISA) and (2) the ISA-independent generation core. Test programs are automatically constructed based on the ISA specifications and test templates, which are descriptions of verification scenarios. The RISC-V ISA specifications are written in nML language [4]. They describe the registers, the memory storage, the addressing modes, and the instructions’ syntax and semantics. The information extracted from the specifications is used in multiple ways: (1) to get the catalogue of supported instructions to be used in test templates; (2) to build the test coverage model that holds constraints describing execution paths of the instructions; (3) to construct the instruction set simulator (ISS) that serves as a reference model. Test templates describe how instruction sequences (test cases) are composed, and what constraints and engines are applied to them. They are created by verification engineers using a Ruby-based domain-specific language [5]. In addition, a basic set of test templates, so-called architecture validation suite (AVS), is automatically generated based on information extracted from the specifications. The generation core provides a set of engines for instruction sequence composition and test data generation. The engines utilize randomization and constraint solving techniques. Supported constraint types include: (1) constraints on instruction operands; (2) constraints related to control flow; (3) floating-point constraints; (4) MMU-related constraints. The TPG architecture facilitates integration of user-defined engines. The built-in ISS 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, and RV64D. In total, the specifications cover about 200 instructions. The effort required to develop specifications (and the TPG) constituted about 3 man-months. The specifications can be easily modified to support more instructions (including custom extensions). The TPG contains a set of test templates that provide basic ISA coverage and demonstrate the TPG facilities. MicroTESK for RISC-V is distributed under Apache License, Version 2.0. The MicroTESK technology has been previously used to create TPGs for several RISC ISAs including ARMv8 and MIPS64 [3][6], which have been successfully applied in industrial projects.