Data for: "On Applications of Dependent Types to Parameterised Digital Signal Processing Circuits"

Dataset

Description

This repository contains all of the source files needed to build and run the motivating examples from the paper "On Applications of Dependent Types to Parameterised Digital Signal Processing Circuits". We present a fully parameterised FIR filter with minimal bit growth and a CIC filter with register pruning, both enabled by Idris' dependent types. These examples show how we can encode aspects of circuits (such as wordlengths) in a circuit generator's types, allowing properties to be checked at compile time by the type checker. This helps preclude many common mistakes when designing and evaluating families of digital circuits.
Date made available19 Apr 2021
PublisherUniversity of Strathclyde
Date of data production19 May 2020 - 18 Apr 2021

Cite this