On applications of dependent types to parameterised digital signal processing circuits

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

2 Downloads (Pure)

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 languageEnglish
Title of host publication2021 IEEE International Midwest Symposium on Circuits and Systems (MWSCAS)
Place of PublicationPiscataway, NJ
PublisherIEEE
Pages787-791
Number of pages5
ISBN (Electronic)9781665424615
ISBN (Print)9781665424622
DOIs
Publication statusPublished - 13 Sep 2021
Event64th IEEE International Midwest Symposium on Circuits and Systems - Michigan State University, East Lansing, United States
Duration: 9 Aug 202111 Aug 2021
Conference number: 64th
https://www.mwscas2021.org/

Publication series

NameIEEE International Midwest Symposium on Circuits and Systems (MWSCAS)
PublisherIEEE
ISSN (Print)1548-3746
ISSN (Electronic)1558-3899

Conference

Conference64th IEEE International Midwest Symposium on Circuits and Systems
Abbreviated titleMWSCAS 2021
Country/TerritoryUnited States
CityEast Lansing
Period9/08/2111/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.

Cite this