From: Christiaan Baaij Date: Wed, 27 Jan 2010 09:25:45 +0000 (+0100) Subject: Use lhs2tex for code and verbatim formatting X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Fdsd-paper.git;a=commitdiff_plain;h=d761eaf56b88d9a83aa096d23e12bb4d724d4c3f Use lhs2tex for code and verbatim formatting --- diff --git a/Makefile b/Makefile index 4271429..f372234 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,5 @@ all: + lhs2TeX -v --poly --haskell < cλash.lhs > cλash.tex latexmk -pdf -pv cλash.tex clean: diff --git a/clash.bib b/clash.bib new file mode 100644 index 0000000..dc49b3b --- /dev/null +++ b/clash.bib @@ -0,0 +1,305 @@ +% This file was created with JabRef 2.4.2. +% Encoding: MacRoman + +@INPROCEEDINGS{Wired, + author = {Emil Axelsson and Koen Claessen and Mary Sheeran}, + title = {{Wired: Wire-Aware Circuit Design}}, + booktitle = {{Proceedings of Conference on Correct Hardware Design and VeriÞcation + Methods (CHARME)}}, + year = {2005}, + volume = {3725}, + series = {{Lecture Notes in Computer Science}}, + pages = {{5--19}}, + publisher = {Springer Verlag}, + owner = {darchon}, + timestamp = {2010.01.21} +} + +@INPROCEEDINGS{Lava, + author = {Bjesse, Per and Claessen, Koen and Sheeran, Mary and Singh, Satnam}, + title = {{Lava: hardware design in Haskell}}, + booktitle = {{ICFP '98: Proceedings of the third ACM SIGPLAN international conference + on Functional programming}}, + year = {1998}, + pages = {174--184}, + address = {New York, NY, USA}, + publisher = {ACM}, + doi = {http://doi.acm.org/10.1145/289423.289440}, + isbn = {1-58113-024-4}, + location = {Baltimore, Maryland, United States}, + owner = {darchon}, + timestamp = {2010.01.20} +} + +@INPROCEEDINGS{Cardelli1981, + author = {Luca Cardelli and Gordon Plotkin}, + title = {{An Algebraic Approach to VLSI Design}}, + booktitle = {{Proceedings of the VLSI 81 International Conference}}, + year = {1981}, + pages = {173-182}, + owner = {darchon}, + timestamp = {2010.01.25} +} + +@INPROCEEDINGS{Hawk2, + author = {Byron Cook and John Launchbury and John Matthews}, + title = {{Specifying superscalar microprocessors in Hawk}}, + booktitle = {{Formal Techniques for Hardware and Hardware-like Systems}}, + year = {1998}, + owner = {darchon}, + timestamp = {2010.01.20} +} + +@ARTICLE{reFLect, + author = {Grundy,Jim and Melham,Tom and O'Leary,John}, + title = {{A reflective functional language for hardware design and theorem + proving}}, + journal = {Journal of Functional Programming}, + year = {2006}, + volume = {16}, + pages = {157-196}, + number = {02}, + doi = {10.1017/S0956796805005757}, + owner = {darchon}, + timestamp = {2010.01.21} +} + +@INPROCEEDINGS{DAISY, + author = {Johnson, Steven D.}, + title = {Applicative programming and digital design}, + booktitle = {POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on + Principles of programming languages}, + year = {1984}, + pages = {218--227}, + address = {New York, NY, USA}, + publisher = {ACM}, + doi = {http://doi.acm.org/10.1145/800017.800533}, + isbn = {0-89791-125-3}, + location = {Salt Lake City, Utah, United States}, + owner = {darchon}, + timestamp = {2010.01.25} +} + +@INPROCEEDINGS{Ruby, + author = {Jones, G. and Sheeran, M.}, + title = {{Circuit Design in Ruby}}, + booktitle = {{Formal Methods for VLSI Design}}, + year = {1990}, + address = {Lyngby, Denmark}, + publisher = {Elsevier Science Publishers}, + citeulike-article-id = {304676}, + journal = {Circuit Design in Ruby}, + keywords = {jones90}, + owner = {darchon}, + posted-at = {2005-08-26 18:08:07}, + priority = {0}, + timestamp = {2010.01.20} +} + +@ARTICLE{HML2, + author = {Yanbing Li and Leeser, M.}, + title = {{HML, a novel hardware description language and its translation to + VHDL}}, + journal = {{Very Large Scale Integration (VLSI) Systems, IEEE Transactions on}}, + year = {2000}, + volume = {8}, + pages = {1-8}, + number = {1}, + month = {Feb}, + doi = {10.1109/92.820756}, + issn = {1063-8210}, + keywords = {ML language, hardware description languages, type theoryHML, SML functional + programming language, VHDL translation, digital design, hardware + description language, polymorphic type, translator, type checker, + type inference}, + owner = {darchon}, + timestamp = {2010.01.20} +} + +@INPROCEEDINGS{HML1, + author = {Yanbing Li and Leeser, M.}, + title = {{HML: an innovative hardware description language and its translation + to VHDL}}, + booktitle = {{Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL + '95/VLSI '95., IFIP International Conference on Hardware Description + Languages; IFIP International Conference on Very Large Scale Integration., + Asian and South Pacific}}, + year = {1995}, + pages = {691-696}, + month = {Aug-1 Sep}, + doi = {10.1109/ASPDAC.1995.486388}, + keywords = {abstract data types, functional languages, functional programming, + hardware description languagesHML, VHDL, advanced type checking, + functional programming language, hardware description language, polymorphic + types, type inference}, + owner = {darchon}, + timestamp = {2010.01.20} +} + +@INPROCEEDINGS{FL, + author = {{Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Seger}}, + title = {{Lifted-FL: A Pragmatic Implementation of Combined Model Checking + and Theorem Proving}}, + booktitle = {{Proceedings of 12th International Conference on Theorem Proving + in Higher Order Logics}}, + year = {1999}, + volume = {1690}, + series = {LNCS}, + pages = {323-340}, + publisher = {Springer Verlag}, + owner = {darchon}, + timestamp = {2010.01.26} +} + +@INPROCEEDINGS{Hawk1, + author = {Matthews, J. and Cook, B. and Launchbury, J.}, + title = {{Microprocessor specification in Hawk}}, + booktitle = {{Proceedings of 1998 International Conference on Computer Languages}}, + year = {1998}, + pages = {90-101}, + month = {May}, + abstract = {Modern microprocessors require an immense investment of time and effort + to create and verify, from the high level architectural design downwards. + We are exploring ways to increase the productivity of design engineers + by creating a domain specific language for specifying and simulating + processor architectures. We believe that the structuring principles + used in modern functional programming languages, such as static typing, + parametric polymorphism, first class functions, and lazy evaluation + provide a good formalism for such a domain specific language, and + have made initial progress by creating a library on top of the functional + language Haskell. We have specified the integer subset of an out + of order, superscalar DLX microprocessor, with register renaming, + a reorder buffer, a global reservation station, multiple execution + units, and speculative branch execution. Two key abstractions of + this library are the signal abstract data type (ADT), which models + the simulation history of a wire, and the transaction ADT, which + models the state of an entire instruction as it travels through the + microprocessor}, + doi = {10.1109/ICCL.1998.674160}, + issn = {1074-8970}, + keywords = {abstract data types, formal specification, functional languages, functional + programming, hardware description languages, microprocessor chips, + software librariesHawk language, design engineers, domain specific + language, first class functions, functional language Haskell, functional + programming languages, global reservation station, high level architectural + design, integer subset, lazy evaluation, microprocessor specification, + multiple execution units, out of order superscalar DLX microprocessor, + parametric polymorphism, processor architecture simulation, register + renaming, reorder buffer, signal abstract data type, simulation history, + software library, speculative branch execution, static typing,, structuring + principles, transaction ADT}, + owner = {darchon}, + timestamp = {2010.01.20} +} + +@INPROCEEDINGS{FHDL, + author = {Meshkinpour, F. and Ercegovac, M. D.}, + title = {A functional language for description and design of digital systems: + sequential constructs}, + booktitle = {DAC '85: Proceedings of the 22nd ACM/IEEE Design Automation Conference}, + year = {1985}, + pages = {238--244}, + address = {New York, NY, USA}, + publisher = {ACM}, + doi = {http://doi.acm.org/10.1145/317825.317865}, + isbn = {0-8186-0635-5}, + location = {Las Vegas, Nevada, United States}, + owner = {darchon}, + timestamp = {2010.01.25} +} + +@INPROCEEDINGS{Hydra, + author = {John O'Donnell}, + title = {{From Transistors to Computer Architecture: Teaching Functional Circuit + Specification in Hydra}}, + booktitle = {{Proceedings of the First International Symposium on Funtional Programming + Languages in Education}}, + year = {1995}, + volume = {1022}, + series = {Lecture Notes in Computer Science}, + pages = {195--214}, + publisher = {Springer-Verlag}, + owner = {darchon}, + timestamp = {2010.01.21} +} + +@ARTICLE{ForSyDe2, + author = {Ingo Sander and Axel Jantsch}, + title = {{System Modeling and Transformational Design Refinement in ForSyDe}}, + journal = {{IEEE Transactions on Computer-Aided Design of Integrated Circuits + and Systems}}, + year = {2004}, + volume = {23}, + pages = {17--32}, + number = {1}, + month = {January}, + key = {ForSyDe}, + owner = {darchon}, + timestamp = {2010.01.21} +} + +@INPROCEEDINGS{ForSyDe1, + author = {Sander, Ingo and Jantsch, Axel}, + title = {{Transformation based communication and clock domain refinement for + system design}}, + booktitle = {{DAC '02: Proceedings of the 39th annual Design Automation Conference}}, + year = {2002}, + pages = {281--286}, + address = {New York, NY, USA}, + publisher = {ACM}, + doi = {http://doi.acm.org/10.1145/513918.513992}, + isbn = {1-58113-461-4}, + location = {New Orleans, Louisiana, USA}, + owner = {darchon}, + timestamp = {2010.01.20} +} + +@INPROCEEDINGS{T-Ruby, + author = {Sharp, Robin and Rasmussen, Ole}, + title = {{Using a language of functions and relations for VLSI specification}}, + booktitle = {FPCA '95: Proceedings of the seventh international conference on + Functional programming languages and computer architecture}, + year = {1995}, + pages = {45--54}, + address = {New York, NY, USA}, + publisher = {ACM}, + doi = {http://doi.acm.org/10.1145/224164.224180}, + isbn = {0-89791-719-7}, + location = {La Jolla, California, United States}, + owner = {darchon}, + timestamp = {2010.01.21} +} + +@INPROCEEDINGS{muFP, + author = {Sheeran, Mary}, + title = {{$\mu$FP, a language for VLSI design}}, + booktitle = {{LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional + programming}}, + year = {1984}, + pages = {104--112}, + address = {New York, NY, USA}, + publisher = {ACM}, + doi = {http://doi.acm.org/10.1145/800055.802026}, + isbn = {0-89791-142-3}, + location = {Austin, Texas, United States}, + owner = {darchon}, + timestamp = {2010.01.20} +} + +@STANDARD{VHDL2008, + title = {{VHDL Language Reference Manual}}, + organization = {IEEE}, + number = {1076-2008}, + year = {2008}, + owner = {darchon}, + timestamp = {2009.11.17} +} + +@comment{jabref-meta: selector_journal:} + +@comment{jabref-meta: selector_author:} + +@comment{jabref-meta: selector_keywords:} + +@comment{jabref-meta: selector_publisher:} + diff --git "a/c\316\273ash.bib" "b/c\316\273ash.bib" deleted file mode 100644 index dc49b3b..0000000 --- "a/c\316\273ash.bib" +++ /dev/null @@ -1,305 +0,0 @@ -% This file was created with JabRef 2.4.2. -% Encoding: MacRoman - -@INPROCEEDINGS{Wired, - author = {Emil Axelsson and Koen Claessen and Mary Sheeran}, - title = {{Wired: Wire-Aware Circuit Design}}, - booktitle = {{Proceedings of Conference on Correct Hardware Design and VeriÞcation - Methods (CHARME)}}, - year = {2005}, - volume = {3725}, - series = {{Lecture Notes in Computer Science}}, - pages = {{5--19}}, - publisher = {Springer Verlag}, - owner = {darchon}, - timestamp = {2010.01.21} -} - -@INPROCEEDINGS{Lava, - author = {Bjesse, Per and Claessen, Koen and Sheeran, Mary and Singh, Satnam}, - title = {{Lava: hardware design in Haskell}}, - booktitle = {{ICFP '98: Proceedings of the third ACM SIGPLAN international conference - on Functional programming}}, - year = {1998}, - pages = {174--184}, - address = {New York, NY, USA}, - publisher = {ACM}, - doi = {http://doi.acm.org/10.1145/289423.289440}, - isbn = {1-58113-024-4}, - location = {Baltimore, Maryland, United States}, - owner = {darchon}, - timestamp = {2010.01.20} -} - -@INPROCEEDINGS{Cardelli1981, - author = {Luca Cardelli and Gordon Plotkin}, - title = {{An Algebraic Approach to VLSI Design}}, - booktitle = {{Proceedings of the VLSI 81 International Conference}}, - year = {1981}, - pages = {173-182}, - owner = {darchon}, - timestamp = {2010.01.25} -} - -@INPROCEEDINGS{Hawk2, - author = {Byron Cook and John Launchbury and John Matthews}, - title = {{Specifying superscalar microprocessors in Hawk}}, - booktitle = {{Formal Techniques for Hardware and Hardware-like Systems}}, - year = {1998}, - owner = {darchon}, - timestamp = {2010.01.20} -} - -@ARTICLE{reFLect, - author = {Grundy,Jim and Melham,Tom and O'Leary,John}, - title = {{A reflective functional language for hardware design and theorem - proving}}, - journal = {Journal of Functional Programming}, - year = {2006}, - volume = {16}, - pages = {157-196}, - number = {02}, - doi = {10.1017/S0956796805005757}, - owner = {darchon}, - timestamp = {2010.01.21} -} - -@INPROCEEDINGS{DAISY, - author = {Johnson, Steven D.}, - title = {Applicative programming and digital design}, - booktitle = {POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on - Principles of programming languages}, - year = {1984}, - pages = {218--227}, - address = {New York, NY, USA}, - publisher = {ACM}, - doi = {http://doi.acm.org/10.1145/800017.800533}, - isbn = {0-89791-125-3}, - location = {Salt Lake City, Utah, United States}, - owner = {darchon}, - timestamp = {2010.01.25} -} - -@INPROCEEDINGS{Ruby, - author = {Jones, G. and Sheeran, M.}, - title = {{Circuit Design in Ruby}}, - booktitle = {{Formal Methods for VLSI Design}}, - year = {1990}, - address = {Lyngby, Denmark}, - publisher = {Elsevier Science Publishers}, - citeulike-article-id = {304676}, - journal = {Circuit Design in Ruby}, - keywords = {jones90}, - owner = {darchon}, - posted-at = {2005-08-26 18:08:07}, - priority = {0}, - timestamp = {2010.01.20} -} - -@ARTICLE{HML2, - author = {Yanbing Li and Leeser, M.}, - title = {{HML, a novel hardware description language and its translation to - VHDL}}, - journal = {{Very Large Scale Integration (VLSI) Systems, IEEE Transactions on}}, - year = {2000}, - volume = {8}, - pages = {1-8}, - number = {1}, - month = {Feb}, - doi = {10.1109/92.820756}, - issn = {1063-8210}, - keywords = {ML language, hardware description languages, type theoryHML, SML functional - programming language, VHDL translation, digital design, hardware - description language, polymorphic type, translator, type checker, - type inference}, - owner = {darchon}, - timestamp = {2010.01.20} -} - -@INPROCEEDINGS{HML1, - author = {Yanbing Li and Leeser, M.}, - title = {{HML: an innovative hardware description language and its translation - to VHDL}}, - booktitle = {{Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL - '95/VLSI '95., IFIP International Conference on Hardware Description - Languages; IFIP International Conference on Very Large Scale Integration., - Asian and South Pacific}}, - year = {1995}, - pages = {691-696}, - month = {Aug-1 Sep}, - doi = {10.1109/ASPDAC.1995.486388}, - keywords = {abstract data types, functional languages, functional programming, - hardware description languagesHML, VHDL, advanced type checking, - functional programming language, hardware description language, polymorphic - types, type inference}, - owner = {darchon}, - timestamp = {2010.01.20} -} - -@INPROCEEDINGS{FL, - author = {{Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Seger}}, - title = {{Lifted-FL: A Pragmatic Implementation of Combined Model Checking - and Theorem Proving}}, - booktitle = {{Proceedings of 12th International Conference on Theorem Proving - in Higher Order Logics}}, - year = {1999}, - volume = {1690}, - series = {LNCS}, - pages = {323-340}, - publisher = {Springer Verlag}, - owner = {darchon}, - timestamp = {2010.01.26} -} - -@INPROCEEDINGS{Hawk1, - author = {Matthews, J. and Cook, B. and Launchbury, J.}, - title = {{Microprocessor specification in Hawk}}, - booktitle = {{Proceedings of 1998 International Conference on Computer Languages}}, - year = {1998}, - pages = {90-101}, - month = {May}, - abstract = {Modern microprocessors require an immense investment of time and effort - to create and verify, from the high level architectural design downwards. - We are exploring ways to increase the productivity of design engineers - by creating a domain specific language for specifying and simulating - processor architectures. We believe that the structuring principles - used in modern functional programming languages, such as static typing, - parametric polymorphism, first class functions, and lazy evaluation - provide a good formalism for such a domain specific language, and - have made initial progress by creating a library on top of the functional - language Haskell. We have specified the integer subset of an out - of order, superscalar DLX microprocessor, with register renaming, - a reorder buffer, a global reservation station, multiple execution - units, and speculative branch execution. Two key abstractions of - this library are the signal abstract data type (ADT), which models - the simulation history of a wire, and the transaction ADT, which - models the state of an entire instruction as it travels through the - microprocessor}, - doi = {10.1109/ICCL.1998.674160}, - issn = {1074-8970}, - keywords = {abstract data types, formal specification, functional languages, functional - programming, hardware description languages, microprocessor chips, - software librariesHawk language, design engineers, domain specific - language, first class functions, functional language Haskell, functional - programming languages, global reservation station, high level architectural - design, integer subset, lazy evaluation, microprocessor specification, - multiple execution units, out of order superscalar DLX microprocessor, - parametric polymorphism, processor architecture simulation, register - renaming, reorder buffer, signal abstract data type, simulation history, - software library, speculative branch execution, static typing,, structuring - principles, transaction ADT}, - owner = {darchon}, - timestamp = {2010.01.20} -} - -@INPROCEEDINGS{FHDL, - author = {Meshkinpour, F. and Ercegovac, M. D.}, - title = {A functional language for description and design of digital systems: - sequential constructs}, - booktitle = {DAC '85: Proceedings of the 22nd ACM/IEEE Design Automation Conference}, - year = {1985}, - pages = {238--244}, - address = {New York, NY, USA}, - publisher = {ACM}, - doi = {http://doi.acm.org/10.1145/317825.317865}, - isbn = {0-8186-0635-5}, - location = {Las Vegas, Nevada, United States}, - owner = {darchon}, - timestamp = {2010.01.25} -} - -@INPROCEEDINGS{Hydra, - author = {John O'Donnell}, - title = {{From Transistors to Computer Architecture: Teaching Functional Circuit - Specification in Hydra}}, - booktitle = {{Proceedings of the First International Symposium on Funtional Programming - Languages in Education}}, - year = {1995}, - volume = {1022}, - series = {Lecture Notes in Computer Science}, - pages = {195--214}, - publisher = {Springer-Verlag}, - owner = {darchon}, - timestamp = {2010.01.21} -} - -@ARTICLE{ForSyDe2, - author = {Ingo Sander and Axel Jantsch}, - title = {{System Modeling and Transformational Design Refinement in ForSyDe}}, - journal = {{IEEE Transactions on Computer-Aided Design of Integrated Circuits - and Systems}}, - year = {2004}, - volume = {23}, - pages = {17--32}, - number = {1}, - month = {January}, - key = {ForSyDe}, - owner = {darchon}, - timestamp = {2010.01.21} -} - -@INPROCEEDINGS{ForSyDe1, - author = {Sander, Ingo and Jantsch, Axel}, - title = {{Transformation based communication and clock domain refinement for - system design}}, - booktitle = {{DAC '02: Proceedings of the 39th annual Design Automation Conference}}, - year = {2002}, - pages = {281--286}, - address = {New York, NY, USA}, - publisher = {ACM}, - doi = {http://doi.acm.org/10.1145/513918.513992}, - isbn = {1-58113-461-4}, - location = {New Orleans, Louisiana, USA}, - owner = {darchon}, - timestamp = {2010.01.20} -} - -@INPROCEEDINGS{T-Ruby, - author = {Sharp, Robin and Rasmussen, Ole}, - title = {{Using a language of functions and relations for VLSI specification}}, - booktitle = {FPCA '95: Proceedings of the seventh international conference on - Functional programming languages and computer architecture}, - year = {1995}, - pages = {45--54}, - address = {New York, NY, USA}, - publisher = {ACM}, - doi = {http://doi.acm.org/10.1145/224164.224180}, - isbn = {0-89791-719-7}, - location = {La Jolla, California, United States}, - owner = {darchon}, - timestamp = {2010.01.21} -} - -@INPROCEEDINGS{muFP, - author = {Sheeran, Mary}, - title = {{$\mu$FP, a language for VLSI design}}, - booktitle = {{LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional - programming}}, - year = {1984}, - pages = {104--112}, - address = {New York, NY, USA}, - publisher = {ACM}, - doi = {http://doi.acm.org/10.1145/800055.802026}, - isbn = {0-89791-142-3}, - location = {Austin, Texas, United States}, - owner = {darchon}, - timestamp = {2010.01.20} -} - -@STANDARD{VHDL2008, - title = {{VHDL Language Reference Manual}}, - organization = {IEEE}, - number = {1076-2008}, - year = {2008}, - owner = {darchon}, - timestamp = {2009.11.17} -} - -@comment{jabref-meta: selector_journal:} - -@comment{jabref-meta: selector_author:} - -@comment{jabref-meta: selector_keywords:} - -@comment{jabref-meta: selector_publisher:} - diff --git "a/c\316\273ash.lhs" "b/c\316\273ash.lhs" new file mode 100644 index 0000000..58caa4b --- /dev/null +++ "b/c\316\273ash.lhs" @@ -0,0 +1,946 @@ + +%% bare_conf.tex +%% V1.3 +%% 2007/01/11 +%% by Michael Shell +%% See: +%% http://www.michaelshell.org/ +%% for current contact information. +%% +%% This is a skeleton file demonstrating the use of IEEEtran.cls +%% (requires IEEEtran.cls version 1.7 or later) with an IEEE conference paper. +%% +%% Support sites: +%% http://www.michaelshell.org/tex/ieeetran/ +%% http://www.ctan.org/tex-archive/macros/latex/contrib/IEEEtran/ +%% and +%% http://www.ieee.org/ + +%%************************************************************************* +%% Legal Notice: +%% This code is offered as-is without any warranty either expressed or +%% implied; without even the implied warranty of MERCHANTABILITY or +%% FITNESS FOR A PARTICULAR PURPOSE! +%% User assumes all risk. +%% In no event shall IEEE or any contributor to this code be liable for +%% any damages or losses, including, but not limited to, incidental, +%% consequential, or any other damages, resulting from the use or misuse +%% of any information contained here. +%% +%% All comments are the opinions of their respective authors and are not +%% necessarily endorsed by the IEEE. +%% +%% This work is distributed under the LaTeX Project Public License (LPPL) +%% ( http://www.latex-project.org/ ) version 1.3, and may be freely used, +%% distributed and modified. A copy of the LPPL, version 1.3, is included +%% in the base LaTeX documentation of all distributions of LaTeX released +%% 2003/12/01 or later. +%% Retain all contribution notices and credits. +%% ** Modified files should be clearly indicated as such, including ** +%% ** renaming them and changing author support contact information. ** +%% +%% File list of work: IEEEtran.cls, IEEEtran_HOWTO.pdf, bare_adv.tex, +%% bare_conf.tex, bare_jrnl.tex, bare_jrnl_compsoc.tex +%%************************************************************************* + +% *** Authors should verify (and, if needed, correct) their LaTeX system *** +% *** with the testflow diagnostic prior to trusting their LaTeX platform *** +% *** with production work. IEEE's font choices can trigger bugs that do *** +% *** not appear when using other class files. *** +% The testflow support page is at: +% http://www.michaelshell.org/tex/testflow/ + + + +% Note that the a4paper option is mainly intended so that authors in +% countries using A4 can easily print to A4 and see how their papers will +% look in print - the typesetting of the document will not typically be +% affected with changes in paper size (but the bottom and side margins will). +% Use the testflow package mentioned above to verify correct handling of +% both paper sizes by the user's LaTeX system. +% +% Also note that the "draftcls" or "draftclsnofoot", not "draft", option +% should be used if it is desired that the figures are to be displayed in +% draft mode. +% +\documentclass[conference,pdf,a4paper,10pt,final,twoside,twocolumn]{IEEEtran} +% Add the compsoc option for Computer Society conferences. +% +% If IEEEtran.cls has not been installed into the LaTeX system files, +% manually specify the path to it like: +% \documentclass[conference]{../sty/IEEEtran} + +% Some very useful LaTeX packages include: +% (uncomment the ones you want to load) + +% *** MISC UTILITY PACKAGES *** +% +%\usepackage{ifpdf} +% Heiko Oberdiek's ifpdf.sty is very useful if you need conditional +% compilation based on whether the output is pdf or dvi. +% usage: +% \ifpdf +% % pdf code +% \else +% % dvi code +% \fi +% The latest version of ifpdf.sty can be obtained from: +% http://www.ctan.org/tex-archive/macros/latex/contrib/oberdiek/ +% Also, note that IEEEtran.cls V1.7 and later provides a builtin +% \ifCLASSINFOpdf conditional that works the same way. +% When switching from latex to pdflatex and vice-versa, the compiler may +% have to be run twice to clear warning/error messages. + + + + + + +% *** CITATION PACKAGES *** +% +\usepackage{cite} +% cite.sty was written by Donald Arseneau +% V1.6 and later of IEEEtran pre-defines the format of the cite.sty package +% \cite{} output to follow that of IEEE. Loading the cite package will +% result in citation numbers being automatically sorted and properly +% "compressed/ranged". e.g., [1], [9], [2], [7], [5], [6] without using +% cite.sty will become [1], [2], [5]--[7], [9] using cite.sty. cite.sty's +% \cite will automatically add leading space, if needed. Use cite.sty's +% noadjust option (cite.sty V3.8 and later) if you want to turn this off. +% cite.sty is already installed on most LaTeX systems. Be sure and use +% version 4.0 (2003-05-27) and later if using hyperref.sty. cite.sty does +% not currently provide for hyperlinked citations. +% The latest version can be obtained at: +% http://www.ctan.org/tex-archive/macros/latex/contrib/cite/ +% The documentation is contained in the cite.sty file itself. + + + + + + +% *** GRAPHICS RELATED PACKAGES *** +% +\ifCLASSINFOpdf + % \usepackage[pdftex]{graphicx} + % declare the path(s) where your graphic files are + % \graphicspath{{../pdf/}{../jpeg/}} + % and their extensions so you won't have to specify these with + % every instance of \includegraphics + % \DeclareGraphicsExtensions{.pdf,.jpeg,.png} +\else + % or other class option (dvipsone, dvipdf, if not using dvips). graphicx + % will default to the driver specified in the system graphics.cfg if no + % driver is specified. + % \usepackage[dvips]{graphicx} + % declare the path(s) where your graphic files are + % \graphicspath{{../eps/}} + % and their extensions so you won't have to specify these with + % every instance of \includegraphics + % \DeclareGraphicsExtensions{.eps} +\fi +% graphicx was written by David Carlisle and Sebastian Rahtz. It is +% required if you want graphics, photos, etc. graphicx.sty is already +% installed on most LaTeX systems. The latest version and documentation can +% be obtained at: +% http://www.ctan.org/tex-archive/macros/latex/required/graphics/ +% Another good source of documentation is "Using Imported Graphics in +% LaTeX2e" by Keith Reckdahl which can be found as epslatex.ps or +% epslatex.pdf at: http://www.ctan.org/tex-archive/info/ +% +% latex, and pdflatex in dvi mode, support graphics in encapsulated +% postscript (.eps) format. pdflatex in pdf mode supports graphics +% in .pdf, .jpeg, .png and .mps (metapost) formats. Users should ensure +% that all non-photo figures use a vector format (.eps, .pdf, .mps) and +% not a bitmapped formats (.jpeg, .png). IEEE frowns on bitmapped formats +% which can result in "jaggedy"/blurry rendering of lines and letters as +% well as large increases in file sizes. +% +% You can find documentation about the pdfTeX application at: +% http://www.tug.org/applications/pdftex + + + + + +% *** MATH PACKAGES *** +% +%\usepackage[cmex10]{amsmath} +% A popular package from the American Mathematical Society that provides +% many useful and powerful commands for dealing with mathematics. If using +% it, be sure to load this package with the cmex10 option to ensure that +% only type 1 fonts will utilized at all point sizes. Without this option, +% it is possible that some math symbols, particularly those within +% footnotes, will be rendered in bitmap form which will result in a +% document that can not be IEEE Xplore compliant! +% +% Also, note that the amsmath package sets \interdisplaylinepenalty to 10000 +% thus preventing page breaks from occurring within multiline equations. Use: +%\interdisplaylinepenalty=2500 +% after loading amsmath to restore such page breaks as IEEEtran.cls normally +% does. amsmath.sty is already installed on most LaTeX systems. The latest +% version and documentation can be obtained at: +% http://www.ctan.org/tex-archive/macros/latex/required/amslatex/math/ + + + + + +% *** SPECIALIZED LIST PACKAGES *** +% +%\usepackage{algorithmic} +% algorithmic.sty was written by Peter Williams and Rogerio Brito. +% This package provides an algorithmic environment fo describing algorithms. +% You can use the algorithmic environment in-text or within a figure +% environment to provide for a floating algorithm. Do NOT use the algorithm +% floating environment provided by algorithm.sty (by the same authors) or +% algorithm2e.sty (by Christophe Fiorio) as IEEE does not use dedicated +% algorithm float types and packages that provide these will not provide +% correct IEEE style captions. The latest version and documentation of +% algorithmic.sty can be obtained at: +% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithms/ +% There is also a support site at: +% http://algorithms.berlios.de/index.html +% Also of interest may be the (relatively newer and more customizable) +% algorithmicx.sty package by Szasz Janos: +% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithmicx/ + + + + +% *** ALIGNMENT PACKAGES *** +% +%\usepackage{array} +% Frank Mittelbach's and David Carlisle's array.sty patches and improves +% the standard LaTeX2e array and tabular environments to provide better +% appearance and additional user controls. As the default LaTeX2e table +% generation code is lacking to the point of almost being broken with +% respect to the quality of the end results, all users are strongly +% advised to use an enhanced (at the very least that provided by array.sty) +% set of table tools. array.sty is already installed on most systems. The +% latest version and documentation can be obtained at: +% http://www.ctan.org/tex-archive/macros/latex/required/tools/ + + +%\usepackage{mdwmath} +%\usepackage{mdwtab} +% Also highly recommended is Mark Wooding's extremely powerful MDW tools, +% especially mdwmath.sty and mdwtab.sty which are used to format equations +% and tables, respectively. The MDWtools set is already installed on most +% LaTeX systems. The lastest version and documentation is available at: +% http://www.ctan.org/tex-archive/macros/latex/contrib/mdwtools/ + + +% IEEEtran contains the IEEEeqnarray family of commands that can be used to +% generate multiline equations as well as matrices, tables, etc., of high +% quality. + + +%\usepackage{eqparbox} +% Also of notable interest is Scott Pakin's eqparbox package for creating +% (automatically sized) equal width boxes - aka "natural width parboxes". +% Available at: +% http://www.ctan.org/tex-archive/macros/latex/contrib/eqparbox/ + + + + + +% *** SUBFIGURE PACKAGES *** +%\usepackage[tight,footnotesize]{subfigure} +% subfigure.sty was written by Steven Douglas Cochran. This package makes it +% easy to put subfigures in your figures. e.g., "Figure 1a and 1b". For IEEE +% work, it is a good idea to load it with the tight package option to reduce +% the amount of white space around the subfigures. subfigure.sty is already +% installed on most LaTeX systems. The latest version and documentation can +% be obtained at: +% http://www.ctan.org/tex-archive/obsolete/macros/latex/contrib/subfigure/ +% subfigure.sty has been superceeded by subfig.sty. + + + +%\usepackage[caption=false]{caption} +%\usepackage[font=footnotesize]{subfig} +% subfig.sty, also written by Steven Douglas Cochran, is the modern +% replacement for subfigure.sty. However, subfig.sty requires and +% automatically loads Axel Sommerfeldt's caption.sty which will override +% IEEEtran.cls handling of captions and this will result in nonIEEE style +% figure/table captions. To prevent this problem, be sure and preload +% caption.sty with its "caption=false" package option. This is will preserve +% IEEEtran.cls handing of captions. Version 1.3 (2005/06/28) and later +% (recommended due to many improvements over 1.2) of subfig.sty supports +% the caption=false option directly: +%\usepackage[caption=false,font=footnotesize]{subfig} +% +% The latest version and documentation can be obtained at: +% http://www.ctan.org/tex-archive/macros/latex/contrib/subfig/ +% The latest version and documentation of caption.sty can be obtained at: +% http://www.ctan.org/tex-archive/macros/latex/contrib/caption/ + + + + +% *** FLOAT PACKAGES *** +% +%\usepackage{fixltx2e} +% fixltx2e, the successor to the earlier fix2col.sty, was written by +% Frank Mittelbach and David Carlisle. This package corrects a few problems +% in the LaTeX2e kernel, the most notable of which is that in current +% LaTeX2e releases, the ordering of single and double column floats is not +% guaranteed to be preserved. Thus, an unpatched LaTeX2e can allow a +% single column figure to be placed prior to an earlier double column +% figure. The latest version and documentation can be found at: +% http://www.ctan.org/tex-archive/macros/latex/base/ + + + +%\usepackage{stfloats} +% stfloats.sty was written by Sigitas Tolusis. This package gives LaTeX2e +% the ability to do double column floats at the bottom of the page as well +% as the top. (e.g., "\begin{figure*}[!b]" is not normally possible in +% LaTeX2e). It also provides a command: +%\fnbelowfloat +% to enable the placement of footnotes below bottom floats (the standard +% LaTeX2e kernel puts them above bottom floats). This is an invasive package +% which rewrites many portions of the LaTeX2e float routines. It may not work +% with other packages that modify the LaTeX2e float routines. The latest +% version and documentation can be obtained at: +% http://www.ctan.org/tex-archive/macros/latex/contrib/sttools/ +% Documentation is contained in the stfloats.sty comments as well as in the +% presfull.pdf file. Do not use the stfloats baselinefloat ability as IEEE +% does not allow \baselineskip to stretch. Authors submitting work to the +% IEEE should note that IEEE rarely uses double column equations and +% that authors should try to avoid such use. Do not be tempted to use the +% cuted.sty or midfloat.sty packages (also by Sigitas Tolusis) as IEEE does +% not format its papers in such ways. + + + + + +% *** PDF, URL AND HYPERLINK PACKAGES *** +% +%\usepackage{url} +% url.sty was written by Donald Arseneau. It provides better support for +% handling and breaking URLs. url.sty is already installed on most LaTeX +% systems. The latest version can be obtained at: +% http://www.ctan.org/tex-archive/macros/latex/contrib/misc/ +% Read the url.sty source comments for usage information. Basically, +% \url{my_url_here}. + + + + + +% *** Do not adjust lengths that control margins, column widths, etc. *** +% *** Do not use packages that alter fonts (such as pslatex). *** +% There should be no need to do such things with IEEEtran.cls V1.6 and later. +% (Unless specifically asked to do so by the journal or conference you plan +% to submit to, of course. ) + +% correct bad hyphenation here +\hyphenation{op-tical net-works semi-conduc-tor} + +% Macro for certain acronyms in small caps. Doesn't work with the +% default font, though (it contains no smallcaps it seems). +\def\VHDL{{\small{VHDL}}} +\def\GHC{{\small{GHC}}} +\def\CLaSH{\textsc{C$\lambda$aSH}} + +% Macro for pretty printing haskell snippets. Just monospaced for now, perhaps +% we'll get something more complex later on. +\def\hs#1{\texttt{#1}} +\def\quote#1{``{#1}"} + +%include polycode.fmt + +\begin{document} +% +% paper title +% can use linebreaks \\ within to get better formatting as desired +\title{\CLaSH: Structural Descriptions \\ of Synchronous Hardware using Haskell} + + +% author names and affiliations +% use a multiple column layout for up to three different +% affiliations +\author{\IEEEauthorblockN{Christiaan P.R. Baaij, Matthijs Kooijman, Jan Kuper, Marco E.T. Gerards, Bert Molenkamp, Sabih H. Gerez} +\IEEEauthorblockA{University of Twente, Department of EEMCS\\ +P.O. Box 217, 7500 AE, Enschede, The Netherlands\\ +c.p.r.baaij@utwente.nl, matthijs@stdin.nl}} +% \and +% \IEEEauthorblockN{Homer Simpson} +% \IEEEauthorblockA{Twentieth Century Fox\\ +% Springfield, USA\\ +% Email: homer@thesimpsons.com} +% \and +% \IEEEauthorblockN{James Kirk\\ and Montgomery Scott} +% \IEEEauthorblockA{Starfleet Academy\\ +% San Francisco, California 96678-2391\\ +% Telephone: (800) 555--1212\\ +% Fax: (888) 555--1212}} + +% conference papers do not typically use \thanks and this command +% is locked out in conference mode. If really needed, such as for +% the acknowledgment of grants, issue a \IEEEoverridecommandlockouts +% after \documentclass + +% for over three affiliations, or if they all won't fit within the width +% of the page, use this alternative format: +% +%\author{\IEEEauthorblockN{Michael Shell\IEEEauthorrefmark{1}, +%Homer Simpson\IEEEauthorrefmark{2}, +%James Kirk\IEEEauthorrefmark{3}, +%Montgomery Scott\IEEEauthorrefmark{3} and +%Eldon Tyrell\IEEEauthorrefmark{4}} +%\IEEEauthorblockA{\IEEEauthorrefmark{1}School of Electrical and Computer Engineering\\ +%Georgia Institute of Technology, +%Atlanta, Georgia 30332--0250\\ Email: see http://www.michaelshell.org/contact.html} +%\IEEEauthorblockA{\IEEEauthorrefmark{2}Twentieth Century Fox, Springfield, USA\\ +%Email: homer@thesimpsons.com} +%\IEEEauthorblockA{\IEEEauthorrefmark{3}Starfleet Academy, San Francisco, California 96678-2391\\ +%Telephone: (800) 555--1212, Fax: (888) 555--1212} +%\IEEEauthorblockA{\IEEEauthorrefmark{4}Tyrell Inc., 123 Replicant Street, Los Angeles, California 90210--4321}} + + + + +% use for special paper notices +%\IEEEspecialpapernotice{(Invited Paper)} + + + + +% make the title area +\maketitle + + +\begin{abstract} +%\boldmath +The abstract goes here. +\end{abstract} +% IEEEtran.cls defaults to using nonbold math in the Abstract. +% This preserves the distinction between vectors and scalars. However, +% if the conference you are submitting to favors bold math in the abstract, +% then you can use LaTeX's standard command \boldmath at the very start +% of the abstract to achieve this. Many IEEE journals/conferences frown on +% math in the abstract anyway. + +% no keywords + + + + +% For peer review papers, you can put extra information on the cover +% page as needed: +% \ifCLASSOPTIONpeerreview +% \begin{center} \bfseries EDICS Category: 3-BBND \end{center} +% \fi +% +% For peerreview papers, this IEEEtran command inserts a page break and +% creates the second title. It will be ignored for other modes. +\IEEEpeerreviewmaketitle + + +\section{Introduction} +Hardware description languages has allowed the productivity of hardware +engineers to keep pace with the development of chip technology. Standard +Hardware description languages, like \VHDL\ and Verilog, allowed an engineer +to describe circuits using a programming language. These standard languages +are very good at describing detailed hardware properties such as timing +behavior, but are generally cumbersome in expressing higher-level +abstractions. These languages also tend to have a complex syntax and a lack of +formal semantics. To overcome these complexities, and raise the abstraction +level, a great number of approaches based on functional languages has been +proposed \cite{T-Ruby,Hydra,HML2,Hawk1,Lava,ForSyDe1,Wired,reFLect}. The idea +of using functional languages started in the early 1980s \cite{Cardelli1981, +muFP,DAISY,FHDL}, a time which also saw the birth of the currently popular +hardware description languages such as \VHDL. + +What gives functional languages as hardware description languages their merits +is the fact that basic combinatorial circuits are equivalent to mathematical +function, and that functional languages lend themselves very well to describe +and compose these mathematical functions. +\section{Hardware description in Haskell} + + \subsection{Function application} + The basic syntactic elements of a functional program are functions + and function application. These have a single obvious \VHDL\ + translation: each top level function becomes a hardware component, + where each argument is an input port and the result value is the + (single) output port. This output port can have a complex type (such + as a tuple), so having just a single output port does not create a + limitation. + + Each function application in turn becomes component instantiation. + Here, the result of each argument expression is assigned to a + signal, which is mapped to the corresponding input port. The output + port of the function is also mapped to a signal, which is used as + the result of the application itself. + + Since every top level function generates its own component, the + hierarchy of of function calls is reflected in the final \VHDL\ + output as well, creating a hierarchical \VHDL\ description of the + hardware. This separation in different components makes the + resulting \VHDL\ output easier to read and debug. + + Example that defines the \texttt{mac} function by applying the + \texttt{add} and \texttt{mul} functions to calculate $a * b + c$: + +\begin{verbatim} +mac a b c = add (mul a b) c +\end{verbatim} + + TODO: Pretty picture + + \subsection{Choices } + Although describing components and connections allows describing a + lot of hardware designs already, there is an obvious thing missing: + choice. We need some way to be able to choose between values based + on another value. In Haskell, choice is achieved by \hs{case} + expressions, \hs{if} expressions, pattern matching and guards. + + The easiest of these are of course case expressions (and \hs{if} + expressions, which can be very directly translated to \hs{case} + expressions). A \hs{case} expression can in turn simply be + translated to a conditional assignment in \VHDL, where the + conditions use equality comparisons against the constructors in the + \hs{case} expressions. + + A slightly more complex (but very powerful) form of choice is + pattern matching. A function can be defined in multiple clauses, + where each clause specifies a pattern. When the arguments match the + pattern, the corresponding clause will be used. + + A pattern match (with optional guards) can also be implemented using + conditional assignments in \VHDL, where the condition is the logical + and of comparison results of each part of the pattern as well as the + guard. + + Contrived example that sums two values when they are equal or + non-equal (depending on the predicate given) and returns 0 + otherwise. This shows three implementations, one using and if + expression, one using only case expressions and one using pattern + matching and guards. + +\begin{verbatim} +sumif pred a b = if pred == Eq && a == b || pred == Neq && a != b + then a + b + else 0 +\end{verbatim} + +\begin{verbatim} +sumif pred a b = case pred of + Eq -> case a == b of + True -> a + b + False -> 0 + Neq -> case a != b of + True -> a + b + False -> 0 +\end{verbatim} + +\begin{verbatim} +sumif Eq a b | a == b = a + b +sumif Neq a b | a != b = a + b +sumif _ _ _ = 0 +\end{verbatim} + + TODO: Pretty picture + + \subsection{Types} + Translation of two most basic functional concepts has been + discussed: function application and choice. Before looking further + into less obvious concepts like higher-order expressions and + polymorphism, the possible types that can be used in hardware + descriptions will be discussed. + + Some way is needed to translate every values used to its hardware + equivalents. In particular, this means a hardware equivalent for + every \emph{type} used in a hardware description is needed + + Since most functional languages have a lot of standard types that + are hard to translate (integers without a fixed size, lists without + a static length, etc.), a number of \quote{built-in} types will be + defined first. These types are built-in in the sense that our + compiler will have a fixed \VHDL\ type for these. User defined types, + on the other hand, will have their hardware type derived directly + from their Haskell declaration automatically, according to the rules + sketched here. + + \subsection{Built-in types} + The language currently supports the following built-in types. Of these, + only the \hs{Bool} type is supported by Haskell out of the box (the + others are defined by the \CLaSH\ package, so they are user-defined types + from Haskell's point of view). + + \begin{description} + \item[\hs{Bit}] + This is the most basic type available. It is mapped directly onto + the \texttt{std\_logic} \VHDL\ type. Mapping this to the + \texttt{bit} type might make more sense (since the Haskell version + only has two values), but using \texttt{std\_logic} is more standard + (and allowed for some experimentation with don't care values) + + \item[\hs{Bool}] + This is the only built-in Haskell type supported and is translated + exactly like the Bit type (where a value of \hs{True} corresponds to a + value of \hs{High}). Supporting the Bool type is particularly + useful to support \hs{if ... then ... else ...} expressions, which + always have a \hs{Bool} value for the condition. + + A \hs{Bool} is translated to a \texttt{std\_logic}, just like \hs{Bit}. + \item[\hs{SizedWord}, \hs{SizedInt}] + These are types to represent integers. A \hs{SizedWord} is unsigned, + while a \hs{SizedInt} is signed. These types are parametrized by a + length type, so you can define an unsigned word of 32 bits wide as + ollows: + + \begin{verbatim} + type Word32 = SizedWord D32 + \end{verbatim} + + Here, a type synonym \hs{Word32} is defined that is equal to the + \hs{SizedWord} type constructor applied to the type \hs{D32}. \hs{D32} + is the \emph{type level representation} of the decimal number 32, + making the \hs{Word32} type a 32-bit unsigned word. + + These types are translated to the \VHDL\ \texttt{unsigned} and + \texttt{signed} respectively. + \item[\hs{Vector}] + This is a vector type, that can contain elements of any other type and + has a fixed length. It has two type parameters: its + length and the type of the elements contained in it. By putting the + length parameter in the type, the length of a vector can be determined + at compile time, instead of only at run-time for conventional lists. + + The \hs{Vector} type constructor takes two type arguments: the length + of the vector and the type of the elements contained in it. The state + type of an 8 element register bank would then for example be: + + \begin{verbatim} + type RegisterState = Vector D8 Word32 + \end{verbatim} + + Here, a type synonym \hs{RegisterState} is defined that is equal to + the \hs{Vector} type constructor applied to the types \hs{D8} (The type + level representation of the decimal number 8) and \hs{Word32} (The 32 + bit word type as defined above). In other words, the + \hs{RegisterState} type is a vector of 8 32-bit words. + + A fixed size vector is translated to a \VHDL\ array type. + \item[\hs{RangedWord}] + This is another type to describe integers, but unlike the previous + two it has no specific bit-width, but an upper bound. This means that + its range is not limited to powers of two, but can be any number. + A \hs{RangedWord} only has an upper bound, its lower bound is + implicitly zero. There is a lot of added implementation complexity + when adding a lower bound and having just an upper bound was enough + for the primary purpose of this type: type-safely indexing vectors. + + To define an index for the 8 element vector above, we would do: + + \begin{verbatim} + type RegisterIndex = RangedWord D7 + \end{verbatim} + + Here, a type synonym \hs{RegisterIndex} is defined that is equal to + the \hs{RangedWord} type constructor applied to the type \hs{D7}. In + other words, this defines an unsigned word with values from + 0 to 7 (inclusive). This word can be be used to index the + 8 element vector \hs{RegisterState} above. + + This type is translated to the \texttt{unsigned} \VHDL type. + \end{description} + \subsection{User-defined types} + There are three ways to define new types in Haskell: algebraic + data-types with the \hs{data} keyword, type synonyms with the \hs{type} + keyword and type renamings with the \hs{newtype} keyword. \GHC\ + offers a few more advanced ways to introduce types (type families, + existential typing, {\small{GADT}}s, etc.) which are not standard + Haskell. These will be left outside the scope of this research. + + Only an algebraic datatype declaration actually introduces a + completely new type, for which we provide the \VHDL\ translation + below. Type synonyms and renamings only define new names for + existing types (where synonyms are completely interchangeable and + renamings need explicit conversion). Therefore, these do not need + any particular \VHDL\ translation, a synonym or renamed type will + just use the same representation as the original type. The + distinction between a renaming and a synonym does no longer matter + in hardware and can be disregarded in the generated \VHDL. + + For algebraic types, we can make the following distinction: + + \begin{description} + + \item[Product types] + A product type is an algebraic datatype with a single constructor with + two or more fields, denoted in practice like (a,b), (a,b,c), etc. This + is essentially a way to pack a few values together in a record-like + structure. In fact, the built-in tuple types are just algebraic product + types (and are thus supported in exactly the same way). + + The \quote{product} in its name refers to the collection of values + belonging to this type. The collection for a product type is the + Cartesian product of the collections for the types of its fields. + + These types are translated to \VHDL\ record types, with one field for + every field in the constructor. This translation applies to all single + constructor algebraic data-types, including those with just one + field (which are technically not a product, but generate a VHDL + record for implementation simplicity). + \item[Enumerated types] + An enumerated type is an algebraic datatype with multiple constructors, but + none of them have fields. This is essentially a way to get an + enumeration-like type containing alternatives. + + Note that Haskell's \hs{Bool} type is also defined as an + enumeration type, but we have a fixed translation for that. + + These types are translated to \VHDL\ enumerations, with one value for + each constructor. This allows references to these constructors to be + translated to the corresponding enumeration value. + \item[Sum types] + A sum type is an algebraic datatype with multiple constructors, where + the constructors have one or more fields. Technically, a type with + more than one field per constructor is a sum of products type, but + for our purposes this distinction does not really make a + difference, so this distinction is note made. + + The \quote{sum} in its name refers again to the collection of values + belonging to this type. The collection for a sum type is the + union of the the collections for each of the constructors. + + Sum types are currently not supported by the prototype, since there is + no obvious \VHDL\ alternative. They can easily be emulated, however, as + we will see from an example: + + \begin{verbatim} + data Sum = A Bit Word | B Word + \end{verbatim} + + An obvious way to translate this would be to create an enumeration to + distinguish the constructors and then create a big record that + contains all the fields of all the constructors. This is the same + translation that would result from the following enumeration and + product type (using a tuple for clarity): + + \begin{verbatim} + data SumC = A | B + type Sum = (SumC, Bit, Word, Word) + \end{verbatim} + + Here, the \hs{SumC} type effectively signals which of the latter three + fields of the \hs{Sum} type are valid (the first two if \hs{A}, the + last one if \hs{B}), all the other ones have no useful value. + + An obvious problem with this naive approach is the space usage: the + example above generates a fairly big \VHDL\ type. Since we can be + sure that the two \hs{Word}s in the \hs{Sum} type will never be valid + at the same time, this is a waste of space. + + Obviously, duplication detection could be used to reuse a + particular field for another constructor, but this would only + partially solve the problem. If two fields would be, for + example, an array of 8 bits and an 8 bit unsigned word, these are + different types and could not be shared. However, in the final + hardware, both of these types would simply be 8 bit connections, + so we have a 100\% size increase by not sharing these. + \end{description} + + +\section{\CLaSH\ prototype} + +foo\par bar + +\section{Related work} +Many functional hardware description languages have been developed over the +years. Early work includes such languages as \textsc{$\mu$fp}~\cite{muFP}, an +extension of Backus' \textsc{fp} language to synchronous streams, designed +particularly for describing and reasoning about regular circuits. The +Ruby~\cite{Ruby} language uses relations, instead of functions, to describe +circuits, and has a particular focus on layout. \textsc{hml}~\cite{HML2} is a +hardware modeling language based on the strict functional language +\textsc{ml}, and has support for polymorphic types and higher-order functions. +Published work suggests that there is no direct simulation support for +\textsc{hml}, and that the translation to \VHDL\ is only partial. + +Like this work, many functional hardware description languages have some sort +of foundation in the functional programming language Haskell. +Hawk~\cite{Hawk1} uses Haskell to describe system-level executable +specifications used to model the behavior of superscalar microprocessors. Hawk +specifications can be simulated, but there seems to be no support for +automated circuit synthesis. The ForSyDe~\cite{ForSyDe2} system uses Haskell +to specify abstract system models, which can (manually) be transformed into an +implementation model using semantic preserving transformations. ForSyDe has +several simulation and synthesis backends, though synthesis is restricted to +the synchronous subset of the ForSyDe language. + +Lava~\cite{Lava} is a hardware description language that focuses on the +structural representation of hardware. Besides support for simulation and +circuit synthesis, Lava descriptions can be interfaced with formal method +tools for formal verification. Lava descriptions are actually circuit +generators when viewed from a synthesis viewpoint, in that the language +elements of Haskell, such as choice, can be used to guide the circuit +generation. If a developer wants to insert a choice element inside an actual +circuit he will have to specify this explicitly as a component. In this +respect \CLaSH\ differs from Lava, in that all the choice elements, such as +case-statements and patter matching, are synthesized to choice elements in the +eventual circuit. As such, richer control structures can both be specified and +synthesized in \CLaSH\ compared to any of the languages mentioned in this +section. + +The merits of polymorphic typing, combined with higher-order functions, are +now also recognized in the `main-stream' hardware description languages, +exemplified by the new \VHDL\ 2008 standard~\cite{VHDL2008}. \VHDL-2008 has +support to specify types as generics, thus allowing a developer to describe +polymorphic components. Note that those types still require an explicit +generic map, whereas type-inference and type-specialization are implicit in +\CLaSH. + +Wired~\cite{Wired},, T-Ruby~\cite{T-Ruby}, Hydra~\cite{Hydra}. + +A functional language designed specifically for hardware design is +$re{\mathit{FL}}^{ect}$~\cite{reFLect}, which draws experience from earlier +language called \textsc{fl}~\cite{FL} to la + +% An example of a floating figure using the graphicx package. +% Note that \label must occur AFTER (or within) \caption. +% For figures, \caption should occur after the \includegraphics. +% Note that IEEEtran v1.7 and later has special internal code that +% is designed to preserve the operation of \label within \caption +% even when the captionsoff option is in effect. However, because +% of issues like this, it may be the safest practice to put all your +% \label just after \caption rather than within \caption{}. +% +% Reminder: the "draftcls" or "draftclsnofoot", not "draft", class +% option should be used if it is desired that the figures are to be +% displayed while in draft mode. +% +%\begin{figure}[!t] +%\centering +%\includegraphics[width=2.5in]{myfigure} +% where an .eps filename suffix will be assumed under latex, +% and a .pdf suffix will be assumed for pdflatex; or what has been declared +% via \DeclareGraphicsExtensions. +%\caption{Simulation Results} +%\label{fig_sim} +%\end{figure} + +% Note that IEEE typically puts floats only at the top, even when this +% results in a large percentage of a column being occupied by floats. + + +% An example of a double column floating figure using two subfigures. +% (The subfig.sty package must be loaded for this to work.) +% The subfigure \label commands are set within each subfloat command, the +% \label for the overall figure must come after \caption. +% \hfil must be used as a separator to get equal spacing. +% The subfigure.sty package works much the same way, except \subfigure is +% used instead of \subfloat. +% +%\begin{figure*}[!t] +%\centerline{\subfloat[Case I]\includegraphics[width=2.5in]{subfigcase1}% +%\label{fig_first_case}} +%\hfil +%\subfloat[Case II]{\includegraphics[width=2.5in]{subfigcase2}% +%\label{fig_second_case}}} +%\caption{Simulation results} +%\label{fig_sim} +%\end{figure*} +% +% Note that often IEEE papers with subfigures do not employ subfigure +% captions (using the optional argument to \subfloat), but instead will +% reference/describe all of them (a), (b), etc., within the main caption. + + +% An example of a floating table. Note that, for IEEE style tables, the +% \caption command should come BEFORE the table. Table text will default to +% \footnotesize as IEEE normally uses this smaller font for tables. +% The \label must come after \caption as always. +% +%\begin{table}[!t] +%% increase table row spacing, adjust to taste +%\renewcommand{\arraystretch}{1.3} +% if using array.sty, it might be a good idea to tweak the value of +% \extrarowheight as needed to properly center the text within the cells +%\caption{An Example of a Table} +%\label{table_example} +%\centering +%% Some packages, such as MDW tools, offer better commands for making tables +%% than the plain LaTeX2e tabular which is used here. +%\begin{tabular}{|c||c|} +%\hline +%One & Two\\ +%\hline +%Three & Four\\ +%\hline +%\end{tabular} +%\end{table} + + +% Note that IEEE does not put floats in the very first column - or typically +% anywhere on the first page for that matter. Also, in-text middle ("here") +% positioning is not used. Most IEEE journals/conferences use top floats +% exclusively. Note that, LaTeX2e, unlike IEEE journals/conferences, places +% footnotes above bottom floats. This can be corrected via the \fnbelowfloat +% command of the stfloats package. + + + +\section{Conclusion} +The conclusion goes here. + + + + +% conference papers do not normally have an appendix + + +% use section* for acknowledgement +\section*{Acknowledgment} + + +The authors would like to thank... + + + + + +% trigger a \newpage just before the given reference +% number - used to balance the columns on the last page +% adjust value as needed - may need to be readjusted if +% the document is modified later +%\IEEEtriggeratref{8} +% The "triggered" command can be changed if desired: +%\IEEEtriggercmd{\enlargethispage{-5in}} + +% references section + +% can use a bibliography generated by BibTeX as a .bbl file +% BibTeX documentation can be easily obtained at: +% http://www.ctan.org/tex-archive/biblio/bibtex/contrib/doc/ +% The IEEEtran BibTeX style support page is at: +% http://www.michaelshell.org/tex/ieeetran/bibtex/ +\bibliographystyle{IEEEtran} +% argument is your BibTeX string definitions and bibliography database(s) +\bibliography{IEEEabrv,clash.bib} +% +% manually copy in the resultant .bbl file +% set second argument of \begin to the number of references +% (used to reserve space for the reference number labels box) +% \begin{thebibliography}{1} +% +% \bibitem{IEEEhowto:kopka} +% H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus +% 0.5em minus 0.4em\relax Harlow, England: Addison-Wesley, 1999. +% +% \end{thebibliography} + + + + +% that's all folks +\end{document} + +% vim: set ai sw=2 sts=2 expandtab: diff --git "a/c\316\273ash.tex" "b/c\316\273ash.tex" deleted file mode 100644 index 4a917f9..0000000 --- "a/c\316\273ash.tex" +++ /dev/null @@ -1,944 +0,0 @@ - -%% bare_conf.tex -%% V1.3 -%% 2007/01/11 -%% by Michael Shell -%% See: -%% http://www.michaelshell.org/ -%% for current contact information. -%% -%% This is a skeleton file demonstrating the use of IEEEtran.cls -%% (requires IEEEtran.cls version 1.7 or later) with an IEEE conference paper. -%% -%% Support sites: -%% http://www.michaelshell.org/tex/ieeetran/ -%% http://www.ctan.org/tex-archive/macros/latex/contrib/IEEEtran/ -%% and -%% http://www.ieee.org/ - -%%************************************************************************* -%% Legal Notice: -%% This code is offered as-is without any warranty either expressed or -%% implied; without even the implied warranty of MERCHANTABILITY or -%% FITNESS FOR A PARTICULAR PURPOSE! -%% User assumes all risk. -%% In no event shall IEEE or any contributor to this code be liable for -%% any damages or losses, including, but not limited to, incidental, -%% consequential, or any other damages, resulting from the use or misuse -%% of any information contained here. -%% -%% All comments are the opinions of their respective authors and are not -%% necessarily endorsed by the IEEE. -%% -%% This work is distributed under the LaTeX Project Public License (LPPL) -%% ( http://www.latex-project.org/ ) version 1.3, and may be freely used, -%% distributed and modified. A copy of the LPPL, version 1.3, is included -%% in the base LaTeX documentation of all distributions of LaTeX released -%% 2003/12/01 or later. -%% Retain all contribution notices and credits. -%% ** Modified files should be clearly indicated as such, including ** -%% ** renaming them and changing author support contact information. ** -%% -%% File list of work: IEEEtran.cls, IEEEtran_HOWTO.pdf, bare_adv.tex, -%% bare_conf.tex, bare_jrnl.tex, bare_jrnl_compsoc.tex -%%************************************************************************* - -% *** Authors should verify (and, if needed, correct) their LaTeX system *** -% *** with the testflow diagnostic prior to trusting their LaTeX platform *** -% *** with production work. IEEE's font choices can trigger bugs that do *** -% *** not appear when using other class files. *** -% The testflow support page is at: -% http://www.michaelshell.org/tex/testflow/ - - - -% Note that the a4paper option is mainly intended so that authors in -% countries using A4 can easily print to A4 and see how their papers will -% look in print - the typesetting of the document will not typically be -% affected with changes in paper size (but the bottom and side margins will). -% Use the testflow package mentioned above to verify correct handling of -% both paper sizes by the user's LaTeX system. -% -% Also note that the "draftcls" or "draftclsnofoot", not "draft", option -% should be used if it is desired that the figures are to be displayed in -% draft mode. -% -\documentclass[conference,pdf,a4paper,10pt,final,twoside,twocolumn]{IEEEtran} -% Add the compsoc option for Computer Society conferences. -% -% If IEEEtran.cls has not been installed into the LaTeX system files, -% manually specify the path to it like: -% \documentclass[conference]{../sty/IEEEtran} - -% Some very useful LaTeX packages include: -% (uncomment the ones you want to load) - -% *** MISC UTILITY PACKAGES *** -% -%\usepackage{ifpdf} -% Heiko Oberdiek's ifpdf.sty is very useful if you need conditional -% compilation based on whether the output is pdf or dvi. -% usage: -% \ifpdf -% % pdf code -% \else -% % dvi code -% \fi -% The latest version of ifpdf.sty can be obtained from: -% http://www.ctan.org/tex-archive/macros/latex/contrib/oberdiek/ -% Also, note that IEEEtran.cls V1.7 and later provides a builtin -% \ifCLASSINFOpdf conditional that works the same way. -% When switching from latex to pdflatex and vice-versa, the compiler may -% have to be run twice to clear warning/error messages. - - - - - - -% *** CITATION PACKAGES *** -% -\usepackage{cite} -% cite.sty was written by Donald Arseneau -% V1.6 and later of IEEEtran pre-defines the format of the cite.sty package -% \cite{} output to follow that of IEEE. Loading the cite package will -% result in citation numbers being automatically sorted and properly -% "compressed/ranged". e.g., [1], [9], [2], [7], [5], [6] without using -% cite.sty will become [1], [2], [5]--[7], [9] using cite.sty. cite.sty's -% \cite will automatically add leading space, if needed. Use cite.sty's -% noadjust option (cite.sty V3.8 and later) if you want to turn this off. -% cite.sty is already installed on most LaTeX systems. Be sure and use -% version 4.0 (2003-05-27) and later if using hyperref.sty. cite.sty does -% not currently provide for hyperlinked citations. -% The latest version can be obtained at: -% http://www.ctan.org/tex-archive/macros/latex/contrib/cite/ -% The documentation is contained in the cite.sty file itself. - - - - - - -% *** GRAPHICS RELATED PACKAGES *** -% -\ifCLASSINFOpdf - % \usepackage[pdftex]{graphicx} - % declare the path(s) where your graphic files are - % \graphicspath{{../pdf/}{../jpeg/}} - % and their extensions so you won't have to specify these with - % every instance of \includegraphics - % \DeclareGraphicsExtensions{.pdf,.jpeg,.png} -\else - % or other class option (dvipsone, dvipdf, if not using dvips). graphicx - % will default to the driver specified in the system graphics.cfg if no - % driver is specified. - % \usepackage[dvips]{graphicx} - % declare the path(s) where your graphic files are - % \graphicspath{{../eps/}} - % and their extensions so you won't have to specify these with - % every instance of \includegraphics - % \DeclareGraphicsExtensions{.eps} -\fi -% graphicx was written by David Carlisle and Sebastian Rahtz. It is -% required if you want graphics, photos, etc. graphicx.sty is already -% installed on most LaTeX systems. The latest version and documentation can -% be obtained at: -% http://www.ctan.org/tex-archive/macros/latex/required/graphics/ -% Another good source of documentation is "Using Imported Graphics in -% LaTeX2e" by Keith Reckdahl which can be found as epslatex.ps or -% epslatex.pdf at: http://www.ctan.org/tex-archive/info/ -% -% latex, and pdflatex in dvi mode, support graphics in encapsulated -% postscript (.eps) format. pdflatex in pdf mode supports graphics -% in .pdf, .jpeg, .png and .mps (metapost) formats. Users should ensure -% that all non-photo figures use a vector format (.eps, .pdf, .mps) and -% not a bitmapped formats (.jpeg, .png). IEEE frowns on bitmapped formats -% which can result in "jaggedy"/blurry rendering of lines and letters as -% well as large increases in file sizes. -% -% You can find documentation about the pdfTeX application at: -% http://www.tug.org/applications/pdftex - - - - - -% *** MATH PACKAGES *** -% -%\usepackage[cmex10]{amsmath} -% A popular package from the American Mathematical Society that provides -% many useful and powerful commands for dealing with mathematics. If using -% it, be sure to load this package with the cmex10 option to ensure that -% only type 1 fonts will utilized at all point sizes. Without this option, -% it is possible that some math symbols, particularly those within -% footnotes, will be rendered in bitmap form which will result in a -% document that can not be IEEE Xplore compliant! -% -% Also, note that the amsmath package sets \interdisplaylinepenalty to 10000 -% thus preventing page breaks from occurring within multiline equations. Use: -%\interdisplaylinepenalty=2500 -% after loading amsmath to restore such page breaks as IEEEtran.cls normally -% does. amsmath.sty is already installed on most LaTeX systems. The latest -% version and documentation can be obtained at: -% http://www.ctan.org/tex-archive/macros/latex/required/amslatex/math/ - - - - - -% *** SPECIALIZED LIST PACKAGES *** -% -%\usepackage{algorithmic} -% algorithmic.sty was written by Peter Williams and Rogerio Brito. -% This package provides an algorithmic environment fo describing algorithms. -% You can use the algorithmic environment in-text or within a figure -% environment to provide for a floating algorithm. Do NOT use the algorithm -% floating environment provided by algorithm.sty (by the same authors) or -% algorithm2e.sty (by Christophe Fiorio) as IEEE does not use dedicated -% algorithm float types and packages that provide these will not provide -% correct IEEE style captions. The latest version and documentation of -% algorithmic.sty can be obtained at: -% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithms/ -% There is also a support site at: -% http://algorithms.berlios.de/index.html -% Also of interest may be the (relatively newer and more customizable) -% algorithmicx.sty package by Szasz Janos: -% http://www.ctan.org/tex-archive/macros/latex/contrib/algorithmicx/ - - - - -% *** ALIGNMENT PACKAGES *** -% -%\usepackage{array} -% Frank Mittelbach's and David Carlisle's array.sty patches and improves -% the standard LaTeX2e array and tabular environments to provide better -% appearance and additional user controls. As the default LaTeX2e table -% generation code is lacking to the point of almost being broken with -% respect to the quality of the end results, all users are strongly -% advised to use an enhanced (at the very least that provided by array.sty) -% set of table tools. array.sty is already installed on most systems. The -% latest version and documentation can be obtained at: -% http://www.ctan.org/tex-archive/macros/latex/required/tools/ - - -%\usepackage{mdwmath} -%\usepackage{mdwtab} -% Also highly recommended is Mark Wooding's extremely powerful MDW tools, -% especially mdwmath.sty and mdwtab.sty which are used to format equations -% and tables, respectively. The MDWtools set is already installed on most -% LaTeX systems. The lastest version and documentation is available at: -% http://www.ctan.org/tex-archive/macros/latex/contrib/mdwtools/ - - -% IEEEtran contains the IEEEeqnarray family of commands that can be used to -% generate multiline equations as well as matrices, tables, etc., of high -% quality. - - -%\usepackage{eqparbox} -% Also of notable interest is Scott Pakin's eqparbox package for creating -% (automatically sized) equal width boxes - aka "natural width parboxes". -% Available at: -% http://www.ctan.org/tex-archive/macros/latex/contrib/eqparbox/ - - - - - -% *** SUBFIGURE PACKAGES *** -%\usepackage[tight,footnotesize]{subfigure} -% subfigure.sty was written by Steven Douglas Cochran. This package makes it -% easy to put subfigures in your figures. e.g., "Figure 1a and 1b". For IEEE -% work, it is a good idea to load it with the tight package option to reduce -% the amount of white space around the subfigures. subfigure.sty is already -% installed on most LaTeX systems. The latest version and documentation can -% be obtained at: -% http://www.ctan.org/tex-archive/obsolete/macros/latex/contrib/subfigure/ -% subfigure.sty has been superceeded by subfig.sty. - - - -%\usepackage[caption=false]{caption} -%\usepackage[font=footnotesize]{subfig} -% subfig.sty, also written by Steven Douglas Cochran, is the modern -% replacement for subfigure.sty. However, subfig.sty requires and -% automatically loads Axel Sommerfeldt's caption.sty which will override -% IEEEtran.cls handling of captions and this will result in nonIEEE style -% figure/table captions. To prevent this problem, be sure and preload -% caption.sty with its "caption=false" package option. This is will preserve -% IEEEtran.cls handing of captions. Version 1.3 (2005/06/28) and later -% (recommended due to many improvements over 1.2) of subfig.sty supports -% the caption=false option directly: -%\usepackage[caption=false,font=footnotesize]{subfig} -% -% The latest version and documentation can be obtained at: -% http://www.ctan.org/tex-archive/macros/latex/contrib/subfig/ -% The latest version and documentation of caption.sty can be obtained at: -% http://www.ctan.org/tex-archive/macros/latex/contrib/caption/ - - - - -% *** FLOAT PACKAGES *** -% -%\usepackage{fixltx2e} -% fixltx2e, the successor to the earlier fix2col.sty, was written by -% Frank Mittelbach and David Carlisle. This package corrects a few problems -% in the LaTeX2e kernel, the most notable of which is that in current -% LaTeX2e releases, the ordering of single and double column floats is not -% guaranteed to be preserved. Thus, an unpatched LaTeX2e can allow a -% single column figure to be placed prior to an earlier double column -% figure. The latest version and documentation can be found at: -% http://www.ctan.org/tex-archive/macros/latex/base/ - - - -%\usepackage{stfloats} -% stfloats.sty was written by Sigitas Tolusis. This package gives LaTeX2e -% the ability to do double column floats at the bottom of the page as well -% as the top. (e.g., "\begin{figure*}[!b]" is not normally possible in -% LaTeX2e). It also provides a command: -%\fnbelowfloat -% to enable the placement of footnotes below bottom floats (the standard -% LaTeX2e kernel puts them above bottom floats). This is an invasive package -% which rewrites many portions of the LaTeX2e float routines. It may not work -% with other packages that modify the LaTeX2e float routines. The latest -% version and documentation can be obtained at: -% http://www.ctan.org/tex-archive/macros/latex/contrib/sttools/ -% Documentation is contained in the stfloats.sty comments as well as in the -% presfull.pdf file. Do not use the stfloats baselinefloat ability as IEEE -% does not allow \baselineskip to stretch. Authors submitting work to the -% IEEE should note that IEEE rarely uses double column equations and -% that authors should try to avoid such use. Do not be tempted to use the -% cuted.sty or midfloat.sty packages (also by Sigitas Tolusis) as IEEE does -% not format its papers in such ways. - - - - - -% *** PDF, URL AND HYPERLINK PACKAGES *** -% -%\usepackage{url} -% url.sty was written by Donald Arseneau. It provides better support for -% handling and breaking URLs. url.sty is already installed on most LaTeX -% systems. The latest version can be obtained at: -% http://www.ctan.org/tex-archive/macros/latex/contrib/misc/ -% Read the url.sty source comments for usage information. Basically, -% \url{my_url_here}. - - - - - -% *** Do not adjust lengths that control margins, column widths, etc. *** -% *** Do not use packages that alter fonts (such as pslatex). *** -% There should be no need to do such things with IEEEtran.cls V1.6 and later. -% (Unless specifically asked to do so by the journal or conference you plan -% to submit to, of course. ) - -% correct bad hyphenation here -\hyphenation{op-tical net-works semi-conduc-tor} - -% Macro for certain acronyms in small caps. Doesn't work with the -% default font, though (it contains no smallcaps it seems). -\def\VHDL{{\small{VHDL}}} -\def\GHC{{\small{GHC}}} -\def\CLaSH{\textsc{C$\lambda$aSH}} - -% Macro for pretty printing haskell snippets. Just monospaced for now, perhaps -% we'll get something more complex later on. -\def\hs#1{\texttt{#1}} -\def\quote#1{``{#1}"} - -\begin{document} -% -% paper title -% can use linebreaks \\ within to get better formatting as desired -\title{\CLaSH: Structural Descriptions \\ of Synchronous Hardware using Haskell} - - -% author names and affiliations -% use a multiple column layout for up to three different -% affiliations -\author{\IEEEauthorblockN{Christiaan P.R. Baaij, Matthijs Kooijman, Jan Kuper, Marco E.T. Gerards, Bert Molenkamp, Sabih H. Gerez} -\IEEEauthorblockA{University of Twente, Department of EEMCS\\ -P.O. Box 217, 7500 AE, Enschede, The Netherlands\\ -c.p.r.baaij@utwente.nl, matthijs@stdin.nl}} -% \and -% \IEEEauthorblockN{Homer Simpson} -% \IEEEauthorblockA{Twentieth Century Fox\\ -% Springfield, USA\\ -% Email: homer@thesimpsons.com} -% \and -% \IEEEauthorblockN{James Kirk\\ and Montgomery Scott} -% \IEEEauthorblockA{Starfleet Academy\\ -% San Francisco, California 96678-2391\\ -% Telephone: (800) 555--1212\\ -% Fax: (888) 555--1212}} - -% conference papers do not typically use \thanks and this command -% is locked out in conference mode. If really needed, such as for -% the acknowledgment of grants, issue a \IEEEoverridecommandlockouts -% after \documentclass - -% for over three affiliations, or if they all won't fit within the width -% of the page, use this alternative format: -% -%\author{\IEEEauthorblockN{Michael Shell\IEEEauthorrefmark{1}, -%Homer Simpson\IEEEauthorrefmark{2}, -%James Kirk\IEEEauthorrefmark{3}, -%Montgomery Scott\IEEEauthorrefmark{3} and -%Eldon Tyrell\IEEEauthorrefmark{4}} -%\IEEEauthorblockA{\IEEEauthorrefmark{1}School of Electrical and Computer Engineering\\ -%Georgia Institute of Technology, -%Atlanta, Georgia 30332--0250\\ Email: see http://www.michaelshell.org/contact.html} -%\IEEEauthorblockA{\IEEEauthorrefmark{2}Twentieth Century Fox, Springfield, USA\\ -%Email: homer@thesimpsons.com} -%\IEEEauthorblockA{\IEEEauthorrefmark{3}Starfleet Academy, San Francisco, California 96678-2391\\ -%Telephone: (800) 555--1212, Fax: (888) 555--1212} -%\IEEEauthorblockA{\IEEEauthorrefmark{4}Tyrell Inc., 123 Replicant Street, Los Angeles, California 90210--4321}} - - - - -% use for special paper notices -%\IEEEspecialpapernotice{(Invited Paper)} - - - - -% make the title area -\maketitle - - -\begin{abstract} -%\boldmath -The abstract goes here. -\end{abstract} -% IEEEtran.cls defaults to using nonbold math in the Abstract. -% This preserves the distinction between vectors and scalars. However, -% if the conference you are submitting to favors bold math in the abstract, -% then you can use LaTeX's standard command \boldmath at the very start -% of the abstract to achieve this. Many IEEE journals/conferences frown on -% math in the abstract anyway. - -% no keywords - - - - -% For peer review papers, you can put extra information on the cover -% page as needed: -% \ifCLASSOPTIONpeerreview -% \begin{center} \bfseries EDICS Category: 3-BBND \end{center} -% \fi -% -% For peerreview papers, this IEEEtran command inserts a page break and -% creates the second title. It will be ignored for other modes. -\IEEEpeerreviewmaketitle - - -\section{Introduction} -Hardware description languages has allowed the productivity of hardware -engineers to keep pace with the development of chip technology. Standard -Hardware description languages, like \VHDL\ and Verilog, allowed an engineer -to describe circuits using a programming language. These standard languages -are very good at describing detailed hardware properties such as timing -behavior, but are generally cumbersome in expressing higher-level -abstractions. These languages also tend to have a complex syntax and a lack of -formal semantics. To overcome these complexities, and raise the abstraction -level, a great number of approaches based on functional languages has been -proposed \cite{T-Ruby,Hydra,HML2,Hawk1,Lava,ForSyDe1,Wired,reFLect}. The idea -of using functional languages started in the early 1980s \cite{Cardelli1981, -muFP,DAISY,FHDL}, a time which also saw the birth of the currently popular -hardware description languages such as \VHDL. - -What gives functional languages as hardware description languages their merits -is the fact that basic combinatorial circuits are equivalent to mathematical -function, and that functional languages lend themselves very well to describe -and compose these mathematical functions. -\section{Hardware description in Haskell} - - \subsection{Function application} - The basic syntactic elements of a functional program are functions - and function application. These have a single obvious \VHDL\ - translation: each top level function becomes a hardware component, - where each argument is an input port and the result value is the - (single) output port. This output port can have a complex type (such - as a tuple), so having just a single output port does not create a - limitation. - - Each function application in turn becomes component instantiation. - Here, the result of each argument expression is assigned to a - signal, which is mapped to the corresponding input port. The output - port of the function is also mapped to a signal, which is used as - the result of the application itself. - - Since every top level function generates its own component, the - hierarchy of of function calls is reflected in the final \VHDL\ - output as well, creating a hierarchical \VHDL\ description of the - hardware. This separation in different components makes the - resulting \VHDL\ output easier to read and debug. - - Example that defines the \texttt{mac} function by applying the - \texttt{add} and \texttt{mul} functions to calculate $a * b + c$: - -\begin{verbatim} -mac a b c = add (mul a b) c -\end{verbatim} - - TODO: Pretty picture - - \subsection{Choices } - Although describing components and connections allows describing a - lot of hardware designs already, there is an obvious thing missing: - choice. We need some way to be able to choose between values based - on another value. In Haskell, choice is achieved by \hs{case} - expressions, \hs{if} expressions, pattern matching and guards. - - The easiest of these are of course case expressions (and \hs{if} - expressions, which can be very directly translated to \hs{case} - expressions). A \hs{case} expression can in turn simply be - translated to a conditional assignment in \VHDL, where the - conditions use equality comparisons against the constructors in the - \hs{case} expressions. - - A slightly more complex (but very powerful) form of choice is - pattern matching. A function can be defined in multiple clauses, - where each clause specifies a pattern. When the arguments match the - pattern, the corresponding clause will be used. - - A pattern match (with optional guards) can also be implemented using - conditional assignments in \VHDL, where the condition is the logical - and of comparison results of each part of the pattern as well as the - guard. - - Contrived example that sums two values when they are equal or - non-equal (depending on the predicate given) and returns 0 - otherwise. This shows three implementations, one using and if - expression, one using only case expressions and one using pattern - matching and guards. - -\begin{verbatim} -sumif pred a b = if pred == Eq && a == b || pred == Neq && a != b - then a + b - else 0 -\end{verbatim} - -\begin{verbatim} -sumif pred a b = case pred of - Eq -> case a == b of - True -> a + b - False -> 0 - Neq -> case a != b of - True -> a + b - False -> 0 -\end{verbatim} - -\begin{verbatim} -sumif Eq a b | a == b = a + b -sumif Neq a b | a != b = a + b -sumif _ _ _ = 0 -\end{verbatim} - - TODO: Pretty picture - - \subsection{Types} - Translation of two most basic functional concepts has been - discussed: function application and choice. Before looking further - into less obvious concepts like higher-order expressions and - polymorphism, the possible types that can be used in hardware - descriptions will be discussed. - - Some way is needed to translate every values used to its hardware - equivalents. In particular, this means a hardware equivalent for - every \emph{type} used in a hardware description is needed - - Since most functional languages have a lot of standard types that - are hard to translate (integers without a fixed size, lists without - a static length, etc.), a number of \quote{built-in} types will be - defined first. These types are built-in in the sense that our - compiler will have a fixed \VHDL\ type for these. User defined types, - on the other hand, will have their hardware type derived directly - from their Haskell declaration automatically, according to the rules - sketched here. - - \subsection{Built-in types} - The language currently supports the following built-in types. Of these, - only the \hs{Bool} type is supported by Haskell out of the box (the - others are defined by the \CLaSH\ package, so they are user-defined types - from Haskell's point of view). - - \begin{description} - \item[\hs{Bit}] - This is the most basic type available. It is mapped directly onto - the \texttt{std\_logic} \VHDL\ type. Mapping this to the - \texttt{bit} type might make more sense (since the Haskell version - only has two values), but using \texttt{std\_logic} is more standard - (and allowed for some experimentation with don't care values) - - \item[\hs{Bool}] - This is the only built-in Haskell type supported and is translated - exactly like the Bit type (where a value of \hs{True} corresponds to a - value of \hs{High}). Supporting the Bool type is particularly - useful to support \hs{if ... then ... else ...} expressions, which - always have a \hs{Bool} value for the condition. - - A \hs{Bool} is translated to a \texttt{std\_logic}, just like \hs{Bit}. - \item[\hs{SizedWord}, \hs{SizedInt}] - These are types to represent integers. A \hs{SizedWord} is unsigned, - while a \hs{SizedInt} is signed. These types are parametrized by a - length type, so you can define an unsigned word of 32 bits wide as - ollows: - - \begin{verbatim} - type Word32 = SizedWord D32 - \end{verbatim} - - Here, a type synonym \hs{Word32} is defined that is equal to the - \hs{SizedWord} type constructor applied to the type \hs{D32}. \hs{D32} - is the \emph{type level representation} of the decimal number 32, - making the \hs{Word32} type a 32-bit unsigned word. - - These types are translated to the \VHDL\ \texttt{unsigned} and - \texttt{signed} respectively. - \item[\hs{Vector}] - This is a vector type, that can contain elements of any other type and - has a fixed length. It has two type parameters: its - length and the type of the elements contained in it. By putting the - length parameter in the type, the length of a vector can be determined - at compile time, instead of only at run-time for conventional lists. - - The \hs{Vector} type constructor takes two type arguments: the length - of the vector and the type of the elements contained in it. The state - type of an 8 element register bank would then for example be: - - \begin{verbatim} - type RegisterState = Vector D8 Word32 - \end{verbatim} - - Here, a type synonym \hs{RegisterState} is defined that is equal to - the \hs{Vector} type constructor applied to the types \hs{D8} (The type - level representation of the decimal number 8) and \hs{Word32} (The 32 - bit word type as defined above). In other words, the - \hs{RegisterState} type is a vector of 8 32-bit words. - - A fixed size vector is translated to a \VHDL\ array type. - \item[\hs{RangedWord}] - This is another type to describe integers, but unlike the previous - two it has no specific bit-width, but an upper bound. This means that - its range is not limited to powers of two, but can be any number. - A \hs{RangedWord} only has an upper bound, its lower bound is - implicitly zero. There is a lot of added implementation complexity - when adding a lower bound and having just an upper bound was enough - for the primary purpose of this type: type-safely indexing vectors. - - To define an index for the 8 element vector above, we would do: - - \begin{verbatim} - type RegisterIndex = RangedWord D7 - \end{verbatim} - - Here, a type synonym \hs{RegisterIndex} is defined that is equal to - the \hs{RangedWord} type constructor applied to the type \hs{D7}. In - other words, this defines an unsigned word with values from - 0 to 7 (inclusive). This word can be be used to index the - 8 element vector \hs{RegisterState} above. - - This type is translated to the \texttt{unsigned} \VHDL type. - \end{description} - \subsection{User-defined types} - There are three ways to define new types in Haskell: algebraic - data-types with the \hs{data} keyword, type synonyms with the \hs{type} - keyword and type renamings with the \hs{newtype} keyword. \GHC\ - offers a few more advanced ways to introduce types (type families, - existential typing, {\small{GADT}}s, etc.) which are not standard - Haskell. These will be left outside the scope of this research. - - Only an algebraic datatype declaration actually introduces a - completely new type, for which we provide the \VHDL\ translation - below. Type synonyms and renamings only define new names for - existing types (where synonyms are completely interchangeable and - renamings need explicit conversion). Therefore, these do not need - any particular \VHDL\ translation, a synonym or renamed type will - just use the same representation as the original type. The - distinction between a renaming and a synonym does no longer matter - in hardware and can be disregarded in the generated \VHDL. - - For algebraic types, we can make the following distinction: - - \begin{description} - - \item[Product types] - A product type is an algebraic datatype with a single constructor with - two or more fields, denoted in practice like (a,b), (a,b,c), etc. This - is essentially a way to pack a few values together in a record-like - structure. In fact, the built-in tuple types are just algebraic product - types (and are thus supported in exactly the same way). - - The \quote{product} in its name refers to the collection of values - belonging to this type. The collection for a product type is the - Cartesian product of the collections for the types of its fields. - - These types are translated to \VHDL\ record types, with one field for - every field in the constructor. This translation applies to all single - constructor algebraic data-types, including those with just one - field (which are technically not a product, but generate a VHDL - record for implementation simplicity). - \item[Enumerated types] - An enumerated type is an algebraic datatype with multiple constructors, but - none of them have fields. This is essentially a way to get an - enumeration-like type containing alternatives. - - Note that Haskell's \hs{Bool} type is also defined as an - enumeration type, but we have a fixed translation for that. - - These types are translated to \VHDL\ enumerations, with one value for - each constructor. This allows references to these constructors to be - translated to the corresponding enumeration value. - \item[Sum types] - A sum type is an algebraic datatype with multiple constructors, where - the constructors have one or more fields. Technically, a type with - more than one field per constructor is a sum of products type, but - for our purposes this distinction does not really make a - difference, so this distinction is note made. - - The \quote{sum} in its name refers again to the collection of values - belonging to this type. The collection for a sum type is the - union of the the collections for each of the constructors. - - Sum types are currently not supported by the prototype, since there is - no obvious \VHDL\ alternative. They can easily be emulated, however, as - we will see from an example: - - \begin{verbatim} - data Sum = A Bit Word | B Word - \end{verbatim} - - An obvious way to translate this would be to create an enumeration to - distinguish the constructors and then create a big record that - contains all the fields of all the constructors. This is the same - translation that would result from the following enumeration and - product type (using a tuple for clarity): - - \begin{verbatim} - data SumC = A | B - type Sum = (SumC, Bit, Word, Word) - \end{verbatim} - - Here, the \hs{SumC} type effectively signals which of the latter three - fields of the \hs{Sum} type are valid (the first two if \hs{A}, the - last one if \hs{B}), all the other ones have no useful value. - - An obvious problem with this naive approach is the space usage: the - example above generates a fairly big \VHDL\ type. Since we can be - sure that the two \hs{Word}s in the \hs{Sum} type will never be valid - at the same time, this is a waste of space. - - Obviously, duplication detection could be used to reuse a - particular field for another constructor, but this would only - partially solve the problem. If two fields would be, for - example, an array of 8 bits and an 8 bit unsigned word, these are - different types and could not be shared. However, in the final - hardware, both of these types would simply be 8 bit connections, - so we have a 100\% size increase by not sharing these. - \end{description} - - -\section{\CLaSH\ prototype} - -foo\par bar - -\section{Related work} -Many functional hardware description languages have been developed over the -years. Early work includes such languages as \textsc{$\mu$fp}~\cite{muFP}, an -extension of Backus' \textsc{fp} language to synchronous streams, designed -particularly for describing and reasoning about regular circuits. The -Ruby~\cite{Ruby} language uses relations, instead of functions, to describe -circuits, and has a particular focus on layout. \textsc{hml}~\cite{HML2} is a -hardware modeling language based on the strict functional language -\textsc{ml}, and has support for polymorphic types and higher-order functions. -Published work suggests that there is no direct simulation support for -\textsc{hml}, and that the translation to \VHDL\ is only partial. - -Like this work, many functional hardware description languages have some sort -of foundation in the functional programming language Haskell. -Hawk~\cite{Hawk1} uses Haskell to describe system-level executable -specifications used to model the behavior of superscalar microprocessors. Hawk -specifications can be simulated, but there seems to be no support for -automated circuit synthesis. The ForSyDe~\cite{ForSyDe2} system uses Haskell -to specify abstract system models, which can (manually) be transformed into an -implementation model using semantic preserving transformations. ForSyDe has -several simulation and synthesis backends, though synthesis is restricted to -the synchronous subset of the ForSyDe language. - -Lava~\cite{Lava} is a hardware description language that focuses on the -structural representation of hardware. Besides support for simulation and -circuit synthesis, Lava descriptions can be interfaced with formal method -tools for formal verification. Lava descriptions are actually circuit -generators when viewed from a synthesis viewpoint, in that the language -elements of Haskell, such as choice, can be used to guide the circuit -generation. If a developer wants to insert a choice element inside an actual -circuit he will have to specify this explicitly as a component. In this -respect \CLaSH\ differs from Lava, in that all the choice elements, such as -case-statements and patter matching, are synthesized to choice elements in the -eventual circuit. As such, richer control structures can both be specified and -synthesized in \CLaSH\ compared to any of the languages mentioned in this -section. - -The merits of polymorphic typing, combined with higher-order functions, are -now also recognized in the `main-stream' hardware description languages, -exemplified by the new \VHDL\ 2008 standard~\cite{VHDL2008}. \VHDL-2008 has -support to specify types as generics, thus allowing a developer to describe -polymorphic components. Note that those types still require an explicit -generic map, whereas type-inference and type-specialization are implicit in -\CLaSH. - -Wired~\cite{Wired},, T-Ruby~\cite{T-Ruby}, Hydra~\cite{Hydra}. - -A functional language designed specifically for hardware design is -$re{\mathit{FL}}^{ect}$~\cite{reFLect}, which draws experience from earlier -language called \textsc{fl}~\cite{FL} to la - -% An example of a floating figure using the graphicx package. -% Note that \label must occur AFTER (or within) \caption. -% For figures, \caption should occur after the \includegraphics. -% Note that IEEEtran v1.7 and later has special internal code that -% is designed to preserve the operation of \label within \caption -% even when the captionsoff option is in effect. However, because -% of issues like this, it may be the safest practice to put all your -% \label just after \caption rather than within \caption{}. -% -% Reminder: the "draftcls" or "draftclsnofoot", not "draft", class -% option should be used if it is desired that the figures are to be -% displayed while in draft mode. -% -%\begin{figure}[!t] -%\centering -%\includegraphics[width=2.5in]{myfigure} -% where an .eps filename suffix will be assumed under latex, -% and a .pdf suffix will be assumed for pdflatex; or what has been declared -% via \DeclareGraphicsExtensions. -%\caption{Simulation Results} -%\label{fig_sim} -%\end{figure} - -% Note that IEEE typically puts floats only at the top, even when this -% results in a large percentage of a column being occupied by floats. - - -% An example of a double column floating figure using two subfigures. -% (The subfig.sty package must be loaded for this to work.) -% The subfigure \label commands are set within each subfloat command, the -% \label for the overall figure must come after \caption. -% \hfil must be used as a separator to get equal spacing. -% The subfigure.sty package works much the same way, except \subfigure is -% used instead of \subfloat. -% -%\begin{figure*}[!t] -%\centerline{\subfloat[Case I]\includegraphics[width=2.5in]{subfigcase1}% -%\label{fig_first_case}} -%\hfil -%\subfloat[Case II]{\includegraphics[width=2.5in]{subfigcase2}% -%\label{fig_second_case}}} -%\caption{Simulation results} -%\label{fig_sim} -%\end{figure*} -% -% Note that often IEEE papers with subfigures do not employ subfigure -% captions (using the optional argument to \subfloat), but instead will -% reference/describe all of them (a), (b), etc., within the main caption. - - -% An example of a floating table. Note that, for IEEE style tables, the -% \caption command should come BEFORE the table. Table text will default to -% \footnotesize as IEEE normally uses this smaller font for tables. -% The \label must come after \caption as always. -% -%\begin{table}[!t] -%% increase table row spacing, adjust to taste -%\renewcommand{\arraystretch}{1.3} -% if using array.sty, it might be a good idea to tweak the value of -% \extrarowheight as needed to properly center the text within the cells -%\caption{An Example of a Table} -%\label{table_example} -%\centering -%% Some packages, such as MDW tools, offer better commands for making tables -%% than the plain LaTeX2e tabular which is used here. -%\begin{tabular}{|c||c|} -%\hline -%One & Two\\ -%\hline -%Three & Four\\ -%\hline -%\end{tabular} -%\end{table} - - -% Note that IEEE does not put floats in the very first column - or typically -% anywhere on the first page for that matter. Also, in-text middle ("here") -% positioning is not used. Most IEEE journals/conferences use top floats -% exclusively. Note that, LaTeX2e, unlike IEEE journals/conferences, places -% footnotes above bottom floats. This can be corrected via the \fnbelowfloat -% command of the stfloats package. - - - -\section{Conclusion} -The conclusion goes here. - - - - -% conference papers do not normally have an appendix - - -% use section* for acknowledgement -\section*{Acknowledgment} - - -The authors would like to thank... - - - - - -% trigger a \newpage just before the given reference -% number - used to balance the columns on the last page -% adjust value as needed - may need to be readjusted if -% the document is modified later -%\IEEEtriggeratref{8} -% The "triggered" command can be changed if desired: -%\IEEEtriggercmd{\enlargethispage{-5in}} - -% references section - -% can use a bibliography generated by BibTeX as a .bbl file -% BibTeX documentation can be easily obtained at: -% http://www.ctan.org/tex-archive/biblio/bibtex/contrib/doc/ -% The IEEEtran BibTeX style support page is at: -% http://www.michaelshell.org/tex/ieeetran/bibtex/ -\bibliographystyle{IEEEtran} -% argument is your BibTeX string definitions and bibliography database(s) -\bibliography{IEEEabrv,cλash.bib} -% -% manually copy in the resultant .bbl file -% set second argument of \begin to the number of references -% (used to reserve space for the reference number labels box) -% \begin{thebibliography}{1} -% -% \bibitem{IEEEhowto:kopka} -% H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus -% 0.5em minus 0.4em\relax Harlow, England: Addison-Wesley, 1999. -% -% \end{thebibliography} - - - - -% that's all folks -\end{document} - -% vim: set ai sw=2 sts=2 expandtab: