FSM Traversal and Image Computation FSM traversal is the core computation in design verification. Efficient traversal requires grouping the MDDs, in a manner optimal for traversal. To traverse the FSM, the present state, input, and next state variables are organized for easy manipulation. All this information is included in an FSM data structure created in the compute_reach command. This also invokes traversal of the entire reachable state set of the FSM representing the design, and may be invoked with different verbosity options to get varying amounts of traversal information. On subsequent calls to compute_reach, the reachability computation is not reperformed, but statistics can be printed using -v. The reachability computation makes extensive use of image computation. There are several user-settable options that affect the performance of image computation. The documentation for the set command lists these options. Use the command set image_method to change the image computation method, and then re-initialize verification (starting at the flatten_hierarchy command ). The print_img_info prints current image information. Notice that while print_partition _stats prints information on the next state functions, print_img_info prints information on the next state transition relations. The command print_img_info creates transition relations from transition functions by clustering several functions together. The result is a partitioned transition relation. It is often a good idea to force dynamic variable reordering (for instance, dynamic_var_ordering -f sift) at this point to reorder these relation MDDs. The reachability computation is an optional step of the model checking algorithm; unreachable states may be used as don't cares to minimize the BDD representation.

Contact 

©2002-2018 U.C. Regents