Issue No. 03 - May/June (1999 vol. 19)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/40.768501
We present a novel use of Term Rewriting Systems (TRS's) to describe micro-architectures. The state of a system is represented as a TRS term while the state transitions are represented as TRS rules. TRS descriptions are amenable to both verification and synthesis. We illustrate the use of TRS's by giving the operational semantics of a simple RISC instruction set. We then present another TRS that implements the same instruction set on a micro-architecture which permits register renaming and speculative execution. The correctness of the speculative implementation is discussed in terms of the ability of the two TRS's to simulate each other. Our method facilitates understanding of important micro-architectural differences without delving into low-level implementation details.
Xiaowei Shen, Arvind , "Using Term Rewriting Systems to Design and Verify Processors", IEEE Micro, vol. 19, no. , pp. 36-46, May/June 1999, doi:10.1109/40.768501