Search papers, labs, and topics across Lattice.
This paper introduces NoC-Out, a library for generating formally-verified k-dimensional Network-on-Chip (NoC) designs that significantly reduces the verification burden associated with hardware design. By extending the K^oika hardware description language within the Rocq theorem prover, the authors enable modular and automated reasoning for concurrent NoC designs, ensuring that each generated NoC adheres to a strong liveness guarantee without additional verification effort. The evaluation demonstrates that NoC-Out not only simplifies the verification process but is also essential for synthesizing efficient NoCs in rule-based HDLs.
Formally-verified NoCs can now be generated effortlessly, eliminating the tedious verification process while ensuring strong liveness guarantees.
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\^oika, 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\^oika, 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.
