Formal verification of microprogrammed architectures
D. Borrione, Paolo Enrico Camurati, J.-L. Paillet, P. Prinetto · HAL (Le Centre pour la Communication Scientifique Directe) · 1989
The paper presents the application of formal verification techniques to a real microprocessor. The device is described and verified resorting to a functional model. A methodology which can be used in a wide number of cases is also presented.