An efficient technique for analysis of minimal buffer requirements of synchronous dataflow graphs with model checking

ABSTRACT

Synchronous Dataflow (SDF) is a widely-used model of computation for digital signal processing and multimedia applications, which are typically implemented on memory constrained hardware platforms. SDF can be statically analyzed and scheduled, and the memory requirement for correct execution can be predicted at compile time. In this paper, we present an efficient technique based on model-checking for exact analysis of minimal buffer requirement of an SDF graph to guarantee deadlock-free execution. Performance evaluation shows that our approach can achieve significant performance improvements compared to related work.

REFERENCES

• 1: http://www.cse.ust.hk/~weichen/sdf_ex.html.
• 2: http://www.es.ele.tue.nl/sadf/.
• 3: M. Ade, R. Lauwereins, and J. A. Peperstraete. Data memory minimisation for synchronous dataflow graphs emulated on DSP-FPGA targets. In Design Automation Conference, pages 64--69, 1997.
• 4: S. S. Bhattacharyya, P. K. Murthy, and E. A. Lee. Software Synthesis from Dataflow Graphs. Kluwer Academic Publishers, 1996.
• 5: A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In International Conference on Computer-Aided Verification (CAV), 2002.
• 6: S. Edelkamp, A. Lluch-Lafuente, and S. Leue. Directed explicit model checking with hsf-spin. In M. B. Dwyer, editor, SPIN, volume 2057 of Lecture Notes in Computer Science, pages 57--79. Springer, 2001.
• 7: M. Geilen, T. Basten, and S. Stuijk. Minimising buffer requirements of synchronous dataflow graphs with model checking. In DAC '05: Proceedings of the 42nd annual conference on Design automation, pages 819--824, New York, NY, USA, 2005. ACM Press.
• 8: S. Goddard and K. Jeffay. Managing memory requirements in the synthesis of real-time systems from processing graphs. In Real-Time Technology and Applications Symposium, 1998. Proceedings. Fourth IEEE, pages 59--70, Jun 1998.
• 9: Z. Gu, M. Yuan, N. Guan, M. Lv, X. He, Q. Deng, and G. Yu. Static scheduling and software synthesis for dataflow graphs with symbolic model-checking. In RTSS '07: Proceedings of the 28th IEEE International Real-Time Systems Symposium, pages 353--364, Washington, DC, USA, 2007. IEEE Computer Society.
• 10: G. J. Holzmann. The model checker spin. IEEE Trans. Software Eng., 23(5):279--295, 1997.
• 11: J. Horstmannshoff and H. Meyr. Optimized system synthesis of complex rt level building blocks from multirate dataflow graphs. In ISSS, pages 38--43, 1999.
• 12: D. Kim, M. Kim, and S. Ha. A case study of system level specification and software synthesis of multimode multimedia terminal. In ESTImedia, pages 57--64, 2003.
• 13: S. Kwon, H. Jung, and S. Ha. H.264 decoder algorithm specification and simulation in simulink and peace. In International SoC Design Conference, pages 9--12, Oct 2004.
• 14: E. A. Lee and D. G. Messerschmitt. Static scheduling of synchronous data flow programs for digital signal processing. IEEE Trans. Comput., 36(1):24--35, 1987.
• 15: P. K. Murthy and S. S. Bhattacharyya. Memory Management for Synthesis of DSP Software. CRC Press, 2006.
• 16: H. Oh, N. Dutt, and S. Ha. Memory optimal single appearance schedule with dynamic loop count for synchronous dataflow graphs. In ASP-DAC '06: Proceedings of the 2006 conference on Asia South Pacific design automation, pages 497--502, New York, NY, USA, 2006. ACM Press.
• 17: T. M. Parks. Bounded Scheduling of Process Networks. PhD thesis, 1994.
• 18: S. Stuijk, M. Geilen, and T. Basten. Exploring trade-offs in buffer requirements and throughput constraints for synchronous dataflow graphs. Design Automation Conference, 2006 43rd ACM/IEEE, pages 899--904, 24{28 July 2006.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Modeling techniques

General Terms:
Algorithms, Performance

Keywords:
memory management, model checking, optimization, scheduling, synchronous dataflow