Projects per year
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 available||19 Apr 2021|
|Publisher||University of Strathclyde|
|Date of data production||19 May 2020 - 18 Apr 2021|
1/10/17 → 1/04/21
Project: Research Studentship - Internally Allocated