Gespeichert in:
| Hauptverfasser: | , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2605.00058 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911637501378560 |
|---|---|
| author | Ernst, Jan Ole Saberi, Dmitri Michelangelo Christ, Derek Zimmermann, Thomas Salegame, Rajath Bhat, Suhaas M. Levental, Stanislav Ahle, Thomas Dybdahl Jung, Matthias |
| author_facet | Ernst, Jan Ole Saberi, Dmitri Michelangelo Christ, Derek Zimmermann, Thomas Salegame, Rajath Bhat, Suhaas M. Levental, Stanislav Ahle, Thomas Dybdahl Jung, Matthias |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_00058 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Autoformalizing Memory Specifications with Agents Ernst, Jan Ole Saberi, Dmitri Michelangelo Christ, Derek Zimmermann, Thomas Salegame, Rajath Bhat, Suhaas M. Levental, Stanislav Ahle, Thomas Dybdahl Jung, Matthias Hardware Architecture Machine Learning 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. |
| title | Autoformalizing Memory Specifications with Agents |
| topic | Hardware Architecture Machine Learning |
| url | https://arxiv.org/abs/2605.00058 |