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.
翻译:设计验证(DV)的首要目标是确保所提出的芯片设计实现(无论是代码形式还是物理形式)完全符合其规范,且不存在功能错误,以避免代价高昂的重新设计。实现这一目标通常需要大量人工解读,将规范文档转化为可测试的形式化表示。尽管人工智能在DV领域已取得进展,但现有方法通常专注于狭窄、孤立的任务,而非现代芯片设计的完整端到端规范合规性验证,未能捕捉到实际验证的复杂性。我们的方法能够自动将自然语言描述的内存芯片规范(针对工业相关的动态随机存取存储器(DRAM)标准)形式化为称为DRAMPyML的形式化表示,该表示可用于下游DV任务,如SystemVerilog断言、激励信号和功能覆盖率的生成。我们还发布了基准测试数据集DRAMBench,该数据集可用于评估硬件自动形式化过程中模型能力(及新方法)的演进。