paperbot · PL 论文追踪

全部论文 待读 收藏

P2 PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency

PipeSynth：面向内存一致性的微架构公理自动合成
ASPLOS Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 32023匹配度 3/10 · 论文研究处理器内存一致性公理的自动合成，属于形式验证/规范合成，与用户“AI→PL 用 LLM/Agent 改进形式化验证”中的形式验证主题有间接关联；但未涉及 LLM/Agent，也不涉及浮点程序分析或贝叶斯程序分析，且聚焦硬件微架构，与用户核心方向（静态分析、Agentic 程序、LLM 交叉）匹配度低。引用 4 inbox
Chase Norman, Adwait Godbole, Yatin A. Manerkar
并发、并行与内存模型语言与体系结构
crossref: 2026-09-12

AI 速览

一句话：提出 PipeSynth，在 RTL 实现完成之前自动合成处理器的微架构内存一致性公理，以支持早期形式验证。

形式验证有助于保证现代处理器的正确性，但其前提是拥有被验证处理器的形式化规约。目前这类微架构规约多由人工编写，过程繁琐且容易出错；硬件架构师与工程师通常又缺乏形式方法经验，使得编写规约更加困难。已有的微架构形式规约自动合成方法以处理器的 RTL 实现为输入，因此必须等到 RTL 实现完成之后才能使用，阻碍了形式验证在设计中前期的介入。PipeSynth 面向这一问题，自动合成刻画内存一致性的微架构公理，使形式验证不再被 RTL 实现的完成度所限制，从而有望在 RTL 之前发现设计缺陷，降低验证开销并缩短整体开发周期。摘要未给出具体合成算法与实验评估结果。

问题
处理器形式验证需要形式化的微架构规约，但人工编写繁琐易错，而现有自动合成方法依赖处理器的 RTL 实现，只能等到 RTL 完成之后才能使用，无法在设计早期捕获缺陷。
方法
提出 PipeSynth，自动合成描述内存一致性的微架构公理（形式规约），从而在缺乏（或尚未完成）RTL 实现的情况下获得可供形式验证使用的微架构规约。
评估
所给摘要未描述具体的评估方式，也未报告实验结果与案例研究。
原文摘要（Abstract）

Formal verification can help ensure the correctness of today’s processors. However, such formal verification requires formal specifications of the processors being verified. Today, these specifications are mostly written by hand, which is tedious and error-prone. Furthermore, architects and hardware engineers generally do not have formal methods experience, making it even harder for them to write formal specifications. Existing methods for the automated synthesis of formal microarchitectural specifications utilise RTL implementations of processors for their synthesis, preventing their usage until RTL implementation of the processor has completed. This hampers the effectiveness of formal verification for processors, as catching design bugs pre-RTL can reduce verification overhead and overall development time.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot10101,
  title = {PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency},
  author = {Chase Norman and Adwait Godbole and Yatin A. Manerkar},
  booktitle = {ASPLOS},
  year = {2023},
  doi = {10.1145/3582016.3582056}
}