Will proof replace simulation?

Within industry, the almost universally accepted method of validating a design against its requirement involves extrapolation from simulation of a (comparatively) small number of test cases to the behaviour of the complete circuit. That such an extrapolation is in general unjustifiable is widely accepted, but despite theorem provers’ ability to provide a mo^e robust link between specification and circuit design, very few industrial engineers are using theorem provers on a daily basis. This paper aims to consider some of the factors that may be preventing the wider application of proof methods. Specifically, RSRE has concentrated on two areas of research: the development of a largely automatic but functionally limited proof system, and more recently on a more general prover based on the concepts of a hardware description language. It is hoped to illustrate that these provers, being designed specifically for hardware design applications, may provide a more familiar environment for designers wishing to do proofs.