CcktFormalizer：自然语言自动形式化为电路表示

LLM 可以根据自然语言规范生成硬件描述，但生成的 Verilog 通常包含宽度不匹配、组合循环和不完整的案例逻辑，这些逻辑通过语法检查但在综合或芯片中失败。我们提出了 CktFormalizer，一个框架，通过 Lean 4 中嵌入的依赖类型 HDL 重定向 LLM 驱动的硬件生成。Lean 具有三个角色：（i）类型检查器：依赖类型编码位宽约束、案例覆盖和非循环性，将硬件缺陷转化为指导迭代修复的编译时错误； (ii) 正确性防火墙：编译的设计在结构上不存在导致无提示后端故障的缺陷（基线在综合和路由过程中丢失了 20% 的正确设计；CktFormalizer 保留了所有这些）； (iii) 证明助手：代理在任意输入序列和参数化宽度上构造机器检查的等价性证明，超出了基于有界 SMT 的检查的范围。在 VerilogEval（156 个问题）、RTLLM（50 个问题）和 ResBench（56 个问题）上，CktFormalizer 实现了与直接生成 Verilog 相媲美的仿真通过率，同时提供了更高的后端可实现性：95--100% 的编译设计完成了完整的综合、布局布线、DRC 和 LVS 流程。通过经过验证的架构探索，闭环 PPA 优化阶段可减少高达 35% 的面积和 30% 的功耗，并通过自动定理证明确保每个优化变体在功能上与其正式规格相同。