1 % This file was created with JabRef 2.5.
5 author = {Emil Axelsson and Koen Claessen and Mary Sheeran},
6 title = {{Wired: Wire-Aware Circuit Design}},
7 booktitle = {{Proceedings of Conference on Correct Hardware Design and VeriÞcation
11 series = {{Lecture Notes in Computer Science}},
13 publisher = {Springer Verlag},
15 timestamp = {2010.01.21}
19 author = {Bjesse, Per and Claessen, Koen and Sheeran, Mary and Singh, Satnam},
20 title = {{Lava: hardware design in Haskell}},
21 booktitle = {{ICFP '98: Proceedings of the third ACM SIGPLAN international conference
22 on Functional programming}},
25 address = {New York, NY, USA},
27 doi = {http://doi.acm.org/10.1145/289423.289440},
28 isbn = {1-58113-024-4},
29 location = {Baltimore, Maryland, United States},
31 timestamp = {2010.01.20}
34 @INPROCEEDINGS{Cardelli1981,
35 author = {Luca Cardelli and Gordon Plotkin},
36 title = {{An Algebraic Approach to VLSI Design}},
37 booktitle = {{Proceedings of the VLSI 81 International Conference}},
41 timestamp = {2010.01.25}
45 author = {Byron Cook and John Launchbury and John Matthews},
46 title = {{Specifying superscalar microprocessors in Hawk}},
47 booktitle = {{Formal Techniques for Hardware and Hardware-like Systems}},
50 timestamp = {2010.01.20}
53 @INPROCEEDINGS{reductioncircuit,
54 author = {M. E. T. Gerards and J. Kuper and A. B. J. Kokkeler and E. Molenkamp},
55 title = {Streaming Reduction Circuit},
56 booktitle = {Proceedings of the 12th EUROMICRO Conference on Digital System Design,
57 Architectures, Methods and Tools, Patras, Greece},
60 address = {Los Alamitos},
62 publisher = {IEEE Computer Society Press},
63 abstract = {Reduction circuits are used to reduce rows of ?oating point values
64 to single values. Binary ?oating point operators often have deep
65 pipelines, which may cause hazards when many consecutive rows have
66 to be reduced. We present an algorithm by which any number of consecutive
67 rows of arbitrary lengths can be reduced by a pipelined commutative
68 and associative binary operator in an efficient manner. The algorithm
69 is simple to implement, has a low latency, produces results in-order,
70 and requires only small buffers. Besides, it uses only a single pipeline
71 for the involved operation. The complexity of the algorithm depends
72 on the depth of the pipeline, not on the length of the input rows.
73 In this paper we discuss an implementation of this algorithm and
74 we prove its correctness.},
76 event_dates = {27-29 Aug 2009},
77 event_type = {Conference},
78 howpublished = {http://eprints.eemcs.utwente.nl/17041/},
79 id_number = {10.1109/DSD.2009.141},
80 international = {Yes},
81 isbn_13 = {978-0-7695-3782-5},
82 ispublished = {Published},
83 location = {Patras, Greece},
85 official_url = {http://dx.doi.org/10.1109/DSD.2009.141},
89 research_groups = {EWI-CAES: Computer Architecture for Embedded Systems},
90 research_programs = {CTIT-WiSe: Wireless and Sensor Systems},
91 research_projects = {EASY: Embedded Adaptive Streaming sYstems},
92 timestamp = {2010.02.26}
96 author = {Grundy,Jim and Melham,Tom and O'Leary,John},
97 title = {{A reflective functional language for hardware design and theorem
99 journal = {Journal of Functional Programming},
104 doi = {10.1017/S0956796805005757},
106 timestamp = {2010.01.21}
109 @INPROCEEDINGS{DAISY,
110 author = {Johnson, Steven D.},
111 title = {Applicative programming and digital design},
112 booktitle = {POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on
113 Principles of programming languages},
116 address = {New York, NY, USA},
118 doi = {http://doi.acm.org/10.1145/800017.800533},
119 isbn = {0-89791-125-3},
120 location = {Salt Lake City, Utah, United States},
122 timestamp = {2010.01.25}
126 author = {Jones, G. and Sheeran, M.},
127 title = {{Circuit Design in Ruby}},
128 booktitle = {{Formal Methods for VLSI Design}},
130 address = {Lyngby, Denmark},
131 publisher = {Elsevier Science Publishers},
132 citeulike-article-id = {304676},
133 journal = {Circuit Design in Ruby},
134 keywords = {jones90},
136 posted-at = {2005-08-26 18:08:07},
138 timestamp = {2010.01.20}
142 author = {Yanbing Li and Leeser, M.},
143 title = {{HML, a novel hardware description language and its translation to
145 journal = {{Very Large Scale Integration (VLSI) Systems, IEEE Transactions on}},
151 doi = {10.1109/92.820756},
153 keywords = {ML language, hardware description languages, type theoryHML, SML functional
154 programming language, VHDL translation, digital design, hardware
155 description language, polymorphic type, translator, type checker,
158 timestamp = {2010.01.20}
162 author = {Yanbing Li and Leeser, M.},
163 title = {{HML: an innovative hardware description language and its translation
165 booktitle = {{Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL
166 '95/VLSI '95., IFIP International Conference on Hardware Description
167 Languages; IFIP International Conference on Very Large Scale Integration.,
168 Asian and South Pacific}},
172 doi = {10.1109/ASPDAC.1995.486388},
173 keywords = {abstract data types, functional languages, functional programming,
174 hardware description languagesHML, VHDL, advanced type checking,
175 functional programming language, hardware description language, polymorphic
176 types, type inference},
178 timestamp = {2010.01.20}
182 author = {{Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Seger}},
183 title = {{Lifted-FL: A Pragmatic Implementation of Combined Model Checking
184 and Theorem Proving}},
185 booktitle = {{Proceedings of 12th International Conference on Theorem Proving
186 in Higher Order Logics}},
191 publisher = {Springer Verlag},
193 timestamp = {2010.01.26}
196 @INPROCEEDINGS{Hawk1,
197 author = {Matthews, J. and Cook, B. and Launchbury, J.},
198 title = {{Microprocessor specification in Hawk}},
199 booktitle = {{Proceedings of 1998 International Conference on Computer Languages}},
203 abstract = {Modern microprocessors require an immense investment of time and effort
204 to create and verify, from the high level architectural design downwards.
205 We are exploring ways to increase the productivity of design engineers
206 by creating a domain specific language for specifying and simulating
207 processor architectures. We believe that the structuring principles
208 used in modern functional programming languages, such as static typing,
209 parametric polymorphism, first class functions, and lazy evaluation
210 provide a good formalism for such a domain specific language, and
211 have made initial progress by creating a library on top of the functional
212 language Haskell. We have specified the integer subset of an out
213 of order, superscalar DLX microprocessor, with register renaming,
214 a reorder buffer, a global reservation station, multiple execution
215 units, and speculative branch execution. Two key abstractions of
216 this library are the signal abstract data type (ADT), which models
217 the simulation history of a wire, and the transaction ADT, which
218 models the state of an entire instruction as it travels through the
220 doi = {10.1109/ICCL.1998.674160},
222 keywords = {abstract data types, formal specification, functional languages, functional
223 programming, hardware description languages, microprocessor chips,
224 software librariesHawk language, design engineers, domain specific
225 language, first class functions, functional language Haskell, functional
226 programming languages, global reservation station, high level architectural
227 design, integer subset, lazy evaluation, microprocessor specification,
228 multiple execution units, out of order superscalar DLX microprocessor,
229 parametric polymorphism, processor architecture simulation, register
230 renaming, reorder buffer, signal abstract data type, simulation history,
231 software library, speculative branch execution, static typing,, structuring
232 principles, transaction ADT},
234 timestamp = {2010.01.20}
238 author = {Meshkinpour, F. and Ercegovac, M. D.},
239 title = {A functional language for description and design of digital systems:
240 sequential constructs},
241 booktitle = {DAC '85: Proceedings of the 22nd ACM/IEEE Design Automation Conference},
244 address = {New York, NY, USA},
246 doi = {http://doi.acm.org/10.1145/317825.317865},
247 isbn = {0-8186-0635-5},
248 location = {Las Vegas, Nevada, United States},
250 timestamp = {2010.01.25}
253 @INPROCEEDINGS{Hydra,
254 author = {John O'Donnell},
255 title = {{From Transistors to Computer Architecture: Teaching Functional Circuit
256 Specification in Hydra}},
257 booktitle = {{Proceedings of the First International Symposium on Funtional Programming
258 Languages in Education}},
261 series = {Lecture Notes in Computer Science},
263 publisher = {Springer-Verlag},
265 timestamp = {2010.01.21}
269 author = {Ingo Sander and Axel Jantsch},
270 title = {{System Modeling and Transformational Design Refinement in ForSyDe}},
271 journal = {{IEEE Transactions on Computer-Aided Design of Integrated Circuits
280 timestamp = {2010.01.21}
283 @INPROCEEDINGS{ForSyDe1,
284 author = {Sander, Ingo and Jantsch, Axel},
285 title = {{Transformation based communication and clock domain refinement for
287 booktitle = {{DAC '02: Proceedings of the 39th annual Design Automation Conference}},
290 address = {New York, NY, USA},
292 doi = {http://doi.acm.org/10.1145/513918.513992},
293 isbn = {1-58113-461-4},
294 location = {New Orleans, Louisiana, USA},
296 timestamp = {2010.01.20}
299 @INPROCEEDINGS{T-Ruby,
300 author = {Sharp, Robin and Rasmussen, Ole},
301 title = {{Using a language of functions and relations for VLSI specification}},
302 booktitle = {FPCA '95: Proceedings of the seventh international conference on
303 Functional programming languages and computer architecture},
306 address = {New York, NY, USA},
308 doi = {http://doi.acm.org/10.1145/224164.224180},
309 isbn = {0-89791-719-7},
310 location = {La Jolla, California, United States},
312 timestamp = {2010.01.21}
316 author = {Sheeran, Mary},
317 title = {{$\mu$FP, a language for VLSI design}},
318 booktitle = {{LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional
322 address = {New York, NY, USA},
324 doi = {http://doi.acm.org/10.1145/800055.802026},
325 isbn = {0-89791-142-3},
326 location = {Austin, Texas, United States},
328 timestamp = {2010.01.20}
332 author = {Strachey, Christopher},
333 title = {Fundamental Concepts in Programming Languages},
334 howpublished = {Lecture Notes, International Summer School in Computer Programming,
338 note = {Reprinted in {\em Higher-Order and Symbolic Computation}, 13(1/2),
341 timestamp = {2010.02.24}
345 author = {{The GHC Team}},
346 title = {{The Glasgow Haskell Compiler}},
347 url = {http://www.haskell.org/ghc/},
349 timestamp = {2010.02.25}
353 title = {{Haskell 98 language and libraries}},
355 editor = {Simon Peyton Jones},
359 series = {{Journal of Functional Programming}},
360 booktitle = {{Journal of Functional Programming}},
361 journal = {Journal of Functional Programming},
363 timestamp = {2010.01.29}
367 title = {{VHDL Language Reference Manual}},
368 organization = {IEEE},
369 number = {1076-2008},
372 timestamp = {2009.11.17}
376 title = {{Verilog Hardware Description Languages}},
377 organization = {{IEEE}},
378 number = {1365-2005},
381 timestamp = {2010.01.29}
384 @comment{jabref-meta: selector_publisher:}
386 @comment{jabref-meta: selector_author:}
388 @comment{jabref-meta: selector_journal:}
390 @comment{jabref-meta: selector_keywords:}