Issue No. 05 - May (1988 vol. 14)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.6134
<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>
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
W. Damm, "A Microprogramming Logic," in IEEE Transactions on Software Engineering, vol. 14, no. , pp. 559-574, 1988.