Experience of deploying event-B in industrial microprocessor development

Stephen Wright*, Kerstin Eder

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapter in a book

Abstract

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.

Original languageEnglish
Title of host publicationIndustrial Deployment of System Engineering Methods
PublisherSpringer Berlin Heidelberg
Pages107-122
Number of pages16
ISBN (Print)9783642331701, 3642331696, 9783642331695
DOIs
Publication statusPublished - 1 Jul 2013

Fingerprint Dive into the research topics of 'Experience of deploying event-B in industrial microprocessor development'. Together they form a unique fingerprint.

Cite this