A Method of Extended Finite State Machines Construction from HDL Descriptions Based on Static Analysis of Source Code.

Authors

S.A. Smolov, A.S. Kamkin.

Abstract

The complexity of digital microelectronic hardware grows steadily, which complicates its functional verification and makes the methods of automated functional verification extremely important. Such methods usually use models that are formal representations of hardware descriptions. Such models are suitable for functional test generation and/or property checking. These models are often manually built, which can cause errors or unexpected behavior.
This paper comes up with a new method of automated extraction of extended finite-state machine models from hardware descriptions. The key feature of the method is automated detection of hardware module's registers that encode the module's state. The experimental results of the method's application are also presented in the paper.

Full text of the paper in pdf (in Russian)

Keywords

digital hardware, functional verification, hardware description language, static analysis, functional test generation, model checking, logic synthesis, extended finite state machine, guarded action.

Edition

St. Petersburg State Polytechnical University Journal. Computer Science, Telecommunications. Iss. 1(212), 2015, pp. 60-73.

DOI: 10.5862/JCTCS.212.6

Research Group

Software Engineering

All publications during 2015

All publications