Model checking of reconfigurable FPGA modules specified by Petri nets

•Formal verification for dynamically reconfigurable logic controllers in FPGA.•Prototyping flow supplemented by multi-stages formal verification.•Each version of a reconfigurable module validated to avoid formal errors.•Usage of an abstract rule-based logical model to simplify the verification proce...

Full description

Saved in:
Bibliographic Details
Published in:Journal of systems architecture 2018-09, Vol.89, p.1-9
Main Author: Grobelna, Iwona
Format: Article
Language:English
Subjects:
Concurrent controllers
Formal verification
FPGA
Model checking
Requirements
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:•Formal verification for dynamically reconfigurable logic controllers in FPGA.•Prototyping flow supplemented by multi-stages formal verification.•Each version of a reconfigurable module validated to avoid formal errors.•Usage of an abstract rule-based logical model to simplify the verification process.•Verifiable model and synthesizable VHDL code generated automatically. 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.
ISSN:1383-7621
1873-6165
DOI:10.1016/j.sysarc.2018.06.005