From signal temporal logic to FPGA monitors

From signal temporal logic to FPGA monitors
复制标题

从信号时序逻辑到 FPGA 监视器

DOI:
10.1109/memcod.2015.7340489
复制
发表时间:
2015
期刊:
2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)
影响因子:
--
通讯作者:
D. Ničković
D. Ničković
中科院分区:
--
文献类型:
--
作者:
Stefan Jakšić;E. Bartocci;R. Grosu;R. Kloibhofer;Thang Nguyen;D. Ničković

文献摘要

被引文献

相似文献

由于系统的系统(SoS)的异构性和复杂性,它们的仿真变得非常耗时,昂贵,因此不切实际。因此,设计模拟越来越多地被更有效的设计仿真所补充。对仿真设计进行连续监测将为此类复杂系统的核查活动提供宝贵的支持。我们提出了新的算法,用于将信号时序逻辑(STL)断言转换为在现场可编程门阵列(FPGA)中实现的硬件运行时监视器。为了适应这种硬件特定的设置,我们限制自己的过去和有界的未来的时间运营商解释离散时间。我们评估我们的方法上两个例子:混合信号有界稳定性和串行外设接口(SPI)通信协议。这些案例研究表明,我们的方法的数字和混合信号系统的运行时监测的适用性。
Due to the heterogeneity and complexity of systems-of-systems (SoS), their simulation is becoming very time consuming, expensive and hence impractical. As a result, design simulation is increasingly being complemented with more efficient design emulation. Runtime monitoring of emulated designs would provide a precious support in the verification activities of such complex systems. We propose novel algorithms for translating signal temporal logic (STL) assertions to hardware runtime monitors implemented in field programmable gate array (FPGA). In order to accommodate to this hardware specific setting, we restrict ourselves to past and bounded future temporal operators interpreted over discrete time. We evaluate our approach on two examples: the mixed signal bounded stabilization property and the serial peripheral interface (SPI) communication protocol. These case studies demonstrate the suitability of our approach for runtime monitoring of both digital and mixed signal systems.