Improving Scalability of Model-Checking for Minimizing Buffer Requirements of Synchronous Dataflow Graphs

Nan Guan, Zonghua Gu, Wang Yi, Ge Yu

Research output: Chapter in book / Conference proceedingConference article published in proceeding or bookAcademic researchpeer-review

8 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationProceedings of the ASP-DAC 2009
Subtitle of host publicationAsia and South Pacific Design Automation Conference 2009
Number of pages6
Publication statusPublished - 20 Apr 2009
Externally publishedYes
EventAsia and South Pacific Design Automation Conference 2009, ASP-DAC 2009 - Yokohama, Japan
Duration: 19 Jan 200922 Jan 2009


ConferenceAsia and South Pacific Design Automation Conference 2009, ASP-DAC 2009

ASJC Scopus subject areas

  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Cite this