A method of hardware
verification is presented, which uses the syntactic definition of a
component on the one hand to verify a specification and on the other
hand to translate this definition into a circuit. More precisely, a
component is described by a term of some higher order formal system. A
higher order system is needed here, since a component can be viewed as
a stream transformer, and streams can be viewed as functions from
natural numbers (ticks of the global clock) to e.g. boolean values.
To be able to deal with signals unrecognisable by the component, we
use as our mathematical model the partial continuous
functionals of D Scott. Then in any type 
we have an
undefined object 
as a first-class citizen. The aim is not
to go into the details of this circuit, but to show by an example (the
min-max unit) how this could be done in principle. Part of the
specification has been proven with the interactive prover Minlog under
development in Munich. The paper has been presented at the first
annual NADA meeting in Bridgend, March 1995.