Ivannikov Institute for System Programming of the RAS

Static Analysis of HDL Description: Extracting Models for Verification.


A. Kamkin, S. Smolov, I. Melnichenko


The increasing complexity of hardware designs makes functional verification a challenge. The key issue of the state-of the-art verification approaches is to obtain a “good” model for automated test generation or formal property checking. In this paper, we describe techniques for deriving EFSM-based models from HDL descriptions and briefly discuss applications of such models for verification. The distinctive feature of the suggested approach is that it automatically determines what registers of a design encode its state and use this information for model reconstruction.

Full text of the paper in pdf


electronic design automation;finite state machines;formal verification;hardware description languages;EFSM-based models;HDL descriptions;automated test generation;extended finite state machines;formal property checking;functional verification;hardware des


East-West Design & Test Symposium (EWDTS), 2013. P. 1-4.

DOI: 10.1109/EWDTS.2013.6673126

Research Group

Software Engineering

All publications during 2013 All publications