关键词：片上网络；服务质量；形式验证；服务质量合成
摘 要：This dissertation presents my recent work toward leveraging formal methods for NoC design and QoS verification.In particular, it addresses the problems of (1) verifying end-to-end latency bounds in a mesh network using abstraction; (2) scalable latency verification using compositional inductive proofs; and(3) optimal buffer sizing based on bounded model checking.