From High-Level Modeling Towards Efficient and Trustworthy Circuits
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.
Cite
@article{arxiv.1409.8146,
title = {From High-Level Modeling Towards Efficient and Trustworthy Circuits},
author = {Mohamad Jaber and Mohamad Noureddine and Fadi A. Zaraket},
journal= {arXiv preprint arXiv:1409.8146},
year = {2014}
}
Comments
arXiv admin note: text overlap with arXiv:1109.5505 by other authors