Skip to Main content Skip to Navigation
Journal articles

Verifying parallel dataflow transformations with model checking and its application to FPGAs

Abstract : Dataflow languages are widely used for programming real-time embedded systems. They offer high level abstraction above hardware, and are amenable to program analysis and optimisation. This paper addresses the challenge of verifying parallel program transformations in the context of dynamic dataflow models, where the scheduling behaviour and the amount of data each actor computes may depend on values only known at runtime. We present a Linear Temporal Logic (LTL) model checking approach to verify a dataflow program transformation, using three LTL properties to identify cyclostatic actors in dynamic dataflow programs. The workflow abstracts dataflow actor code to Fiacre specifications to search for counterexamples of the LTL properties using the Tina model checker. We also present a new refactoring tool for the Orcc dataflow programming environment, which applies the parallelising transformation to cyclostatic actors. Parallel refactoring using verified transformations speedily improves FPGA performance, e.g.15.4 ×  speedup with 16 actors.
Complete list of metadata

https://hal.laas.fr/hal-02347401
Contributor : Silvano Dal Zilio <>
Submitted on : Tuesday, November 5, 2019 - 11:02:41 AM
Last modification on : Thursday, June 10, 2021 - 3:06:29 AM

Links full text

Identifiers

Citation

Robert Stewart, Bernard Berthomieu, Paulo Garcia, Idris Ibrahim, Greg Michaelson, et al.. Verifying parallel dataflow transformations with model checking and its application to FPGAs. Journal of Systems Architecture, Elsevier, 2019, 101, pp.101657. ⟨10.1016/j.sysarc.2019.101657⟩. ⟨hal-02347401⟩

Share

Metrics

Record views

155