A Formal Instruction Set Architecture Definition of the XCor
Posted: Thu Sep 29, 2011 11:52 am
Version: 1
Status: Public release
License: BSD
As part of an Engineering and Physical Sciences Research Council and Bristol University Knowledge Transfer Secondment (KTS) (Grant EP/H500316/1), a formal model of the complete XCore ISA was constructed in Event-B formal notation , 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. XMOS Ltd hosted Dr Wright in the period October 2010 to October 2011.
You can find it all at:
http://deploy-eprints.ecs.soton.ac.uk/346/
Status: Public release
License: BSD
As part of an Engineering and Physical Sciences Research Council and Bristol University Knowledge Transfer Secondment (KTS) (Grant EP/H500316/1), a formal model of the complete XCore ISA was constructed in Event-B formal notation , 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. XMOS Ltd hosted Dr Wright in the period October 2010 to October 2011.
You can find it all at:
http://deploy-eprints.ecs.soton.ac.uk/346/