The XCore microprocessor is an embedded device developed by XMOS Ltd. of Bristol, UK. The Instruction Set Architecture (ISA) contains a range of typical instructions, for example, for control flow, register-to-register calculation and memory access, but also provides support for efficient multi-threaded programming, parallelism and communication with other devices via fast interconnects. Support for these features is integrated into the ISA of the XCore. This greatly improves run-time performance, at the cost of introducing specialist instructions to the ISA, which comprises 170 instructions. The ISA contains instructions of both two and four byte length, and implements a very compact encoding scheme. The XCore is general-purpose and has been exploited in a range of different markets, including audio, display, communications, robotics and motor control. As part of a Knowledge Transfer Secondment (Grant EP/H500316/1) at the University of Bristol, a formal model of the complete ISA was constructed in Event-B notation, using the Rodin toolset. This project applied the Event-B and Rodin-based techniques for ISA analysis, developed at the University of Bristol, and extended them to an industrial setting.
|Title of host publication||Industrial Deployment of System Engineering Methods|
|Publisher||Springer Berlin Heidelberg|
|Number of pages||16|
|ISBN (Print)||9783642331701, 3642331696, 9783642331695|
|Publication status||Published - 1 Jul 2013|