Linking BDD-Based Symbolic Evaluation to Interactive Theorem-Proving?

Jeffrey J. Joyce
Carl-Johan H. Seger
Department of Computer Science
University of British Columbia
Vancouver, B.C. V6T 1Z2 Canada

Abstract ? A novel approach to formal hardware verification results from the combination of symbolic trajectory evaluation and interactive theorem-proving. From symbolic trajectory evaluation we inherit a high degree of automation and accurate models of circuit behaviour and timing. From interactive theoremproving we gain access to powerful mathematical tools such as induction and abstraction. We have 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 systems in VLSI technology usually involves working at several levels of abstraction, ranging from very high level behavioral specifications down to physical layout. 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. Despite major simulation efforts, serious design errors often remain undetected. Consequently, there has been a growing interest in using formal methods to verify the correctness of designs. There are several approaches to formal hardware verification: theorem-proving, state machine analysis, and symbolic simulation to mention a few [11]. These methods all have strengths and weaknesses. In this paper we will illustrate how theorem-proving can be rigorously linked with symbolic simulation to gain a verification methodology that draws on the strengths of each approach. In particular, we have developed a novel approach to formal hardware verification which extends BDD-based symbolic simulation techniques with more generalpurpose reasoning tools such as abstraction and mathematical induction. The result is a hybrid approach to formal hardware verification that offers considerable promise in bridging the current gap between conventional verification techniques, such as switch-level simulation, and more esoteric formal techniques. We have implemented a prototype tool for our hybrid approach and used this tool to derive verification results that would be difficult to achieve with previously published techniques.

?This paper will appear in the Proceedings of the 30th Design Automation Conference to be published bythe IEEE.Copyright to this paper has beentransferred to the ACM. This research was supported by operating grants OGPO 109688 and OGPO 046196 from the Natural Sciences Research Council of Canada, by research contract 92-DJ-295 from the Semiconductor Research Corporation, and by fellowships from the Advanced Systems Institute.

Our hybrid approach can be seen as the latest step in a chain of evolution which began with the development of circuit models for switch-level simulation in the early 1980's [2]. Switch-level simulation is a commonly used verification technique supported by a number of commercial tools. The next step in this evolutionary chain was the development of symbolic switch-level simulation in the mid 1980's [3]. This symbolic approach to switch-level simulation is supported by tools such as the COS- MOS system from Carnegie-Mellon University [4]. Symbolic simulation can be seen as an extension of ordinary switch-level simulation where node values may be treated symbolically, that is, variables may be used to represent node values instead of constants such as T and F. A symbolic simulator can be used to verify assertions about the state of a circuit that results from a given sequence of inputs ? for instance, to show that the value of a particular output node is accurately described by a formula parameterized by a set of variables representing input values. Next in this evolutionary development was an extension to symbolic simulation that made it possible to verify assertions about state trajectories, that is, sequences of states rather just single states. In addition to treating node values symbolically, symbolic trajectory evaluation provides a rigorous technique for verifying temporal relationships between these node values. Recent versions of both COSMOS and a related system called Voss [12] from the University of British Columbia provide support for symbolic trajectory evaluation. Finally, our hybrid approach, as the latest step in this evolutionary chain, extends symbolic trajectory evaluation with a set of general-purpose reasoning tools. We have implemented a prototype software tool for our hybrid approach by means of an interface between the Voss system and an interactive theorem-prover called HOL from the University of Cambridge [10].

As an extension of symbolic trajectory evaluation, our hybrid approach has inherited the following strengths:

ffl In contrast to other formal approaches which often involve the use of over-simplified models, verification results obtained by means of our hybrid approach are basedon models of circuit behaviour and timing which are widely used in conventional CAD.

ffl Unlike several other approaches to formal hardware verification which require extensive re-training before any useful results can be achieved, there is a relatively smooth learning curve which allows a novice to start using our hybrid

Page 1