Efabless Logo
Temporal Runtime...
public project
MPW-6   

This project implements a runtime monitoring component for the Caravel SoC that is capable of monitoring a temporal logic safety property. The component has two SRAM blocks for storing its configuration (1 kB and 2 kB each) and implements a lookup table-based approach to monitoring a reactive system.

Many modern reactive systems, such as those implemented using microcontrollers or system on chips (SoCs) need to be behave correctly in all situations in order for them to be usable. It not always possible to verify the implementation of a reactive system upfront before its deployment. The research area of runtime verification deals with approaches to detect specification violations at runtime, so that they can at least be detected after deployment of the reactive system. With a reported specification violation, the system's implementation can then be revised or the system can switch to a fail-safe mode.

Runtime verification techniques typically need to be lightweight, i.e., they should not slow down the monitored system too much. Especially for monitoring temporal specifications that describe how the system evolves and reacts over time, implementing efficient monitors is far from trivial. Such specification can for example be given in linear temporal logic (LTL). Previous approaches to monitoring such specifications have mostly relied on either:

  1. using a real-time operating system (RTOS) with a separate monitoring process for which the input is buffered and that is scheduled from time to time,
  2. using an external FPGA chip that observes the monitored system's behavior by computing runs of an automaton whose runs encode the ways in which a specification can be violated, or
  3. augmenting the microcontroller code with instructions that simulate the possible runs of an automaton whose runs encode the ways in which a specification can be violated.

Solution 1 is mostly suitable for bigger embedded systems that actually employ real-time operating systems, and it requires a careful selection of what exactly is monitored in order for the monitoring process not to require too much computation time. Solution 2 is quite expensive, as the FPGA chip can be more costly than the microcontroller/SoC being monitored. In solution 3, the overhead due to the added instructions can be quite substantial.

A specialized runtime monitoring component for microcontrollers, as implemented in this project, can help to reduce monitoring overhead. Once programmed, the component performs the monitoring process on its own, while the microcontroller/SoC only needs to send the elements of the system execution to be monitored to the component by writing to one of its control registers via the bus connecting the SoC core and the monitoring component.

Description

This is a specialized on-chip microcontroller/SoC component for performing runtime monitoring of temporal logic formulas. The component executes a monitor that has been compiled using a specialized compiler and uploaded to the component's SRAMs. After initialization, there is a specific address in the address space of the SoC to which the current valuation of the propositions to be monitored can be written - updating the runtime monitor is then done by the monitor component.

Category

acc

Process

sky130A