Projects per year
Abstract
We explore the use of dependent types to address the disparity between the theory and the practical hardware description of DSP circuits. After discussing an approach to modeling synchronous circuit behaviour in Idris (a pure functional language with dependent types), two DSP case studies are introduced — an FIR filter with optimal wordlengths and a CIC decimator with register pruning. Both of these scenarios prove difficult to describe in a parameterised fashion using traditional HDLs and, as such, many implementations rely on ad hoc circuit generators which are challenging to test and evaluate. This work demonstrates that such circuits are readily described in an environment with dependent types. Dependent types can also encode various contracts between the IP designer and its user. These contracts are automatically verified by the Idris type checker before compilation, precluding many common mistakes in IP development and evaluation.
Original language | English |
---|---|
Title of host publication | 2021 IEEE International Midwest Symposium on Circuits and Systems, MWSCAS 2021 - Proceedings |
Place of Publication | Piscataway, NJ |
Publisher | IEEE |
Pages | 787-791 |
Number of pages | 5 |
ISBN (Electronic) | 9781665424615 |
ISBN (Print) | 9781665424622 |
DOIs | |
Publication status | Published - 13 Sept 2021 |
Event | 64th IEEE International Midwest Symposium on Circuits and Systems - Michigan State University, East Lansing, United States Duration: 9 Aug 2021 → 11 Aug 2021 Conference number: 64th https://www.mwscas2021.org/ |
Publication series
Name | IEEE International Midwest Symposium on Circuits and Systems (MWSCAS) |
---|---|
Publisher | IEEE |
ISSN (Print) | 1548-3746 |
ISSN (Electronic) | 1558-3899 |
Conference
Conference | 64th IEEE International Midwest Symposium on Circuits and Systems |
---|---|
Abbreviated title | MWSCAS 2021 |
Country/Territory | United States |
City | East Lansing |
Period | 9/08/21 → 11/08/21 |
Internet address |
Keywords
- digital signal processing (DSP)
- field programmable gate arrays (FPGA)
- dependent types
- verification
- digital circuits
- functional programming
Fingerprint
Dive into the research topics of 'On applications of dependent types to parameterised digital signal processing circuits'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Doctoral Training Partnership (DTP 2016-2017 University of Strathclyde) | Ramsay, Craig
Crockett, L. (Principal Investigator), Stewart, R. (Co-investigator) & Ramsay, C. (Research Co-investigator)
EPSRC (Engineering and Physical Sciences Research Council)
1/10/17 → 18/01/24
Project: Research Studentship - Internally Allocated
Datasets
-
Data for: "On Applications of Dependent Types to Parameterised Digital Signal Processing Circuits"
Ramsay, C. (Creator), Crockett, L. H. (Supervisor) & Stewart, R. (Supervisor), University of Strathclyde, 19 Apr 2021
DOI: 10.15129/db040cb9-9e48-4823-8616-cbc0ace1b6cd, https://github.com/cramsay/idris_dsp_circuits
Dataset