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

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.