MicroTESK-Based Test Program Generator for the RISC-V Architecture

 
Kamkin A.S., Protsenko A.S., Smolov S.A., Tatarnikov A.D. (Institute for System Programming of the Russian Academy of Sciencies)
 
Abstract - 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 describe how instruction sequences (test cases) are composed, and what constraints and generation methods are applied. Test templates are created using a Ruby-based domain-specific language. The generation core provides a set of components for instruction sequence composition and test data generation. They utilize 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, and RV64D. In total, the specifications cover 220 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 - microprocessors; formal specifications; instruction set architecture; functional verification; test program generation; RISC-V; nML; MicroTESK.

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

 
Камкин А.С., Проценко А.С., Смолов С.А., Татарников А.Д. (Институт системного программирования РАН, г. Москва)
 
Аннотация - В работе рассматривается генератор тестовых программ для функциональной верификации микропроцессоров с архитектурой RISC-V. Генератор разработан на основе инструмента MicroTESK и состоит из двух частей: формальных спецификаций архитектуры RISC-V и архитектурно-независимого ядра генерации тестовых программ. Спецификации описывают синтаксис и семантику поддерживаемых микропроцессором команд. Ядро реализует расширяемый набор техник построения последовательностей команд и генерации тестовых данных. Генерация осуществляется на основе шаблонов, которые задают используемые команды и техники генерации. Предлагаемый подход позволяет упростить поддержку новых расширений системы команд и новых техник генерации. Генератор позволяет создавать тесты с использованием случайных, комбинаторных и основанных на ограничениях техник генерации.

Ключевые слова - микропроцессоры; формальные спецификации; система команд; функциональная верификация; генерация тестовых программ; RISC-V; nML; MicroTESK.