This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Using Term Rewriting Systems to Design and Verify Processors
May/June 1999 (vol. 19 no. 3)
pp. 36-46
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.

1. J.R. Burch and D.L. Dill, "Automatic Verification of Pipelined Microprocessor Control," Proc. Computer-Aided Verification (CAV 94), Springer-Verlag, 1994, pp. 68-80.
2. B. Cook, J. Launchbury, and J. Matthews, "Specifying Superscalar Microprocessors in Hawk," Proc. Workshop on Formal Techniques for Hardware and Hardware-Like Systems,Marstrand, Sweden; published by Dept. of Computer Science, Chalmers Univ. of Tech nology, June 1998.
3. K.L. McMillan, "Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking," Proc. Workshop on Formal Techniques for Hardware and Hardware-Like Systems,Marstrand, Sweden; published by Dept. of Computer Science, Chalmers Univ. of Tech nology, June 1998.
4. P.J. Windley, "Formal Modeling and Verification of Microprocessors," IEEE Trans. Computers, Vol. 44, No. 1, Jan. 1995, pp. 54-72.
5. J. Hennessy and D. Patterson, Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1995.
6. X. Shen, Arvind, and L. Rudolph, "Commit-Reconcile&Fences (CRF): A New Memory Model for Architects and Compiler Writers," Proc. 26th Int'l Symp. Computer Architecture, IEEE Computer Society Press, Los Alamitos, Calif., May 1999, pp. 150-161.
7. X. Shen, Arvind, and L. Rudolph, "CACHET: An Adaptive Cache Coherence Protocol for Distributed Shared-Memory Systems," Proc. 13th ACM Int'l Conf. Supercomputing, ACM, New York, June 1999.
8. F. Baader and T. Nipkow, Term Rewriting and All That, Cambridge Univ. Press, Cambridge, UK, 1998.
9. J.W. Klop, "Term Rewriting System," in Handbook of Logic in Computer Science, Vol. 2, S. Abramsky, D. Gabbay, and T. Maibaum, eds., Oxford University Press, 1992.
10. X. Shen and Arvind, "Design and Verification of Speculative Processors," Proc. Workshop on Formal Techniques for Hardware and Hardware-Like Systems,Marstrand, Sweden, June 1998; also appears as CSG Memo 400B, Laboratory for Computer Science, MIT, Cambridge, Mass., http://www.csg.lcs.mit.edu/pubscsgmemo.html .
11. J.C. Hoe and Arvind, "Hardware Synthesis from Term Rewriting Systems," CSG Memo 421, Laboratory for Computer Sci., MIT, Cambridge, Mass., 1999; http://www.csg.lcs.mit.edu/pubscsgmemo.html .

Citation:
Arvind , Xiaowei Shen, "Using Term Rewriting Systems to Design and Verify Processors," IEEE Micro, vol. 19, no. 3, pp. 36-46, May-June 1999, doi:10.1109/40.768501
Usage of this product signifies your acceptance of the Terms of Use.