Loading...
Please wait, while we are loading the content...
Similar Documents
Modeling and Veriication of Isa Implementations Computation Structures Group Memo 400 (a) Modeling and Veriication of Isa Implementations
| Content Provider | Semantic Scholar |
|---|---|
| Author | Shen, Xiaowei Arvindxwshen, Arvind |
| Copyright Year | 1998 |
| Abstract | We propose a method to precisely model implementations of Instruction Set Ar-chitectures (ISA) using term rewriting systems (TRS). Our method facilitates understanding of important micro-architectural diierences without delving into low-level implementation details. More importantly, the use of TRS allows us to prove rigorously the equivalence of diierent implementations. We rst deene AX, a simple RISC ISA, by specifying its operational semantics using a simple in-order execution model. We then give an AX implementation which uses register renaming and permits out-of-order instruction execution. The equivalence of the two models is proved by showing that the two TRS's can simulate each other. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-400a.ps.gz |
| Alternate Webpage(s) | http://www.csg.lcs.mit.edu/Users/xwshen/papers/memo400a.ps |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
