Мне было интересно, как люди реализуют бит-взрыв арифметических конструкций с плавающей запятой в решателях SMT. Существуют ли какие-либо существующие библиотеки или средства для этого (VHDL, ...) или они реализованы с нуля? Это представляет, сколько строк кода (C? C++?)?
Заранее спасибо.
Насколько мне известно, существует следующая реализация:
https://github.com/diffblue/cbmc/blob/master/src/solvers/floatbv/float_utils.cpp
Примерно 2KLoC в C++ (но построенный поверх служебных функций для всех операций с битовыми векторами, что является еще одним 2KLoC). Я полагаю, что это было первоначально написано из книги Мюллера и Пола. ESBMC содержит ответвление более ранней версии этого кода.
Смотрите ответ Кристофа выше. В Z3 была более ранняя реализация прототипа, которая была «вдохновлена» реализацией CBMC, но она потеряна в тумане времени.
Исходный код недоступен, реализация «вдохновлена» CBMC и, таким образом, аналогична по размеру и т. д.
Одна из моих ветвей CVC4:
https://github.com/martin-cs/CVC4/tree/floating-point-symfpu
имеет бит-взрывной движок с плавающей запятой. Она написана как «автономная» библиотека (см. src/symfpu — я бы дал полную ссылку, но github запрещает более двух ссылок на сообщение...), которая будет выпущена отдельно... скоро. Он параметризован во «внутренней части», поэтому его можно использовать как библиотеку с плавающей запятой произвольной точности, генерировать выражения битового вектора для разных решателей и т. д. Это около 3,5 тыс. LoC кода, но он содержит несколько реализаций некоторых операции. Он был написан с нуля (хотя я читал Handbook of Floating-Point).
Источник недоступен, я полагаю, что он реализован на C++, и мне кажется, что кто-то сказал мне, что он основан на книге Мюллера и Пола.
Обратите внимание, что были предприняты многочисленные серьезные независимые попытки (перекрестной) проверки и проверки этих реализаций. Я не буду утверждать, что все идеально (мы все еще пытаемся получить полную уверенность в остатке и FMA), но вы должны найти там, что они свободны от очевидных ошибок.
Вы можете использовать проекты VHDL или Verilog, но ... то, что делает хороший синтезируемый FPU, не является (обязательно) тем, что делает хорошее кодирование. Я знаю, что некоторые использовали SoftFloat в качестве источника реализации, но аналогичные комментарии остаются в силе.
В SMT-решателях пока не так много реализаций, но Z3 — одна из тех, что реализует все. Код находится в fpa2bv_converter.cpp и это довольно очевидно. На большие части кода меня вдохновила книга Мюллера и Пола «Архитектура компьютера», в которой есть глава о схемах с плавающей запятой. «Справочник по арифметике с плавающей запятой» (Мюллер и др.) Также содержит много информации/программ/схем.
