This paper presents a new Property-Driven Design (PDD) method that starts from an abstract system model and integrates formal property checking early into a top-down design methodology for register transfer level (RTL) hardware. In PDD the role of formal verification is not limited to “bug hunting” alone. Instead, the formal techniques are applied in such a way that a formal relationship is provided between the abstract system model and its concrete implementation at the RTL. In order to avoid the high efforts associated with verification by property checking the proposed PDD approach automatically generates abstract properties from a system-level description and later refines them along the design process. The advantage of this methodology is to obtain a formally verified design at lower costs when compared to conventional design flows with property checking. The main benefit of the proposed approach results from the fact that a formally sound system model is available together with the RTL design. Specifically, LTL properties proven on the abstract model also hold on the concrete implementation. This facilitates many complex analysis and verification tasks in today's design flows and contributes to emancipating system-level models from prototypes to golden design models. Several open-source and industrial case studies are reported that demonstrate the high potential of a PDD-based design paradigm.

Formal techniques for the functional verification of System-on-Chip (SoC) hardware have matured significantly over the last years. They can penetrate deeply into a design to exhibit complex functional dependencies between various design components in terms of detailed logical and temporal relationships. They can also provide a well-defined formal relationship between an abstract system model of a design and its concrete implementation at the register-transfer level (RTL). This paper shows how such knowledge available from formal verification can be “condensed” into a database that stores all registers and flip-flops, at which time points they are actually relevant for the correct behavior of the design and when they are not. We show that the comprehensive information on temporary unobservabilities in the design can be of great value to reach two nonfunctional design goals that play a dominant role in many design flows: safety and low power consumption. This paper presents techniques to assess the effects of soft errors by single-event upsets (SEUs) with formal precision and to relate the results of the proposed analysis to an abstract system model. For example, our analysis can determine which soft errors may lead to a system “crash” and which are guaranteed not to cause any harm. For the application of the proposed approach in power optimization, this paper presents techniques for clock gating and power gating. For the examined designs, we observe a reduction of power consumption between 10% and 50% on top of the state-of-the-art commercial power synthesis.

Driven by the demand for highly customizable processor cores for IoT and related applications, there is a renewed interest in effective but low-cost techniques for verifying systems-on-chip (SoCs). This paper revisits the problem of processor verification and presents a radically different approach when compared to the state of the art. The proposed approach is highly automated and leverages recent progress in the field of post-silicon validation by the method of Quick Error Detection (QED) and Symbolic Quick Error Detection (SQED). In this paper, we modify SQED by incorporating a symbolic initial state in its BMC-based analysis and generalize the approach into the S2QED method. As a first advantage, S2QED can separate logic bugs from electrical bugs in QED-based postsilicon validation. Secondly, it also makes a strong contribution to pre-silicon verification by proving that the execution of each instruction is independent of its context in the program. The manual efforts for the proposed approach are orders of magnitude smaller than for conventional property checking. Our experimental results demonstrate the potential of S2QED using the Aquarius open-source processor example.

This paper discusses the possible role of formal verification techniques in system-level design flows. It is argued that the role of formal verification techniques should not be limited to “bug hunting” alone. Instead, formal technology should be applied in such a way that a formal relationship is provided between an abstract system model and its concrete implementation at the Register Transfer Level (RTL). In order to avoid the high efforts associated with verification by property checking this paper advocates for a top-down methodology where abstract properties are automatically generated from a system-level description and are later refined along the design process. One advantage of this methodology is to obtain a formally verified design at lower costs when compared to conventional property checking. Moreover, the proposed approach can be beneficial also when analyzing non-functional design targets. The paper demonstrates this for safety. We present experimental results that show how the effects of Single Event Upsets (SEUs) at the gate level of an SoC module can be related to safety requirements at the system's transaction level with formal precision.

This paper works towards a new design flow in which a design model at an architectural system level is refined into an RTL implementation in such a way that architectural model and RTL implementation stand in a well-defined formal relationship to each other. Functional properties valid at the system level are guaranteed to hold also in the concrete implementation without any additional verification efforts at the RTL. Based on the notion of path predicate abstraction (PPA) introduced in previous work, this paper contributes an "architectural modeling language (AML)" which formalizes the semantics of the architectural description level w.r.t. a PPA. The language is intended to be used only as an intermediate description automatically derived from standardized ESL languages such as SystemC when these descriptions are restricted to a mappable subset. Such an intermediate representation is needed to overcome the limitations of SystemC in precisely defining the semantics of the design model and its interfaces as well as to cope with the overwhelming expressive power of SystemC and the large syntactical diversity it allows. With an AML description of the architectural model as a starting point, the paper will show how properties in a standard language like SVA can be automatically generated that guarantee the correctness of the implementation when proven on the design after all refinement steps in the design and the property set have been completed.

A formal methodology for system verification of system-on-chip (SoC) designs is proposed. It ensures that system-level models are created that are sound abstractions of the concrete implementations at the register transfer level (RTL). For each SoC module at the RTL, an abstract description is obtained by path predicate abstraction. Path predicate abstraction is introduced based on the notion of operational graph coloring. It is shown to what extent the proposed abstraction mechanism is related to the notion of a stuttering bisimulation employed in the field of theorem proving. The proposed methodology, however, does not rely on theorem proving but is entirely based on standard techniques of property checking. Path predicate abstraction leads to time-abstract system models that can be composed into abstract system models. We demonstrate the practical feasibility of our approach by two comprehensive industrial case studies.

A new methodology for formal system verification of System-on-Chip (SoC) designs is proposed. It does not only ensure correctness of the system-level models but also of the concrete implementation at the Register-Transfer-Level (RTL). For each SoC module at the RTL an abstract description is obtained by path predicate abstraction. Since this leads to time-abstract system models the main challenge is to deal with the concurrency between the individual RTL components. We propose a compositional scheme describing the communication between SoC modules independently of their individual processing speed. The composed abstract system is modeled as an asynchronous composition and can be verified using the SPIN model checker. We demonstrate the practical feasibility of our approach by a comprehensive case study based on Infineon's FPI Bus.