精选理由
硬件设计自动化领域终于有了突破——大推理模型让自然语言写规范成为可能，做 EDA 工具或形式验证的团队值得关注这个端到端方案。
反应式综合是从逻辑规范自动构建硬件电路的经典难题，既算法困难又需手写形式规范。本文提出神经符号方法，将大推理模型与模型检查器结合，通过符号反馈迭代修复 Verilog 实现，在年度综合竞赛中解决更多基准问题，甚至能处理参数化系统（已知不可判定问题）。同时引入自动形式化步骤，将规范任务从时序逻辑迁移到自然语言，并创建了自然语言规范数据集用于评估。实验表明，从自然语言出发的性能与从形式规范出发相当，使自然语言综合成为可行的端到端工作流。
AI 翻译 · 中文
反应式综合是从逻辑规范自动构建硬件电路的经典难题，既算法困难又需手写形式规范。本文提出神经符号方法，将大推理模型与模型检查器结合，通过符号反馈迭代修复 Verilog 实现，在年度综合竞赛中解决更多基准问题，甚至能处理参数化系统（已知不可判定问题）。同时引入自动形式化步骤，将规范任务从时序逻辑迁移到自然语言，并创建了自然语言规范数据集用于评估。实验表明，从自然语言出发的性能与从形式规范出发相当，使自然语言综合成为可行的端到端工作流。
Reactive synthesis, the problem of automatically constructing a hardware circuit from a logical specification, is a long-standing challenge in formal verification. It is elusive for two reasons: It is algorithmically har…