The Compiler of Tabular Representations of Mealy Machines into Programs in the SMV Language that Automates Verification of Computer Projects Using the Model Verification

This paper describes a digital systems verification tool based on the ASM (Algorithmic State Machine) method. The program “mealy2smv” in C++ which performs automatic transformation of ASM flowcharts into SMV descriptions has been developed. The structures produced by the program “mealy2smv” are similar to Kripke structures. Therefore the program enables to reduce consider-ably the cost of the formal model verification in the process of digital systems development.