Abstract
In [1] Bounded Model Checking with the aid of satisfiability solving (SAT) was introduced 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 that experience, we propose a verification methodology that we feel can bring model checking into the mainstream of industrial chip design.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Biere, A. Cimatti, Edmund M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS’99, 1999. to appear. 60, 61, 61, 61, 61, 62
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992. Originally presented at the 1990 Symposium on Logic in Computer Science (LICS90). 61
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, May 1981. 60
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Proc. 19th Ann. ACM Symp. on Principles of Prog. Lang., Jan., 1992. 66, 70
O. Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In Proc. 10th Int’l Computer Aided Verification Converence, pages 23–32, 1990. 61
O. Grumberg and D. E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16:843–872, May, 1994. 66, 70
M. Kaufmann, A. Martin, and C. Pixley. Design constraints in symbolic model checking. In Proc. 10th Int’l Computer Aided Verification Converence, June, 1998. 66, 69
R. P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, pages 170–172. Princeton University Press, Princeton, New Jersey, 1994. 63
K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993. 61, 65
C. Pixley. Verifying temporal properties of sequential machines without building their state diagrams. In Proc. 10th Int’l Computer Aided Verification Converence, pages 54–64, 1990. 61
D. Plaisted and S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2:293–304, 1986. 63
J. P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. 5th Int. Symp. in Programming, 1981. 60
J. P. M. Silva. Search algorithms for satisfiability problems in combinational switching circuits. Ph.D. Dissertation, EECS Department, University of Michigan, May 1995. 61, 63, 65
G. Stalmarck and M. Säflund. Modeling and verifying systems and software in propositional logic. In B. K. Daniels, editor, Safety of Computer Control Systems (SAFECOMP’90), pages 31–36. Pergamon Press, 1990. 61, 63
H. Zhang. A decision procedure for propositional logic. Assoc. for Automated Reasoning Newsletter, 22:1–3, 1993. 61, 63, 65
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Biere, A., Clarke, E., Raimi, R., Zhu, Y. (1999). Verifying Safety Properties of a PowerPC− Microprocessor Using Symbolic Model Checking without BDDs. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_8
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive