Article Preview
Top1. Introduction
As the technologies improved and the electronic systems became increasingly complex with many independent modules communicating with each other on a single PCB board, a need for a well defined inter–communication scheme arose. Several manufacturers introduced so called bus–based System–on–Chip (SoC) communication frameworks in order to deal with the increased complexity. One of such products is the AMBA 2 AHB interface bus (ARM, 2005). The common feature of these frameworks is that there is a bus to which master modules, such as processor cores and DSPs, must connect in order to access slave modules such as memories. In such bus–based SoC architectures the bus is a shared communication resource with the masters competing for the access to the slaves. Because it is a shared resource, it can become overloaded quickly, especially when several master modules are connected to it (Lahiri, Raghunathan, & Dey, 2001).
In order to overcome the single bus overloading, bus matrix–based architectures (Nakajima, Yamamoto, Ozaki, Sezaki, Kanakagi, Furuzono, Sakamoto, Aruga, Sumita, Tsutsumi, Ueda, & Ichinomiya, 2002) appeared consisting of several parallel buses to offer the bandwidth required for complex SoCs. The main drawback of this approach is that every master is connected to every slave in the system, resulting in a very large number of buses. To overcome this disadvantage, approaches for creating a partial bus matrix for a given application have been proposed (Pasricha, Ben–Romdhane, & Dutt, 2007) in order to reduce complexity and power consumption as well as increase efficiency. During the same time, the Network–on–Chip communication paradigm (Hemani, Jantch, Kumar, Postula, Öberg, Millberg, & Lindqvist, 2000) has been introduced offering very high communication bandwidth and network scalability through its regular structure. Depending on the requirements and priorities of a given application (high communication bandwidth, latency, reduced power consumption, etc) a system designer can choose a suitable communication scheme out of the aforementioned ones.
Multi–Processor Systems–on–Chips (MPSoC) are used in many important applications, from home use electronics and embedded systems to large control and data transfer systems. Hence efficient methods are needed in order to specify, model the communication and verify their design. Formal methods of concurrent programming, such as CSP (Hoare, 1985), Petri Nets (Desel & Juhás, 2001) and Action Systems (Back & Kurki – Suonio, 1983) can be used to design these systems. Action Systems, the modeling language of this paper, provides a rigorous framework for MPSoC design (Back, Martin, & Sere, 1995; Plosila, Seceleanu, & Sere, 2004) and it is sufficient for the work presented here. There is adequate tool support from the B Method (Abrial, 1996), by converting Action Systems to B Action Systems (Waldén & Sere, 1998), as well as the notion of stepwise refinement (Back & Sere, 1996) is built in the framework which allows an abstract system to be refined to a more concrete one preserving its original functionality. Note that refinement is out of the scope of this paper.