creators_name: Wright, Stephen creators_id: stephen.wright@bris.ac.uk type: deploy_associate_item datestamp: 2011-09-27 12:02:46 lastmod: 2011-09-27 12:02:46 metadata_visibility: show title: A Formally Constructed Instruction Set Architecture Definition of the XCore Microprocessor subjects: Code_generation subjects: Proof subjects: deploy_industrial_other subjects: examples subjects: rt_modelling full_text_status: public keywords: Instruction Set Architecture Microprocessor 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. institution: University of Bristol department: Computer Science citation: Wright, Stephen A Formally Constructed Instruction Set Architecture Definition of the XCore Microprocessor. [DEPLOY Associate Item] document_url: http://deploy-eprints.ecs.soton.ac.uk/346/1/XCore%20Deploy%20Covering%20Document.pdf document_url: http://deploy-eprints.ecs.soton.ac.uk/346/7/XCore%20ISA%20Formal%20Specification.pdf document_url: http://deploy-eprints.ecs.soton.ac.uk/346/13/XCoreBundle.zip