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}
95 @UNPUBLISHED{kansaslava,
96 author = {Andy Gill and T. Bull and Garrin Kimmell and Erik Perrins and Ed
98 title = {Introducing Kansas Lava},
99 note = {Submitted to The International Symposia on Implementation and Application
100 of Functional Languages (IFL){\textquoteright}09},
103 abstract = {Kansas Lava is a domain specific language for hardware description.
104 Though there have been a number of previous implementations of Lava,
105 we have found the design space rich, with unexplored choices. We
106 use a direct (Chalmers style) specification of circuits, and make
107 significant use of Haskell overloading of standard classes, leading
108 to concise circuit descriptions. Kansas Lava supports both simulation
109 (inside GHCi), and execution via VHDL, by having a dual shallow and
110 deep embedding inside our Signal type. We also have a lightweight
111 sized-type mechanism, allowing for MATLAB style matrix based specifications
112 to be directly expressed in Kansas Lava.},
113 journal = {Submitted to IFL{\textquoteright}09},
115 timestamp = {2010.03.11},
116 url = {http://ittc.ku.edu/~andygill/papers/kansas-lava-ifl09.pdf}
120 author = {Grundy,Jim and Melham,Tom and O'Leary,John},
121 title = {{A reflective functional language for hardware design and theorem
123 journal = {Journal of Functional Programming},
128 doi = {10.1017/S0956796805005757},
130 timestamp = {2010.01.21}
133 @BOOK{lambdacalculus,
134 title = {{The Lambda Calculus: its Syntax and Semantics}},
135 publisher = {{Elsevier Science}},
137 author = {{H.P. Barendregt}},
139 series = {{Studies in Logic and the Foundations of Mathematics}},
140 edition = {{Revised}},
142 timestamp = {2010.03.02}
145 @INPROCEEDINGS{DAISY,
146 author = {Johnson, Steven D.},
147 title = {Applicative programming and digital design},
148 booktitle = {POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on
149 Principles of programming languages},
152 address = {New York, NY, USA},
154 doi = {http://doi.acm.org/10.1145/800017.800533},
155 isbn = {0-89791-125-3},
156 location = {Salt Lake City, Utah, United States},
158 timestamp = {2010.01.25}
162 author = {Jones, G. and Sheeran, M.},
163 title = {{Circuit Design in Ruby}},
164 booktitle = {{Formal Methods for VLSI Design}},
166 address = {Lyngby, Denmark},
167 publisher = {Elsevier Science Publishers},
168 citeulike-article-id = {304676},
169 journal = {Circuit Design in Ruby},
170 keywords = {jones90},
172 posted-at = {2005-08-26 18:08:07},
174 timestamp = {2010.01.20}
178 author = {Yanbing Li},
179 title = {{HML: An Innovative Hardware Description Language and Its Translation
181 school = {Cornell University},
185 timestamp = {2010.03.08}
189 author = {Yanbing Li and Leeser, M.},
190 title = {{HML, a novel hardware description language and its translation to
192 journal = {{Very Large Scale Integration (VLSI) Systems, IEEE Transactions on}},
198 doi = {10.1109/92.820756},
200 keywords = {ML language, hardware description languages, type theoryHML, SML functional
201 programming language, VHDL translation, digital design, hardware
202 description language, polymorphic type, translator, type checker,
205 timestamp = {2010.01.20}
209 author = {Yanbing Li and Leeser, M.},
210 title = {{HML: an innovative hardware description language and its translation
212 booktitle = {{Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL
213 '95/VLSI '95., IFIP International Conference on Hardware Description
214 Languages; IFIP International Conference on Very Large Scale Integration.,
215 Asian and South Pacific}},
219 doi = {10.1109/ASPDAC.1995.486388},
220 keywords = {abstract data types, functional languages, functional programming,
221 hardware description languagesHML, VHDL, advanced type checking,
222 functional programming language, hardware description language, polymorphic
223 types, type inference},
225 timestamp = {2010.01.20}
229 author = {{Mark D. Aagaard and Robert B. Jones and Carl-Johan H. Seger}},
230 title = {{Lifted-FL: A Pragmatic Implementation of Combined Model Checking
231 and Theorem Proving}},
232 booktitle = {{Proceedings of 12th International Conference on Theorem Proving
233 in Higher Order Logics}},
238 publisher = {Springer Verlag},
240 timestamp = {2010.01.26}
243 @INPROCEEDINGS{Hawk1,
244 author = {Matthews, J. and Cook, B. and Launchbury, J.},
245 title = {{Microprocessor specification in Hawk}},
246 booktitle = {{Proceedings of 1998 International Conference on Computer Languages}},
250 abstract = {Modern microprocessors require an immense investment of time and effort
251 to create and verify, from the high level architectural design downwards.
252 We are exploring ways to increase the productivity of design engineers
253 by creating a domain specific language for specifying and simulating
254 processor architectures. We believe that the structuring principles
255 used in modern functional programming languages, such as static typing,
256 parametric polymorphism, first class functions, and lazy evaluation
257 provide a good formalism for such a domain specific language, and
258 have made initial progress by creating a library on top of the functional
259 language Haskell. We have specified the integer subset of an out
260 of order, superscalar DLX microprocessor, with register renaming,
261 a reorder buffer, a global reservation station, multiple execution
262 units, and speculative branch execution. Two key abstractions of
263 this library are the signal abstract data type (ADT), which models
264 the simulation history of a wire, and the transaction ADT, which
265 models the state of an entire instruction as it travels through the
267 doi = {10.1109/ICCL.1998.674160},
269 keywords = {abstract data types, formal specification, functional languages, functional
270 programming, hardware description languages, microprocessor chips,
271 software librariesHawk language, design engineers, domain specific
272 language, first class functions, functional language Haskell, functional
273 programming languages, global reservation station, high level architectural
274 design, integer subset, lazy evaluation, microprocessor specification,
275 multiple execution units, out of order superscalar DLX microprocessor,
276 parametric polymorphism, processor architecture simulation, register
277 renaming, reorder buffer, signal abstract data type, simulation history,
278 software library, speculative branch execution, static typing,, structuring
279 principles, transaction ADT},
281 timestamp = {2010.01.20}
285 author = {Meshkinpour, F. and Ercegovac, M. D.},
286 title = {A functional language for description and design of digital systems:
287 sequential constructs},
288 booktitle = {DAC '85: Proceedings of the 22nd ACM/IEEE Design Automation Conference},
291 address = {New York, NY, USA},
293 doi = {http://doi.acm.org/10.1145/317825.317865},
294 isbn = {0-8186-0635-5},
295 location = {Las Vegas, Nevada, United States},
297 timestamp = {2010.01.25}
300 @INCOLLECTION{Bluespec,
301 author = {Rishiyur S. Nikhil},
302 title = {{Bluespec: A General-Purpose Approach to High-Level Synthesis Based
303 on Parallel Atomic Transactions}},
304 booktitle = {{High-Level Synthesis - From Algorithm to Digital Circuit}},
305 publisher = {Springer Netherlands},
307 editor = {{Philippe Coussy and Adam Morawiec}},
310 timestamp = {2010.03.09}
313 @INPROCEEDINGS{Hydra,
314 author = {John O'Donnell},
315 title = {{From Transistors to Computer Architecture: Teaching Functional Circuit
316 Specification in Hydra}},
317 booktitle = {{Proceedings of the First International Symposium on Funtional Programming
318 Languages in Education}},
321 series = {Lecture Notes in Computer Science},
323 publisher = {Springer-Verlag},
325 timestamp = {2010.01.21}
329 author = {Ingo Sander and Axel Jantsch},
330 title = {{System Modeling and Transformational Design Refinement in ForSyDe}},
331 journal = {{IEEE Transactions on Computer-Aided Design of Integrated Circuits
340 timestamp = {2010.01.21}
343 @INPROCEEDINGS{ForSyDe1,
344 author = {Sander, Ingo and Jantsch, Axel},
345 title = {{Transformation based communication and clock domain refinement for
347 booktitle = {{DAC '02: Proceedings of the 39th annual Design Automation Conference}},
350 address = {New York, NY, USA},
352 doi = {http://doi.acm.org/10.1145/513918.513992},
353 isbn = {1-58113-461-4},
354 location = {New Orleans, Louisiana, USA},
356 timestamp = {2010.01.20}
359 @INPROCEEDINGS{T-Ruby,
360 author = {Sharp, Robin and Rasmussen, Ole},
361 title = {{Using a language of functions and relations for VLSI specification}},
362 booktitle = {FPCA '95: Proceedings of the seventh international conference on
363 Functional programming languages and computer architecture},
366 address = {New York, NY, USA},
368 doi = {http://doi.acm.org/10.1145/224164.224180},
369 isbn = {0-89791-719-7},
370 location = {La Jolla, California, United States},
372 timestamp = {2010.01.21}
376 author = {Sheeran, Mary},
377 title = {{$\mu$FP, a language for VLSI design}},
378 booktitle = {{LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional
382 address = {New York, NY, USA},
384 doi = {http://doi.acm.org/10.1145/800055.802026},
385 isbn = {0-89791-142-3},
386 location = {Austin, Texas, United States},
388 timestamp = {2010.01.20}
392 author = {Strachey, Christopher},
393 title = {Fundamental Concepts in Programming Languages},
394 howpublished = {Lecture Notes, International Summer School in Computer Programming,
398 note = {Reprinted in {\em Higher-Order and Symbolic Computation}, 13(1/2),
401 timestamp = {2010.02.24}
404 @INPROCEEDINGS{Sulzmann2007,
405 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton
406 and Donnelly, Kevin},
407 title = {{System F with Type Equality Coercions}},
408 booktitle = {{TLDI '07: Proceedings of the 2007 ACM SIGPLAN international workshop
409 on Types in languages design and implementation, Nice, France}},
412 address = {{New York, NY, USA}},
415 doi = {http://doi.acm.org/10.1145/1190315.1190324},
416 isbn = {1-59593-393-X},
417 location = {Nice, Nice, France},
419 timestamp = {2009.10.23}
423 author = {{The GHC Team}},
424 title = {{The Glasgow Haskell Compiler}},
425 url = {http://www.haskell.org/ghc/},
427 timestamp = {2010.02.25}
431 title = {{Haskell 98 language and libraries}},
433 editor = {Simon Peyton Jones},
437 series = {{Journal of Functional Programming}},
438 booktitle = {{Journal of Functional Programming}},
439 journal = {Journal of Functional Programming},
441 timestamp = {2010.01.29}
445 title = {{VHDL Language Reference Manual}},
446 organization = {IEEE},
447 number = {1076-2008},
450 timestamp = {2009.11.17}
454 title = {{Verilog Hardware Description Languages}},
455 organization = {{IEEE}},
456 number = {1365-2005},
459 timestamp = {2010.01.29}
462 @comment{jabref-meta: selector_publisher:}
464 @comment{jabref-meta: selector_author:}
466 @comment{jabref-meta: selector_journal:}
468 @comment{jabref-meta: selector_keywords:}