Tiny-: a novel formal method for specification. Analysis, and verification of dynamic partial reconfiguration processes
André Seffrin, Alexander Biedermann, Sorin Alexander Huss · 2010
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 reconflgurable FPGA platform.