Verifying correctness of hdl-model behavior on the basis of dynamical trace matching

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.