ARCH HDL中形式化验证的可综合浮点数据类型

# 形式上已验证的综合浮点数据类型 (ARCH HDL)  
来源: https://arxiv.org/html/2607.23715  

###### 摘要

我们报告了一等 IEEE-754 binary32 (FP32) 和 bfloat16 (BF16) 算术在 ARCH 上的设计与端到端验证。ARCH 是一种硬件描述语言，设计用于由语言模型根据自然语言规范生成。每个浮点运算符——包括两种格式下的比较、转换、加法、减法、乘法以及融合乘加——都在宿主语言嵌入式 DSL 中针对单一位向量中间表示描述一次，并从一个源渲染为三种形式：可综合的 SystemVerilog（硬件）、SMT-LIB（形式模型）和 Lean 4（结构化证明模型）。由于三个后端共用同一个描述和同一个线性化，硬件、形式模型与证明模型在结构上不会漂移：它们是同一数据流图以三种语法打印出来的结果。三者之间仅剩的是约二十个打印器的每节点语法表；在硬件侧，即便是那部分也由机器检查——Yosys 独立读取生成的 SystemVerilog，求解器证明其对所有运算符都与 SMT 模型等价。我们采用一种贴合求解器可处理边界的混合策略来验证运算符：**无乘法器**运算符（所有六种 FP32 比较和整个 $2^{64}$ 输入空间上的有界加法/减法、格式转换，以及所有**二元** BF16 算术，覆盖 $2^{32}$ 空间）被穷举地证明等价于 SMT-LIB 的 FloatingPoint 理论；**带乘法器** 运算符（FP32 的 `mul` 和 `fma`——对任何位爆炸器而言都是 SAT 困难问题）则通过在 Lean 中进行代数提升来机器证明其正确舍入，且不含 `sorry`。（唯一的刻意例外：BF16 的 `fma` 是一个 FP32 累积融合——遵循 Tensor-Core/TPU 约定——其机器特性描述明确为此，并非声称正确舍入。）随后进行的物理特性分析（开源 Yosys 综合和 OpenSTA 时序分析）暴露出 `fma` 是时序异常点：其精确宽 470 位对齐加法器是一个组合锥，我们的综合流程无法对其流水线化（ABC 重定时在任何测试配置下都未将寄存器移过该锥）。因此我们将 `fma` 重新实现为一个有界 98 位保护/舍入/粘滞数据路径，它能够干净地流水线化至 268MHz——并在 Lean 中**无 `sorry`** 地证明该有界数据路径在全部 $2^{96}$ 个输入上与精确宽参考**比特一致**，从而无需重新处理乘法器即可继承参考的正确舍入证明。等价性的可证性恰恰在于共享乘法器出现在两侧并相互抵消。我们给出了架构、双层证明方法、综合结果、信任基础（标准的三个公理加上 `bv_decide` 的原生检查 LRAT 证书公理），以及一次独立的对抗性审计。

## 1 引言

ARCH¹¹ 是一个为微架构工作设计的专用硬件描述语言，其语言表层能够由语言模型从自然语言硬件描述正确生成，并编译为确定、可读的 SystemVerilog。一种旨在描述真实数据路径的语言需要一等浮点支持：不是附加的库，而是将 FP32\[1\] 和 BF16\[2\] 作为内置类型，其运算符需要 (i) **正确舍入** 至 IEEE-754，(ii) **可综合** 为高效的 RTL，且 (iii) **可信**，因为机器生成的硬件最需要机器检查的保证。这三个目标相互冲突。正确舍入是一个精确但微妙的规范。穷举形式等价检查在对于吞吐量最重要的一个运算符——融合乘加——处碰壁，因为其尾数乘法器使得 miter 成为 SAT 困难问题\[9,11\]（miter 将待比较的两个电路连接到共享输入并异或输出，从而将等价性归约为该异或的不可满足性）。而最明显正确的 fma 数据路径（先计算精确的宽乘积和，再舍入）在时序上又是最差的。

本文报告了我们如何在 ARCH 中解决所有这三个问题，而这条解决路径本身与最终结果同样重要：

1.  **单一源，三个后端**。每个运算符直接基于共享的位向量 IR（一个通过构造共享子项的 DAG）定义一次；三个渲染器从该描述和同一个线性化分别生成可综合的 SystemVerilog、SMT-LIB 和 Lean 4（第 3 节）。硬件、SMT 模型和证明模型在**结构上**是三种语法下的同一工件；SystemVerilog 打印器的语义对应性通过 Yosys 到 SMT 的 miter 进行机器检查，Lean 打印器的则通过字节相同的重新生成审计（第 10 节）。
2.  **在易解性边界上的双层证明方法**。无乘法器运算符通过 SMT 针对 IEEE-754 的 FloatingPoint 理论**穷举**处理；带乘法器运算符则在 Lean 中通过将比特模式提升为代数值进行**结构化**证明，从而 $24 \times 24$ 数组永远不会被位爆炸（第 4 节）。
3.  **时序驱动设计，事后验证**。综合和静态时序分析（第 5 节）表明精确宽的 fma 是异常点，且抵制重定时（ABC 在任何测试配置下都未将寄存器移过该锥）；我们将其重新设计为一个有界的粘滞折叠数据路径（第 6 节），可流水线化至 268 MHz，并在全部 $2^{96}$ 个输入上证明其与精确宽参考**比特一致**（第 7 节），因此快速数据路径继承了参考的正确舍入证明。等价性无需重新处理乘法器即可证明，因为共享乘法器抵消了。

最终结果是浮点特性中的每个运算符都根据其声明的契约（对于 BF16 的 fma，一个 FP32 累积融合，声明的是该契约而非正确舍入；第 4.3 节）要么被穷举验证，要么被结构化验证，其模型可证明就是生成的 RTL，具有清晰的公理基础和一次独立审计（第 8 节）。

## 2 背景

#### 正确舍入。

对于具有 $p$ 位尾数的目标格式，正确舍入运算返回 $\mathrm{RNE}(v)$，其中 $v$ 是**精确**实数结果，$\mathrm{RNE}$ 是向最近舍入、偶数舍入\[1\]。对于 fma，$v = a \cdot b + c$ 且无中间舍入形成。因此“正确舍入”包含两个声明：形成精确值，并对其舍入。

#### 保护/舍入/粘滞。

硬件保留结果尾数加上三个汇总位：保护位（保留尾数之下的第一位）、舍入位（下一位）和粘滞位（所有更低位的或）。对 GRS 编码值的 RNE 是精确的——当且仅当 $\text{guard} \land (\text{round} \lor \text{sticky})$ 时向上舍入，偶数舍入——因此工程问题是在不具体化整个精确值的情况下生成 GRS 位。

#### 乘法器壁垒。

在特殊值被处理后，算术电路与其规范之间的等价性是一个无量词位向量（和浮点）公式。位爆炸将 $24 \times 24$ 尾数乘法器转换为二次门网络，其合取范式在 binary32 输入空间上难以处理。乘法器 miter 是典型的困难 SAT 实例——正是出于这个原因，它们是一个标准基准家族\[9\]——并附带关于求解器为何在非线性整数算术上困难的下界分析\[10\]——困难到最先进的乘法器验证放弃普通 SAT 而转向计算机代数\[11\]。一致地，z3、cvc5 和 Lean 策略 `bv_decide`\[8\] 在此处都在 `mul` 和 `fma` 上停滞。所有不含乘法器的运算——比较、转换以及数据路径保持狭窄的有界加/减——都是可穷举判定的；带乘法器的运算符则不是。我们的方法论正是围绕这条边界组织的。

## 3 单一源架构

![图 1: 一个描述，三个后端。分叉线以上的所有内容是一个单一的共享工件（结构一致性通过构造保证）；残余信任是分叉线以下的每节点语法表；SystemVerilog 侧通过 Yosys 到 SMT 的 miter 进行机械处理（所有 24 个运算符均为 unsat，第 10 节），Lean 侧通过字节相同的重新生成审计。](https://arxiv.org/html/2607.23715/x1.png)

每个运算符在 Rust 中直接基于指针共享的位向量 IR 构建一次（图 1）：一个节点（add、sub、mul、ite、extract、concat、zero_extend、位向量比较和命名调用）的有向无环图，其中构建器复用的子项是一个节点，而不是副本。一次共享的**线性化**过程将该 DAG 展平为一个直线程序：一个单一拓扑顺序的临时赋值序列 `_t0`, `_t1`, ...，采用静态单赋值形式——每个临时变量仅定义一次，仅引用较早的临时变量，每个共享节点仅发射一次。三个渲染器遍历该单一编号序列（表 1），区别仅在于通过每节点语法表如何拼写一行（例如，`Bin::Add` 节点在 SystemVerilog 中打印 `+`，在 SMT-LIB 中打印 `bvadd`，在 Lean 中打印 `+` on `BitVec`）；因此 `_t44` 在硬件、SMT 模型和证明模型中命名的是**同一个节点**。

| 节点 | 比特宽 | SV 打印 | SMT 打印 | Lean 打印 |
|------|--------|--------|----------|-----------|
| `Add(n,m)` | `max(n,m)` | `t_i + t_j` | `(bvadd t_i t_j)` | `t_i + t_j` |
| `Mul(n,m)` | `n+m` | `t_i * t_j` | `(bvmul t_i t_j)` | `t_i * t_j` |
| … | … | … | … | … |

表 1：单一比特向量 IR，三个渲染器。共享 IR **和**线性化，渲染器不可能在结构上不一致——仅可能在每运算符语法表上不一致。

由于三个消耗的是同一个 IR 和同一个线性化，它们在共享、控制流或节点顺序上不可能不一致；Lean 证明模型是 `render_lean` 生成的一个快照，我们确认（第 8 节）它与新鲜重新生成的结果字节一致——因此证明是关于所生成工件的，而非一种转述。三个工件可能**产生分歧**的唯一途径是语法表中某个条目错误——单个节点种类的误译，这将均匀出现在使用该节点的每个运算符中，而非作为运算符特定的错误。第 10 节将这种失效模式界定为残余的渲染器信任——而 Yosys 到 SMT 的 miter 现在针对 SystemVerilog 渲染器自动处理了该问题。运算符集合涵盖六种 FP32 比较；FP32 的 add、sub、mul、fma；转换 FP32→BF16（窄化，RNE）、BF16→FP32（加宽，精确）以及 FP32→有符号/无符号整数（向零，饱和）；以及 BF16 的比较和算术（这些通过 FP32 数据路径路由）。NaN 规范化遵循一个可选择的配置（例如 RISC-V 与 CUDA 约定）。

## 4 验证方法

### 4.1 第一层——针对无乘法器运算符的穷举 SMT

SMT 渲染器将每个运算符发射为一个 `define-fun`；一个 miter 断言其与 SMT-LIB 的 FloatingPoint 理论\[7\]——IEEE-754 RNE 的标准化形式化，与 Berkeley SoftFloat 实现的值语义相同——的等价性的否定。`unsat` 裁决意味着生成的 RTL 运算符与其理论的 RNE **值**语义在整个输入空间上匹配（结果位模式，我们的规范化 NaN 选择在 miter 中明确固定）。我们**穷举**处理以下内容：

- 所有六种 FP32 比较和转换，覆盖其全部定义域（$2^{64}$ 比较空间；FP32→BF16 窄化覆盖 $2^{32}$；BF16→FP32 加宽覆盖 $2^{16}$；FP32→整数对于范围内的输入，部分函数边界已记录而非无声声称）；
- FP32 的 `add` 和 `sub` 与 `fp.add`/`fp.sub` 在全部 $2^{64}$ 输入上比较。决定性因素是数据路径宽度而非输入空间：有界加法器将对齐后的幅度保持在约 56 位（无乘法器），因此位爆炸后的 miter 保持较小；
- 所有**二元** BF16 算术（`mul`、`add`、`sub` 和六种比较）覆盖整个 $2^{32}$ 输入空间。BF16 的小输入空间使得即使是带乘法器的二元运算符也变得可处理（尽管它们通过 FP32 数据路径路由）；跨求解器相互检查。三元 BF16 的 `fma`（$2^{48}$ 空间）故意**不在**此列表中：它是 FP32 累积的，其独特契约在第 4.3 节中声明。

#### 精确契约。

本文中的“IEEE-754”仅指 **在固定舍入制度下的结果位值语义**，不含其他含义。舍入在算术和格式转换中静态为 RNE（饱和浮点转整数路径为向零舍入）；没有动态舍入模式输入，也没有状态标志——invalid、inexact、overflow、underflow 不予计算。NaN 处理通过显式的规范化配置：IEEE-754 和 SMT-LIB 都抽象了 NaN 的有效载荷，因此每个 miter 的 NaN 分支固定我们规范化后的输出，而非诉诸理论。比较实现静默谓词（`fp.eq` 及其同类）；没有信号变体，因此也没有无效操作的侧通道。浮点转整数在 ARCH 级别定义为**饱和**，具有确定的 NaN 和范围外结果；SMT-LIB 的 `fp.to_sbv`/`fp.to_ubv` 在那里未定义，因此 miter 仅覆盖理论定义的范围内的定义域，而饱和/NaN 行为是文档化的 ARCH 契约，由定向模拟而非形式证明验证。最后，所有三个模型都是**二态**的：IR 及其 SMT 和 Lean 渲染没有 X/Z，因此 SystemVerilog 的四态行为（X 传播、高阻抗）不在验证契约之内——该契约针对完全驱动的二进制输入。

### 4.2 第二层——针对乘法器壁垒的结构化 Lean

FP32 的 `mul` 和 `fma` 携带 $24 \times 24$ 乘法器，对于任何位爆炸器都会超时。结构化证明器通过**不**进行位爆炸来突破壁垒。遵循 Flocq / FloVer 方法\[3,4\]，证明将比特模式提升为代数 $(sign, significand, exponent)$ 视图，对应一个有理数值，并显示运算符**结构化地**计算 $\mathrm{RNE}(a \cdot b \, [+\, c])$：$24 \times 24$ 数组坍缩为一个单一的 `Nat` 乘法，其代数基础是初等的。开发被分解为一个可重用的**舍入器**特性——即共享的向最近偶数舍入编码器找到真正的领先位（通过前导零计数/最高有效位桥），执行一次精确的往返，并满足 $1 \cdot x = x$——以及在此基础上每个运算符的归约。对于 fma，这得到 `arch_round470_correct` 以及一个**无 `sorry`** 的证明，表明有限 FP32 的 fma 是针对值级别模型正确舍入的。