从高层建模迈向高效可信的电路
软件工程
2014-09-30 v1
摘要
行为 - 交互 - 优先级 (BIP) 是一种分层嵌入式系统设计与验证框架，它通过分离功能、同步和优先级关注点来简化系统设计并建立构造正确性。该框架配有运行时引擎和一套验证工具，使用 D-Finder 和 NuSMV 作为模型检测器。在本文中，我们提供了一种方法和支持工具，该方法接收一个 BIP 系统和一组不变量，计算出一个具有系统特定调度器的简化时序电路，并设有一个当不变量成立时为真的指定输出。我们的方法利用 ABC（一个时序电路综合与验证框架）来：(1) 生成系统的高效 FPGA 实现，以及 (2) 验证系统并在发现反例时进行调试。此外，我们生成了该电路的并发 C 实现，可直接用作仿真器。我们在两个大型系统上评估了我们的方法，结果表明其性能优于现有技术。
引用
@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}
}
备注
arXiv admin note: text overlap with arXiv:1109.5505 by other authors