Resumen

Desarrollamos un procedimiento de verificación formal para comprobar que los diseños de procesadores elásticos con pipelines implementan correctamente sus especificaciones de arquitectura de conjuntos de instrucciones (ISA). La noción de corrección que utilizamos se basa en el refinamiento. Las pruebas de refinamiento se basan en mapas de refinamiento que, en el contexto de este problema, son funciones que asignan estados del procesador elástico a estados del modelo de especificación ISA. El flujo de datos en arquitecturas elásticas se complica por la inserción de cualquier número de búferes en cualquier lugar del diseño, lo que dificulta la construcción sistemática de mapas de refinamiento para sistemas elásticos. Introducimos las funciones de finalización conscientes de los tokens, que incorporan un mecanismo para seguir el flujo de datos en los conductos elásticos, como un enfoque altamente automatizado y sistemático para construir mapas de refinamiento. Demostramos la eficacia del procedimiento general de verificación basado en funciones de finalización con reconocimiento de testigo utilizando seis modelos de procesadores elásticos en canalización basados en la arquitectura DLX.

• Materias:Ingeniería electrónica Redes Inalámbricas Banda ancha Procesamiento de señales asistido por computador Teoría de códigos
• Subjects:Electronic engineering Wireless Networks Broadband Signal processing computer-assisted Code theory
• Palabras claves:funciones de finalización conscientes, mapas de refinamiento, diseños de procesadores elásticos pipelined, modelo de especificación isa, estados de procesadores elásticos, procedimiento de verificación formal, procedimiento de verificación global, arquitectura dlx, flujo de datos, pruebas de refinamiento
• Keywords:aware completion functions, refinement maps, elastic pipelined processor designs, isa specification model, elastic processor states, formal verification procedure, overall verification procedure, dlx architecture, data flow, refinement proofs