Verification of timing properties of VHDL

Abstract

This paper shows how timing properties of VHDL processes can be verified using timed transition systems. The timing model being adopted is the timed automaton model used in the timing extension of Kurshan’s COSPAN system. It demonstrates how a VHDL process can be translated into a timed automaton by describing the construction of the corresponding timed process that handles the scheduled signal assignments of the VHDL specification. Verification is performed in the case in which the complement of the timing properties to be verified are provided in terms of a timed automaton. Interestingly enough, this is the case for a large class of hardware properties expressed in terms of timing diagrams.