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

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.