State-of-the-art RV frameworks that implement runtime monitors in hardware synthesize monitoring circuits from formal specifications of properties. Such frameworks resynthesize or reconfigure monitoring circuits if the input properties change post-deployment. This is typically handled using reconfigurable fabrics such as FPGAs. Runtime monitors implemented on FPGAs have two disadvantages as compared to a fixed implementation (ASIC): (i) lower operating frequencies and (ii) inefficient use of area (on silicon). In this work, we propose an RV framework called faRM-LTL, that overcomes these two disadvantages by keeping the design of the runtime monitor unchanged even if the input properties change, thereby making it amenable for an ASIC implementation. We achieve this using a Linear Temporal Logic (LTL) Monitoring Instruction Set Architecture (LM-ISA), a compiler that translates properties specified in LTL into a sequence of LM-ISA instructions, and an associated programmable hardware runtime monitor that implements the LM-ISA. The flexibility of the faRM-LTL Monitor was evaluated on 53 LTL properties from several prior works. We also implemented the Monitor on an ASIC and found its area overhead to be under \(0.5\%\) .

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

faRM-LTL: A Domain-Specific Architecture for Flexible and Accelerated Runtime Monitoring of LTL Properties

  • Amrutha Benny,
  • Sandeep Chandran,
  • Rajshekar Kalayappan,
  • Ramchandra Phawade,
  • Piyush P. Kurur

摘要

State-of-the-art RV frameworks that implement runtime monitors in hardware synthesize monitoring circuits from formal specifications of properties. Such frameworks resynthesize or reconfigure monitoring circuits if the input properties change post-deployment. This is typically handled using reconfigurable fabrics such as FPGAs. Runtime monitors implemented on FPGAs have two disadvantages as compared to a fixed implementation (ASIC): (i) lower operating frequencies and (ii) inefficient use of area (on silicon). In this work, we propose an RV framework called faRM-LTL, that overcomes these two disadvantages by keeping the design of the runtime monitor unchanged even if the input properties change, thereby making it amenable for an ASIC implementation. We achieve this using a Linear Temporal Logic (LTL) Monitoring Instruction Set Architecture (LM-ISA), a compiler that translates properties specified in LTL into a sequence of LM-ISA instructions, and an associated programmable hardware runtime monitor that implements the LM-ISA. The flexibility of the faRM-LTL Monitor was evaluated on 53 LTL properties from several prior works. We also implemented the Monitor on an ASIC and found its area overhead to be under \(0.5\%\) .