Phillip J. Windley: A Hierarchical Methodology for Verifying Microprogrammed Microprocessors. S&P 1990: 345-359