Synchronous digital circuits as functional programs

Abstract

Functional programming techniques have been used to describe synchronous digital circuits since the early 1980s. Here we survey the systems and formal underpinnings that constitute this tradition. We situate these techniques with respect to other formal methods for hardware design and discuss the work yet to be done.

References

1. Abbott, M., Altenkirch, T., and Ghani, N. 2005. Containers: Constructing strictly positive types. Theor. Comput. Sci. 342, 1, 3--27.
2. Abel, A. 2010. MiniAgda: Integrating sized and dependent types. In Proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR'10), A. Bove, E. Komendantskaya, and M. Niqui, Eds. EPTCS, vol. 43, 14--28.
3. André, C. and Peraldi-Frati, M.-A. 2000. Behavioral specification of a circuit using SyncCharts: A case study. In Proceedings of the 26th EUROMICRO 2000 Conference, Informatics: Inventing the Future (EUROMICRO'00). IEEE Computer Society, Washington, DC, 1091.
4. Arvind and Nikhil, R. S. 2008. Hands-on introduction to Bluespec System Verilog (BSV) (abstract). In Proceedings of 6th ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE'08). IEEE Computer Society, Washington, DC, 205--206.
5. Axelsson, E. 2003. Description and Analysis of Multipliers Using Lava. M.S. thesis, Chalmers University of Technology.
6. Axelsson, E., Claessen, K., and Sheeran, M. 2005. Wired: Wire-aware circuit design. In Proceedings of the 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'05), D. Borrione and W. J. Paul, Eds. LNCS, vol. 3725. Springer, Berlin, 5--19.
7. Axelsson, E., Claessen, K., Sheeran, M., Svenningsson, J., Engdal, D., and Persson, A. 2010. The design and implementation of Feldspar - an embedded language for digital signal processing. In Selected Papers from the 22nd International Symposium on Implementation and Application of Functional Languages (IFL'10), J. Hage and M. T. Morazán, Eds. LNCS, vol. 6647. Springer, Berlin, 121--136.
8. Backus, J. W. 1978. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. Commun. ACM 21, 8, 613--641.
9. Barthe, G., Frade, M. J., Giménez, E., Pinto, L., and Uustalu, T. 2004. Type-based termination of recursive definitions. Math. Struct. Comput. Sci. 14, 1, 97--141.
10. Benveniste, A., Caspi, P., Edwards, S. A., Halbwachs, N., Le Guernic, P., and de Simone, R. 2003. The synchronous languages 12 years later. Proc. IEEE 91, 1, 64--83.
11. Berry, G. 1989. Real time programming: Special purpose or general purpose languages? In Proceedings of the IFIP 11th World Computer Congress (Information Processing'89), G. Ritter, Ed. North-Holland/IFIP, Amsterdam, 11--17.
12. Berry, G. 1999. The Esterel v5 language primer. Draft book.
13. Bertot, Y. and Komendantskaya, E. 2008. Using structural recursion for corecursion. In Revised Selected Papers from the International Conference on Types for Proofs and Programs (TYPES'08), S. Berardi, F. Damiani, and U. de'Liguoro, Eds. LNCS, vol. 5497. Springer, Berlin, 220--236.
14. Bird, R. S. 1987. An introduction to the theory of lists. In Logic of Programming and Calculi of Discrete Design, M. Broy, Ed. Springer, Berlin, 3--42.
15. Bjesse, P., Claessen, K., Sheeran, M., and Singh, S. 1998. Lava: Hardware design in Haskell. In Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP'98). ACM, New York.
16. Bose, B. and Johnson, S. D. 1993. DDD-FM9001: Derivation of a verified microprocessor. In Proceedings of the IFIP WG 10.5 Advanced Research Working Conference Correct Hardware Design and Verification Methods (CHARME'93), G. J. Milne and L. Pierre, Eds. LNCS, vol. 683. Springer, Berlin, 191--202.
17. Boulton, R. J., Gordon, A. D., Gordon, M. J. C., Harrison, J., Herbert, J., and Van Tassel, J. 1992. Experience with embedding hardware description languages in HOL. In Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience (TPCD'92), V. Stavridou, T. F. Melham, and R. T. Boute, Eds. IFIP Transactions, vol. A-10. North-Holland, Amsterdam, 129--156.
18. Bourdoncle, F. and Merz, S. 1997. Type-checking higher-order polymorphic multi-methods. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'97), P. Lee, F. Henglein, and N. D. Jones, Eds. ACM, New York, 302--315.
19. Braibant, T. 2011. Coquet: A Coq library for verifying hardware. In Proceedings of the 1st International Conference on Certified Programs and Proofs (CPP'11), J.-P. Jouannaud and Z. Shao, Eds. LNCS, vol. 7086. Springer, Berlin, 330--345.
20. Brookes, S. D. 1993. Historical introduction to “Concrete Domains” by G. Kahn and G. D. Plotkin. Theor. Comput. Sci. 121, 1--2, 179--186.
21. Brooks Jr., F. P. 1995. The Mythical Man-Month—Essays on Software Engineering, 2nd ed. Addison-Wesley, Reading, MA.
22. Browning, S. and Weaver, P. 2010. Designing tunable, verifiable cryptographic hardware using Cryptol. In Design and Verification of Microprocessor Systems for High-Assurance Applications, D. S. Hardin, Ed. Springer, Berlin.
23. Broy, M. and Stølen, K. 2001. Specification and Development of Interactive Systems: FOCUS on Streams, Interfaces, and Refinement. Monographs in Computer Science. Springer, Berlin.
24. Brzozowski, J. A. and Seger, C.-J. 1995. Asynchronous Circuits. Springer, Berlin.
25. Burch, J. R., Dill, D. L., Wolf, E., and De Micheli, G. 1993. Modeling hierarchical combinational circuits. In Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design (ICCAD'93), M. R. Lightner and J. A. G. Jess, Eds. IEEE Computer Society, Washington, DC, 612--617.
26. Burstall, R. M. and Darlington, J. 1977. A transformation system for developing recursive programs. J. ACM 24, 1, 44--67.
27. Camilleri, A., Gordon, M., and Melham, T. 1986. Hardware verification using higher-order logic. Tech. rep. 91, Computer Laboratory, University of Cambridge.
28. Cardelli, L. 1982. An Algebraic Approach to Hardware Description and Verification. Ph.D. thesis, University of Edinburgh.
29. Cardelli, L. and Plotkin, G. D. 1981. An algebraic approach to VLSI design. In VLSI, J. P. Gray, Ed. Academic Press, New York.
30. Cardoso, J. M. P., Diniz, P. C., and Weinhardt, M. 2010. Compiling for reconfigurable computing: A survey. ACM Comput. Surv. 42, 4.
31. Carette, J., Kiselyov, O., and Shan, C. 2009. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. J. Funct. Program. 19, 5, 509--543.
32. Caspi, P. 1992. Clocks in dataflow languages. Theor. Comput. Sci. 94, 1, 125--140.
33. Caspi, P. and Pouzet, M. 1998. A co-iterative characterization of synchronous stream functions. Elec. Notes Theor. Comput. Sci. 11, 1--21.
34. Chakravarty, M. M. T., Keller, G., Lee, S., McDonell, T. L., and Grover, V. 2011. Accelerating Haskell array codes with multicore GPUs. In Proceedings of the Workshop on Declarative Aspects of Multicore Programming (DAMP'11), M. Carro and J. H. Reppy, Eds. ACM, New York, 3--14.
35. Chakravarty, M. M. T., Keller, G., Peyton Jones, S., and Marlow, S. 2005. Associated types with class. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05). ACM, New York.
36. Claessen, K. 2001. Embedded Languages for Describing and Verifying Hardware. Ph.D. thesis, Chalmers University of Technology.
37. Claessen, K. 2003. Safety property verification of cyclic synchronous circuits. In Proceedings of Workshop on Synchronous Languages Applications and Programs (SLAP'03). Elsevier, Amsterdam.
38. Claessen, K., Sheeran, M., and Singh, S. 2003. Using Lava to design and verify recursive and periodic sorters. Int. J. Software Tools Technol. Transfer 4, 3, 349--358.
39. Clarke, E., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press, Cambridge, MA.
40. Colaço, J.-L., Girault, A., Hamon, G., and Pouzet, M. 2004. Towards a higher-order synchronous dataflow language. In EMSOFT, G. C. Buttazzo, Ed. ACM, New York.
41. Coquand, T. 1993. Infinite objects in type theory. In Proceedings of the International Workshop on Types for Proofs and Programs (TYPES'93), H. Barendregt and T. Nipkow, Eds. LNCS, vol. 806. Springer, Berlin, 62--78.
42. Danielsson, N. A., Hughes, J., Jansson, P., and Gibbons, J. 2006. Fast and loose reasoning is morally correct. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'06), J. G. Morrisett and S. Peyton Jones, Eds. ACM, New York, 206--217.
43. Day, N. A., Aagaard, M., and Cook, B. 2000. Combining stream-based and state-based verification techniques. In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD'00), W. A. Hunt Jr. and S. D. Johnson, Eds. LNCS, vol. 1954. Springer, Berlin, 126--142.
44. de Roever, W.-P. and Engelhardt, K. 1998. Data Refinement: Model-Oriented Proof Methods and their Comparison. Number 47 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, U.K.
45. Diatchki, I. S., Jones, M. P., and Leslie, R. 2005. High-level views on low-level representations. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming (ICFP'05), O. Danvy and B. C. Pierce, Eds. ACM, New York, 168--179.
46. Erkök, L. 2002. Value Recursion in Monadic Computations. Ph.D. thesis, OGI School of Science and Engineering, OHSU, Portland, Oregon.
47. Fox, A. C. J., Gordon, M. J. C., and Myreen, M. O. 2010. Specification and verification of ARM hardware and software. In Design and Verification of Microprocessor Systems for High-Assurance Applications, D. S. Hardin, Ed. Springer, Berlin.
48. Frankau, S. and Mycroft, A. 2003. Stream processing hardware from functional language specifications. In Proceedings of the 36th Hawaii International Conference on System Sciences (HICSS'03). IEEE Computer Society, Washington, DC, 278.
49. Friedman, D. P. and Wise, D. S. 1976. CONS should not evaluate its arguments. In Proceedings of the 3rd International Colloquium on Automata, Languages and Programming (ICALP'76). Edinburgh University Press, Edinburgh, UK, 257--284.
50. Gammie, P. 2011. Short note: Strict unwraps make worker/wrapper fusion totally correct. J. Funct. Program. 21, 2, 209--213.
51. Ghica, D. R. 2007. Geometry of synthesis: A structured approach to VLSI design. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07), M. Hofmann and M. Felleisen, Eds. ACM, New York, 363--375.
52. Ghica, D. R., Smith, A., and Singh, S. 2011. Geometry of synthesis IV: Compiling affine recursion into static hardware. In Proceedings of the International Conference on Functional Programming (ICFP'11), M. M. T. Chakravarty, Z. Hu, and O. Danvy, Eds. ACM, New York, 221--233.
53. Gill, A. 2009. Type-safe observable sharing in Haskell. In Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell (Haskell'09), S. Weirich, Ed. ACM, New York.
54. Gill, A. and Farmer, A. 2011. Deriving an efficient FPGA implementation of a low density parity check forward error corrector. In Proceedings of the International Conference on Functional Programming (ICFP'11), M. M. T. Chakravarty, Z. Hu, and O. Danvy, Eds. ACM, New York, 209--220.
55. Gill, A. and Hutton, G. 2009. The worker/wrapper transformation. J. Funct. Program. 19, 2, 227--251.
56. Gillenwater, J., Malecha, G., Salama, C., Zhu, A. Y., Taha, W., Grundy, J., and O'Leary, J. 2010. Synthesizable high level hardware descriptions. New Generation Comput. 28, 4, 339--369.
57. Gordon, M. J. C. 1995. The semantic challenge of Verilog HDL. In Proceedings of the 10th IEEE Symposium on Logic in Computer Science (LICS'95). IEEE Computer Society, Washington, DC, 136--145.
58. Greibach, S. 1975. Theory of Program Structures: Schemes, Semantics, Verification. LNCS, vol. 36. Springer, Berlin.
59. Grov, G. and Michaelson, G. 2010. Hume box calculus: Robust system development through software transformation. Higher-Order and Symbolic Comput. 23, 2, 191--226.
60. Grundy, J., Melham, T. F., and O'Leary, J. W. 2006. A reflective functional language for hardware design and theorem proving. J. Funct. Program. 16, 2, 157--196.
61. Gunter, C. A. 1992. Semantics of Programming Languages: Structures and Techniques. MIT Press, Cambridge, MA.
62. Halbwachs, N., Caspi, P., Raymond, P., and Pilaud, D. 1991. The synchronous dataflow programming language Lustre. Proc. IEEE 79, 9, 1305--1320.
63. Halbwachs, N., Lagnier, F., and Raymond, P. 1993. Synchronous observers and the verification of reactive systems. In Algebraic Methodology and Software Technology (AMAST'93), M. Nivat, C. Rattray, T. Rus, and G. Scollo, Eds. Workshops in Computing. Springer, Berlin, 83--96.
64. Hamon, G. 2006. Synchronous dataflow pattern matching. Elec. Notes Theor. Comput. Sci. 153, 4, 37--54.
65. Hanna, F. K. 2000. Reasoning about analog-level implementations of digital systems. Formal Methods Syst. Des. 16, 2, 127--158.
66. Harel, D. 2009. Statecharts in the making: A personal account. Commun. ACM 52, 3, 67--75.
67. Harrison, W. L., Procter, A. M., Agron, J., Kimmell, G., and Allwein, G. 2009. Model-driven engineering from modular monadic semantics: Implementation techniques targeting hardware and software. In Proceedings of the IFIP TC 2 Working Conference on Domain-Specific Languages (DSL'09), W. Taha, Ed. LNCS, vol. 5658. Springer, Berlin.
68. Henderson, P. 1982. Functional geometry. In Proceedings of the 1982 ACM Symposium on LISP and Functional Programming (LFP'82). ACM, New York, 179--187.
69. Hinze, R. and James, D. W. H. 2011. Proving the unique fixed-point principle correct: an adventure with category theory. In Proceedings of the International Conference on Functional Programming (ICFP'11), M. M. T. Chakravarty, Z. Hu, and O. Danvy, Eds. ACM, New York, NY, 359--371.
70. Hudak, P. 1996. Building domain-specific embedded languages. ACM Comput. Surv. 28, 4es, 196.
71. Hughes, J. 1983. The Design and Implementation of Programming Languages. Ph.D. thesis, Programming Research Group, Oxford University.
72. Hughes, J. 1989. Why functional programming matters. Comput. J. 32, 2, 98--107.
73. Hughes, J. 2000. Generalising monads to arrows. Sci. Comput. Program. 37, 67--111.
74. Hughes, J., Pareto, L., and Sabry, A. 1996. Proving the correctness of reactive systems using sized types. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'96). ACM, New York, 410--423.
75. Hunt Jr., W. A., Swords, S., Davis, J., and Slobodova, A. 2010. Use of formal verification at Centaur Technology. In Design and Verification of Microprocessor Systems for High-Assurance Applications, D. S. Hardin, Ed. Springer, Berlin.
76. Jantsch, A. and Sander, I. 2005. Models of computation and languages for embedded system design. IEE Proc. Comput. Digital Tech. 152, 2, 114--129.
77. Johnson, S. D. 1983. Synthesis of Digital Designs from Recursion Equations. ACM Distinguished Dissertation Series. MIT Press, Cambridge, MA.
78. Johnson, S. D. 2001. View from the fringe of the fringe. In Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'01), T. Margaria and T. F. Melham, Eds. LNCS, vol. 2144. Springer, Berlin, 1--12.
79. Johnson, S. D. and Bose, B. 1997. DDD: A system for mechanized digital design derivation. Tech. rep. 323, Indiana University.
80. Jones, G. and Sheeran, M. 1993. Designing arithmetic circuits by refinement in Ruby. In Proceedings of the 2nd International Conference on Mathematics of Program Construction (MPC'93). Springer, Berlin, 208--232.
81. Jones, M. P. 2000. Type classes with functional dependencies. In Proceedings of the 9th European Symposium on Programming (ESOP'00), G. Smolka, Ed. LNCS, vol. 1782. Springer, Berlin, 230--244.
82. Kaes, S. 1988. Parametric overloading in polymorphic programming languages. In Proceedings of the 2nd European Symposium on Programming (ESOP'88), H. Ganzinger, Ed. LNCS, vol. 300. Springer, Berlin, 131--144.
83. Kahn, G. 1974. The semantics of a simple language for parallel programming. In Proceedings of IFIP Congress 1974 (Information Processing'74), J. L. Rosenfeld, Ed. North-Holland, Amsterdam.
84. Keller, G., Chakravarty, M. M. T., Leshchinskiy, R., Peyton Jones, S., and Lippmeier, B. 2010. Regular, shape-polymorphic, parallel arrays in Haskell. In ICFP, P. Hudak and S. Weirich, Eds. ACM, New York, 261--272.
85. Kiselyov, O. 2011. Implementing explicit and finding implicit sharing in embedded DSLs. In Proceedings of the IFIP Working Conference on Domain-Specific Languages (DSL'11), O. Danvy and C.-C. Shan, Eds. EPTCS, vol. 66, 210--225.
86. Kiselyov, O., Swadi, K. N., and Taha, W. 2004. A methodology for generating verified combinatorial circuits. In Proceedings of the International Conference on Embedded Software (EMSOFT'04), G. C. Buttazzo, Ed. ACM, New York.
87. Kloos, C. D. 1987. Semantics of Digital Circuits. LNCS, vol. 285. Springer, Berlin.
88. Landin, P. J. 1966. The next 700 programming languages. Commun. ACM 9, 3, 157--166.
89. Launchbury, J., Lewis, J. R., and Cook, B. 1999. On embedding a microarchitectural design language within Haskell. In Proceedings of the 4th International Conference on Functional Programming (ICFP'99). ACM, New York, 60--69.
90. Lewis, J. R., Launchbury, J., Meijer, E., and Shields, M. 2000. Implicit parameters: Dynamic scoping with static types. In Proceedings of the 27th ACM SIGPLAN-SIGACT on Principles of Programming Languages (POPL'00). ACM, New York, 108--118.
91. Malik, S. 1993. Analysis of cyclic combinational circuits. In Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design (ICCAD'93). IEEE Computer Society, Washington, DC, 618--625.
92. Manna, Z. 1974. Introduction to Mathematical Theory of Computation. McGraw-Hill, New York.
93. Manna, Z. and Pnueli, A. 1992. The Temporal Logic of Reactive and Concurrent Systems. Springer, Berlin.
94. Maraninchi, F. and Halbwachs, N. 1996. Compositional semantics of non-deterministic synchronous languages. In Proceedings of the 6th European Symposium on Programming (ESOP'96), H. R. Nielson, Ed. LNCS, vol. 1058. Springer, Berlin, 235--249.
95. Maraninchi, F. and Rémond, Y. 2001. Argos: An automaton-based synchronous language. Comput. Lang. 27, 1/3, 61--92.
96. Matthews, J. 1999. Recursive function definition over coinductive types. In Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'99), Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, Eds. LNCS, vol. 1690. Springer, Berlin, 73--90.
97. Matthews, J. 2000. Algebraic Specification and Verification of Processor Microarchitectures. Ph.D. thesis, Oregon Graduate Institute of Science and Technology.
98. Matthews, J., Cook, B., and Launchbury, J. 1998. Microprocessor specification in Hawk. In Proceedings of the 1998 International Conference on Computer Languages (ICCL'98). IEEE Computer Society, Washington, DC, 90.
99. McBride, C. and Paterson, R. 2008. Applicative programming with effects. J. Funct. Program. 18, 1, 1--13.
100. McEvoy, K. and Tucker, J. V. 1990. Theoretical foundations of hardware design. Number 10 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK, Chapter 1.
101. Mead, C. and Conway, L. 1980. Introduction to VLSI systems. Addison-Wesley, Reading, MA.
102. Meertens, L. G. L. T. 1986. Algorithmics. In Towards programming as a mathematical activity. Mathematics and Computer Science, CWI monographs, vol. 1. North-Holland, 289--334.
103. Megacz, A. 2011. Hardware design with generalized arrows. In Proceedings of the 23rd International Symposium on the Implementation and Application of Functional Languages (IFL'11), A. Gill and J. Hage, Eds. LNCS, vol. 7257. Springer, Berlin, 164--180.
104. Meijer, E., Fokkinga, M. M., and Paterson, R. 1991. Functional programming with bananas, lenses, envelopes and barbed wire. In Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA'91), J. Hughes, Ed. LNCS, vol. 523. Springer, Berlin, 124--144.
105. Mendler, M., Shiple, T. R., and Berry, G. 2012. Constructive Boolean circuits and the exactness of timed ternary simulation. Formal Methods Syst. Des.i. 40, 3, 283--329.
106. Mernik, M., Heering, J., and Sloane, A. M. 2005. When and how to develop domain-specific languages. ACM Comput. Surv. 37, 4, 316--344.
107. Milne, G. J. 1985. CIRCAL and the representation of communication, concurrency, and time. ACM Trans. Program. Lang. Syst. 7, 2, 270--298.
108. Milne, G. J. 2006. Modelling dynamically changing hardware structure. Elec. Notes Theor. Comput. Sci. 162, 249--254.
109. Milner, R. 1983. Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25, 267--310.
110. Milner, R. 1989. Communication and Concurrency. Prentice-Hall, Englewood Cliffs, NJ.
111. Möller, B. and Tucker, J. V., Eds. 1998. Prospects for Hardware Foundations, ESPRIT Working Group 8533, NADA - New Hardware Design Methods, Survey Chapters. LNCS, vol. 1546. Springer, Berlin.
112. Moran, A. K. 1998. Call-by-Name, Call-by-Need and McCarthy's Amb. Ph.D. thesis, Department of Computing Science, Chalmers University of Technology.
113. Mycroft, A. and Sharp, R. 2003. Higher-level techniques for hardware description and synthesis. Int. J. Software Tools Technol. Transfer 4, 3, 271--297.
114. Naylor, M. and Runciman, C. 2009. Expressible sharing for functional circuit description. Higher-Order Symb. Comput. 22, 1, 67--80.
115. Naylor, M. and Runciman, C. 2012. The Reduceron reconfigured and re-evaluated. J. Funct. Program. 22, 4--5, 574--613.
116. Neiroukh, O., Edwards, S. A., and Song, X. 2008. Transforming cyclic circuits into acyclic equivalents. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27, 10, 1775--1787.
117. Nikhil, R. S. 2011. Abstraction in hardware system design. Commun. ACM 54, 10, 36--44.
118. Nipkow, T., Paulson, L. C., and Wenzel, M. 2002. Isabelle/HOL—A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin.
119. O'Donnell, J. 1987. Hardware description with recursion equations. In Proceedings of the IFIP 8th International Symposium on Computer Hardware Description Languages and Their Applications.
120. O'Donnell, J. 1992. Generating netlists from executable circuit specifications. In Proceedings of the 1992 Glasgow Workshop on Functional Programming (Functional Programming'92), J. Launchbury and P. M. Sansom, Eds. Workshops in Computing. Springer, Berlin, 178--194.
121. O'Donnell, J. 1995. From transistors to computer architecture: Teaching functional circuit specification in Hydra. In Proceedings of 1st International Symposium on Functional Programming Languages in Education (FPLE'95), P. H. Hartel and M. J. Plasmeijer, Eds. LNCS, vol. 1022. Springer, Berlin, 195--214.
122. O'Donnell, J. 2003. Embedding a hardware description language in template Haskell. In Domain-Specific Program Generation, C. Lengauer, D. S. Batory, C. Consel, and M. Odersky, Eds. LNCS, vol. 3016. Springer, Berlin, 143--164.
123. O'Donnell, J. and Rünger, G. 2004. Derivation of a logarithmic time carry lookahead addition circuit. J. Funct. Program. 14, 6, 697--713.
124. Park, S. and Im, H. 2011. A calculus for hardware description. J. Funct. Program. 21, 1, 21--58.
125. Paterson, R. 2001. A new notation for Arrows. In Proceedings of the 6th ACM SIGPLAN International Conference on Functional Programming (ICFP'01). ACM, New York, NY, 229--240.
126. Paterson, R. 2003. Arrows and Computation. In The Fun of Programming, J. Gibbons and O. de Moor, Eds. Cornerstones in Computing. Palgrave Macmillan, New York, 201--222.
127. Paulin-Mohring, C. 1995. Circuits as streams in Coq: Verification of a sequential multiplier. In International Workshop on Types for Proofs and Programs (TYPES'95), S. Berardi and M. Coppo, Eds. LNCS, vol. 1158. Springer, Berlin, 216--230.
128. Peyton Jones, S. 1987. The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs, NJ.
129. Peyton Jones, S., Ed. 2003. Haskell 98 Language and Libraries: the Revised Report. Cambridge University Press, Cambridge, U.K.
130. Peyton Jones, S., Vytiniotis, D., Weirich, S., and Shields, M. 2007. Practical type inference for arbitrary-rank types. J. Funct. Program. 17, 1, 1--82.
131. Plotkin, G. D. 1977. LCF considered as a programming language. Theor. Comput. Sci. 5, 223--255.
132. Potop-Butucaru, D., Edwards, S. A., and Berry, G. 2007. Compiling Esterel. Springer, Berlin.
133. Riedel, M. D. and Bruck, J. 2003. The synthesis of cyclic combinational circuits. In Proceedings of the 40th Design Automation Conference (DAC'03). ACM, New York, 163--168.
134. Rocheteau, F. and Halbwachs, N. 1991. POLLUX: A Lustre based hardware design environment. In Algorithms and Parallel VLSI Architectures, P. Quinton and Y. Robert, Eds. Elsevier, Amsterdam, 335--346.
135. Seger, C.-J. H., Jones, R. B., O'Leary, J. W., Melham, T. F., Aagaard, M., Barrett, C., and Syme, D. 2005. An industrially effective environment for formal hardware verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24, 9, 1381--1405.
136. Selinger, P. 2011. A survey of graphical languages for monoidal categories. In New Structures for Physics, B. Coecke, Ed. Lecture Notes in Physics, vol. 813. Springer, Berlin.
137. Sharp, R. and Rasmussen, O. 1997. The T-Ruby design system. Formal Methods in System Design 11, 3, 239--264.
138. Sheard, T. 2007. Types and hardware description languages. In Hardware Design and Functional Languages, A. Martin, C. Seger, and M. Sheeran, Eds.
139. Sheard, T. and Peyton Jones, S. 2002. Template metaprogramming for Haskell. In Proceedings of the 2002 Haskell Workshop (Haskell 2002), M. M. T. Chakravarty, Ed. ACM, New York, 1--16.
140. Sheeran, M. 1984. μFP, a language for VLSI design. In Proceedings of the 1984 ACM Symposium on LISP and Functional Programming (LFP'84). ACM, New York, 104--112.
141. Sheeran, M. 1990. Describing and reasoning about circuits using relations. Number 10 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK, Chapter 6.
142. Sheeran, M. 2005. Hardware design and functional programming: a perfect match. J. Universal Comput. Sci. 11, 7, 1135--1158.
143. Sheeran, M. 2011. Functional and dynamic programming in the design of parallel prefix networks. J. Funct. Program. 21, 1, 59--114.
144. Shiple, T. R., Berry, G., and Touati, H. 1996. Constructive analysis of cyclic circuits. In Proceedings of the 1996 European Conference on Design and Test (EDTC'96). IEEE Computer Society, Washington, DC.
145. Singh, S. 2004. Designing reconfigurable systems in Lava. In Proceedings of the 17th International Conference on VLSI Design (VLSI Design'04). IEEE Computer Society, Washington, DC, 299--306.
146. Singh, S. 2007. New parallel programming techniques for hardware design. In Proceedings of the IFIP WG 10.5 International Conference on Very Large Scale Integration of System-on-Chip (IFIP VLSI-SoC'07). IEEE, Los Alamitos, CA, 163--167.
147. Singh, S. 2011. The RLOC is dead -- long live the RLOC. In Proceedings of the ACM/SIGDA 19th International Symposium on Field Programmable Gate Arrays (FPGA'11), J. Wawrzynek and K. Compton, Eds. ACM, New York, 185--188.
148. Singh, S. and James-Roxby, P. 2001. Lava and JBits: From HDL to bitstream in seconds. In Proceedings of the the 9th IEEE Symposium on Field-Programmable Custom Computing Machines (FCCM'01). IEEE Computer Society, Washington, DC, 91--100.
149. Stavridou, V. 1993. Formal Methods in Circuit Design. Number 37 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, U.K.
150. Stavridou, V. 1994. Gordon's computer: A hardware verification case study in OBJ3. Formal Methods Syst. Des. 4, 3, 265--310.
151. Sweeney, T. 2009. The end of the GPU roadmap. Keynote at High Performance Graphics.
152. Taha, W. 2000. A sound reduction semantics for untyped CBN multi-stage computation. or, the theory of MetaML is non-trivial (extended abstract). In Proceedings of the 2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'00). ACM, New York, 34--43.
153. Veldhuizen, T. L. 2004. Active Libraries and Universal Languages. Ph.D. thesis, Indiana University Computer Science.
154. Vuillemin, J. 1994. On circuits and numbers. IEEE Trans. Comput. 43, 8, 868--879.
155. Wadler, P. 1990. Deforestation: Transforming programs to eliminate trees. Theor. Comput. Sci. 73, 2, 231--248.
156. Wadler, P. 1997. How to declare an imperative. ACM Comput. Surv. 29, 3, 240--263.
157. Wadler, P. and Blott, S. 1989. How to make ad-hoc polymorphism less ad-hoc. In Proceedings of the 16th ACM Symposium on Principles of Programming Languages (POPL'89). ACM, New York, 60--76.
158. Wand, M. 1982. Deriving target code as a representation of continuation semantics. ACM Trans. Program. Lang. Syst. 4, 3, 496--517.
159. Winskel, G. 1986. Lectures on models and logic of MOS circuits. In Logic of Programming and Calculi of Discrete Design, M. Broy, Ed. NATO ASI Series F, vol. 36. Springer, Berlin.
160. Winskel, G. 1993. The Formal Semantics of Programming Languages. MIT Press, Cambridge, MA.

Index Terms

• General and reference

  • Document types

    • Surveys and overviews

• Hardware

  • Electronic design automation

    • Hardware description languages and compilation

    • High-level and register-transfer level synthesis

    • Physical design (EDA)

      • Partitioning and floorplanning

  • Hardware validation

    • Functional verification

      • Simulation and emulation

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Functional languages