Ivannikov Institute for System Programming of the RAS

Verifying Correctness of HDL-Model Behavior on the Basis of Dynamical Trace Matching.


V.P. Ivannikov, A.S. Kamkin, M.M. Chupilko.


Correctness checking of HDL-model behavior is an integral part of dynamical verification of hardware. As a rule, it is based on comparing of HDL-model behavior and reference model behavior, developed in high-level programming languages. Being verified, both models are applied with the same stimulus sequences; their reactions are caught and checked against each other. Due to the abstractness of the reference model, the checking is not a trivial task as event sequences can be different and some events of one trace may miss in the other one. A methodology of dynamical trace matching for hardware models of different abstraction levels is considered in the paper. The methodology has been successfully used in a number of industrial projects of unit-level microprocessor verification.

Full text of the paper in pdf (in Russian)


dynamical verification; unit-level verification; HDL; trace matching; partially ordered multisets.


St. Petersburg State Polytechnical University Journal. Computer Science. Telecommunication and Control Systems, 2(193), 2014, pp. 130-142.

Research Group

Software Engineering

All publications during 2014 All publications