Data for "Toatie --- Functional Hardware Description with Dependent Types"
收藏DataCite Commons2023-07-12 更新2024-07-13 收录
下载链接：
https://pureportal.strath.ac.uk/en/datasets/fd83f191-2dc1-4839-adbb-684bac5ecd0c
下载链接
链接失效反馈官方服务：
资源简介：
This repository contains all of the source files the "toatie" hardware description language and its compiler. The dataset includes a reproducible build environment using nix, the compiler sources, standard libraries, example circuits, and test scripts. This is an extension of Tiny Idris --- introduced by Edwin Brady at SPLV20. Our main additions to support hardware description include erasure/irrelevance of non-synthesisable terms, staging for circuit generators, deriving bit representations, and the synthesis itself.
提供机构：
University of Strathclyde
创建时间：
2023-07-12
