Extending the FSMD Framework for Validating Code Motions of Array-Handling Programs

The finite state machine with datapath (FSMD) models provide a formalism to represent any sequential behavior. Literature has many examples where this model has been successfully applied for behavioral verification of programs. All these methods, however, cannot handle an important class of programs, namely those involving arrays. This limitation is now overcome with finite state machine with datapath having arrays (FSMDA) models which are an extension of FSMD models; the corresponding equivalence checking algorithm has also been enhanced so that code motions of array-intensive behaviors can be validated. The new mechanism has been successfully tested with several examples.