Efficient model checking by automated ordering of transition relation partitions

Abstract

In symbolic model checking, the behavior of a model to be verified is captured by the transition relation of the state space implied by the model. Unfortunately, the size of the transition relation grows rapidly with the number of states even for small models, rendering them impossible to verify. A recent work [5] described a method for partitioning the transition relation, thus reducing the overall space requirement. Using this method, actions that require the transition relation can be executed by using one partition at a time. This process, however, strongly depends on the order in which the partitions are processed during the action. This paper describes a criterion for ordering partitions which is independent of the circuit details. Based on this criterion, a heuristic algorithm for ordering partitions is described. The algorithm, which may be used in preparation for each symbolic simulation step, has been successfully implemented and has resulted in significant speed-ups of symbolic model checking. Specifically, this algorithm has made it possible to verify blocks inside an example microprocessor. The run time results are given here.