--- 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. \r\n\r\nAs 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." accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: stephen.wright@bris.ac.uk copyright_holders: [] corp_creators: [] creators_id: - stephen.wright@bris.ac.uk creators_name: - family: Wright given: Stephen honourific: '' lineage: '' data_type: ~ date: ~ date_type: ~ datestamp: 2011-09-27 12:02:46 department: Computer Science dir: disk0/00/00/03/46 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 346 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: application/pdf;http://deploy-eprints.ecs.soton.ac.uk/346/1/XCore%20Deploy%20Covering%20Document.pdf|application/pdf;http://deploy-eprints.ecs.soton.ac.uk/346/7/XCore%20ISA%20Formal%20Specification.pdf|application/zip;http://deploy-eprints.ecs.soton.ac.uk/346/13/XCoreBundle.zip full_text_status: public funders: [] id_number: ~ importid: ~ institution: University of Bristol isbn: ~ ispublished: ~ issn: ~ item_issues_comment: [] item_issues_count: ~ item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: Instruction Set Architecture Microprocessor lastmod: 2011-09-27 12:02:46 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: ~ output_media: ~ pagerange: ~ pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: ~ producers_id: [] producers_name: [] projects: [] publication: ~ publisher: ~ refereed: ~ referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 13 series: ~ skill_areas: [] source: ~ status_changed: 2011-09-27 12:02:46 subjects: - Code_generation - Proof - deploy_industrial_other - examples - rt_modelling succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: A Formally Constructed Instruction Set Architecture Definition of the XCore Microprocessor type: deploy_associate_item userid: 100 volume: ~