TAM: An Abstract Machine Specification in Z

Resumen

Encontrar errores en las últimas etapas del desarrollo del diseño de hardware es costoso. En particular, para una arquitectura de microprocesador, la falta de ambigüedad es una propiedad esencial. Los métodos formales pueden ayudar a los diseñadores a identificar inconsistencias en las especificaciones de un sistema dado. Este artículo presenta una descripción formal de un subconjunto del conjunto de instrucciones de la arquitectura Triangle Abstract Machine (TAM) en Z. TAM es una máquina abstracta adecuada para la implementación de lenguajes de programación tipo Algol estructurados en bloques, como Pascal, Modula , Oberon y Triangle. La arquitectura de TAM se basa en la pila, lo que simplifica la generación de código. La notación matemática de Z y la estructura de su esquema ayudan a describir instrucciones lógicas y aritméticas y también proporcionan mecanismos adecuados para modelar instrucciones complejas que acceden a registros, memorias y la pila. Esta investigación propone un enfoque preciso, aunque abstracto, que evita la especificación de conceptos de bajo nivel, como los bits. El trabajo presentado aquí es un estudio de caso en especificación formal aplicado a una asignatura de Ciencias de la Computación.