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

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. Autom...

Full description

Bibliographic Details
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

Similar Items

Test Generation for Digital Hardware Based on High-Level Models
by: M. M. Chupilko, et al.
Published: (2018-10-01)

Extracting Assertions for Conflicts in HDL Descriptions
by: Alexander Sergeevitch Kamkin, et al.
Published: (2019-09-01)

A Survey of Methods and Tools for Test Program Generation for Microprocessors
by: A. D. Tatarnikov
Published: (2018-10-01)

Tools for Functional Verification of Microprocessors
by: A. Kamkin, et al.
Published: (2018-10-01)

On the model checking of finite state transducers over semigroups
by: A. R. Gnatenko, et al.
Published: (2018-10-01)

An Extended Finite State Machine-Based Approach to Code Coverage-Directed Test Generation for Hardware Designs
by: I. . Melnichenko, et al.
Published: (2018-10-01)

Locating a faulty component of an EFSM composition
by: Svetlana Prokopenko
Published: (2018-10-01)

On the Designing of Model Checkers for Real-Time Distributed Systems
by: D. Yu. Volkanov, et al.
Published: (2012-01-01)

Graph learning by a set of automata
by: Igor Burdonov, et al.
Published: (2018-10-01)

Checking experiments with non-observable tree FSMs
by: N. . Kushik
Published: (2018-10-01)

How the story of UniTESK technology applications mirrors development of model based testing
by: V. P. Ivannikov, et al.
Published: (2018-10-01)

Deriving checking sequences for nondeterministic FSMs
by: Anton Ermakov
Published: (2018-10-01)

A Survey of Methods for Model Extraction from HDL Descriptions
by: S. A. Smolov
Published: (2018-10-01)

FSM abstraction based method for deriving test suites with guaranteed fault coverage against nondeterministic Finite State Machines with timed guards and timeouts
by: Aleksandr Sergeevitch Tvardovskii, et al.
Published: (2019-10-01)

Input data generation for reaching specific function in program by iterative dynamic analysis
by: A. Y. Gerasimov, et al.
Published: (2018-10-01)

Verification and analysis of variable operating systems
by: V. V. Kuliamin, et al.
Published: (2018-10-01)

Formal Verification of Linux Kernel Library Functions
by: D. V. Efremov, et al.
Published: (2018-10-01)

Component-based verification of operating systems
by: V. V. Kuliamin, et al.
Published: (2019-02-01)

On Verification of PLC-Programs Written in the LD-Language
by: E. V. Kuzmin, et al.
Published: (2012-01-01)

Generation of the weakest preconditions of programs with dynamic memory in symbolic execution
by: A. V. Misonizhnik, et al.
Published: (2024-12-01)

Language for Describing Templates for Test Program Generation for Microprocessors
by: A. D. Tatarnikov
Published: (2018-10-01)

Combinatorial generation of operation system software configurations
by: V. V. Kuliamin
Published: (2018-10-01)

Static Verification Tools for C Programs and Linux Device Drivers: A Survey
by: M. U. Mandrykin, et al.
Published: (2018-10-01)

An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation Mechanisms
by: A. . Kamkin, et al.
Published: (2018-10-01)

MicroTESK-Based Test Program Generator for the ARMv8 Architecture
by: A. S. Kamkin, et al.
Published: (2018-10-01)

A TEFSM-based Framework for QoE Evaluation of OTT Services
by: D. Rivera, et al.
Published: (2018-10-01)

Deriving adaptive checking sequence for nondeterministic Finite State Machines
by: A. D. Ermakov, et al.
Published: (2018-10-01)

Deriving adaptive distinguishing sequences for Finite State Machines
by: A. S. Tvardovskii, et al.
Published: (2018-10-01)

Test Readability Optimization in Context of Symbolic Execution
by: I. A. Yakimov, et al.
Published: (2018-10-01)

STRUCTURAL STATE MACHINES IN THE FORM OF THE TENSORS OF THE THIRD RANK SUDOKU TYPE
by: Юрий Михайлович Пенкин, et al.
Published: (2019-12-01)

On the possibilities of FSM description of Parallel composition of Timed Finite State Machines
by: A. S. Tvardovskii, et al.
Published: (2018-10-01)

A polynomial algorithm for checking the equivalence in models of programs with commutation and vast operators
by: V. V. Podymov, et al.
Published: (2018-10-01)

Linux Driver Verification
by: D. Beyer, et al.
Published: (2018-10-01)

Finite state automata in the theory of algebraic program schemata
by: R. I. Podlovchenko
Published: (2018-10-01)

Verifying functional properties of smart contracts using symbolic model-checking
by: E. S. Shishkin
Published: (2018-12-01)

Construction of validation modules based on reference functional models in a standalone verification of communication subsystem
by: D. A. Lebedev, et al.
Published: (2018-10-01)

Verified program code execution system prototype
by: A. V. Kozachok, et al.
Published: (2018-10-01)

The final models of specification
by: Igor Bourdonov, et al.
Published: (2018-10-01)

Improving out of vocabulary words recognition accuracy for an end-to-end Russian speech recognition system
by: A. Yu. Andrusenko, et al.
Published: (2024-12-01)

Static verification for memory safety of Linux kernel drivers
by: A. A. Vasilyev
Published: (2019-02-01)