Conference «Tools & Methods of Program Analysis – 2013»

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

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

Institute for System Programming of the Russian Academy of Sciences

Abstract: 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.

Keywords: hdl, dynamical verification, unit-level verification, hdl, trace matching, partially ordered multisets.

UDC: 004.415.53