Model checking of reconfigurable FPGA modules specified by Petri nets

The paper proposes a novel formal verification method of reconfigurable modules implemented in FPGA devices. The modules are specified by Petri nets and can be exchanged in the already implemented and running system using dynamic partial reconfiguration. The model checking technique is used together with the abstract rule-based logical model to verify whether the new modules still satisfy the global requirements for the whole control system. The additional advantage of using the rule-based logical model is the possibility to automatically generate the VHDL code, hence the final implementation reflects the already verified specification. It allows to ensure high quality of the released product and eliminates errors related to hand-code writing. A case study is presented to illustrate the approach, as well as some experimental results.