港大开源芯片设计Agent infra，用证明定理的方式来做形式化验证

智猩猩AI整理

最近，一个让大模型设计电路，还能为电路写证明的芯片设计项目开源了。

这套系统分为两层：底层基础设施 CKTLean，以及上层 Agent 框架 CktFormalizer。

CKTLean 提供嵌入 Lean 4 的带类型硬件描述语言、编译器和交互式环境（REPL）；CktFormalizer 则在此基础上调度大模型与工具，完成电路生成、修复、优化和等价性证明。

项目来自香港大学研究团队。它将类型检查和证明反馈引入电路设计过程，为 Agent 的生成、修复与优化提供可检查的依据。

设计通过 Lean 的类型检查后，由 CKTLean 导出 SystemVerilog，再进入仿真、综合和布局布线流程，逐步推进到物理版图。

论文报告，CktFormalizer 搭配 CKTLean，在 VerilogEval 的 156 道题上实现了 99.4% 的编译通过率。在四个评测基准中，以通过 RTL 功能仿真的设计为统计对象，综合通过率为 100%，布局布线、设计规则检查（DRC）和版图与原理图一致性检查（LVS）的通过率均不低于 95%。

围绕同一份 CKTLean 代码，系统还支持功耗、性能和面积（PPA）优化，以及源代码层面的等价性证明。在优化实验中，综合面积最大降幅达到 58.6%；引入交互式证明后，证明完成率从 53.3% 提升至 63.3%。

CktFormalizer 整体流程图

如上图所示，CktFormalizer 将电路设计串成五个环节：

（1）输入规格（左上）：提供自然语言规格、参考设计和 Lean 示例代码。

（2）生成代码（紫色）：大模型编写 Lean 代码，并根据编译器反馈，在“修改—编译—诊断”的循环中逐步修复问题。

（3）形式化验证（青色）：将描述预期行为的形式化规格与编译通过的电路实现进行比较，由 Agent 逐步构建两者等价的证明。

（4）综合与物理设计（橙色）：从 Lean 导出 SystemVerilog，依次进行功能仿真、逻辑综合和布局布线。

（5）PPA 优化（底部粉色）：将面积、时序等指标反馈给 Agent，驱动其调整架构、重新证明等价性；若优化失败则回滚，并持续保留表现最好的版本。

图右上角列出了流程中使用的工具，它们统一运行在 Docker 环境中。最左侧展示最终产出，包括 Lean 源码、等价性证明、SystemVerilog、GDSII 版图和 PPA 指标。

在这套流程中，CKTLean 提供语言、编译和交互式证明工具，CktFormalizer 负责组织 Agent 的生成、验证与优化循环。两者的具体分工如下：

当前，利用大模型生成寄存器传输级（RTL）设计的一种常见做法，是直接生成 Verilog，再根据仿真结果反复修正。

这条路径的一个难点在于，Verilog 工具未必会把所有潜在问题都当作错误。位宽不匹配、case 分支遗漏等情况，有时只会触发警告，甚至不会给出明显提示，问题可能直到仿真或综合阶段才暴露。

论文将这一挑战归纳为两点。首先，仅靠语法检查和 RTL 仿真，无法充分保证设计正确。语法检查只能确认代码符合语法规则，仿真也只能覆盖有限的测试轨迹；它们既不能保证实现与原始规格完全一致，也不能保证设计能够完成物理实现。

其次，优化会进一步放大这一挑战。PPA 优化需要反复修改设计，每次修改都必须保持功能一致，并继续通过综合与物理实现流程。

提高硬件描述的抽象层级，有助于组织复杂设计，但仍需配套的正确性保障。Chisel、Bluespec、Clash 等高层硬件语言都能编译为 RTL。这项工作进一步选择将硬件描述与机器可检查的推理结合起来，在 Lean 4 中构建硬件语言。

要走通这条路径，基础设施是关键。论文指出，已有的 Lean 硬件语言 Sparkle 支持带类型的电路描述和 SystemVerilog 导出，但可覆盖的设计范围有限，对 Lean 生态中现有引理和证明策略的利用也有待扩展。Agent 能表达哪些电路、编译哪些设计，以及如何在迭代中修改和验证，都受到这一层能力的约束。

因此，论文关注的核心问题是：将嵌入 Lean 的带类型硬件中间表示，与交互式类型检查和证明反馈结合，能否帮助 Agent 生成正确的硬件，并完成源代码层面的等价性证明？

CKTLean 为模型提供了一种嵌入 Lean 4 的硬件描述方式，将电路表示为带类型的程序。

在这种表示中，位宽是类型的一部分，模式匹配必须覆盖所有情况，相关错误会在类型检查阶段被拦截。模型因此能更早获得指向具体代码位置和类型不匹配的诊断信息，在进入仿真之前就修复一部分问题。

CKTLean 基于开源项目 Sparkle HDL 扩展而来。团队先通过来自 CVDP 的 17 个代表性硬件任务，识别出原版 Sparkle 在五类场景中的局限：带状态的参数化设计、存储器、位操作、有符号运算和多时钟设计。

针对这些场景，CKTLean 扩展了类型化中间表示与编译流程，并提供常驻的 Lean REPL，支持交互式类型检查与定理证明。Agent 可以将不同电路实现在给定假设下的等价性表述为 Lean 定理，借助 REPL 返回的证明目标和诊断信息逐步构建证明，完成的证明由 Lean 内核检查。

在 CKTLean 提供的语言和工具之上，CktFormalizer 负责调度大模型、编译器和后端工具。基础的生成与评测流程分为四步：

（1）生成：Agent 读取自然语言规格，编写 Lean 文件，并根据编译器诊断反复修复。每道题的总交互预算为 100 轮，其中初始生成阶段最多使用 40 轮。

（2）导出：设计编译通过后，由工具链自动生成 SystemVerilog。

（3）功能验证：使用基准自带的测试平台（testbench）进行仿真。在这一评测流程中，仿真结果不回传给 Agent。

（4）物理实现：结合 SkyWater 130 nm 工艺库，调用 OpenROAD 等工具，完成综合、布局布线、DRC、LVS 和门级仿真。

论文在四个公开基准上进行了端到端评测，共涉及 430 道题。

其中，CVDP 更贴近实际 RTL 设计与验证场景，覆盖状态机控制、算术数据通路、互连和存储器等多类任务。本研究使用其中的 168 道题进行评测。这些任务也对底层基础设施提出了更高要求：硬件语言能否表达不同类型的复杂电路，编译流程能否保留参数关系并正确处理这些结构，都会影响 Agent 最终能够完成哪些设计。

下表展示了 CktFormalizer 搭配 CKTLean 的结果：

表中“综合”及后续各列，均以通过 RTL 功能仿真、进入后端流程的设计为统计分母。布局布线、DRC 和 LVS 三项检查在各基准上的通过率相同，因此合并展示。

第一组对比：评估整套系统，与直接生成 Verilog 的方法比较。

论文设置了直接生成 Verilog 的基线。其中，Verilog Agent 使用相同的大模型和 100 轮交互预算，直接生成 SystemVerilog，并依据编译器反馈修复代码。

在 ResBench 上，综合通过率的差距尤为明显：两个直接生成 Verilog 的基线分别为 60.5% 和 57.4%，而 CktFormalizer 搭配 CKTLean 达到 100%。在布线后门级仿真中，后者在 RTLLM 和 ResBench 上的通过率分别为 88.2% 和 100%，也均高于这两个基线。

第二组对比：固定 Agent 流程，比较 CKTLean 与原版 Sparkle。

为单独评估基础设施的贡献，实验保持 CktFormalizer 的 Agent 流程不变，仅将底层从原版 Sparkle 替换为 CKTLean。在 CVDP 上，编译通过率从 77.4% 提升至 91.1%，综合通过率从 67.4% 提升至 100%；综合、布局布线、DRC 和 LVS 全部通过的比例，从 67.4% 提升至 97.1%。在 ResBench 上，最后这一比例从 95.3% 提升至 100%。

不过，CVDP 的门级仿真仍是各方法共同面临的难点。CktFormalizer 搭配 CKTLean 的布线后门级仿真通过率为 27.9%，两个直接生成 Verilog 的基线分别为 29.8% 和 33.3%，都在三成左右。

这些结果表明，CKTLean 的类型化硬件抽象有助于提高设计完成物理实现流程的成功率；而在 CVDP 等复杂任务上，布线后的功能正确性仍有改进空间。

在 CKTLean 提供的硬件表示、编译工具和交互式反馈基础上，CktFormalizer 从微架构探索、等价性证明和闭环优化三个方向展开实验。

第一项探索：让模型生成并比较多种微架构。

在 VerilogEval 中较复杂的 63 道题上，模型为每个设计生成 4 种不同的微架构，并通过综合结果比较候选方案。其中，27 个设计获得了多个可综合的候选，10 个设计实现了超过 5% 的面积降幅。

论文列举的六个案例中，面积下降了 9.9% 至 35.2%，布线后功耗下降了 2.0% 至 30.3%，降幅最大的案例是一个状态机设计。

第二项探索：用 agentic loop 构建电路等价性证明。

Agent 将电路实现与形式化规格之间的等价关系表述为 Lean 定理，并在 agentic loop 中逐步构建证明：提出证明步骤，调用 Lean REPL 获取当前的证明目标和诊断信息，再据此选择或修改下一步，持续迭代。完成的证明由 Lean 内核检查，确立的是给定假设下的源码级等价性。

论文在 30 道 VerilogEval 题目上比较了两种方式：一次性生成电路实现、形式化规格和完整证明，以及在 agentic loop 中利用 REPL 反馈逐步构建证明。后者将证明完成率从 53.3%（16/30）提升至 63.3%（19/30），编译通过率也从 77% 提升至 100%。

论文也明确了证明的边界：它验证的是 Lean 实现与模型生成的形式化规格是否一致，既不保证这份规格忠实于自然语言需求，也不覆盖从 Lean 导出 SystemVerilog 的编译过程。

第三项探索：让硬件评测反馈驱动迭代优化。

在闭环优化中，Agent 从已有设计出发，根据综合面积和单元数等评测结果修改 Lean 代码，再重新编译、仿真和综合；通过评测且满足接受条件的候选被保留，否则回滚，最终恢复迭代过程中表现最好的版本。

在 5 轮迭代优化实验中，54 个设计进入优化循环，31 个实现了面积下降，其中 28 个的降幅超过 5%。降幅最大的设计，面积从 196 μm² 降至 81 μm²，减少了 58.6%。

论文还单独探索了布线后的时序反馈。在一个时钟约束较紧的案例中，加入时序反馈后，建立时间裕量从 −0.37 ns 改善至 +0.35 ns，实现了时序收敛；仅依据面积反馈进行优化时，裕量则仍为 −0.37 ns。

项目采用 Apache-2.0 许可证开源。按照语言基础设施、Agent 框架和实验工具的分工，仓库主要包含三部分：

CKTLean（Sparkle/ 目录）：包含带类型的硬件描述语言、编译前端和 SystemVerilog 后端。

CktFormalizer（cktarchon/ 和 agent/ 目录）：实现模型生成 Lean 代码、调用编译检查和限制文件读写范围的 Agent 循环，并提供各基准的适配与评分功能。

实验脚本（experiments/ 目录）：提供各基准的启动脚本、后端评测流程，以及直接生成 Verilog 的基线。

运行环境需要 Lean 4（通过 elan 安装）、Python 3.13 和 Icarus Verilog。下列命令使用 uv 管理 Python 依赖；将“<仓库地址>”替换为项目的实际仓库地址后，即可克隆并构建：

git clone <仓库地址> cktleancd cktleanlake builduv sync

配置模型 API 密钥和数据集后，可用以下命令运行 VerilogEval 基准：

uv run python -m cktarchon.run --dataset verilogeval \  --results-dir results/verilogeval --workers 4

每道题依次经历：自然语言规格 → Agent 编写 Lean → 编译检查与修复 → 导出 SystemVerilog → 仿真评分。

如需继续评测后端流程，可添加 --synth、--pnr、--drc、--lvs 参数，将通过仿真的设计送入综合与物理实现流程。若要比较直接生成 Verilog 的效果，可将运行入口替换为 cktarchon.run_verilog。

项目链接已放在置顶评论区，大家可以运行体验。