Ivannikov Institute for System Programming of the RAS

Dynamic verification of the digital equipment based on formal specifications.


M.M. Chupilko.


The thesis was aimed at unit-level simulation-based hardware verification. The novelty of the subject was caused by the importance of verification of HDL-descriptions whereas there were not ready-to-use solutions, which would completely fit industrial application at different development stages. The problems of industrial HDL-description development having been analyzed, the method of simulation-based verification was proposed in the work, that accounted peculiarities both of HDL-descriptions themselves and of the processes of their development, i.e.: the objective complexity, the incremental nature of development process stages, the requirement incompleteness (especially at early development stages). The thesis introduces the following newly created methods. The first one is the method of verification of digital hardware, based on formal specifications in the form of C++-program models, which fits the requirements of industrial processes of HDL-description development. The second one is the method of digital hardware specification, being suitable for usage at different abstraction levels. The third one is the method of matching of digital hardware reactions and reference model reactions, allowing automatizing the hardware checking procedure. The above-mentioned methods are implemented in a verification toolkit named C++TESK.

Full text of the paper in pdf (in Russian)


Diss. Institute for System Programming of the Russian Academy of Sciences, 2012. Print.

Research Group

Software Engineering

All publications during 2012 All publications