用AI自动将内存规格文档转为可测试的正式语言，提升芯片验证效率。
Autoformalizing Memory Specifications with Agents
- 通过智能代理自动将自然语言规格转化为可执行的正式表示
- 支持DRAM标准的完整形式化，生成SystemVerilog断言与测试用例
- 发布DRAMBench数据集，推动硬件自动形式化技术评测
设计验证（DV）的核心目标是确保芯片设计实现与规格完全一致且无功能错误，避免昂贵的返工。传统方法依赖大量人工解读，将规格文档转化为可测试的正式表达。尽管人工智能在DV领域取得进展，现有方法多聚焦于孤立任务，难以应对现代芯片设计的复杂性。本文提出一种自动化方法，将动态随机存取存储器（DRAM）行业标准的自然语言规格自动形式化为名为DRAMPyML的正式表示，可用于生成SystemVerilog断言、测试激励和功能覆盖率。同时，我们发布了基准数据集DRAMBench，用于评估模型在硬件自动形式化上的演进能力及新方法性能。
原文摘要 · Abstract (English)
The primary goal of Design Verification (DV) is to ensure that a proposed chip design implementation (either in code, or physical form) exactly matches its specification and is free of functional errors in order to avoid costly re-designs. Achieving this often demands extensive manual interpretation, translating the specification document into a formal, testable representation. While AI has made progress in DV, current approaches typically focus on narrow, isolated tasks rather than full end-to-end specification compliance of modern chip designs, failing to capture the complexity of real-world verification. Our method automatically formalizes natural language memory chip specifications, for industry relevant Dynamic Random Access Memory (DRAM) standards, into a formal representation called DRAMPyML that can be used for downstream DV tasks like the generation of SystemVerilog assertions, stimulus, and functional coverage. We also release our benchmarking dataset, DRAMBench, which can be used to evaluate the evolution of model capabilities (and new approaches) at hardware autoformalization.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。