NoC-Out：用于基于规则的硬件设计的形式化验证片上网络库
NoC-Out: A Formally-verified Network-on-Chip Library for Rule-based Hardware Designs
浏览论文内容
中文总结 AI 辅助
本文实现了首个形式化验证k维NoC的库NoC-Out，通过扩展Kôika支持高效NoC设计与自动推理，生成的NoC符合形式化规范，其验证方法是合成高效NoC的必要手段。
中文摘要 AI 辅助
片上网络（NoC）是任何多处理器芯片的通信骨干，NoC故障会对整个系统造成严重后果。然而，目前尚无方法能提供形式化验证的NoC并具备强保障，同时又无需繁琐的验证工作。任何生成形式化验证NoC的库都需要在NoC结构上具备参数化能力，这要求硬件描述语言（HDL）既能支持参数化、并发且高效的硬件设计，又能提供必要的程序逻辑以模块化方式对其进行推理。目前，HDL在这两方面均存在不足。本文实现了NoC-Out，这是首个用于形式化验证k维NoC设计的库/生成器。为构建NoC-Out，我们扩展了Rocq定理证明器中基于规则的HDL——Kôika，使其支持并发且高效的NoC设计，以及用于模块化自动推理的程序逻辑。给定配置后，NoC-Out会在Kôika中生成一个k维环面NoC，该NoC可被编译为Verilog。每个生成的NoC都附带一份证明，证明其符合我们的形式化NoC规范，无需额外验证工作。我们的规范证明了强活性保障，因此该保障适用于所有生成的NoC。在评估中，我们发现我们的验证方法甚至是在基于规则的HDL中合成高效NoC所必需的。
英文摘要
The Network-on-Chip (NoC) is the communication backbone of any multiprocessor chip. A failure of the NoC has severe consequences for the whole system. Yet, no approach exists that provides formally-verified NoCs with strong guarantees but without tedious verification effort. Any library that generates formally-verified NoCs needs to be parametric in the structure of the NoC. This requires a hardware description language (HDL) that allows for parametric and concurrent yet efficient hardware designs as well as the necessary program logic to reason about them in a modular fashion. So far, HDLs fall short in both aspects. In this paper, we implement NoC-Out, the first library/generator for formally-verified k-dimensional NoC designs. In order to build NoC-Out, we extended Kôika, a rule-based HDL in the Rocq theorem prover, with support for concurrent yet efficient NoC designs and a program logic for modular, automated reasoning. Given a configuration, NoC-Out produces a k-dimensional torus NoC in Kôika, which can then be compiled to Verilog. Each produced NoC is equipped with a proof that it refines our formal NoC specification; no additional verification effort is required. Our specification proves a strong liveness guarantee, which consequently applies to all generated NoCs. In our evaluation, we find that our verification approach is even required to synthesize efficient NoCs in rule-based HDLs.
