From High-Level Modeling Towards Efficient and Trustworthy Circuits
This work addresses the challenge of simplifying embedded system design and verification for engineers by providing a method to automatically generate efficient FPGA implementations and concurrent C simulators from BIP models.
The paper tackles the problem of generating efficient and trustworthy circuits from high-level BIP models by computing reduced sequential circuits with system-specific schedulers, and it demonstrates that the method outperforms existing techniques on two large systems.
Behavior-Interaction-Priority (BIP) is a layered embedded system design and verification framework that provides separation of functionality, synchronization, and priority concerns to simplify system design and to establish correctness by construction. The framework comes with a runtime engine and a suite of verification tools that uses D-Finder and NuSMV as model checkers. In this paper we provide a method and a supporting tool that takes a BIP system and a set of invariants and computes a reduced sequential circuit with a system-specific scheduler and with a designated output that is true when the invariants hold. Our method uses ABC, a sequential circuit synthesis and verification framework to (1) generate an efficient FPGA implementation of the system, and to (2) verify the system and debug it in case a counterexample was found. Moreover we generate a concurrent C implementation of the circuit that can be directly used as a simulator. We evaluated our method with two large systems and our results outperform those possible with existing techniques.