We gave a formal specification of the Aethereal protocol and its underlying architecture for packet switching networks on chip (NoC). All elements of the network and their operations were specified using the theorem prover PVS. Based on this model, we gave a (partially formalized) proof of absence of deadlock .
Designing a NoC that meets all the requirements for best-effort and guaranteed traffic clearly is a difficult task, and the resulting design intrinsically has to be quite complex. During the design process, the designers play around with thousands of design alternatives. It is difficult to keep track of all the design options in a systematic way, and to make sure that the choices that have been made are not inconsistent.
Our contribution  is that for one of the numerous design alternatives we produced (although at an abstract level) a very precise, formal model. Within this model we were able to establish a key correctness property of the system, namely absence of deadlock. It is very unlikely that the design as we have formalized it in our paper will be the one that is going to be implemented in hardware. However, since our specification is highly abstract and very modular, we think it will be relatively easy to modify our spec to reflect variations of the design.
In fact, we believe that our work illustrates that formal specification languages such as supported by PVS can be most useful to document complex designs, to force designers to clarify design choices, and to resolve problematic inconsistencies in an early stage of the design process.
Henrik Bohnenkamp 2004-05-06