Types and Type Families for Hardware Simulation and Synthesis

The Internals and Externals of Kansas Lava
  • Andy Gill
  • Tristan Bull
  • Andrew Farmer
  • Garrin Kimmell
  • Ed Komp
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6546)


In this paper, we overview the design and implementation of our latest version of Kansas Lava. Driven by needs and experiences of implementing telemetry circuits, we have made a number of recent improvements to both the external API and the internal representations used. We have retained our dual shallow/deep representation of signals in general, but now have a number of externally visible abstractions for combinatorial, sequential, and enabled signals. We introduce these abstractions, as well as our new abstractions for memory and memory updates. Internally, we found the need to represent unknown values inside our circuits, so we made aggressive use of type families to lift our values in a principled and regular way. We discuss this design decision, how it unfortunately complicates the internals of Kansas Lava, and how we mitigate this complexity.


Type Family Sequential Circuit Combinatorial Circuit Abstract Syntax Tree Clock Domain 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Berry, G.: The constructive semantics of pure Esterel (1999),
  2. 2.
    Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: Hardware design in haskell. In: International Conference on Functional Programming, pp. 174–184 (1998)Google Scholar
  3. 3.
    Chakravarty, M.M.T., Keller, G., Jones, S.P.: Associated type synonyms. In: ICFP 2005: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, pp. 241–253. ACM, New York (2005)CrossRefGoogle Scholar
  4. 4.
    Claessen, K.: Embedded Languages for Describing and Verifying Hardware. PhD thesis, Dept. of Computer Science and Engineering, Chalmers University of Technology (April 2001)Google Scholar
  5. 5.
    Gill, A.: Type-safe observable sharing in Haskell. In: Proceedings of the 2009 ACM SIGPLAN Haskell Symposium (September 2009)Google Scholar
  6. 6.
    Gill, A., Bull, T., Kimmell, G., Perrins, E., Komp, E., Werling, B.: Introducing Kansas Lava. In: Morazán, M.T., Scholz, S.-B. (eds.) IFL 2009. LNCS, vol. 6041, pp. 18–35. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. 7.
    Jantsch, A., Sander, I.: Models of computation and languages for embedded system design. IEE Proceedings on Computers and Digital Techniques 152(2), 114–129 (2005); Special issue on Embedded Microelectronic SystemsCrossRefGoogle Scholar
  8. 8.
    Jones, S.P., Shields, M.: Lexically scoped type variables,
  9. 9.
    Leijen, D., Meijer, E.: Domain specific embedded compilers. In: 2nd USENIX Conference on Domain Specific Languages (DSL 1999), Austin, Texas, pp. 109–122 (October 1999)Google Scholar
  10. 10.
    Matlage, K., Gill, A.: ChalkBoard: Mapping functions to polygons. In: Morazán, M.T., Scholz, S.-B. (eds.) IFL 2009. LNCS, vol. 6041, pp. 55–71. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  11. 11.
    McBride, C., Patterson, R.: Applicative programing with effects. Journal of Functional Programming 16(6) (2006)Google Scholar
  12. 12.
    Sander, I.: System Modeling and Design Refinement in ForSyDe. PhD thesis, Royal Institute of Technology, Stockholm, Sweden (April 2003)Google Scholar
  13. 13.
    Sheeran, M.: mufp, a language for vlsi design. In: LFP 1984: Proceedings of the 1984 ACM Symposium on LISP and Functional Programming, pp. 104–112. ACM, New York (1984)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Andy Gill
    • 1
  • Tristan Bull
    • 1
  • Andrew Farmer
    • 1
  • Garrin Kimmell
    • 1
  • Ed Komp
    • 1
  1. 1.Information Technology and Telecommunication Center, Department of Electrical Engineering and Computer ScienceThe University of KansasLawrenceUSA

Personalised recommendations