Dynamically Reprogrammable Runtime Monitors for Bounded-time MTL

TL;DR

This paper introduces a reprogrammable runtime monitor for bounded-time Metric Temporal Logic (MTL) that is implemented with standard cells, enabling at-speed, in-field property verification on the same die as high-performance systems.

Contribution

It presents a novel, reprogrammable monitor architecture using standard cells, capable of supporting bounded-time MTL properties at high speed and post-deployment reprogramming.

Findings

Supports MTL formulae with up to 16 atomic propositions

Operates at 1.25 GHz frequency

Occupies only 0.55 mm^2 area

Abstract

A Runtime Verification (RV) framework that supports online, at-speed verification of properties that can change dynamically (during in-field operations) will benefit a large variety of applications. Several state-of-the-art RV frameworks propose to implement monitors on FPGAs. While this approach can support changes to the property being monitored during in-field operations, they struggle to keep pace with the system under verification which use high-performance processors. In this work, we propose a novel, reprogrammable monitor that is implemented using standard cells instead of FPGAs. This allows the monitor to be co-located with the system under verification (on the same die), and hence is amenable to at-speed monitoring of properties. Our proposed design consists of a programmable unit that implements five basic operations and a set of queue-update rules. We show that a composition of such programmable units faithfully implements discrete time, bounded MTL. We demonstrate through simulations that our proposed monitor can be reprogrammed (through its I/O pins) post deployment. A fairly large monitor which can support MTL formulae upto 16 atomic propositions occupies only 0.55 mm^2, while operating at a frequency of 1.25 GHz.