Industrial deployment of system engineering methods providing high dependability and productivity

 

A Formally Constructed Instruction Set Architecture Definition of the XCore Microprocessor

Wright, Stephen A Formally Constructed Instruction Set Architecture Definition of the XCore Microprocessor. [DEPLOY Associate Item]

[img]
Preview
PDF
493Kb
[img]
Preview
PDF
2704Kb
[img] ZIP Archive
20Mb

Abstract

The XCore microprocessor is an embedded device developed by XMOS Ltd of Bristol, UK. The processor is general-purpose and has therefore been deployed in a range of different markets, including audio, display, communications, robotics and motor control. The technology is re-used in multiple products, including the XS1-G4 (a four-core device that can run up to 32 real time tasks), and the XS1-L1 (a single core device that can run up to 8 real time tasks). The ISA contains a range of typical instructions such as control-flow, register-to-register calculation and memory access, but also provides support for efficient synchronized multi-threaded programming and parallelism with other devices via fast interconnects. Support for these features is integrated into the ISA of the XCore, in contrast to a conventional memory-mapped device approach. This greatly improves run-time performance, at the cost of introducing specialist instructions to the ISA, which comprises 176 instructions. As part of a Bristol University Knowledge Transfer Secondment (KTS) (Grant EP/H500316/1), a formal model of the complete ISA was constructed in Event-B, using the Rodin toolset. This project applied and extended the Event-B and RODIN based techniques for Instruction Set Architecture (ISA) analysis, developed by Dr Stephen Wright during his doctoral research, to an industrial setting. To that end, XMOS Ltd hosted Dr Wright in the period October 2010 to October 2011.

Item Type:DEPLOY Associate Item
Uncontrolled Keywords:Instruction Set Architecture Microprocessor
Subjects:Tool developments > Code generation
Tool developments > Provers
Industrial Deployment > Other
Event-B > Event-B Examples
Methodology > Real-time systems
ID Code:346
Deposited By: Mr Stephen Wright
Deposited On:27 Sep 2011 12:02
Last Modified:27 Sep 2011 12:02

Repository Staff Only: item control page

Deploy-Project - All right reserved