Офіційна перевірка конструкції апаратного забезпечення з плаваючою комою: математичний підхід

Це перша книга, яка присвячена проблемі забезпечення коректності проектів обладнання з плаваючою комою за допомогою математичних методів. Друге видання Formal Verification of Floating-Point Hardware Design пропонує методологію перевірки, засновану на єдиній теорії логіки передачі регістрів і арифметики з плаваючою комою, яка була розроблена та застосована для формальної перевірки комерційних модулів з плаваючою комою протягом більше двох десятиліть, протягом яких автор працював у кількох великих компаніях з розробки мікропроцесорів. Теорія поширена на аналіз кількох алгоритмів і методів оптимізації, які зазвичай використовуються в комерційних реалізаціях елементарних арифметичних операцій. Як основу для формальної перевірки таких реалізацій, високорівневі специфікації базових арифметичних інструкцій кількох основних промислових – представлені стандартні архітектури з плаваючою комою, включаючи всі деталі, що стосуються обробки виняткових умов. Методологія проілюстрована всебічною перевіркою різноманітних найсучасніших комерційних проектів із плаваючою комою, розроблених Arm Holdings. Це переглянуте видання відображає розвиток мікроархітектури та зростаючу складність процесорів Arm, а також варіацію в цілях проектування. швидкість виконання, вимоги до апаратної площі та енергоспоживання. Багато нових результатів було додано до частин I-III (логіка реєстру-передачі, арифметика з плаваючою комою та реалізація елементарних операцій), розширюючи теорію та описуючи нові методи. Вони були отримані відповідно до вимог верифікації нових проектів RTL, описаних у частині V.

• Автор: Девід М. Руссінофф
• Видавець: Springer
• Рік випуску: 2022
• Обкладинка: тверда обкладинка
• Кількість сторінок: 436
• Розміри: 23,5 x 15,5 x 0 см
• Ілюстрації: 40 ілюстрацій, чорно-білі; XXVIII, 436 стор. 40 іл.
• Мова: англійська
• ISBN: 9783030871802