The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - May (1988 vol.14)
pp: 559-574
ABSTRACT
<p>A universal syntax-directed proof system is presented for the verification of horizontal computer architectures. The system is based on the axiomatic architecture description language AADL, which is sufficiently rich to allow the specification of target architectures while providing a concise model for clocked microarchitectures. For each description A epsilon AADL of a host, it is shown how to construct systematically a (Hoare-style) axiomatic definition of an A-dependent high-level microprogramming language based on S*. The axiomatization of A's microoperations together with a powerful proof-rule dealing with the inherent low-level parallelism of horizontal architectures allow a complete axiomatic treatment of the timing behavior and dynamic conflicts of microprograms written in S*(A).</p>
INDEX TERMS
microprogramming logic; syntax-directed proof system; horizontal computer architectures; architecture description language; AADL; specification; clocked microarchitectures; axiomatic definition; microoperations; low-level parallelism; timing behavior; dynamic conflicts; computer architecture; formal logic; microprogramming; specification languages; theorem proving
CITATION
W. Damm, "A Microprogramming Logic", IEEE Transactions on Software Engineering, vol.14, no. 5, pp. 559-574, May 1988, doi:10.1109/32.6134
88 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool