PEak：硬件设计与验证的单一真实来源

《ACM Transactions on Embedded Computing Systems》：PEak: A Single Source of Truth for Hardware Design and Verification

PEak是一款开源硬件设计语言，整合功能模型、形式规格说明和RTL代码，提升设计生产力和验证能力。该语言已在多个学术项目中应用，生成的RTL被三个实际硬件加速器采用，其形式能力支持了新颖设计空间探索和自动编译器合成。

　　

摘要

针对硬件的领域特定语言能够显著提高设计人员的效率，但有时会牺牲验证的便捷性。另一方面，指令集架构（ISA）规范语言过于静态，无法在设计的早期阶段用于探索不同的设计方案。我们提出了PEak，这是一种开源的硬件设计和规范语言，旨在同时提升设计效率和验证能力。PEak通过为功能模型、正式规范以及RTL（硬件描述语言）提供统一的数据源来实现这一目标。PEak已被应用于多个学术项目，其生成的RTL也被集成到了三款实际制造的硬件加速器中。在这些项目中，PEK的形式化特性对于实现新颖的设计探索技术和自动化编译器合成至关重要。