Managing Complexity Through Abstraction: A refinement-based approach to formalize Instruction Set Architectures

Fangfang Yuan, Stephen Wright, Kerstin I Eder, David May

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

1 Citation (Scopus)


Verifying the functional correctness of a processor requires a sound and complete specification of its Instruction Set Architecture (ISA). Current industrial practice is to describe a processor's ISA informally using natural language often with added semi-formal notation to capture the functional intent of the instructions. This leaves scope for errors and inconsistencies. In this paper we present a method to specify, design and construct sound and complete ISAs by stepwise refinement and formal proof using the formal method Event-B. We discuss how the automatically generated Proof Obligations help to ensure self-consistency of the formal ISA model, and how desirable properties of ISAs can be enforced within this modeling framework. We have developed a generic ISA modeling template in Event-B to facilitate reuse. The key value of reusing such a template is increased model integrity. Our method is now being used to formalize the ISA of the XMOS XCore processor with the aim to guarantee that the documentation of the XCore matches the silicon and the silicon matches the architectural intent.
Original languageEnglish
Title of host publication13th International Conference on Formal Engineering Methods (ICFEM)
Subtitle of host publicationLecture Notes in Computer Science
ISBN (Print)978-3-642-24558-9
Publication statusPublished - Oct 2011

Publication series

NameLecture Notes in Computer Science


  • verification
  • foramal methods
  • instruction set formalization
  • event b


Dive into the research topics of 'Managing Complexity Through Abstraction: A refinement-based approach to formalize Instruction Set Architectures'. Together they form a unique fingerprint.

Cite this