VHDL semantics and validating transformations

• Published in: IEEE transactions on computer-aided design of integrated circuits and systems 1999-07, Vol.18 (7), p.936-955
• Main Authors: Pandey, S.L., Umamageswaran, K., Wilsey, P.A.
• Format: Article
• Language: English
• Subjects: Applied sciences; Circuit simulation; Circuit synthesis; Computational modeling; Delay; Design automation; Design. Technologies. Operation analysis. Testing; Dynamics; Electronics; Exact sciences and technology; Hardware design languages; Integrated circuits; Logic; Mathematical models; Semantics; Semiconductor electronics. Microelectronics. Optoelectronics. Solid state devices; Temporal logic; Time measurements; Time warp simulation; Timing; Transformations; Very high speed integrated circuits; VHDL
• ISSN: 0278-0070; 1937-4151
• DOI: 10.1109/43.771177

Formal models are used to provide an unambiguous definition of the semantics of very high speed integrated circuit hardware description language (VHDL) and to prove equivalences of VHDL programs. This paper presents a formal model of the dynamic semantics of VHDL that characterizes several important features of VHDL such as delta delays, pulse rejection limits, disconnection delays, postponed processes, sequential statements, and resolution functions. The underlying logic is interval temporal logic, which assists in characterizing the timing information contained in a VHDL program. The semantic definition is not dependent on the VHDL simulation cycle since it only defines the net effect of evaluating a VHDL program. It is argued that this declarative style coupled with the inherent advantages of temporal logic makes it possible to validate transformations (or rewrite rules) on VHDL programs and to formally reason about the timing aspects of VHDL. In particular, we present proofs of soundness of rewrite rules such as process folding and signal collapsing, and use temporal logic to derive an algorithm for determining when a given VHDL program is free of transaction preemption.