Wright, Stephen (2009) MIDAS: A Formally Constructed Virtual Machine. [DEPLOY Interest Group Item] (Unpublished)
ZIP Archive (WinRar bundle of enclosed zip/rar files.) - Supplemental Material 117Mb | ||
| PDF (Description and installation instructions) - Submitted Version 203Kb |
Abstract
MIDAS (Microprocessor Instruction and Data Abstraction System) is a specification of an Instruction Set Architecture (ISA) capable of executing binary images compiled from the C language. It was developed to demonstrate a methodology for formal construction of various ISAs in Event-B via a generic model. It is intended to be representative of typical microprocessor ISAs, but using a minimal number of defined instructions, in order to make complete refinement practical. The intention is to simplify the number and complexity of the defined instructions at the cost of compiler complexity, run-time performance and code density, without compromising representativeness. There are two variants: a stack-based machine and a randomly accessible register array machine. The two variants employ the same instruction codes, the differences being limited to register file behavior.
Item Type: | DEPLOY Interest Group Item |
---|---|
Uncontrolled Keywords: | Event-B Virtual Machine Instruction Set Architecture |
Subjects: | Event-B > Event-B Examples |
ID Code: | 84 |
Deposited By: | Mr Stephen Wright |
Deposited On: | 06 Jun 2009 11:51 |
Last Modified: | 19 Apr 2010 16:05 |
Repository Staff Only: item control page