A Model Checking-Based Method of Functional Test Generation for HDL Descriptions
| Autor: | S. A. Smolov, M. S. Lebedev |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Model checking
Source code Computer science media_common.quotation_subject цифровая аппаратура lcsh:QA75.5-76.95 VHDL Influence diagram высокоуровневая решающая диаграмма General Environmental Science media_common computer.programming_language Functional verification функциональная верификация Extended finite-state machine HARDWARE DESIGN FUNCTIONAL VERIFICATION STATIC ANALYSIS TEST GENERATION GUARDED ACTION HIGH-LEVEL DECISION DIAGRAM EXTENDED FINITE STATE MACHINE MODEL CHECKING ЦИФРОВАЯ АППАРАТУРА ФУНКЦИОНАЛЬНАЯ ВЕРИФИКАЦИЯ СТАТИЧЕСКИЙ АНАЛИЗ ГЕНЕРАЦИЯ ТЕСТОВ ОХРАНЯЕМОЕ ДЕЙСТВИЕ ВЫСОКОУРОВНЕВАЯ РЕШАЮЩАЯ ДИАГРАММА РАСШИРЕННЫЙ КОНЕЧНЫЙ АВТОМАТ ПРОВЕРКА МОДЕЛИ Static analysis проверка модели охраняемое действие расширенный конечный автомат статический анализ генерация тестов General Earth and Planetary Sciences Verilog lcsh:Electronic computers. Computer science Algorithm computer |
| Zdroj: | Труды Института системного программирования РАН, Vol 28, Iss 4, Pp 41-56 (2018) |
| ISSN: | 2220-6426 2079-8156 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|