Application of formal methods to the VIPER microprocessor

The VIPER 32-bit microprocessor has been invented at the UK Royal Signals and Radar Establishment (RSRE) for use in highly safetycritical military and civil systems. Throughout, formal mathematical methods have been used to prove that the gate-level realisations conform to a top-level specification. The paper explains the various layers of documentation produced, starting with the use of Michael Gordon´s LCF-LSM (based on Meta-Language, ML) at the higher levels, proceeding via the use of John Morison´s ELLA hardware description language at lower levels, to multiple VLSI implementations. It is intended to show that this route for designing synchronous VLSI circuits promises a practical means for industry to produce validated designs.