在 SMT 中实现浮点运算的位爆破

Question

我想知道人们如何实施位爆破 SMT求解器中的浮点算术结构。在那里 任何现有的库或设施（VHDL，...），或 他们是从头开始实施的吗？这代表了多少 (C ? C++ ?) 代码行？

提前致谢。

Answer 1

据我所知，存在以下实现：

CBMC（不是严格意义上的 SMT 求解器，但包含必要的位）

https://github.com/diffblue/cbmc/blob/master/src/solvers/floatbv/float_utils.cpp

在 C++ 中大约为 2KLoC（但构建在所有位向量操作的实用函数之上，这是另一个 2KLoC）。我相信它最初是从穆勒和保罗的书中写的。 ESBMC 包含此代码早期版本的一个分支。

Z3

请参阅上面克里斯托夫的回答。 Z3 中有一个较早的原型实现，它受到 CBMC 实现的“启发”，但这已经被时间的迷雾迷失了。

数学SAT

来源不可用，实施受到 CBMC 的“启发”，因此大小相似，等等。

CVC4

我的 CVC4 分支之一：

https://github.com/martin-cs/CVC4/tree/floating-point-symfpu

具有位爆破浮点引擎。它被编写为一个“独立”库（请参阅 src/symfpu - 我会提供完整链接，但 github 会阻止每个帖子超过两个链接......），它将单独发布......很快。它在“后端”中被参数化，因此它可以用作任意精度的浮点库，为不同的求解器生成位向量表达式等。它大约 3.5KLoC 的代码，但确实包含一些的多个实现操作。它是从头开始编写的（虽然我已经阅读了浮点手册）。

声波

来源不可用，我相信它是用 C++ 实现的，并且感觉有人告诉我它是基于 Mueller 和 Paul 的书。

请注意，为了（交叉）验证和验证这些实现，已经进行了多次、认真、独立的努力。我不会声称一切都是完美的（我们仍在努力对剩余和 FMA 充满信心），但您应该会发现它们没有明显的错误。

您可以使用 VHDL 或 Verilog 设计，但是......制作好的可合成 FPU 并不是（必然）制作好的编码。我知道有些人使用 SoftFloat 作为实现的来源，但类似的 cmets 也有。

Answer 2

在 SMT 求解器中还没有“很多”实现，但 Z3 是实现所有功能的解决方案之一。代码在fpa2bv_converter.cpp 中，它是相当不言自明的。对于大部分代码，我从 Mueller 和 Paul 的“计算机体系结构”一书中获得灵感，其中有一章是关于浮点电路的。 “Handbook of Floating-Point Arithmetic”（Muller 等人）也提供了大量信息/程序/电路。