Relevant Papers

[Breuer et al. 94b]

P T Breuer, L Sánchez, and C Delgado Kloos, Proof Theory and a Validation Condition Generator For VHDL, in Proc. EURO-DAC'94 with EURO-VHDL'94, Grenoble, 19 -- 23 September 1994. Los Alamitos, California: IEEE Computer Society Press 1994, 51 -- 517.

This paper gave a set of axioms for reasoning about ``core" VHDL, and also described a program that calculates hypotheses that have to be satisfied in order that a VHDL circuit description satisfy a given assertion about its behaviour.

The assertions are expressed in a fragment of temporal logic that is not that expressive, but can be extended easily. The main problem is that only constant values of time can be referenced. So, in practice, meta-reasoning has to be applied to time variables that are regarded as constants within the logic, but which can be thought of as variables outside the logic.

[Breuer et al. 94c]

P T Breuer, L Sánchez, and C Delgado Kloos, Proving VHDL Hardware Designs, in Proc. 11'th International Conference on Logic Programming, Santa Margherita, Italy, June 1994. MIT Press, Cambridge, Mass., p745.

This short presentation gave an lead-in for Prolog programmers to the programming techniques used to code the validation condition generator for VHDL.

[Breuer et al. 95]

P T Breuer, L Sánchez, and C Delgado Kloos, A Simple Denotational Semantics, Proof Theory and a Validation Condition Generator for Unit-Delay VHDL, in Formal Methods for System Design 1995, to appear.

This paper represents the state of the art in terms of our knowledge of the axiomatic and model semantics of VHDL. The logic presented in earlier papers has been strengthened and the paper includes a completeness proof for it with respect to the model semantics. the latter is also presented in relational form, which represents something of an improvement over earlier presentations.

A formal connection with the operational semantics of VHDL originally presented by John van Tassel in 1989 is also sketched.

[Delgado Kloos et al. 95a]

C Delgado Kloos, E Lecha, M More, L Sánchez Fernández, Ll Terés, Introducción a los lenguajes VHDL, Verilog y UDL/I, Novática, No. 112 -- 113, Nov. 94 -- Feb. 95, pp. 25 -- 34.

This paper provides an introduction to the three most popular Hardware Description Languages: VHDL, Verilog and UDL/I. The basic concepts behind HDLs are presented and compared with those of standard (imperative) programming languages. How the three languages cover the different concepts is studied.

[Delgado Kloos et al. 95b]

C Delgado Kloos, E Lecha, M More, L Sánchez Fernández, Ll Terés, Comparación de los lenguajes Verilog y UDL/I con VHDL, Novática, No. 112 -- 113, Nov. 94 -- Feb. 95, pp. 35 -- 44.

This paper compares the hardware description languages Verilog and UDL/I with VHDL.

[Delgado Kloos, Breuer 95]

C Delgado Kloos, P T Breuer (eds.), Formal Semantics for VHDL, London, Dordrecht, Boston, Kluwer Academic Publishers 1995, 250pp.

The book collects specialist Scientific Output from several authors, including ourselves, on various semantics for VHDL.

Our contribution sets out a functional semantics for VHDL --- a refinement of the relational model presented in other papers and a variant of a functional semantics given by ourselves in the previous year. The difference is that this semantics is embedded in a looser domain setting, so the fact that it still appears to work right on examples gives greater credence to the notion that it is right. The chapter gives a recipe for constructing VHDL simulators in compositional style.

The chapter also contains one of the few theorems we know to have been proved about the behaviour of VHDL programs in general: if we take the results of a simulation and feed them in to the simulator as an initial driver set, then the same things happen again, in exactly the same sequence. Reality is an invariant of VHDL simulators (or VHDL simulators are idempotent on reality).

Being able to express --- and prove --- such notions about VHDL behaviours is a significant advance in our understanding of the capabilities of this widely used specification and design language.