Efficient model checking by automated ordering of

Authors: Daniel Geist Ilan Beer

Publish Date: 1994/6/21

Volume: , Issue: , Pages: 299-310

PDF Link

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 workThis 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 speedups 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

Keywords: