AI 硬件与加速器
突破级
暂无讲解视频
收录解读
LLM 用于 RTL 生成已经不少，但真正卡住工业可用性的仍然是 formal correctness。尤其在 datapath-centric、规格模糊且复杂度高的设计里，单靠 simulation-driven debug 很难建立可靠的设计闭环。
FormalRTL 的关键做法是把 software reference model 作为 formal、可执行的 specification，再把 planning、RTL synthesis 和 formal equivalence checking 串成一个端到端框架。这样生成不再只是从 prompt 到 HDL，而是始终围绕可验证语义进行，形成比普通 Verilog codegen 更强的 correctness anchor。
对本仓库来说，这篇论文代表的是 EDA workflow 的结构性变化：AI 不是单独写 RTL，而是和 formal spec、验证、规划共同组成一个更可信的设计流程。这正符合新范围里 `电路设计与仿真` 以及 `硬软件一体设计/验证` 的要求。
它还不是更高一级，因为影响仍集中在 RTL synthesis / verification 这一层，没有继续深入到后端物理设计、系统级协同仿真或量产约束。