A Model Checking-Based Method of Functional Test Generation for HDL Descriptions

• Published in: Труды Института системного программирования РАН
• Main Authors: M. S. Lebedev, S. A. Smolov
• Format: Article
• Language: English
• Published: Russian Academy of Sciences, Ivannikov Institute for System Programming 2018-10-01
• Subjects: цифровая аппаратура; функциональная верификация; статический анализ; генерация тестов; охраняемое действие; высокоуровневая решающая диаграмма; расширенный конечный автомат; проверка модели
• Online Access: https://ispranproceedings.elpub.ru/jour/article/view/138

Automated test generation is a promising direction in hardware verification research area. Functional test generation methods based on models are widespread at the moment. In this paper, a functional test generation method based on model checking is proposed and compared to existing solutions. Automated model extraction from the hardware design’s source code is used. Supported HDLs include VHDL and Verilog. Several kinds of models are used at different steps of the test generation method: guarded action decision diagram (GADD), high-level decision diagram (HLDD) and extended finite-state machine (EFSM). The high-level decision diagram model (which is extracted from the GADD model) is used as a functional model. The extended finite-state machine model is used as a coverage model. The aim of test generation is to cover all the transitions of the extended finite state machine model. Such criterion leads to the high HDL source code coverage. Specifications based on transition and state constraints of the EFSM are extracted for this purpose. Later, the functional model and the specifications are automatically translated into the input format of the nuXmv model checking tool. nuXmv performs model checking and generates counterexamples. These counterexamples are translated to functional tests that can be simulated by the HDL simulator. The proposed method has been implemented as a part of the HDL Retrascope framework. Experiments show that the method can generate shorter tests than the FATE and RETGA methods providing the same or better source code coverage.