On applications of dependent types to parameterised digital signal processing circuits

Ramsay, Craig and Crockett, Louise H. and Stewart, Robert W.; (2021) On applications of dependent types to parameterised digital signal processing circuits. In: 2021 IEEE International Midwest Symposium on Circuits and Systems, MWSCAS 2021 - Proceedings. IEEE International Midwest Symposium on Circuits and Systems (MWSCAS) . IEEE, USA, pp. 787-791. ISBN 9781665424615 (https://doi.org/10.1109/MWSCAS47672.2021.9531730)

[thumbnail of Ramsay-etal-IEEE-IMSCS-2021-On-applications-of-dependent-types-to-parameterised-digital-signal]
Preview
 Text. Filename: Ramsay_etal_IEEE_IMSCS_2021_On_applications_of_dependent_types_to_parameterised_digital_signal.pdf
Accepted Author Manuscript
Download (640kB)| Preview

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.

  • Item type:Book Section
    ID code:77721
    Dates:
    Date
    Event
    13 September 2021
    Published
    11 August 2021
    Published Online
    24 May 2021
    Accepted
    Notes:© 2021 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting /republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
    Subjects:Technology > Electrical engineering. Electronics Nuclear engineering
    Department:Faculty of Engineering > Electronic and Electrical Engineering
    Depositing user: Pure Administrator
    Date deposited:08 Sep 2021 15:53
    Last modified:20 Apr 2024 00:07
    Related URLs:
    URI:https://strathprints.strath.ac.uk/id/eprint/77721
CORE (COnnecting REpositories)