ISSN:
1572-8102
Keywords:
formal verification
;
digital circuits
;
denotational semantics
;
VHDL
;
program logic
;
timed logic
;
PROLOG
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract A denotational semantics and a Hoare programming logic for a subset of the standard hardware description languageVHDL are set out here. Both define the behaviour of synchronously clockedVHDL simulators in declarative and compositional style. The logic is proved complete with respect to the denotational semantics and a natural implementation of the logic inPROLOG as a validation condition generator forVHDL is also described. The subset of the language referred to above essentially consists of elaboratedVHDL excluding only deltadelayed signal assignments and zero waits. However, for brevity, only one of the two forms ofVHDL signal assignment is treated here. Moreover, for simplicity, signal resolution functions and local state are assumed to have been encoded away via expressions and signals.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF01383872
Permalink