Tiny-π: A novel formal method for specification, analysis, and verification of dynamic partial reconfiguration processes

On FPGA-platforms, the feature of dynamic partial reconfiguration offers a wide range of applications. We propose a new formal method for design, analysis, and verification of the reconfiguration process on such devices. The π-calculus, also known as the calculus of mobile processes, is a type of process algebra typically used to describe dynamic communicating processes. We propose the π-calculus as a foundation to model dynamic partial reconfiguration of hardware modules. A subset of this calculus that we call tiny-π can be executed in resource-restricted, embedded environments which feature reconfiguration properties. As a proof-of-concept, we present a small virtual machine implementation for tiny-π. We have also implemented a compilation flow from a textual description of tiny-π specifications into executable bytecode. The virtual machine, running on an embedded Microblaze processor on an FPGA, can execute the bytecode and trigger corresponding reconfiguration commands for a dynamically reconfigurable FPGA platform.