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

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 x speedup with 16 actors.