Especificación, exploración y simulación arquitectónicas a través de la lógica de reescritura

Abstract

En los últimos años, el Grupo Arvind del MIT ha demostrado la utilidad de la teoría de la reescritura de términos para la especificación de arquitecturas de procesadores. En sus procesadores de enfoque Los sistemas de reescritura de términos especificados se traducen en una descripción de hardware estándar lenguaje con fines de simulación. En este trabajo presentamos nuestra investigación actual sobre el uso de Reescritura-Lógica, que es un marco teórico más poderoso que el puro reescritura, para especificación, exploración y verificación de arquitecturas de procesador a un mayor nivel de abstracción. Adoptamos el entorno de lógica de reescritura ELAN para especificar, explorar y verificar arquitecturas sin necesidad de recurrir a los detalles del hardware lenguajes de descripción para fines de simulación. Nuestra investigación muestra que la simulación a nivel de lógica de reescritura puede proporcionar información útil para guiar el diseño arquitectónico.