Symbolic Simulation of Microprocessor Models Using Type Classes in Haskell

  • Nancy A. Day
  • Jeffrey R. Lewis
  • Byron Cook
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


We present a technique for doing symbolic simulation of microprocessor models in the functional programming language Haskell.We use polymorphism and the type class system, a unique feature of Haskell, to write models that work over both concrete and symbolic data.We offer this approach as an alternative to using uninterpreted constants. When the full generality of rewriting is not needed, the performance of symbolic simulation by evaluation is much faster than previously reported symbolic simulation efforts in theorem provers.


Theorem Prover Type Class Symbolic Data Binary Decision Diagram Functional Programming Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    P. Bjesse, K. Claessen, M. Sheeran, and S. Singh. Lava: Hardware design in Haskell. In ACM Int. Conf. on Functional Programming, 1998.Google Scholar
  2. 2.
    R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.CrossRefGoogle Scholar
  3. 3.
    B. Cook, J. Launchbury, and J. Matthews. Specifying superscalar microprocessors in Hawk. In Workshop on Formal Techniques for Hardware, 1998.Google Scholar
  4. 4.
    F. Corella, Z. Zhou, X. Song, M. Langevin, and E. Cerny. Multiway decision graphs for automated hardware verification. Technical Report RC19676, IBM, 1994. Also Formal Methods in Systems Design, 10(1), pages 7–46, 1997.Google Scholar
  5. 5.
    N. A. Day and J. J. Joyce. Symbolic functional evaluation. To appear in TPHOLs’99.Google Scholar
  6. 6.
    N. A. Day, J. Launchbury, and J. Lewis. Logical abstractions in Haskell. Submitted for publication.Google Scholar
  7. 7.
    N. A. Day, J. R. Lewis, and B. Cook. Symbolic simulation of microprocessor models using type classes in Haskell. Technical Report CSE-99-005, Oregon Graduate Institute, 1999.Google Scholar
  8. 8.
    D. A. Greve. Symbolic simulation of the JEM1 microprocessor. In FMCAD, volume 1522 of LNCS, pages 321–333. Springer, 1998.Google Scholar
  9. 9.
    J. Joyce. Multi-Level Verification of Microprocessor Based Systems. PhD thesis, Cambridge Comp. Lab, 1989. Technical Report 195.Google Scholar
  10. 10.
    J. J. Joyce. Generic specification of digital hardware. In Designing Correct Circuits, pages 68–91. Springer-Verlag, 1990.Google Scholar
  11. 11.
    J. Matthews, B. Cook, and J. Launchbury. Microprocessor specification in Hawk. In International Conference on Computer Languages, 1998.Google Scholar
  12. 12.
    J. Moore. Symbolic simulation: An ACL2 approach. In FMCAD, volume 1522 of LNCS, pages 334–350. Springer, 1998.Google Scholar
  13. 13.
    J. Peterson and K. Hammond, editors. Report on the Programming Language Haskell. Yale University, Department of Computer Science, RR-1106, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Nancy A. Day
    • 1
  • Jeffrey R. Lewis
    • 1
  • Byron Cook
    • 1
  1. 1.Oregon Graduate InstituteORUSA

Personalised recommendations