The use of hoare logic in the verification of horizontal microprograms

In recent years, much effort has been devoted to the design and implementation of microprogramming languages that support the production of highly reliable yet efficient run time microcode. One of the goals for such languages is to facilitate the formal verification of microprograms using Hoare's inductive assertion method. Essential to the use of this method is an axiomatic definition of the microprogramming language.In this paper, we describe the axiomatization of a machine dependent microprogramming language called S*(QM-1)⁽¹⁾. This language is an instantiation of the machine independent language schema S*^(2,3) based on the Nanodata QM-1 nanolevel architecture, and is designed for the development and specification ofhorizontal microprograms. We discuss the rationale underlying the design and axiomatization of this language and we show, using S*(QM-1) as a case study, some of the important points in which the verification of firmware differs from software verification.