The AETHEREAL protocol enables both guaranteed and best effort communication in an on-chip packet switching network. We discuss a formal specification of AETHEREAL and its underlying network in terms of the PVS specification language. Using PVS we prove absence of deadlock for an abstract version of our model.
展开▼
