{'fraction_non_alphanumeric': 0.030986104284884502, 'fraction_numerical': 0.008042536079710469, 'mean_word_length': 4.70447304702434, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Formal Approach to the Verification of Networks on Chip

The current technology allows the integration on a single die of complex systems-on-chip (SoCs) that are composed of manufactured blocks (IPs), interconnected through specialized networks on chip (NoCs). IPs have usually been validated by diverse techniques (simulation, test, formal verification) and the key problem remains the validation of the communication infrastructure. This paper addresses the formal verification of NoCs by means of a mechanized proof tool, the ACL2 theorem prover. A metamodel for NoCs has been developed and implemented in ACL2. This metamodel satisfies a generic correctness statement. Its verification for a particular NoC instance is reduced to discharging a set of proof obligations for each one of the NoC constituents. The methodology is demonstrated on a realistic and state-of-the-art design, the Spidergon network from STMicroelectronics.


Introduction
Up-to-date systems-on-chip (SoCs) are built by assembling modules such as processor cores, memories, and specialized Intellectual Property (IP) blocks. Networks on chip (NoCs) are emerging as a promising solution for the realization of communications in such complex systems [1,2]. NoCs such as Faust [3] or SoCBUS [4] provide configurable communication infrastructures that are particularly attractive for the design of advanced SoCs and embedded systems. NoCs are usually made of point-to-point data links interconnected by switches; widespread topologies include meshes and fat-tree architectures.
SoC design must be supported by appropriate design methods and flows. We place ourselves in the context of "platform-based design," where a platform is defined as "an abstraction layer in the design flow that facilitates a number of possible refinements into a subsequent abstraction layer (platform)" [5]. Verification is indispensable at all stages and layers. It consumes almost 60 to 70% of the total resources in a typical chip design cycle [6]. In an NoCbased architecture, two main verification problems arise: the functional validation of each core or IP and the verification of the communications in the network. This paper addresses the latter aspect.
The application of formal methods to embedded communication infrastructures has received a recent attention. The sparse literature on that topic is targeted to specific designs described at the register transfer level (RTL) and below. In the context of platform-based design, the trend in the design flow is to raise the level of abstraction of the initial phase and to ground the flow on verified parameterized library modules. Yet, on-chip communications are not supported by a general and formal theory, which is necessary to obtain verified parameterized communication modules. Our utmost objective is to provide a formal foundation to the verification of on-chip communication architectures, spanning from their initial design specifications to their RTL implementation.
As a first step toward this objective, we proposed the generic network on chip model (GeNoC) [7,8]. It consists of a metamodel of on-chip communication architectures and its implementation in the logic of a theorem proving system. The peculiar aspect of this model is to represent a large class of systems. It is a highly generic and parameterized object. While performing the proofs, parameters such as the 2 EURASIP Journal on Embedded Systems size of the network or the length of messages need not to be instantiated. Its implementation in a theorem proving system provides mechanized support and partial automation in the verification effort. The model is implemented in the ACL2 theorem prover [9]. An important feature of ACL2 is to denote both a powerful theorem proving system and an execution engine in the same environment. The theorem proving system has a high degree of automation. ACL2 specifications are written in an applicative subset of Common Lisp and are thus executable. These constitute two important advantages of using ACL2.
Our first versions of the model contained unrealistic simplifying hypotheses, concerning the granularity of moves and the time when messages were introduced in the network. As a consequence, while the final result of the communications was correctly portrayed, the intermediate steps were abstracted away: where and when a message is temporarily delayed by the presence of other messages in the network could not be shown.
The enhanced formalization presented in this article constitutes a significant progress, both mathematically simpler and offering a much larger expressive power: (i) the current metamodel covers a network specification from the transport layer to the data link layer of the OSI model; (ii) the progression of the messages in the network is specified step by step instead of considering their transfer atomically from their source to their destination, thus allowing a great variety of scheduling policies (circuit, wormhole, priority, etc.); (iii) new messages may enter the model at arbitrary times and arbitrary nodes; (iv) the same model can be used for formal verification and for simulation.
The metamodel detailed in this paper represents the transmission of messages on a generic communication architecture, with an arbitrary network characterization (topology and node interfaces), routing algorithm, and switching technique. The main function of this model, called GeNoC, is recursive. Each recursive call represents one step of execution, where messages progress by at most one hop. Such a step defines our time unit. A correctness theorem is associated with function GeNoC. It states that for all topology T , interfaces I, routing algorithm R, and scheduling policy S that satisfy associated constraints P 1 , P 2 , P 3 , and P 4 , GeNoC fulfills a correctness property ℘: ∀T ∀I ∀R ∀S, ⇒ ℘(GeNoC(T , I, R, S)). (1) Roughly speaking, the property ℘ asserts that every message arrived at some node n was actually issued at some source node s and originally addressed to node n, and that it reaches its destination without modification of its content.
The constituents of the metamodel are characterized by constraints P 1 , P 2 , P 3 , and P 4 that express essential properties of the key components, for example, wellformedness of the network or termination of the routing function. The proof of formula (1) above is derived from these constraints, without considering the actual definitions of the constituents. Consequently, the global correctness of the network model is preserved for all particular definitions satisfying the constraints.
It follows that, for any instance of a network, that is, for any T 0 , I 0 , R 0 , and S 0 , the property ℘(GeNoC(T 0 , I 0 , R 0 , S 0 )) holds provided that P 1 (T 0 ), P 2 (I 0 ), P 3 (R 0 ), and P 4 (S 0 ) are satisfied. Hence, verifying formula (1) for a given NoC is reduced to discharging these instantiated constraints on the NoC constituents. This verification methodology is illustrated hereinafter on a realistic and state-of-the-art NoC, the Spidergon from STMicroelectronics [10]. ( The ACL2 scripts of our model and its instantiation for Spidergon are available at http://tima.imag.fr/vds/GeNoC/genoc.html. )

Related Works
Intensive research efforts have been devoted to the development of performance, traffic, or behavior analyzers for NoCs. Most proposed solutions are simulation-or emulationoriented. Few approaches address the use of (semi)formal methods, essentially toward the detection of faults or debug. A methodology based on temporal assertions is proposed in [11]. It targets a two-level hierarchical ring structure. PSL properties [12] are used to express interfacelevel requirements and are transformed into synthesizable checkers (monitors). In case of assertion failures, special flits are propagated to a station responsible for analyzing these failures. Goossens et al. [13] advocate communicationcentric debug instead of computation-centric debug for complex SoCs and also use a monitor-based solution. They discuss the temporal granularity at which debug can be performed and propose a specific debug architecture with four interconnects. Both approaches rely on a formal expression of properties (assertions), but are indeed founded on a dynamic, nonformal, execution/emulation of a detailed design, where all architectural parameters and implementation decisions have been settled. In contrast, our work applies to the validation of an early specification stage.
Widespread formal methods can be classified in two categories: algorithmic techniques (e.g., model-checking) and deductive ones (theorem proving). Many approaches have been proposed in the fields of protocol or network verification in general. Most of them are based on modelchecking techniques and target very specific designs. Clarke et al. [14] use the notion of regular languages and abstraction functions to verify temporal properties of families of systems represented by context-free network grammars, for instance, the Dijkstra token ring and a network of binary trees. Creese and Roscoe [15] exploit the inductive structure of branching tree networks and put the emphasis on data independence: data are abstracted in order to use the FDR model checker to prove properties of CSP specifications. Roychoudhury et al. use the SMV model checker [16] to debug an academic implementation of the AMBA AHB protocol [17]; the model is written at the RTL and without any parameter. Salaün et al. focus on the verification of asynchronous systems using the CADP tool and report the verification of an NoC input controller [18]. Again, the application of model-checking techniques is restricted to architectures where all sizes have been fixed, a later design stage than the one addressed by our model.
Results with theorem provers, or combinations of theorem provers and model-checkers, have also been proposed. Most of them concern specific architectures. The HOL theorem prover [19] is used by Curzon [20] to verify a specific network component, the Fairisle ATM switching fabric. Its structural description is compared to a behavioral specification. Bharadwaj et al. [21] use the combination of the Coq theorem prover [22] and the SPIN model-checker [23] to verify a broadcasting protocol in a binary tree network. Amjad [24] uses a model checker implemented in HOL to verify the AMBA APB and AHB protocols and their composition in a single system. Using model checking, safety properties are verified on each protocol individually, and HOL is used to verify their composition. In Gebremichael et al. [25], the AEthereal protocol of Philips is specified in the PVS logic. The main property that is verified is the absence of deadlock for an arbitrary number of masters and slaves. The correctness properties checked by these various methods are different from the ones we consider, and the proofs cannot easily be ported from one network structure to another one. We consider this set of works as complementary to ours and applicable to an instantiation of our metamodel to a particular architecture.
The research results that most closely relate to our work tackle the formalization from a generic perspective. Moore [26] defines a formal model of asynchrony by a function in the Boyer-Moore logic [27] and shows how to use this general model to verify a biphase mark protocol. More recently, Herzberg and Broy [28] present a formal model of stacked communication protocols, in the sense of the OSI reference model. They define operators and conditions to navigate between protocol layers and consider all OSI layers. This work is more general than Moore work, which is targeted at the lowest layer. In contrast, Moore provides mechanized support. Both studies focus on protocols and do not consider the underlying interconnection structure explicitly. In the context of time-triggered architectures, the work of Rushby [29] proposes a general model of time-triggered implementations and their synchronous specifications. The simulation relation between these two models is proven for a large class of algorithms using an axiomatic theory. Pike recently improved the application domain of this theory [30,31]. Miner et al. [32] define a unified fault-tolerant protocol acting as a generic specification framework that can be instantiated for particular applications. These studies focus on time-triggered protocols. The framework presented in this paper aims at a more general network model and concentrates on the actual interconnect rather than the protocols based on top of this structure.

The Spidergon NoC
The Spidergon NoC from STMicroelectronics [10] is used as a running example throughout this paper. It is an extension of the Octagon network [33] to an arbitrary even number of nodes. Figure 1 gives a 16-node version of the Spidergon. Like the Octagon, it is equipped with a shortest-path routing algorithm. Spidergon forms a regular architecture, where all nodes are connected to three neighbors and a local IP. Let NumNode be its number of nodes. The maximum number of hops is NumNode/4 if NumNodeis a multiple of four. We place our formal representation in that context, we assume a global parameter N such that NumNode = 4 · N.
The routing of a message is done as follows. Each node compares the destination address of the message (DestAd) to its own address (NodeAd) to determine the next action. The node computes the relative address of a message as At each node, the route of the message is a function of RelAd as follows.

Principles of Our Approach: The Generic Network Model
The main function of the metamodel is function GeNoC sketched in Figure 2. It takes as main argument a list of messages emitted at source nodes and returns a list of messages received at destination nodes. Various intermediate data types are used, which are not described here for the sake of simplicity and clarity. In addition to the data that it is carrying, a message contains the following information: its source, destination, current position, the time at which it is injected in the network, and optionally the number of flits in the message. Each message is also uniquely identified by a natural number. Function GeNoC produces two output lists: the list of messages that have reached their destination, and the list of messages that are still at their source, or traveling in the network. It entails the following components: (i) a global network state representing the current status of the memory elements associated with the ports of the nodes and an explicit notion of time (Section 5); (ii) at the Transport layer (Section 6), interfaces are represented by two functions used to encode messages to be sent in the network (send) and to decode them (recv). Function R4D ("ready for departure") determines which messages can be in the network at the current time. Messages may be injected only at a specific execution time or under constraints on the network load (e.g., credit-based flow control); (iii) at the Network layer (Section 7), the routing algorithm is represented by function Routing and the switching technique is represented by function Scheduling. The routing algorithm is represented by the successive application of unitary moves (e.g., routing hops). For each message, the routing function computes all possible routes from the current position to the destination. Function Scheduling returns a list of messages that have reached their destination and a list of messages that are en route to their destination. The model also allows the modeling of priorities between messages (e.g., using a round-robin policy); (iv) at the data link layer (Section 8), the transmission protocol is specified. The possibility of moving one message from one port to another depends on the current state of the network, which itself depends on the other messages.
Function GeNoC makes use of functions R4D, Routing, and Scheduling to compute the arrived and the delayed messages. It takes as parameters a list of messages (M), the structure of the network, reduced to the set of addresses of its nodes (A), a finite number of attempts (att), the set of arrived messages (T, originally empty), the current state of EURASIP Journal on Embedded Systems If no attempt is left, GeNoC stops and returns a pair composed of the arrived (T) and the delayed or en route (M) messages. Otherwise, every recursive call processes a list of messages, where some are waiting at their source, and some are traveling in the network. First, function R4D extracts the messages that are allowed to move at current time z (TR). For each one of them, routes are computed using function Routing. Then, function Scheduling computes the list of the arrived messages (Arr), the list of messages that are still traveling in the network (TM), the remaining attempts (att ), and a new state (st ). The recursive call processes the traveling messages together with the messages D delayed by R4D. Time is incremented by 1.

Addresses and Parameters.
Networks are assumed to be built from the interconnection of an unbounded, but finite, number of generic switches that have several input and output ports connected to the neighboring switches and to the local IP ( Figure 3). Each switch has a unique identifier that can be its position or coordinate.
Tuples composed of a coordinate, a port, and its direction (i.e., tuples of the form coor, port, dir ) constitute the basis of the model. We shall refer to such an element as an address, abbreviated a.
The set of valid addresses is denoted by A. It is computed by a generic function, named AGen. The set of valid input arguments to AGen is noted P A . These parameters may represent the dimensions of the network or its number of nodes. The main proof obligation on AGen is its typing property.

Input ports Output ports
Local ports Position (coordinate) Example 2. In the Spidergon NoC, each switch has four ports: local, clockwise, counterclockwise, and across. The instantiated address tuple is coor, port, dir , where coor is the switch id, port belongs to {cw, ccw, acr, loc} and dir is either "i" for input or "o" for output ( Figure 4). The instantiation of function AGen for the Spidergon network is denoted by SpiderGen. It generates the address space of the network. The only parameter of this function is the integer N such that 4 · N is the number of nodes in the network. Assume N = 4. Then, 5, cw, i is a member in the address space whereas 17, ccw, i is not. In general and in our verification effort, the address space of the Spidergon contains 4·N ·4·2 addresses (4·N is the number of nodes, 4 is the number of ports per node, and 2 is for the two directions of each port).

EURASIP Journal on Embedded Systems
The ACL2 verification of Proof Obligation 1 for the Spidergon instantiation is automatic. It involves 4 theorems and 10 functions.

Network State.
A memory element (buffer) is associated to each address, noted mem. No assumption is made on that element. If the address has no storage element, mem is empty. Otherwise, the structure of this field can be adapted to model the storage elements of a particular instance.
The state of the network consists of a collection of state entries, one for each address. Each state entry is a tuple of the form a, mem, [opt] , where a is the node address, mem gives the state of its memory element(s), and [opt] is an optional field that may be used for extra information needed for particular instances (e.g., synchronization signals).
The set of valid states is denoted by S. The set of valid state entries is denoted by E . An entry exists for each element of the address space of a network. Four functions are specified: (i) Validntkstate, recognizes a valid state; (ii) StGen, generates the network initial state; (iii) loadBuffer, loads a message in a buffer; (iv) readSEntry, returns a state entry.
Function StGen takes as arguments the parameter used to generate the address space and user-defined parameters, for example, used to dimension the memory elements. The valid set of parameters is denoted by P st . The typing property of function StGen constitutes a proof obligation.

Proof Obligation 2.
Example 3. In our specification of the Spidergon, the addresses generated by function AGen (Section 5.1) constitute the address field of state entries. We consider that addresses (or ports) have a one-place buffer. Therefore, the field mem is either a message or empty, which is represented by the empty set ∅. (More precisely, a nonempty buffer contains one message flit. In this section, we write message for brevity.) We consider the Spidergon with a handshake transmission protocol. When transferring data from a port p s to a port p d , signal Rx is used by p s to request a transmission, and signal Ackrx is used by p d to acknowledge receipt. The field [opt] of the generic state entry is instantiated by a 2-bit vector representing the values of these two signals for such a port. An example of a valid state entry is 5, cw, i , m, 10 . This is the state entry of the clockwise input port of node number 5, which contains message m, and where signal Rx is 1 and signal Ackrx is 0.
The function loadBuffer takes as parameters an address, a message, and a network state. It updates the contents of the memory element of the address with the new message. Let D msg be the domain of messages. The following typing property is a proof obligation for loadBuffer.
Example 4. Function SpiderLoadBuffer(a, m, st) updates the field mem of the state entry of address a with message m. To empty a buffer, one loads it with ∅.
The function readSEntry takes as parameters an address and a network state. It returns the state entry of the address. The typing property of function readSEntry constitutes a proof obligation.

Proof Obligation 4.
readSEntr y : Example 5. Function SpiderReadSEntr y(a, st) simply returns the state entry with address a.
The most important proof obligation establishes that each state entry corresponds to a valid address (e.a accesses the address field of the state entry).
Example 6. The ACL2 verification of this state specification for Spidergon is largely automatic, only two additional lemmas are needed.

Transport Layer
This layer is responsible for encapsulating data into packets suitable for transfer to the network infrastructure or managing the reverse transaction for delivering messages to the destination node. Our model specifies this encoding/decoding process as well as the flow control services of the transport layer.
6.1. Interfaces. The interfaces are modeled by two functions. Function send represents message encoding, and function recv specifies decoding. To guarantee the compatibility between these two functions, a proof obligation states that their composition is the identity function.
6.2. Network Access Control. The network access control function checks whether a message can be injected into the network. This is modeled by function R4D. This function splits a list l of messages into the list R4D.traveling(l) of messages that satisfy the departure conditions, and the list R4D.delayed(l) of delayed messages. ( This notation is used to represent the constituent of R4D(l) that contains the traveling messages. Similar notations are used throughout the rest of this paper) . The three lists belong to D lm , which denotes the set of all possible lists of messages. We can consider various access control conditions. Example conditions are credits allowed for each node to send messages (e.g., in the Faust network [3]), or a maximum number of messages allowed in the network (e.g., in the Nostrum network [34]).
Function R4D takes as arguments a list of messages and a user-defined parameter used to model particular departing conditions. We use " * " to represent the arbitrary domain of this parameter. The typing property of function R4D constitutes a proof obligation.

Proof Obligation 7.
Each one of the outputs of function R4D must be a subset of the input message list.
A message cannot be in both lists at the same time, that is, the intersection of these two lists must be the empty set.
Example 7. The instance of function R4D for the Spidergon is called SpiderR4D.
We are not aware of any flow control mechanism for the Spidergon network. Only the message injection time (simulation step) is considered in SpiderR4D. Each message can depart if its injection time is equal to the current simulation step. In that case, it is put in list SpiderR4D.traveling. Otherwise, it is added to list SpiderR4D.delayed. Once put in list SpiderR4D.traveling, it becomes a traveling message, and it will remain in this list in the recursive calls.
All the proof obligations have been discharged for function SpiderR4D. Proof Obligation 8 needed 2 intermediate lemmas for a total proof time of 2.41 seconds. As for Proof Obligation 9, one intermediate lemma is needed for a proof time of 1.45 seconds.

Network Layer
The Network layer is responsible for the end-to-end (i.e., source to destination) message delivery. In particular, it implements the routing method that determines the intermediate nodes from the source to the destination. The congestion and conflict management of the switching technique is also a Network layer responsibility [35].

Routing. Our representation of the routing algorithm involves the main function
Routing that computes all possible routes from the current position to the destination for all traveling messages, as well as two auxiliary functions: (i) RCore, computes all possible routes from the current position to the destination for one message; (ii) RLogic, implements the routing logic, that is, computes the next step node.
In case of deterministic algorithms like the Spidergon routing algorithm, there is only one possible route. Several routes are feasible when adaptive algorithms are considered. Function RCore simply applies RLogic recursively. Function Routing also recursively applies RCore to all messages. Function RLogic takes two addresses curr and dest as parameters and computes the next hop on the route from curr to dest. These three nodes must belong to A.

Proof Obligation 10.
RLogic : Example 8. The routing logic determines the possible moves between two adjacent addresses. The Spidergon routing logic offers four possible moves: clockwise, counterclockwise, across, and to the local IP. These four moves are represented by four functions. For instance, the function for a clockwise move is as shown in Algorithm 2.
The routing logic, represented by function SpiderRLogic, is then defined from these four moves following the Spidergon routing algorithm described in Section 3 as shown in Algorithm 3.
This function constitutes a valid instance of function RLogic and satisfies the above proof obligation.
Function RCore takes as parameters two addresses: the current one and the destination. In case of deterministic algorithms, it computes the route from the current node to the destination by recursive applications of function RLogic. The set of all possible routes in the network is denoted by R. Function RCore returns an element of R.

Proof Obligation 11.
RCore : Example 9. Function SpiderRCore recursively calls function SpiderRLogic, as shown in Algorithm 4. This function satisfies the above proof obligation.
A route r for a message m is correct if its first element is the current position of m and its last element is the destination of m. All addresses of a route must belong to the address space. Predicate ValidRoutep checks the conjunction of these conditions (m.curr, and m.dest represent the current position and destination of m): Function Routing takes as arguments a list of messages and the address space. It returns a list of routed messages, that is, messages associated with routes. D lm denotes the set of lists of messages, and D lrm denotes the set of lists of routed messages.

Example 10. Function Routing is instantiated by function
SpiderRouting as shown in Algorithm 5.
Functions first and tail return the first element of a list and the tail of the list (i.e., the list without its first element).
The well-formedness of the routes produced by function Routing is expressed by predicate CorrectRoutesp. This predicate takes as arguments a list of messages lm, the list of the corresponding routed messages lrm, and the address space A. It verifies that, for every message m of lrm, there exists a unique routed message rm in lrm such that m and rm have the same id and that the route of rm is correct with respect to message m.
The main proof obligation guarantees that all routes produced by function Routing are correct. Proof Obligation 13.

CorrectRoutesp(lm, Routing(lm, A), A). (17)
Example 11. We first prove that function SpiderRCore produces valid routes, that is, its result satisfies predicate ValidRoutep. The proof proceeds by induction on the length of a route. The remaining properties are trivial. Overall, the specification and the validation of the routing algorithm of Spidergon amount to 1200 lines of ACL2 code. Most of the difficulty comes from arithmetic reasoning in ACL2.

Scheduling. Function
Scheduling determines the progression of messages in the network. From a list of messages, it returns the list of messages that have reached their destination and the list of messages that are still en route to their destination. En route messages may be blocked on their current node or able to move forward. Two layers of the OSI stack are concerned here (i) At the Network layer, priorities are used to resolve the competition for the next resource (e.g., a port). Their specifications are discussed in Section 7.3. Other aspects, specific to a switching technique, can also be implemented at this layer. For example, in wormhole switching, flits belonging to the same message must follow the same route in a pipelined fashion, without the introduction of flits belonging to other messages between them [36].
(ii) At the data link layer, data transmission follows a low-level protocol that determines whether the next resource is ready to receive. This is the purpose of Section 8.
Function Scheduling takes as arguments a list of routed messages, the current value of the attempts (of type D att ), the current network state, and an additional parameter that EURASIP Journal on Embedded Systems 9 models the priority order to be used. This parameter is user defined and we use an " * " to denote its domain. Function Scheduling returns two lists (en route messages used in the recursive call of GeNoC, and arrived messages), the updated attempts, and the updated network state.

Proof Obligation 14.
Scheduling : Example 12. WHS is the core function in modeling the wormhole switching technique. It takes as arguments a list of routed messages, three accumulators (initially empty) and the global state. The first two accumulators collect the messages that are still en route (ER) and those that have reached their destination (Arr). The last accumulator (2Bmoved) collects the ports from which a message moves: their buffer must be emptied (see function WHScheduling thereafter). WHS returns the three accumulators and a new state. If a move is possible (lines 10 to 23), the message is added to 2Bmoved (lines 14 and 21). The memory element of the target of the hop (second element of the route) is updated with the content of the message (lines 15 and 22). If the message has reached its destination, it is added to Arr (line 13). Otherwise, the first address of its route is removed-the second address becomes its current position simulating the action of making a hop-and the message is then added to ER (line 20). If no move is possible, the message is simply added to ER without any modification (lines 26 to 28) (see Algorithm 6). Function WHScheduling is the top level function in the model of the scheduling policy and the instance of function Scheduling. It includes the priority ordering between the ports of a node and the low-level protocols used in the data link layer. Function WHScheduling first calls these functions to order its input argument (line 2) and to compute the first phase of our handshake protocol (line 3). Function rrSort implements a round-robin priority scheme. Function WHS is called with empty accumulators (only represented as ". . ." in the definition).
To build the returned state, WHScheduling empties the buffer of the addresses that were left by a message (line 9), produced by function WHS above in accumulator 2Bmoved. Function free simply loads all these addresses with ∅, the empty buffer as shown in Algorithm 7.
The main property required for the arrived messages is that their routes are left unchanged. Predicate ArrivedCorrp below checks that for every routed message rm of the list lrm , there exists a routed message rm of the list lrm such that rm and rm have the same id and the same routes r.
The following proof obligation ensures that the arrived messages satisfy this predicate. ArrivedCorr p (Scheduling.arr(lrm, a, s, o), lrm). (20) Similarly, predicate EnrouteCorrp is designed for the correctness of the enRoute messages and used in the next proof obligation. Formally, it checks that for every enRoute message, there exists a routed message of the input list of Scheduling which has the same id, origin, injection time, and so forth.

Proof Obligation 16.
EnrouteCorr p (Scheduling.enRoute(lrm, a, s, o), lrm). (21) The next proof obligation states that the two output lists of function Scheduling are subsets of the parameter lrm.
The last proof obligation states that a message cannot be in both lists at the same time, that is, the intersection of these two list is the empty set.

Priorities. Function
PrioSort is used to model the priority scheme at the Network layer. It takes as parameter a list of messages and sorts it according to the user-defined parameter passed to function Scheduling. The priority policy can be based on a round-robin rule such as in the Hermes NoC [37], determined by the "age" of the messages like in Nostrum [34], or any other ordering. The signature of PrioSort is given by the following proof obligation.
Example 14. We instantiate the priority scheme with a round-robin policy, implemented in function rrSort. The user-defined parameter is simply the initial ordering at a node. At each simulation step, we permute this ordering. The initial ordering is loc, cw, ccw, acr, meaning that the local port has the priority. At every step, this ordering is shifted starting at the position of the port that has been served in the current step. For instance, if a node performs a read or a write to port ccw, the new ordering will be acr, loc, cw, ccw.
Another proof obligation guarantees that PrioSort is actually a sorting function, that is, its result is a permutation of its parameter lm. IsPerm(l 1 , l 2 ) is the predicate that checks whether l 1 is a permutation of l 2 .

Data Link Layer
The data link layer is responsible for the point-to-point transmission between two adjacent nodes. In particular, it implements the transmission protocol. Various types of protocols exist, such as simple handshake protocols [37] or sophisticated algorithms based, for instance, on load analysis [34].
The main function of our representation is TestRoutes that checks the feasibility of the next hop on the route. As mentioned in Section 5.2, an optional field can be added to the network state, for instance, to specify the request and acknowledge signals of a handshake protocol. In that case, the protocol is represented using two auxiliary functions: (i) ReqTrans, expresses the transmission of requests; (ii) AckTrans, expresses the transmission of acknowledgments.
Function ReqTrans updates the optional fields of the current state by setting request signals to 1. It takes the current state as parameter and returns the updated state.
Example 16. This function is instantiated by function Spi-derReqTrans. Every port with a nonempty buffer requests a transfer (we have one-place buffers, thus nonemptiness means that a flit has to be transferred). Function ActivReq sets the Rx signal of state element e to 1 as shown in Algorithm 8. This function statisfies the above proof abligation.
Function AckTrans takes as parameters the current network state and an address. It returns a new state in which the acknowledgment signal of this address is set to 1 if transmission to this address is possible. Proof Obligation 22.
Example 17. This function is instantiated by function Spider-AckTrans, which sets the Ackrx signal to 1 if the target address has an empty buffer. This is done by function ActivAck (see Algorithm 9).
Function TestRoutes takes as parameters a state and a routed message (of type D rm ). It returns a new state and a route. If the route is empty, it means that no route is possible for the message, that will temporarily remain blocked on its current node. Otherwise, the next hop on the route is valid for the message.

Proof Obligation 23.
TestRoutes : Example 18. Function SpiderTestRoutes is the valid Spidergon instance of function TestRoutes (see Algorithm 10). The instance for the handshake protocol needed 80 lines of ACL2 code.
In the case of adaptive algorithms, several routes would be possible and the instance of function TestRoutes would check all possible routes. Table 1 summarizes the proof effort for the generic model and for the Spidergon instantiation. Such instantiations can be performed by an experienced ACL2 user; a good understanding of the principles and of the proof obligations of the generic model is necessary. All proof times are measured on an Intel Core Duo T2400, 1.83 GHz, with 1.5 GBs of RAM. In the introduction, we sketched the correctness theorem (1) associated with function GeNoC that amounts to verifying the property ℘: every message arrived at some node n was actually issued at some source node s and originally addressed to node n, and the message reaches its destination without modification of its content.
In other words, for each arrived message (i.e., each element of GeNoC.T(M, A, att, T, st, z)), there exists a message in M with the same id, the same destination (dest), and the same content, denoted by f rm. The corresponding formalization is as follows.
Example 19. The GeNoC instance of the Spidergon network is given in Algorithm 11. It follows the pattern of Section 4, with the Spidergon instances SpiderR4D, SpiderRouting, and WHScheduling.
Once the different proof obligations of each component have been proven, the general correctness property (the theorem above) is directly obtained from the instantiated proof obligations. No additional verification effort is required.

Simulation.
We mentioned in the introduction that ACL2 provides both a theorem proving system and an execution engine. With the ACL2 implementation of our model, we not only perform formal proofs, but we also can execute the NoC behavior on test cases. A real synergy is thus obtained. While global safety properties can be demonstrated with theorem proving techniques, the detailed analysis of message progression and interaction in the network still requires the simulation of test scenarios. It is of utmost importance that these two verification techniques be applicable to the same model. Our model enables this synergy. We now illustrate this characteristic with a simple simulation of the Spidergon. In the simulation scenario described by Table 2, four messages are considered. Message 1 is split into 2 flits (hence its total number of flits is 4 due to the presence of the header flit and of the number of flits one), message 2 is split into 3 flits (its total number of flits is 5), and messages 3 and 4 occupy 3 and 4 flits.
The ACL2 execution of GeNoC yields textual results, made of lists. For readability, we have developed an animated visualization tool in Java. From ACL2 results in list form, it performs an animation of the evolution of the messages in the network. Figure 5 gives a screenshot of the 5th simulation step. Flits are numbered in decreasing order, from Nbflits-1 downto 0.
Messages 1 and 2 on the one hand and 3 and 4 on the other hand have the same destination. The messages follow the routes given in Table 3, where each location is associated with the iteration cycle (iteration 1 corresponds to time 0).
Message 1 departs at iteration cycle 2 and reaches the local port of node 8 before message 2, thus blocking it on port cw of node 8, as shown on the screenshot, until step 10. Message 4 arrives on the ccw port of node 4 when the first flit of message 3 departs on the local port of this node. The round-robin rule gives the priority to message 3, and message 4 completes its travel to its destination as soon as this node is freed (step 8). This simulation is faithful to the expected behavior.

Conclusion
In this paper, we presented a formal metamodel for reasoning about network specifications, from the transport to the data link layer of the OSI architectural model. In the metamodel, the main constituents of an NoC architecture-(1) topology, (2) interfaces, (3) routing, (4) scheduling-are characterized by their essential properties rather than their size or detailed behavior. Reasoning is based on the properties in order to prove safety correctness statements about the overall network architecture. In the metamodel, it is proved once and for all that the characteristic properties of the components imply the correctness statement.
To instantiate the metamodel on a particular NoC architecture, one has to fix (1) the node interconnection and how addresses are formed, (2) the interfaces and state holding elements of the nodes, (3) the progression of messages between neighboring nodes and the corresponding state transition functions, and (4) the priority or conflict resolution policy. Each one of these decisions is documented as a high level, executable algorithmic specification for the corresponding NoC constituent. For each one of them, all that needs to be done is the proof that the essential properties hold on the algorithmic specification. This is a modular proof, each constituent is processed in isolation. The number of ancillary definitions and intermediate lemmas, the size of the proof script, and the execution time of the proof system are reasonable.
Once all the proof obligations for the four constituents have been discharged, the overall correctness statement holds on the model of the NoC architecture as an immediate consequence of the proof performed on the metamodel. What has been obtained at this point is a high-level correctness statement for a parameterized design. All reasoning has been made irrespective of the message/flit size, number of nodes, link width, or other magnitude parameters, all of which will be set at a later design stage for a particular implementation of the NoC in a particular circuit.
In our work, the metamodel and its instantiations are coded in Lisp and the verification flow is supported by the ACL2 proof system. This is a beneficial feature for the credibility of our work seen from the point of view of the NoC designer. The same model that is used for proof is also executable and can be run dynamically on numeric test cases. In a previous case study, the Hermes NoC, for which a VHDL design was available to us, we could show the exact same results on the same test scenarios between the VHDL simulation and the GeNoC execution.
The GeNoC metamodel has been instantiated on a variety of network definitions (Octagon [33], Hermes [37], Spidergon [10]), and for each topology on the various routing and scheduling policies considered by their designers. We are now confident that the current metamodel has reached a sufficient level of expressiveness to support the usual message forwarding on regular structures. The correctness statement discussed in this paper is just one of the many safety properties that must be established; its merit is twofold. We believe that we are first to have formally proved it, and it has served the purpose of demonstrating our approach and proof process. We are now turning our attention to formalizing the absence of deadlocks and livelocks in the metamodel.
In terms of formal verification platform for NoCs, GeNoC constitutes the most abstract layer in the verification flow. The next step will be the refinement of the metamodel to support register transfer level. We want to provide a verification method, supported by proof tools, to show that a cycle accurate RTL model correctly implements a GeNoC instantiation and propagate in the process the satisfaction of the proof obligations. This is the direction of our research in the near future.