A Mathematically Precise Two-Level Formal

Hardware Verification Methodology?

Carl-Johan H. Seger

Jeffrey J. Joyce

Department of Computer Science

University of British Columbia

Vancouver, B.C. V6T 1Z2 Canada

Abstract

Theorem-proving and symbolic trajectory evaluation are both described as methods for the formal verification of hardware. They are both used to achieve a common goal|correctly designed hardware|and both are intended to be an alternative to conventional methods based on non-exhaustive simulation. However, they have different strengths and weaknesses. The main significance of this paper is the description of a two-level approach to formal hardware verification, where the HOL theorem prover is combined with the Voss verification system. From symbolic trajectory evaluation we inherit a high degree of automation and accurate models of circuit behavior and timing. From interactive theorem-proving we gain access to powerful mathematical tools such as induction and abstraction. The interface between the HOL and Voss is, however, more than just an ad hoc translation of verification results obtained by one tool into input for the other tool. We have developed a mathematical" interface where the results of the Voss system is embedded in HOL. We have also prototyped a hybrid tool and used this tool to obtain verification results that could not be easily obtained with previously published techniques.

1 Introduction

Designing complex digital system in VLSI technology usually involves working at several levels of abstraction, ranging from very high level behavioral specifications down to physical layout at the lowest. One of the main difficulties in this process is to verify the consistency of the different levels of abstraction. Simulation is often used as the main tool for checking" the consistency. Typically the designer tries relatively few test cases, one at a time, and checks whether the results are correct. Towards the end of the design phase, the circuit is then often

?This research was supported by operating grants OGPO 109688 and OGPO O46196 from the Natural Sciences Research Council of Canada, fellowships from the Advanced Systems Institute, and by research contract 92-DJ-295 from the Semiconductor Research Corporation.