Imperial College London
Portrait Picture

DrNicolasWu

Faculty of Engineering, Department of Computing

Reader in Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8189n.wu Website

 
 
//

Location

 

374Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Tahir:2023:10.1145/3597031.3597051,
author = {Tahir, O and Luk, W and Wu, N},
doi = {10.1145/3597031.3597051},
title = {Extensible Embedded Hardware Description Languages with Compilation, Simulation and Verification},
url = {http://dx.doi.org/10.1145/3597031.3597051},
year = {2023}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - Typical hardware description languages, such as Verilog and VHDL, are low-level declarative languages with little room for flexibility. Extending, verifying, or reinterpreting programs in these languages is typically done with external tools and at great cost. This paper presents an implementation of a relational hardware description language, Ruby, in the programming language and proof assistant Agda. Using our system, an engineer can easily write, compile, simulate, and verify new designs. The language is modular, allowing for new constructs and libraries to be added easily, and supports formal reasoning about circuit transformations. Symbolic simulation and compilation to a netlist format are also provided. We demonstrate our tool by designing, compiling, and simulating a priority queue design, and showcase how equational reasoning can be used to prove properties of circuits.
AU  - Tahir,O
AU  - Luk,W
AU  - Wu,N
DO  - 10.1145/3597031.3597051
PY  - 2023///
TI  - Extensible Embedded Hardware Description Languages with Compilation, Simulation and Verification
UR  - http://dx.doi.org/10.1145/3597031.3597051
ER  -
Download