?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=A+Formally+Constructed+Instruction+Set+Architecture+Definition+of+the+XCore+Microprocessor&rft.creator=Wright%2C+Stephen&rft.subject=Code+generation&rft.subject=Provers&rft.subject=Other&rft.subject=Event-B+Examples&rft.subject=Real-time+systems&rft.description=The+XCore+microprocessor+is+an+embedded+device+developed+by+XMOS+Ltd+of+Bristol%2C+UK.+The+processor+is+general-purpose+and+has+therefore+been+deployed+in+a+range+of+different+markets%2C+including+audio%2C+display%2C+communications%2C+robotics+and+motor+control.+The+technology+is+re-used+in+multiple+products%2C+including+the+XS1-G4+(a+four-core+device+that+can+run+up+to+32+real+time+tasks)%2C+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%2C+register-to-register+calculation+and+memory+access%2C+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%2C+in+contrast+to+a+conventional+memory-mapped+device+approach.+This+greatly+improves+run-time+performance%2C+at+the+cost+of+introducing+specialist+instructions+to+the+ISA%2C+which+comprises+176+instructions.+%0D%0A%0D%0AAs+part+of+a+Bristol+University+Knowledge+Transfer+Secondment+(KTS)+(Grant+EP%2FH500316%2F1)%2C+a+formal+model+of+the+complete+ISA+was+constructed+in+Event-B%2C+using+the+Rodin+toolset.+This+project+applied+and+extended+the+Event-B+and+RODIN+based+techniques+for+Instruction+Set+Architecture+(ISA)+analysis%2C+developed+by+Dr+Stephen+Wright+during+his+doctoral+research%2C+to+an+industrial+setting.+To+that+end%2C+XMOS+Ltd+hosted+Dr+Wright+in+the+period+October+2010+to+October+2011.&rft.type=DEPLOY+Associate+Item&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F346%2F1%2FXCore%2520Deploy%2520Covering%2520Document.pdf&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F346%2F7%2FXCore%2520ISA%2520Formal%2520Specification.pdf&rft.format=application%2Fzip&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F346%2F13%2FXCoreBundle.zip&rft.identifier=++Wright%2C+Stephen+++A+Formally+Constructed+Instruction+Set+Architecture+Definition+of+the+XCore+Microprocessor.++%5BDEPLOY+Associate+Item%5D+++++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F346%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>