Abstract
We describe the techniques we have used to search for bugs in the memory subsystem of a next-generation Alpha microprocessor. Our approach is based on two model checking methods that use satisfiability (SAT) solvers rather than binary decision diagrams (BDDs). We show that the first method, bounded model checking, can reduce the verification runtime from days to minutes on real, deep, microprocessor bugs when compared to a state-of-the-art BDD-based model checker. We also present experimental results showing that the second method, a version of symbolic trajectory evaluation that uses SAT-solvers instead of BDDs, can find as deep bugs, with even shorter runtimes. The tradeoff is that we have to spend more time writing specifications. Finally, we present our experiences with the two SAT-solvers that we have used, and give guidelines for applying a combination of bounded model checking and symbolic trajectory evaluation to industrial strength verification.
The bugs we have found are significantly more complex than those previously found with methods based on SAT-solvers.
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
M. Aagaard, R.B. Jones, T.F. Melham, J.W. O’Leary, and C.-J. H. Seger. A methodology for large-scale hardware verification. In Formal Methods in Computer Aided Design, November 2000.
P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic reachability analysis based on SAT-solvers. In Proc. TACAS’ 00, 9 th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 2000.
A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS’ 99, 8 th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 1999.
A. Biere, E.M. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC[tm] microprocessor using symbolic model checking without BDDs. In Proc. 11 th Int. Conf. on Computer Aided Verification, 1999.
P. Bjesse and K. Claessen. SAT-based verification without state space traversal. In Formal Methods in Computer Aided Design, November 2000.
E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, December 1999.
A. Gupta, Z. Yang, and P. Ashar. SAT-based image computation with application in reachability analysis for verification. In Formal Methods in Computer Aided Design, November 2000.
C.N. Ip and D. Dill. Better verification through symmetry. Formal Methods in System Design, 9(1/2):41–75, August 1996.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
K.L. McMillan. The SMV language. Technical report, Cadence Berkeley Labs, 1999.
Prover Technology AB. Prover 4.0 Application Programming Reference Manual, 2000. PPI-01-ARM-1.
C.-J. H. Seger and R.E. Bryant. Formal verification by symbolic evaluation of partially ordered trajectories. Formal Methods in System Design, 6(2):147–190, March 1995.
M. Sheeran, S. Singh, and G. Stälmarck. Checking safety properties using induction and a SAT-solver. In Formal Methods in Computer Aided Design, November 2000.
M. Sheeran and G. Stälmarck. A tutorial on Stälmarck’s proof procedure for propositional logic. Formal Methods in System Design, 16(1):23–58, January 2000.
J.P.M. Silva. Search algorithms for satisfiability problems in combinational switching circuits. PhD thesis, EECS Department, University of Michigan, May 1995.
P.F. Williams, A. Biere, E.M. Clarke, and A. Gupta. Combining decision diagrams and SAT procedures for efficient symbolic model checking. In Proc. 12th Int. Conf. on Computer Aided Verification, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bjesse, P., Leonard, T., Mokkedem, A. (2001). Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_44
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_44
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive