Automatic verification of models described in VHDL

A scheme for the automatic verification of models described in VHDL (the VHSIC hardware description language) is proposed. For models with many constraints it becomes exceedingly difficult to verify their validity. In the proposed scheme the specifications for the system, i.e. the timing constraints and relations between the inputs and outputs, are described by the designer in modified linear time temporal logic, which is an extension of traditional logic and can describe timing relations among variables. Tests and simulations are conducted on the model described in VHDL, based on the given specifications. The outputs of the simulations are evaluated and compared with expected results. Discrepancies from the given specifications are reported