Path Predicate Abstraction for Sound System-Level Modeling of Digital Circuits

Dissertation

Joakim Henrik Urdahl
Fachbereich Elektrotechnik und Informationstechnik der Technische Universität Kaiserslautern

December, 15 2015

Motivation and Overview

Even after years of progress both in simulation-based and formal verification techniques, System- on-Chip (SoC) verification at the Register-Transfer-Level (RTL) has remained the main bottle- neck in the design flow. While more and more sub-systems of increasing size become integrated on a single chip the level of abstraction for state-of-the-art verification techniques has remained unchanged. Even with the advent of new design methodologies based on Electronic System Level (ESL) descriptions, it is still the RTL that has remained the point of reference for creating the “golden” design model.

A comparison with verification practices at lower design levels may illustrate the problem: as a matter of course, when verifying the logic behavior of a large combinational circuit, we consider its gate-level description. Simulating its transistor-level description instead, in princi- ple, is possible but would be considered highly inefficient and inappropriate. Similarly, when verifying the micro-architecture of an SoC design, we base this verification on its RTL descrip- tion rather than its gate netlist. This is standard procedure, because we can trust the gate netlist and the RTL description: they are considered sound abstractions for the next lower levels.

By contrast, when evaluating the global system behavior of an SoC, this verification is done at the RTL. Verification of high-level models can be useful to build confidence in the specification at an early design phase, but it is not adequate to render a full-blown, system-wide RTL verification superfluous. We only trust the actual implementation of our SoC after chip wide simulations on the RTL have been running for weeks and months on large workstation clusters. Why do we not rely on verifying the global system behavior at the system level? Obviously, we do not trust our system-level models as much as we trust our RTL models and our gate-level models. The reason for this lack of confidence is well known and has often been addressed as the “semantic gap” between the system and the RT level. In fact, establishing a well-defined, formal relationship between these two levels is a difficult problem. It is one of the main hurdles when attempting to integrate system-level models into standard SoC design and verification flows.

The main objective of this thesis is to show how standard property checking techniques and commercially available tools can be used to close the semantic gap. The thesis contributes a theoretical basis as well as a practical methodology to describe a sound relationship between models at the RT level and models at the system level. The methodology can be used both “bottom-up”, to create sound abstractions from already existing RTL descriptions, and “top- down”, as part of a design flow where RTL descriptions are created from system-level de- scriptions in a guided refinement process that ensures the same soundness. We envision that, based on the proposed methodology, system-level verification techniques, e.g., based on Sys- temC [35, 53, 52, 28, 38, 14, 13] can be used to replace chip-level verification at the RTL in the future.

Sound abstraction based on a stack of sound functional models above the RTL has been investigated extensively in the context of formal verification by theorem proving, for example in [48, 39, 47, 30, 29, 7].
An important difference between these previous works and sound abstractions based on path predicate abstraction (PPA), as proposed in this thesis, lies in the fact that the methodol- ogy developed in our work is entirely based on standardized property languages such as System Verilog Assertions (SVA) and relies exclusively on fully automatic property checking using a bounded circuit model [16, 43]. This does not only support an intuitive formulation of design properties but also facilitates proof procedures that can handle industrial RTL designs of realistic complexity.

Not many other attempts has been made for creating sound abstract models based on standard property checking. A notable exception is [24]. Their work describes an approach from mathematical logic based on interpretation of theories to relate time-abstract system descrip- tions to cycle-accurate implementations. In contrast, the approach investigated in this thesis is based on the conventional formalisms of model checking such as Kripke structures. Moreover, the theoretical framework proposed here extends over [24] in that it is fully compositional. The proposed approach can handle the concurrency between RTL modules that are each represented by time-abstract models at the system level [58].

The thesis is structured as follows: Chapter 2 introduces relevant formalisms and summa- rizes the state of the art in formal verification techniques. Chapter 3 introduces a criterion to the completeness of a property set and an algorithm to check this criterion. It ensures that the properties of the set, in sum, describe the full behavior of the considered design. This very important attribute is required in the sound abstraction technique introduced in later chapters and is possessed by any property set generated in the proposed design flow.

Own contributions are presented from Chapter 4 and onwards. Chapter 4 presents the de- veloped formalism of a Path Predicate Abstraction (PPA) and shows how it can be applied to an RTL implementation by proving a complete set of properties. It is an abstraction tailored to describe a sound relationship between a non-cycle-accurate and non-bit-accurate system model and an RT-level implementation. First it is defined for directed graphs; this definition eases an intuitive understanding and enables the comparison with other known abstraction techniques in Sec. 4.5.

In Sec. 4.2, the PPA definition is extended for FSMs before it is shown in Sec. 4.3 how C-IPC can be used to create such a PPA from the FSM of an RTL description. The chapter end in Sec. 4.4 where it is shown how the soundness of PPA guarantees a correspondence between important model checking properties of the abstract model and the concrete implementation.
Chapter 5 contributes important extensions to make path predicate abstraction composi- tional and a theorem for the soundness of a system composed of path predicate abstraction is postulated and proven.

Later chapters are devoted to technical applications of path predicate abstraction. In Chapter 6 it is shown, at the example of a telecommunication module, how a path predicate abstrac- tion is created based on standard property checking on an RTL implementation. The chapter ends with experimental results reported for two case studies where this method was applied to industrial RTL designs. In Chapter 7 a novel design flow is presented where the processes of creating a path predicate abstraction is reversed. In this proposed design flow system-level models are methodologically refined while preserving the relationship of a path predicate ab- straction through a set of automatically generated properties. The methodology has been tested in a student project which is reported at the end of the chapter. Note that the verification re- sults obtained by analysis of the abstractions are, for both of the above methods, valid also for the RTL implementation and therefore also for the realized circuit. If such methodologies are followed it would render expensive chip-wide simulations at the RT level superfluous.

At last, in Chapter 8, it is discussed how the above techniques can be exploited for opti- mizations of the RT level, and for improved power estimates at the system level. A case study has been made where the full behavior of a SONET/SDH framer owned by Alcatel Lucent was re-designed and its energy consumption was compared with the original.

LINK to .PDF: 2015-Urdahl-1