Abstract:With the growing increase in software/hardware system scale and function, the further development and application of model checking has been greatly limited by state space explosion, which has been the bottleneck of verifying large industrial designs. Based on the Murphi, an explicit state model checking tool, the problem of organization of reachable state space of model checking was studied, and a novel organization method of reachable state space based on integer pointer and Fibonacci hash was presented. In the approach, an efficient model checking system was suggested. The new approach can effectively shorten verification cycle, and give counter example when the system specification is unsatisfiable. All this greatly helped rapid error location. The analysis and experiment results prove the effectiveness of our method.