Timing models in VAL/VHDL

A detailed description is given of the timing model of VHDL (VHSIC hardware description language). VHDL uses a two-level timing model based on discrete event simulation. Timed assignment statements are preemptive, and two forms of preemption are supported in the language: inertial and transport. The author describes the VAL (VHDL annotation language) timing model and features of VAL designed to work with the VHDL timing model. VAL introduces assertions that understand the two-level timing framework in VHDL. In contrast to the preemptive assignment of VHDL, VAL models the same behavior using only anticipatory semantics (no preemption). The anticipatory model enables VAL descriptions to be treated as constraints on the input/output behavior of a device that may be directly translated into predicates. The author demonstrates by a simple example the application of formal techniques for manipulating these predicates.<>