Functional semantics of microprocessors at the microprogram level and correspondence with the machine instruction level

In order to apply formal verification methods to actual microprocessors, the author studies the functional semantics of microprocessors of the Von Neumann machine type, at different specification and description levels. She settles a functional formalism from which the semantic equivalence between adjacent levels is proved. Here, she proposes a general methodology to define the functional semantics of a processor at the microprogram level. She also presents the correspondence between this level and the machine instruction level