Domain-specific languages for hardware can significantly enhance designer productivity, but sometimes at the cost of ease of verification. On the other hand, ISA specification languages are too static to be used during early stage design space exploration. We present PEak, an open-source hardware design and specification language, which aims to improve both design productivity and verification capability. PEak does this by providing a single source of truth for functional models, formal specifications, and RTL. PEak has been used in several academic projects, and PEak-generated RTL has been included in three fabricated hardware accelerators. In these projects, the formal capabilities of PEak were crucial for enabling both novel design space exploration techniques and automated compiler synthesis.

翻译：领域专用硬件语言可显著提升设计人员生产力，但有时会以牺牲验证简便性为代价。另一方面，ISA规范语言过于静态，无法在早期设计空间探索中使用。我们提出PEak——一种开源硬件设计与规范语言，旨在同时提升设计生产力和验证能力。PEak通过为功能模型、形式化规范和RTL提供单一可信源来实现这一目标。PEak已在多个学术项目中使用，由PEak生成的RTL已被集成至三款已流片的硬件加速器中。在这些项目中，PEak的形式化能力对于实现新型设计空间探索技术和自动化编译器综合至关重要。