Abstract
Original language | Undefined |
---|---|
Awarding Institution |
|
Supervisors/Advisors |
|
Sponsors | |
Date of Award | 23 Jan 2015 |
Place of Publication | Enschede |
Print ISBNs | 978-90-365-3803-9 |
DOIs | |
State | Published - 23 Jan 2015 |
Fingerprint
Keywords
- EC Grant Agreement nr.: FP7/610686
- EC Grant Agreement nr.: FP7/248465
- EWI-23939
- Rewrite Systems
- Digital Circuits
- Lambda calculus
- IR-93962
- Functional Programming
- FPGA
- Hardware
- Haskell
- METIS-308711
Cite this
}
Digital circuit in CλaSH: functional specifications and type-directed synthesis. / Baaij, C.P.R.
Enschede, 2015. 208 p.Research output: Scientific › PhD Thesis - Research UT, graduation UT
TY - THES
T1 - Digital circuit in CλaSH: functional specifications and type-directed synthesis
AU - Baaij,C.P.R.
N1 - eemcs-eprint-23939
PY - 2015/1/23
Y1 - 2015/1/23
N2 - Over the last three decades, the number of transistors used in microchips has increased by three orders of magnitude, from millions to billions. The productivity of the designers, however, lags behind. Managing to implement complex algorithms, while keeping non-functional properties within desired bounds, and thoroughly verifying the design against its specification, are the main difficulties in circuit design. As a motivation for our work we make a qualitative analysis of the tools available to circuit designers. Here we see that progress has been slow, and that the same techniques have been used for over 20 years. We claim that functional languages can be used to raise the abstraction level in circuit design. Especially higher-order functional languages, where functions are first-class and can be manipulated by other functions, offer a single abstraction mechanism that can capture many design patterns. This thesis explores the idea of using the functional language Haskell directly as a hardware specification language, and move beyond the limitations of embedded languages. Additionally, we can use normal functions from existing Haskell libraries to model the behaviour of our circuits. This thesis describes the inner workings of our C$\lambda$aSH compiler, which translates the aforementioned circuit descriptions written in Haskell to low-level descriptions in VHDL. The challenge then becomes the reduction of the higher-level abstractions in the descriptions to a form where synthesis is feasible. This thesis describes a term rewrite system (with bound variables) to achieve this reduction. We prove that this term rewrite system always reduces a polymorphic, higher-order circuit description to a synthesisable variant. Even when descriptions use high-level abstractions, the C$\lambda$aSH compiler can synthesize efficient circuits. Case studies show that circuits designed in Haskell, and synthesized with the C?aSH compiler, are on par with hand-written VHDL, in both area and gate propagation delay. This thesis thus shows the merits of using a modern functional language for circuit design. The advanced type system and higher-order functions allow us to design circuits that have the desired property of being correct-by-construction. Finally, our synthesis approach enables us to derive efficient circuits from descriptions that use high-level abstractions.
AB - Over the last three decades, the number of transistors used in microchips has increased by three orders of magnitude, from millions to billions. The productivity of the designers, however, lags behind. Managing to implement complex algorithms, while keeping non-functional properties within desired bounds, and thoroughly verifying the design against its specification, are the main difficulties in circuit design. As a motivation for our work we make a qualitative analysis of the tools available to circuit designers. Here we see that progress has been slow, and that the same techniques have been used for over 20 years. We claim that functional languages can be used to raise the abstraction level in circuit design. Especially higher-order functional languages, where functions are first-class and can be manipulated by other functions, offer a single abstraction mechanism that can capture many design patterns. This thesis explores the idea of using the functional language Haskell directly as a hardware specification language, and move beyond the limitations of embedded languages. Additionally, we can use normal functions from existing Haskell libraries to model the behaviour of our circuits. This thesis describes the inner workings of our C$\lambda$aSH compiler, which translates the aforementioned circuit descriptions written in Haskell to low-level descriptions in VHDL. The challenge then becomes the reduction of the higher-level abstractions in the descriptions to a form where synthesis is feasible. This thesis describes a term rewrite system (with bound variables) to achieve this reduction. We prove that this term rewrite system always reduces a polymorphic, higher-order circuit description to a synthesisable variant. Even when descriptions use high-level abstractions, the C$\lambda$aSH compiler can synthesize efficient circuits. Case studies show that circuits designed in Haskell, and synthesized with the C?aSH compiler, are on par with hand-written VHDL, in both area and gate propagation delay. This thesis thus shows the merits of using a modern functional language for circuit design. The advanced type system and higher-order functions allow us to design circuits that have the desired property of being correct-by-construction. Finally, our synthesis approach enables us to derive efficient circuits from descriptions that use high-level abstractions.
KW - EC Grant Agreement nr.: FP7/610686
KW - EC Grant Agreement nr.: FP7/248465
KW - EWI-23939
KW - Rewrite Systems
KW - Digital Circuits
KW - Lambda calculus
KW - IR-93962
KW - Functional Programming
KW - FPGA
KW - Hardware
KW - Haskell
KW - METIS-308711
U2 - 10.3990/1.9789036538039
DO - 10.3990/1.9789036538039
M3 - PhD Thesis - Research UT, graduation UT
SN - 978-90-365-3803-9
ER -