Microprocesador VIPER

VIPER es un diseño de microprocesador de 32 bits creado por el Royal Signals and Radar Establishment (RSRE) en la década de 1980, destinado a ser utilizado en sistemas críticos para la seguridad, como la aviónica . ^{[ 1 ]} Fue el primer diseño de microprocesador comercial cuya corrección se demostró formalmente , aunque hubo cierta controversia en torno a esta afirmación y la definición de prueba. ^{[ 2 ]}

El diseño se completó en 1987 y fue implementado inicialmente por RSRE en una matriz de puertas lógicas. Posteriormente, Marconi Electronics obtuvo la licencia del diseño, implementándolo como el MAS1908 VIPER-1, fabricado con tecnologías CMOS y de silicio sobre zafiro, y empaquetado como un producto de matriz de rejilla de 120 pines. ^{[ 3 ]}

Desde el punto de vista arquitectónico, VIPER es un procesador de 32 bits que admite direccionamiento orientado a palabras de 20 bits para la memoria y el "espacio de E/S" (y, por lo tanto, 4 megabytes de cada uno). Aunque emplea una disposición de instrucciones uniforme que recuerda a las arquitecturas RISC, los tiempos de ejecución de las instrucciones varían de 6 a 26 ciclos de reloj, en contraste con el rendimiento de una instrucción por ciclo que buscan las arquitecturas RISC convencionales. ^{[ 3 ]}

Ian Currie, de RSRE, diseñó en 1984 un lenguaje de programación crítico para la seguridad llamado Newspeak para su uso con VIPER. Su característica principal era que todo comportamiento excepcional en los programas debía ser manejado en tiempo de compilación. ^{[ 4 ] [ 5 ]}

• MacKenzie, Donald. Conociendo las máquinas: ensayos sobre el cambio técnico.