zbMATH — the first resource for mathematics

Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs. (English) Zbl 1046.68578
Halbwachs, Nicolas (ed.) et al., Computer aided verification. 11th international conference, CAV ’99. Trento, Italy, July 6–10, 1999. Proceedings. Berlin: Springer (ISBN 3-540-66202-2). Lect. Notes Comput. Sci. 1633, 60-71 (1999).
Summary: In 1999, A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu introduced Bounded Model Checking with the aid of satisfiability solving (SAT) as an alternative to symbolic model checking with BDDs. In this paper we show how bounded model checking can take advantage of specialized optimizations. We present a bounded version of the cone of influence reduction. We have successfully applied this idea in checking safety properties of a PowerPC microprocessor at Motorola’s Somerset PowerPC design center. Based on tliat experience, we propose a verification methodology that we feel can bring model checking into the mainstream of industrial chip design.
For the entire collection see [Zbl 0925.68015].

68Q60 Specification and verification (program logics, model checking, etc.)