Generic Specification of Digital Hardware

ID
TR-90-27
Authors
Jeffrey J. Joyce
Publishing date
September 1990
Abstract
This paper argues that generic description is a powerful concept in the context of formal verification, in particular, the formal verification of digital hardware. The paper also describes a technique for creating generic specifications in any language with (at least) the expressive power of higher-order logic. This technique is based on the use of higher-order predicates parameterized by function variables and type variables. We believe that this technique is a very direct (if not the most direct) way to specify hardware generically. Two examples of generic specification are given in the paper: a resettable counter and the programming level model of a very simple microprocessor.