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

[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.

    ORCID iDs

    Ramsay, Craig, Crockett, Louise H. and Stewart, Robert W. ORCID logoORCID: https://orcid.org/0000-0002-7779-8597;