The SECD Microprocessor: A Verification Case Study

This is a milestone in machine-assisted microprocessor verification. Gordon [20] and Hunt [32] led the way with their verifications of sim­ ple designs, Cohn [12, 13] followed this with the verification of parts of the VIPER microprocessor. This work illustrates how much these, and other, pioneers achieved in developing tractable models, scalable tools, and a robust methodology. A condensed review of previous research, emphasising the behavioural model underlying this style of verification ...