The ÆTHEREAL protocol enables both guaranteed and best effort communication in an on-chip packet switching network. We discuss a formal specification of ÆTHEREAL 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.
|Title of host publication||Correct hardware design and verification methods : 13th IFIP WG 10.5 advanced research working conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005 : proceedings|
|Editors||D. Borrione, W. Paul|
|Place of Publication||Berlin|
|Publication status||Published - 2005|
|Name||Lecture Notes in Computer Science|