A functional approach for formalizing regular hardware structures

Abstract. An approach for formalizing hardware behaviour is presented which is based on a small functional programming language called primitive ML (PML). Since the basic constructs of PML are simply typed h-terms, PML lends itself both to simulation and verification. The semantics of PML is formally embedded in higher-order logic. The formalization scheme is based on PML-functions that allow hardware descriptions from the logical level up to the algorithmic level. Besides de-scriptions of real circuits, abstract forms of hardware descriptions can also be dealt with in PML. The main emphasis is thereby put on regular hard-ware structures which are described by means of primitive recursion. PML-descriptions can easily be converted to syntactic structures, called hardware formulae, which can then be verified by the MEPHISTO system. 1 In t roduct ion Embedding hardware description languages (HDLs) in a logic or some calculi is essential for verification. The semantics of such embedded I/DLs, which correspon