Meta-functional languages for hardware design

Abstract

The concept of embedding a hardware description language in a pure functional language has been largely explored and has been shown to provide various techniques to establish high levels of abstraction capable to aid the design and verification of hardware systems. The two-stage language environment that is achieved enables the description of circuit generators, capable of describing generic circuits and connection patterns, allowing the possibility to apply further analysis, modifications and translations. Nonetheless, despite the advantages gained, no access is granted to the circuit generators themselves, restricting the possibility to inspect and analyse circuits at even higher levels of abstraction. Unless explicitly inserted, the resulting circuits lack information about their generators and manipulators, which can be used for non-functional features such as placement. We propose the embedding of a hardware description language within a meta-functional language, thus having the possibility to access the circuit generators explicitly through the use of code quotations. We present a framework capable of maintain hierarchical block markings of subcomponents within structural descriptions, and optionally add placement combinators to such markings. Furthermore, we propose a technique to automate the generation and extraction of verification modes used to formally check the correctness of hardware compilers.