University of Twente Student Theses
Beating Logic: Dependent types with time for synchronous circuits
Elderen, Sybren van (2014) Beating Logic: Dependent types with time for synchronous circuits.
|
PDF
490kB |
| Abstract: | Existing functional structural hardware description languages are based on single-cycle descriptions, which makes it difficult to understand the computational essence of the circuit. Multi-cycle descriptions may provide more intuitive descriptions. In this thesis, we present a system which allows such multi-cycle descriptions through the use of timed types. This means that the temporal spread of a computation is encoded in its type. The innovation of this thesis is that we use dependent types as a basis for the timed types. This allows us to describe an instance of a computation, and abstract it over time to form a circuit description. As a side-effect, we gain the potential to describe time varying circuits. We show that by adding a simplistic theorem prover, we gain a rudimentary ability to check the synchronisation of circuits without the need for explicit delay mechanisms. As a proof of concept, we have implemented the type system. Aside from validating the use of dependent types as a basis for timed types, this revealed that the definition of timed sequences affects the folding behaviour over those sequences, and the kinds of circuits that can be described with those folds. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Embedded Systems MSc (60331) |
| Link to this item: | https://purl.utwente.nl/essays/65915 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page