Proving Hardware Designs
Pascal Van Hentenryck · 1994
VHDL is a standardized hardware description language with almost universal market penetration. Originally developed in the 1980s with the support of the US DoD, several formalizations of its hardware simulation semantics have appeared in the last few years, including operational semantics in higher order logic and translations to Petri Nets and finite state machines. But in recent work [1] we have set out the first simple, formal compositional denotational semantics for VHDL. It generates an axiomatic pre-post-condition semantics and, in classic style, when read as a PROLOG program, the logical rules run as a validation condition generator, automating the derivation of correctness proofs.