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

Author

Banerjee, Kunal ; Sarkar, Debdeep ; Mandal, Chittaranjan

Author_Institution

Dept. of Comput. Sci. & Eng., Indian Inst. of Technol. Kharagpur, Kharagpur, India

Volume

33

Issue

12

fYear

2014

fDate

Dec. 2014

Firstpage

2015

Lastpage

2019

Abstract

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.

Keywords

finite state machines; formal verification; parallel processing; FSMD models; array-handling programs; behavioral verification; code motions; finite state machine with datapath; sequential behavior; Automata; Benchmark testing; Embedded systems; Modeling; Code motion validation; equivalence checking; finite state machine with datapath (FSMD); normalization;

fLanguage

English

Journal_Title

Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on

Publisher

ieee

ISSN

0278-0070

Type

jour

DOI

10.1109/TCAD.2014.2354298

Filename

6951853