Andy Ray：用 OCaml 设计 FPGA 并在其上运行软件

标题里有个谎言：这并不完全是从上到下都是 OCaml。我们可以用 HardCaml 领域专用语言设计 FPGA 和 ASIC 硬件，也可以用 OCaml 编写嵌入式软件，但这次演示使用的是厂商提供的软 CPU，而不是用 HardCaml 设计的 CPU。后端布局布线工具也来自厂商。

第一个演示让 LED 闪烁。你可能觉得这只要十行 Verilog，我更愿意说它用了 20 万行 OCaml。重置 FPGA 后，加载的设计包含 MicroBlaze CPU、256 MB DDR3 内存和一个定时器，还有通过总线和寄存器接口连接到 CPU 的 HardCaml 设计。

这个设计连接了三个核心：驱动灯带的 DigiLED 驱动器、连接光传感器的 SPI 接口，以及 CORDIC 核。CORDIC 用加法和移位计算正弦、余弦和双曲函数等。自定义引导程序从 SPI 闪存加载程序到 DDR 内存；LED 闪烁表示加载进度，大约每加载 64 KB 更新一次。

可以把 FPGA 想象成由查找表（LUT）和寄存器组成的网格，它们通过快速局部布线相连。交换盒将 LUT 输出连接到全局布线资源，信号可以借此穿过整个芯片。这是一种抽象，但有助于理解逻辑阵列。

一个四输入 LUT 可以由 16 个静态 RAM 单元构成，其内容在 FPGA 加载时设定。输入选择其中一个单元，因此它能实现任何四输入布尔函数。除最后一个单元外全部设为零，就得到与门；反过来设置就得到或门。现代器件常用六输入 LUT。可选寄存器可以保存结果，也可以绕过它来构建更大的组合函数。

FPGA 还有块 RAM，在我讨论的例子中，每块约为 10 到 288 千比特，现代器件包含数百到数万个块。它们的总带宽可以非常大。专用 DSP 模块提供乘法器和相关算术运算；时钟资源则产生并分配不同频率和相位的时钟。

配置通常来自闪存，USB 接口使我们可以方便地从 PC 对开发板编程。I/O 引脚本身也是复杂的资源。厂商还会加入实现 PCIe、以太网等功能的硬核硅电路，有些 FPGA 还包含 ARM 处理器核心。

RTL 设计位于抽象层次的较底层。它将加法器、编码器等组合逻辑与寄存器、RAM 等时钟驱动元件结合起来。软 CPU 又引入了嵌入式编程、指令集和操作系统；即使没有常规 CPU，可编程状态机也可以有自己的指令集。

主要的 RTL 语言包括 VHDL、Verilog，以及日益普及的 SystemVerilog。SystemC 主要是一种建模语言；另一些工具尝试把无时序的 C 转换为硬件，效果各不相同。这些硬件语言最初是作为文档语言构想出来的，其事件驱动语义需要时间适应。

在 Verilog 中，always 块可以在输入变化时更新输出，描述组合逻辑；对时钟上升沿敏感的块则每周期加载一次寄存器。RTL 是被动的，因此测试平台需要产生变化和延迟来驱动它。这些生成事件的结构用于仿真，不能综合成硬件。

商业仿真器包括 ModelSim 和 VCS，开源选择包括 Icarus Verilog 和 GHDL。Verilator 将可综合的 Verilog 转换成优化过的 C++ 模型，速度可以很快。在这次演讲时，我认为开源 SystemVerilog 仿真支持仍有缺口，尤其是厂商正在将 IP 转向这种语言。

RTL 调试往往意味着查看波形，也就是按时间绘制信号变化。即使是小型仿真，画面也很繁杂，真实设计可能大得多。约束随机激励和覆盖率驱动框架有助于测试设计中值得关注的部分，例如网络核心支持的数据包协议。

时序断言可以检查某个事件是否在另一个事件发生后的五个时钟周期内出现。仿真只检查实际运行的轨迹；形式验证则试图证明性质对所有轨迹成立。即使其中的机制像黑魔法，这仍是最有意思的部分。

HardCaml 的核心是用 OCaml 数据结构表示硬件，其中包含寄存器、存储器、多路复用器和操作等节点。它类似编译器的抽象语法树，但导线可以先创建和使用、之后再赋值，因此允许形成环。把设计看成硬件节点及其连接构成的可能带环的图更有帮助。

核心 API 提供适用于任意宽度位向量的算术、逻辑、比较、常量和多路复用操作。设计可以查询信号宽度，再构造与之适配的逻辑。实例化还允许我们在 HardCaml 图中留一个空位，之后填入第三方 Verilog 或 VHDL、厂商原语或宏。

运算符区分无符号或与符号无关的操作，以及乘法、比较等需要考虑有符号性的操作。很多检查在构建图的展开阶段进行，而不是在硬件运行时进行。API 对宽度要求严格：例如，把两位值和三位值相加就会报错。

API 使用两种表示。Bits 直接计算值，signals 则记录计算过程。我们用 signals 描述硬件图，在仿真时用 bits 向端口提供具体值。

HardCaml 的时序原语是寄存器和异步读取存储器；状态机等更高层结构在此基础上构建。always DSL 类似 Verilog 的 always 块：保护条件、if 语句和 switch 决定对寄存器或组合值的赋值。我们尤其用它来构建状态机和下一状态逻辑。

将存储器的地址或输出寄存起来，可以产生不同的读写行为，厂商工具应当能够推断它们，但推断并不总能成功。某些结构，包括真正的双端口 RAM，需要使用厂商宏；Verilog 也有同样的问题。

我心目中的硬件版 Hello World 是有限冲激响应滤波器。四个寄存器保存最近四个样本的滑动窗口。每个样本乘以一个常数系数，再由平衡树将结果相加。HardCaml 把寄存器窗口构造成列表，在其上映射有符号乘法，再用可复用的树函数归约结果。

HardCaml 提供周期精确仿真，而不是事件驱动仿真。构建仿真器、设置输入端口、推进一个周期、读取输出，然后重复即可。这适合简单设计，但硬件可能有 FIFO、寄存器和内存等多个独立接口，单一控制流就会变得难以使用。

HardCaml 的 step 测试平台大致相当于用于硬件测试的 Async：多个独立任务可以驱动不同接口，同时相互通信。我们将它与 Mark 编写的 MicroBlaze 指令集仿真器集成。该仿真器加载 MicroBlaze ELF 程序，以几兆赫的速度运行，并通过 AXI 等标准总线与仿真硬件交互。

为了调试，我编写了一个交互式终端波形查看器。HardCaml 也可以生成标准 VCD 文件，供 GTKWave 等工具查看，或者在仿真运行时将数据流送到 GTKWave。波形期望测试将预期波形写进测试本身，因此行为变化时，持续集成系统可以显示差异。

文本波形在大约 30 个周期之后就可能变得难以处理，但它很适合记录那些应保持稳定的小型协议细节。测试发生变化时，差异会清楚地提示哪里需要关注。

假设要证明一个十位加法器正确。两个输入共 20 位，大约有一百万个测试用例；到了 200 位，穷举测试就不可行了。SAT 求解器则寻找能让布尔函数为真的输入赋值。如果存在这样的赋值，它返回 SAT 和对应的值；如果不存在，则返回 UNSAT。

要证明某个性质始终成立，可以向求解器询问其否定。UNSAT 意味着没有任何输入能让否定成立，因此原性质成立；SAT 则提供一个反例，指出失败的位置。HardCaml 可以将组合电路上的一位性质转换成 SAT 问题。

我们还有一个时序等价性检查框架。为了验证从 Verilog 移植到 HardCaml 的结果，我用 Yosys 将 Verilog 转成低层网表，载入 HardCaml，然后检查两者的输出是否始终相同。这种方法要求两个电路的对应位置都有寄存器。

有界模型检查可以使用时序性质，在固定长度的轨迹上比较状态不同的电路。对 100 个周期的证明并不能说明第 101 个周期的情况。我的检查器在小案例上可以工作，虽然我还没有完全信任它；即使有边界，这项技术仍很强大。

软件栈运行在 MicroBlaze 上，这是用 FPGA 逻辑阵列构建的 Xilinx 软 RISC CPU。这个架构没有原生 OCaml 编译器，但有 GCC 交叉编译器。我交叉编译了 OCaml 的 C 运行时和 Zinc 字节码解释器，然后使用在 x86 上正常构建的字节码库，尽管目标平台是 32 位。

OCaml 的 `-output-obj` 选项会生成一个 C 文件，将程序字节码放在整数数组中，交叉编译器可以编译该文件。棘手之处在于找到、编译并链接 OCaml 库使用的 C 桩代码；我总共找到了大约 40 个 C 文件。

在这个环境中，信号和线程都不能工作，也没有文件系统或 Unix 环境。RTOS 可能提供线程，但我不确定它们是否符合 OCaml 的预期。Base、Core_kernel 和 Async_kernel 可以工作，OCaml 顶层环境也可以：编译器本身就在 FPGA 上运行。

代价是程序体积。最小的可执行文件约为 400 KB；加入 Jane Street 库后约为 700 KB，使用更多功能则很快达到 4–5 MB。带这些库的顶层环境总共约 23 MB：它无法剔除可能用到的代码，而用于类型检查的 CMI 文件占了大约 16 MB。

现场顶层环境演示中，处理器的标准输入和输出通过 USB 传到笔记本电脑的驱动程序，再桥接到 TCP 套接字；我用 netcat 连接。输入 `let a = 1` 后，运行在 FPGA 上的 OCaml 会编译它并显示结果。

脉宽调制演示快速开关 LED，使其看起来具有中间亮度。改变亮度就产生呼吸效果。Cylon 演示让一盏灯沿灯带来回移动，用忙等待循环减慢速度，并在每次更新时将每个 LED 的亮度减半，留下逐渐消失的尾迹。

光传感器 Pmod 通过 SPI 读取：启动传输，等待完成，再读取结果。低四位舍弃，接下来的八位表示光强。我不确定读数波动是灯光闪烁还是传感器精度造成的，所以演示将大约 500 次读数取平均，并在 LED 灯带上显示结果。

一位观众询问 LED 驱动器。Mark 用 HardCaml 编写了 DigiLED 驱动器。一根线路传送代表 RGB 值的脉宽调制位，驱动器沿灯带依次对 LED 编程。

另一个演示使用 HardCaml 的 CORDIC 核计算余弦。该核心也能计算反正切、双曲函数和坐标旋转等。它同时计算正弦和余弦；我配置输入、设定角度并等待计算完成。由于收敛范围大约限于负二分之一 π 到正二分之一 π，代码先约简角度，再利用象限对称性。

余弦值显示在 LED 上，颜色区分正负，亮度表示大小。逐步增加相位会让波形沿灯带移动。我最喜欢的演示在 FPGA 上运行 Async：三个独立移动的彩色光点覆盖不同范围，第四个任务则不断将亮度减半，形成尾迹。

在演讲时，我预计一两天内会在 Jane Street 仓库发布大幅改进的 HardCaml 版本，尤其增加了大量测试。我希望之后发布旧版波形工具、step 测试平台和 MicroBlaze 仿真器。演示代码还需要整理，而为 OPAM 打包交叉编译的 C 依赖是发布过程中的难点。

一位观众问，软件是否运行在 FPGA 内实现的处理器上。是的：MicroBlaze 是五级 RISC 软 CPU。这块板没有硬处理器；如果 FPGA 有硬处理器，我会使用它。软 CPU 用于管理或调试工作，而不是性能关键路径。

有人问能否直接用硬件执行 OCaml 字节码。我说，我以前在 HardCaml Zinc 项目中构建过一个状态机，可以执行约四分之三的 Caml 字节码虚拟机。我希望完成它，但 Caml 的很多部分仍用 C 实现，因此还需要一个 RISC CPU。

一位观众问“没有 Unix”是什么意思。Unix 模块处理文件和网络，但这个软 CPU 没有文件系统。设计实际上有网络接口，只是我还没有让它工作；要支持 Unix 风格套接字，需要模拟层，我们可能会改用更低层的 API。

HardCaml 在 PC 内存中描述硬件图，再为后端工具生成 Verilog。它并非仅仅以字节码形式运行设计。缺点是生成的 Verilog 很难阅读，而且要仔细处理，才能让有用的名称一直保留到网表中，供时序收敛使用。

被问到 Bluespec 时，我解释说 HardCaml 的抽象层次接近 Verilog 和 VHDL；它不会像 Bluespec 那样推断微架构。我喜欢 Bluespec 的思路，虽然我只是读过相关论文；我们正在考虑在 HardCaml 之上建立一个模拟原子操作的 DSL。

对于时序问题，架构很重要。HardCaml 生成的 Verilog 与工程师编写的设计紧密对应。给 HardCaml 设计中的每个寄存器命名后，时序报告就可以显示从一个命名元件到另一个命名元件的路径，尽管生成的 Verilog 本身仍然难读。

我希望用 RISC-V 取代 MicroBlaze。除了个人兴趣，掌控这部分技术也可能让升级和编译器管理更容易，不必依赖频繁变化的大型厂商工具链。

在小板子上运行交互式顶层环境，一部分是为了好玩，但软 CPU 在我们的设计中确实有实际用途。某些嵌入式代码，例如紧急停止开关，可能非常关键，需要经过审查。团队熟悉 OCaml 代码审查，而引入大量 C 代码则不那么让人放心。交互式顶层环境还可以让工程师检查寄存器，帮助早期调试。

最后，有人问到求解器。我说我目前使用的是 SAT 工具，主要是 MiniSat，而不是 SMT。Z3 及其 OCaml 绑定最近进入了仓库，我希望有时间时尝试一下。