On embedding a microarchitectural design language within Haskell

ABSTRACT

Based on our experience with modelling and verifying microarchitectural designs within Haskell, this paper examines our use of Haskell as host for an embedded language. In particular, we highlight our use of Haskell's lazy lists, type classes, lazy state monad, and unsafe Perform I0, and point to several areas where Haskell could be improved in the future. We end with an example of a benefit gained by bringing the functional perspective to microarchitectural modelling.

References

1. 1.Hawk website. http://www.cse.ogi.edu/PacSoft/projects/Hawk/.]]
2. 2.AAGAARD, M., AND LEESER, M. Reasoning about pipelines with structural hazards. In Second International Conference on Theorem Provers in Circuit Design (Bad Herrena}b, Germany, Sept. 1994).]]
3. 3.BJESSE, P., CLAESSEN, K., SHEERAN, M., AND SINGH, S. Lava: Hardware design in Haske}l. In International Conference on Functional Programming (Baltimore, July 1998).]]
4. 4.BRYANT, R.. E. Symbolic boolean manipulation with ordered binary decision diagrams. AUM Computing Surveys 25, 3 (1992).]]
5. 5.COOK, B., LAUNCHBUR~, J., AND MATTHEWS, J. Specifying superscalar microprocessors with Hawk. In Workshop on Formal Techniques for Hardware (Maarstrand, Sweden, June 1998).]]
6. 6.COOK, B., L^vNCnnUaY, J., M^~TH~ws, J., ^NO KmBURTZ, D. Formal verification of explicitly parallel microprocessors. In Conference on Correct Hardware Design and Verification Methods (1999).]]
7. 7.DAY, N. A., LAUNCItBURY, J., ANt) LEWIS, J. R. Logical abstractions in Haskell. submitted for publication, 1999.]]
8. 8.DAY, N. A., LEWIS, J. R., AND COOK, B. Symbolic simulation of microprocessor models using type classes in Haskell. Tech. Rep. CSE-99-005, Department of Computer Science and Engineering, Oregon Graduate Institute: 1999.]]
9. 9.DULONG, C. The IA-64 architecture at work. IEEE Computer 31~ 7 (1998).]]
10. 10.ELLIOTT, C. An embedded modeling language approach to interactive 3D and multimedia animation. To appear in iEEE Transaet~ions on Software Engineering (1999).]]
11. 11.ELLIOTT, C., AND HUDAg, P. Functional reactive animation. In The International Conference on Func. tional Programming (Amsterdam, The Netherlands, June 1997).]]
12. 12.FJr/NE, S., LE~J~N, D., MEiJER, E., Arqo JoNEs, S. P. H/Direct: A binary foreign language interface for Haskell. In International Conference o~ Functional Programming (Baltimore, July 1998).]]
13. 13.GWENNAP, L. First Merced patent surfaces;. Microprocessor Report 11, 3 (1997).]]
14. 14.GWr, NNAP, L. Intel, HP make EPIC disclosure. Microprocessor Report 11, 14 (1997).]]
15. 15.HAZELHURST, S., AND SEGER, C.-J. H. Symbolic trajectory evaluation. In Formal Hardware Verification, Springer-Verlog, 1997.]]
16. 16.JONES, G., AND SHEERAN, M. Collecting butterflies. Tech. rep., Oxford University Computing Laboratory, 1991.]]
17. 17.JONES, G., AND SHEERAN, M. Designing arithmetic circuits by refinement in ruby. In Mathemati. cs of Program Construction (1993), vol. 669 of LNC5', Springer Verlag.]]
18. 18.JONES, M. P. Qualified Types: Theory and Practice. PhD thesis, Department of Computer Science, Oxford University, 1992.]]
19. 19.JONES, S. P., AND MARLOW, S. Stretching the storage manager: weak pointers and stable names in. Haskell, 1999. Submitted for publication.]]
20. 20.LANDiN, P. J. The Next 700 Programming La,nguages. Communications of the A CM 9, 3 (March 1966), 157- 164.]]
21. 21.LAUNCHBUR~, J., AND JONES, S. P. Lazy functional state threads. In Programming Languages Design and Implementation (Orlando, Florida, 1994), ACM Press.]]
22. 22.LAUNCHBUR~, J., AND PATT~tSON, R. Parametricity and unboxing with unpointed types. In The l%ternational Conference on Functional Programming (1996).]]
23. 23.LAUNC~BUR~, j., AND PEYTON JONES, $. L. State in Haskell. Lisp and Symbolic Computation 8, 4 (December 1995), 293-341.]]
24. 24.MATTHEWS, J. Re'cursive function definition over coinductive types. In The l~th international Conference on Theorem Proving in Higher Order Logics (Sept. 1999).]]
25. 25.MATTHBWS, J., AND LAUNCHBURY, J. Elementary mio croaxchitecture algebra. In International Conference on Computer-Aided Verification (Trento, Italy, July 1999).]]
26. 26.MATTHEWS, J., AND LAUNCnBUR~, J. Elementary microarchitecture algebra: Top-level proof of pipelined microarchitecture. Tech. Rep. CSE-99-O02, Oregon Graduate Institute, Computer Science Department, Portland, Oregon, Mar. 1999.]]
27. 27.MATTHEWS, J., LAUNCHBURY, J., AND COOK, B, Specifying microprocessors in Hawk. In IEEE International Conference on Computer Languages (Aug. 1998).]]
28. 28.O'DONNELL, J. From transistors to computer architecture: Teaching functional circuit specification in Hydra. In Symposium on Functional Programming Languages in Education (July 1995).]]
29. 29.OKASAKI, C. Purely Functional Data Structures. PhD thesis, School of Computer Science, Carnegie Mellon University, September 1996.]]
30. 30.PAULSON, L. IsabeUe: A Generic Theorem Prover. Springer-Verlag, 1994.]]
31. 31.SECER, C.-J. Voss - a formal hardware verification system. Tech. Rep. 93-45, University of British Columbia, 1993.]]
32. 32.SHARP, R., AND RASMUSSEN, O. An introduction to Ruby. Teaching Notes ID-U: 1995-80, Dept. of Computer Science, Technical University of Denmark, October 1995.]]
33. 33.SHRWEa, B., AND SMITH, B. The Anatomy of a High- IEEE Computer Society Press, 1998.]]
34. 34.SR!VAS, M., AND BICKFORO, M. Formal verification of a pipelined microprocessor. IEEE Software 7, 5 (1990).]]
35. 35.TULLSEN, D. M., EGGERS, S. J., EMER, J. S., LEVY, H. M., Lo, J. L., AND STAMM, R. L. Exploiting choice: Instruction fetch and issue on an implementable simultaneous multithreading processor, in 23rd Annual International Symposium on Computer Architecture (Philadelphia, PA, May 1996).]]
36. 36.WADLER, P. Views: a way for pattern matching to cohabit with data abstraction. In 1~ 'th A CM Symposium on Principles of Programming Languages (Munich, Germany, January 1987).]]
37. 37.WAr)LEa, P., TAHA, W., AND MACQUEEN, D. B. How to add laziness to a strict language withouth even being odd. In Proceedings of the 1998 A(YM Workshop on ML (Sept. 1998), pp. 24-30. Baltimore, MD.]]

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language features

• Theory of computation

  • Semantics and reasoning

    • Program constructs