Abstract
Original language  Undefined 

Awarding Institution 

Supervisors/Advisors 

Sponsors  
Date of Award  23 Jan 2015 
Place of Publication  Enschede 
Print ISBNs  9789036538039 
DOIs  
State  Published  23 Jan 2015 
Fingerprint
Keywords
 EC Grant Agreement nr.: FP7/610686
 EC Grant Agreement nr.: FP7/248465
 EWI23939
 Rewrite Systems
 Digital Circuits
 Lambda calculus
 IR93962
 Functional Programming
 FPGA
 Hardware
 Haskell
 METIS308711
Cite this
}
Digital circuit in CλaSH: functional specifications and typedirected 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 typedirected synthesis
AU  Baaij,C.P.R.
N1  eemcseprint23939
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 nonfunctional 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 higherorder functional languages, where functions are firstclass 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 lowlevel descriptions in VHDL. The challenge then becomes the reduction of the higherlevel 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, higherorder circuit description to a synthesisable variant. Even when descriptions use highlevel 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 handwritten 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 higherorder functions allow us to design circuits that have the desired property of being correctbyconstruction. Finally, our synthesis approach enables us to derive efficient circuits from descriptions that use highlevel 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 nonfunctional 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 higherorder functional languages, where functions are firstclass 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 lowlevel descriptions in VHDL. The challenge then becomes the reduction of the higherlevel 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, higherorder circuit description to a synthesisable variant. Even when descriptions use highlevel 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 handwritten 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 higherorder functions allow us to design circuits that have the desired property of being correctbyconstruction. Finally, our synthesis approach enables us to derive efficient circuits from descriptions that use highlevel abstractions.
KW  EC Grant Agreement nr.: FP7/610686
KW  EC Grant Agreement nr.: FP7/248465
KW  EWI23939
KW  Rewrite Systems
KW  Digital Circuits
KW  Lambda calculus
KW  IR93962
KW  Functional Programming
KW  FPGA
KW  Hardware
KW  Haskell
KW  METIS308711
U2  10.3990/1.9789036538039
DO  10.3990/1.9789036538039
M3  PhD Thesis  Research UT, graduation UT
SN  9789036538039
ER 