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 re- search, emphasising the behavioural model underlying this style of verification is followed by a careful, and remarkably readable, ac- count of the SECD architecture, its...