A method of extended finite state machines construction from HDL descriptions based on static analysis of source code

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.