A framework for macro- and micro-time to model VHDL attributes

摘要

The work presented introduces a formal definition of somenimportant constructs of VHDL, using a formally defined language. Bothnmacro time and micro time scales are used. The inclusion of micro time,nor time deltas, allows the authors to describe variables as well asnsignals. For the purpose of illustration they present the signalnattributes of VHDL. This work represents a prelude to the completentranslation of VHDL into the formal verification language SIGNAL. SIGNALncan then provide a basis for verifying VHDL programs