Extensible Embedded Hardware Description Languages with Compilation, Simulation and Verification

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.