A unified approach for combining different formalisms for hardware verification

Model Checking as the predominant technique for automati- cally verifying circuits suffers from the well-known state explosion prob- lem. This hinders the verification of circuits which contain non-trivial data paths. Recently, it has been shown that for those circuits it may be useful to separate the control and data part prior to verification. This paper is also based on this idea and presents an approach for combining various proof approaches like model checking and theorem proving in a unifying framework. In contrast to other approaches, special proof proce- dures are available to verify circuits with data sensitive controllers, where a bidirectional signal flow between controller and data path can be found. Generic circuits can be verified by induction or by model checking finite instantiations. By giving the system 'proof hints', also the verification effort for model checking based proofs can be considerably reduced in many cases. The paper presents an introduction to the different proof strategies as well as an algorithm for their combination. The underlying Cr system also allows the efficiency evaluation of different approaches to verify the same circuits. This is shown in different case studies, demonstrating the trade* off between interaction and verifiable circuit size.