Formal models of cache coherent communication fabrics: from micro-architectures to RTL designs

The xMAS primitives form a suitable basis for modelling interconnection networks, even nontrivial structures such as the Spidergon network. By implementing iterative and/or recursive modelling features in the supporting toolset (WickedXmas), a network can be constructed that remains generic in the number of nodes. Using a formally specified syntax for the equations in source, switch, function et cetera, the necessary packet routing decisions can be defined unambiguously. There remains a small amount of ambiguity in the expression language that should be addressed. Assumptions about the tacit resolution of identical data fields for multi-input primitives should be formalized in order to avoid different interpretations across toolchains. In conjuction with the generation of a flattened netlist and an automated translation to a simulation-capable language such as Verilog, the network can be verified. The generalisation of xMAS primitives to their n-input or -output equivalents is straightforward, with only minor remarks for the arbitration of n-input merges. A particular area where xMAS is lacking expressivity is pipelining. Using the k >= 2-deep queue primitives, data processing stages can be formed that are locally decoupled from each other using elastic buffers (FIFOs). When extending the notion of a queue to k = 1, however, pipelining becomes severely limited in bandwidth and cannot be used to model the typical register stages used in manually crafted digital logic. Combining the xMAS formalism with the SELF protocol used by Cortadella et al. could address this shortcoming. The xMAS primitives are not semantically complete and are lacking some expressivity that would be available when modelling directly in an underlying hardware description language. Shortcomings in expressivity that presented themselves during the design of the Write- Once example algorithm were addressed by the introduction of new primitives (ctrljoin, forkany, joitch, peek). Although not all of these will adhere to the persistence assumption, their existence is indicative that a more rigorous exploration of possible Boolean equations for control and data flow will give rise to additional useful primitives