Resumen

Desarrollamos dos técnicas de optimización, flush-machine y collapsed flushing, para mejorar la eficiencia de la verificación automática basada en refinamiento de modelos de procesadores fuera de orden (ooo). El refinamiento es una noción de equivalencia que puede utilizarse para comprobar que un procesador ooo implementa correctamente todos los comportamientos de su arquitectura de conjunto de instrucciones (ISA), incluida la detección de bloqueos. Las técnicas de optimización actúan reduciendo la complejidad computacional del mapa de refinamiento, una función fundamental para las pruebas de refinamiento que asigna los estados del modelo de procesador ooo a los estados de la ISA. Esto repercute directamente en la eficacia de la verificación, que se estudia utilizando 23 ooo modelos de procesador. Flush-machine, es una novedosa técnica de optimización. La descarga colapsada se ha empleado anteriormente en el contexto de los procesadores de orden interno. Mostramos cómo aplicar la descarga colapsada a modelos de ooo procesadores. Utilizando las dos optimizaciones juntas, podemos manejar 9 ooo modelos que no podían verificarse utilizando la descarga estándar. Además, las optimizaciones proporcionan un aumento de velocidad del 23,29 con respecto a la descarga estándar.

• Materias:Ingeniería electrónica Redes Inalámbricas Codificación de video Procesamiento de señales asistido por computador Procesamiento de datos
• Subjects:Electronic engineering Wireless Networks Video Coding Signal processing computer-assisted Data processing
• Palabras claves:modelos de procesadores ooo, estados de modelos de procesadores ooo, arquitectura de conjuntos de instrucciones, novedosa técnica de optimización, técnicas de optimización funcionan, eficiencia, máquina, optimizaciones, verificación, estados isa
• Keywords:ooo processor models, ooo processor model states, instruction set architecture, novel optimization technique, optimization techniques work, efficiency, machine, optimizations, verification, isa states