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. / Master of Science