用 Bluespec 风格推导高效硬件设计

文章以多核 CPU 缓存一致性协议为例，展示如何用 Bluespec 风格的单向重写规则从规范逐步推导出硬件实现，并保证正确性。作者提出将硬件模块分别证明、再以近似黑盒的方式组合，从而验证更大系统；该方法此前多用于证明手写硬件设计正确。作者认为这种逐步推导方式可替代当前 AI 编程智能体在软件工程中的使用方式。