Формальная проверка конструкции аппаратного обеспечения с плавающей запятой: математический подход

Это первая книга, посвященная проблеме обеспечения корректности аппаратных средств с плавающей запятой с помощью математических методов. «Формальная проверка конструкции аппаратного обеспечения с плавающей запятой», второе издание, развивает методологию проверки, основанную на единой теории логики передачи регистров и арифметики с плавающей запятой, которая была разработана и применена для формальной проверки коммерческих единиц с плавающей запятой в течение более двух десятилетий, в течение которых автор работал в нескольких крупных компаниях, занимающихся разработкой микропроцессоров. Теория расширена до анализа нескольких алгоритмов и методов оптимизации, которые обычно используются в коммерческих реализациях элементарных арифметических операций. В качестве основы для формальной проверки таких реализаций используются высокоуровневые спецификации основных арифметических инструкций нескольких крупных промышленных предприятий. представлены стандартные архитектуры с плавающей запятой, включая все детали, относящиеся к обработке исключительных условий. Методология проиллюстрирована в ходе всесторонней проверки различных современных коммерческих проектов с плавающей запятой, разработанных Arm Holdings. Это пересмотренное издание отражает развитие микроархитектур и растущую сложность процессоров Arm, а также изменение целей проектирования. скорости выполнения, требований к аппаратной площади и энергопотребления. В части I–III (логика передачи регистров, арифметика с плавающей запятой и реализация элементарных операций) было добавлено множество новых результатов, расширяющих теорию и описывающих новые методы. Они были получены в соответствии с требованиями проверки новых конструкций RTL, описанных в Части V.