A formally-verified Network-on-Chip in Coq

This thesis presents a formally-verified Network-on-Chip (NoC) library implemented inCoq, aimed at improving the trustworthiness of communication architectures. Due to thediminishing returns of transistor scaling, System-on-Chips (SoCs) have become the preferredmethod for building high-performance chips. Inter-core communication is often facilitatedby a communication subsystem known as NoC. However, verifying the correctness of NoCsremains a significant challenge because of their large state space and configurable parameters.This work introduces a novel approach that leverages Kôika, an embedded domain-specificlanguage in Coq, to generate NoCs with formal guarantees. The thesis explores the use ofmetaprogramming and dependent programming to generalize these NoCs, enabling designs ofarbitrary sizes with formal correctness proofs. The proposed library aims to reduce verificationoverhead by proving properties over generic instances, thus eliminating the need to verify everyinstance of NoC separately. Kôika ’s formally-verified compiler generates the NoC’s Verilogcode, which is synthesized to obtain expected hardware resource characteristics.