Verification of a model describing a hardware system is very important for modeling and
simulation purposes. It is necessary to ensure that the model accurately describes the
hardware system. A scheme for the automatic verification of VHDL (VHSIC Hardware
Description Language) models has been proposed. In the proposed scheme the
specifications for the hardware system, i.e.,the timing constraints and relations between
input and output signals are described by the designer in Modified Linear Time Temporal
Logic,. which is an extension to traditional boolean logic and can describe timing relation
between signals. A semantic similarity between temporal operators and VHDL timings
and delays has been drawn and an algorithm for comparing the VHDL model and
temporal specifications has been developed. Comparisons are made between the
simulation results on the VHDL model and the temporal logic specifications and
discrepancies are reported.