From High-Level Modeling Towards Efficient and Trustworthy Circuits

TL;DR

This paper introduces a method and tool that convert BIP system models into optimized FPGA and C implementations, enhancing efficiency and verification capabilities for embedded systems.

Contribution

It presents a novel approach using ABC to synthesize FPGA and C implementations from BIP models, improving performance and verification over existing methods.

Findings

Outperforms existing techniques on large systems

Generates efficient FPGA implementations

Provides direct C simulation code

Abstract

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.