Recurrence in Dense-time AMS Assertions

TL;DR

This paper introduces a formal semantics for recurrence over dense time in AMS assertions, extending existing assertion languages with real-time intervals and predicates, and provides a verification methodology using interval arithmetic and a compatible toolkit.

Contribution

It extends SVA with dense real-time semantics and offers a runtime verification methodology for AMS behaviors using interval arithmetic.

Findings

Formal semantics for dense-time recurrence introduced

Methodology for runtime verification using interval arithmetic developed

Toolkit interfaces with standard EDA tools via VPI

Abstract

The notion of recurrence over continuous or dense time, as required for expressing Analog and Mixed-Signal (AMS) behaviours, is fundamentally different from what is offered by the recurrence operators of SystemVerilog Assertions (SVA). This article introduces the formal semantics of recurrence over dense time and provides a methodology for the runtime verification of such properties using interval arithmetic. Our property language extends SVA with dense real-time intervals and predicates containing real-valued signals. We provide a tool kit which interfaces with off-the-shelf EDA tools through standard VPI.