Improving scalability of model-checking for minimizing buffer requirements of synchronous dataflow graphs

ABSTRACT

Synchronous Dataflow (SDF) is a well-known model of computation for dataflow-oriented applications such as embedded systems for signal processing and multimedia. It is important to minimize the buffer size requirements of applications generated from SDF graphs, since memory space is often a scarce resource in these systems due to cost or power consumption constraints. Some authors have proposed to use model-checking for finding the minimum buffer size requirements, but the scalability of model-checking is limited by state space explosion. In this paper, we present several techniques for reducing state space size and improving scalability of model-checking by exploiting problem-specific properties of SDF graphs.

REFERENCES

• 1: Shuvra S. Battacharyya , Edward A. Lee , Praveen K. Murthy, Software Synthesis from Dataflow Graphs, Kluwer Academic Publishers, Norwell, MA, 1996
• 2: Alessandro Cimatti , Edmund M. Clarke , Enrico Giunchiglia , Fausto Giunchiglia , Marco Pistore , Marco Roveri , Roberto Sebastiani , Armando Tacchella, NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.359-364, July 27-31, 2002
• 3: Marija Cubric , Prakash Panangaden, Minimal Memory Schedules for Dataflow Networks, Proceedings of the 4th International Conference on Concurrency Theory, p.368-383, August 23-26, 1993
• 4: Marc Geilen , Twan Basten , Sander Stuijk, Minimising buffer requirements of synchronous dataflow graphs with model checking, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, Anaheim, California, USA [doi>10.1145/1065579.1065796]
• 5: Zonghua Gu , Mingxuan Yuan , Nan Guan , Mingsong Lv , Xiuqiang He , Qingxu Deng , Ge Yu, Static Scheduling and Software Synthesis for Dataflow Graphs with Symbolic Model-Checking, Proceedings of the 28th IEEE International Real-Time Systems Symposium, p.353-364, December 03-06, 2007 [doi>10.1109/RTSS.2007.46]
• 6: Edward Ashford Lee , David G. Messerschmitt, Static scheduling of synchronous data flow programs for digital signal processing, IEEE Transactions on Computers, v.36 n.1, p.24-35, Jan. 1987 [doi>10.1109/TC.1987.5009446]
• 7: Praveen K. Murthy , Shuvra S. Bhattacharyya, Memory Management for Synthesis of DSP Software, CRC Press, Inc., Boca Raton, FL, 2006
• 8: Hyunok Oh , Nikil Dutt , Soonhoi Ha, Memory optimal single appearance schedule with dynamic loop count for synchronous dataflow graphs, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan [doi>10.1145/1118299.1118420]
• 9: Sander Stuijk , Marc Geilen , Twan Basten, SDF^3: SDF For Free, Proceedings of the Sixth International Conference on Application of Concurrency to System Design, p.276-278, June 28-30, 2006 [doi>10.1109/ACSD.2006.23]
• 10: R. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal of Computer., 1972.