Cooperation of SMV and Jeda for the property checking of mixed control and data intensive designs

For a mixed control and data intensive design, neither model checking nor simulation alone can handle the property-checking problem effectively. Model checking is more suitable for checking the control part and simulation of the data part. In this paper, we propose to let the two techniques cooperate to complete the problem. We choose SMV, a symbolic model checking tool, and Jeda, a hardware verification language for the cooperation work. The work flow of cooperation is described. Experimental results show that by cooperation, the verification is speedup considerably.