Meta-functional Languages for Hardware Design and Verification

General purpose functional languages have been widely used as host languages for the embedding of domain specific languages, especially for hardware description languages. The embedding approach provides various abstraction techniques, enabling the description of generators for whole families of circuits, in particular parameterised regular circuits. The two-stage language setting that is achieved by means of embedding, provides a means to reason about the generated circuits as data objects within the host language. Nonetheless, these circuit objects lack information about their generators, and about the manner in which these where generated. In this paper, we explore the use of a meta-programming language to extend the embedding approach thus enabling us to access the underlying circuit generators, and not just the circuits themselves. We show the applicability of this approach by using circuit generator analysis techniques to extract information from a hardware compiler to enable verification, through the use of model-checking, of compiler invariants. The main contribution of this paper is to show how automatic verification of whole families of circuits can be used in an embedded language setting to verify hardware compiler invariants.