Details

Autor(en) / Beteiligte

• Eder, Kerstin
• Wright, Stephen

Titel

Experience of Deploying Event-B in Industrial Microprocessor Development

Ist Teil von

• Industrial Deployment of System Engineering Methods, 2013, p.107-122

Ort / Verlag

Germany: Springer Berlin / Heidelberg

Erscheinungsjahr

2013

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• 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.