Descripción
Este es el primer libro que se centra en el problema de garantizar la corrección de los diseños de hardware de punto flotante mediante métodos matemáticos. Formal Verification of Floating-Point Hardware Design, Second Edition presenta una metodología de verificación basada en una teoría unificada de lógica de transferencia de registros y aritmética de punto flotante que ha sido desarrollada y aplicada a la verificación formal de unidades de punto flotante comerciales durante más de dos décadas, tiempo durante el cual el autor fue empleado por varias de las principales empresas de diseño de microprocesadores. La teoría se extiende al análisis de varios algoritmos y técnicas de optimización que se utilizan comúnmente en implementaciones comerciales de operaciones aritméticas elementales.
Como base para la verificación formal de dichas implementaciones, se presentan especificaciones de alto nivel de las instrucciones aritméticas básicas de varias arquitecturas de punto flotante estándar de la industria, incluyendo todos los detalles relacionados con el manejo de condiciones excepcionales. La metodología se ilustra en la verificación exhaustiva de una variedad de diseños comerciales de punto flotante de última generación desarrollados por Arm Holdings.
Esta edición revisada refleja las microarquitecturas en evolución y la creciente sofisticación de los procesadores Arm, y la variación en los objetivos de diseño de velocidad de ejecución, requisitos de área de hardware y consumo de energía. Se han añadido muchos resultados nuevos a las Partes I-III (Lógica de transferencia de registros, Aritmética de punto flotante e Implementación de operaciones elementales), ampliando la teoría y describiendo nuevas técnicas. Estos se derivaron según fue necesario en la verificación de los nuevos diseños RTL descritos en la Parte V.Autor: David M. Russinoff
Editorial: Springer
Publicado: 03/05/2023
Páginas: 436
Tipo de encuadernación: Tapa blanda
Peso: 1.43 libras
Tamaño: 9.21h x 6.14w x 0.94d
ISBN13: 9783030871833
ISBN10: 3030871835
Categorías BISAC:
- Informática | Desarrollo e ingeniería de software | General
- Tecnología e Ingeniería | Electrónica | Circuitos | General
- Informática | Arquitectura de computadoras
Acerca del Autor
David M. Russinoff es Ingeniero Principal Senior en Arm Holdings. Es licenciado por el Instituto Tecnológico de Massachusetts y doctor por la Universidad de Nueva York, ambos en matemáticas, y tiene un máster en ciencias de la computación por la Universidad de Texas en Austin. Ha dedicado veinticinco años al desarrollo de métodos matemáticos de verificación de hardware, con énfasis en la demostración interactiva de teoremas, y a su aplicación en el análisis de diseños comerciales, especialmente circuitos aritméticos.