Capturing timing diagrams in operational SVA

In order to formally verify design functionality, the intended behavior of the design under verification (DUV) must be captured in a formal language. Frequently, a specification document contains timing diagrams, which provide an excellent starting point for capturing the intended behavior of designs. However, the standard formal languages SVA and PSL, which are based on the paradigm of sequences (SEREs = Sequential Extended Regular Expressions), do not provide direct constructs for capturing timing diagrams.

This paper presents the language constructs required for easily deriving properties from timing diagrams and waveforms, and their implementation in Siemens EDA’s operational SVA.

Introducing operational SVA

When the SVA standard was defined and got adopted, ITL users requested to unite the best of two worlds: the advantage of a widely accepted standard and the ease-of-use of ITL. As a solution to this demand, Siemens EDA developed an SVA modeling layer, called operational SVA. Rather than using the full set of language constructs of SVA, operational SVA is built on a small library of SVA constructs, called the “Timing Diagram Assertion Library” (TiDAL). Built on more than a decade of experience with ITL, TiDAL facilitates assertion writing from timing diagrams, as will be demonstrated below.

When using operational SVA, users need not learn most of the intricacies of SVA, but only a few simple constructs for expressing temporal aspects. The modeling layer avoids semantic pitfalls and complications, such as nested sequences, local variable flow rules, weak and strong semantics, to name just a few. The library TiDAL itself consists of less than 5 pages of standard SVA code, defining constructs that enable direct transcription of timing diagrams
into SVA. Figure 1 illustrates the concept of a modelling layer: well- known modelling layers for dynamic verification are VMM and OVM. They unburden the user largely from programming directly in the base languages SystemVerilog, SystemC or C++. Similarly,
TiDAL eases the use of SVA. The narrow middle block at the lower right side indicates that a basic subset of SVA is used within operational SVA.