Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2011 | Book

Introduction Read chapter Read first chapter

High-Level Verification

Methods and Tools for Verification of System-Level Designs

Authors: Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta

Publisher: Springer New York

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

Given the growing size and heterogeneity of Systems on Chip (SOC), the design process from initial specification to chip fabrication has become increasingly complex. This growing complexity provides incentive for designers to use high-level languages such as C, SystemC, and SystemVerilog for system-level design. While a major goal of these high-level languages is to enable verification at a higher level of abstraction, allowing early exploration of system-level designs, the focus so far for validation purposes has been on traditional testing techniques such as random testing and scenario-based testing. This book focuses on high-level verification, presenting a design methodology that relies upon advances in synthesis techniques as well as on incremental refinement of the design process. These refinements can be done manually or through elaboration tools. This book discusses verification of specific properties in designs written using high-level languages, as well as checking that the refined implementations are equivalent to their high-level specifications. The novelty of each of these techniques is that they use a combination of formal techniques to do scalable verification of system designs completely automatically. The verification techniques presented in this book include methods for verifying properties of high-level designs and methods for verifying that the translation from high-level design to a low-level Register Transfer Language (RTL) design preserves semantics. Used together, these techniques guarantee that properties verified in the high-level design are preserved through the translation to low-level RTL.

Table of Contents

Frontmatter
Chapter 1. Introduction
Abstract
The quantitative changes brought about by Moore’s law in design of integrated circuits (ICs) affect not only the scale of the designs, but also the scale of the process to design and validate such chips. While designer productivity has grown at an impressive rate over the past few decades, the rate of improvement has not kept pace with chip capacity growth leading to the well known design-productivity-gap [105]. The problem of reducing the design-productivity-gap is crucial in not only handling the complexity of the design, but also combating the increased fragility of the composed system consisting of heterogeneous components. Unlike software programs, integrated circuits are not repairable. The development costs are so high that multiple design spins are ruled out, a design must be correct in the one and often the only one design iteration to implementation.
Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
Chapter 2. Background
Abstract
We envision a design methodology that is built around advances in high-level design and verification to improve the quality and time to design microelectronic systems. In this chapter, we will present a brief overview of the three different parts of high-level verificationas shown in Fig. 1.1 on which the verification algorithms are applied. We first present in Sect. 2.1 and in Sect. 2.2 a description of high-level designs and RTL designs respectively. We then in Sect. 2.3 give a brief introduction of high-level synthesis. In the next two sections we introduce the concept of model checking, and our program representation scheme that is used throughout the book.
Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
Chapter 3. Related Work
Abstract
Each one of the three areas of high-level verificationoutlined in Chap. 1, namely high-level property checking, translation validation, and synthesis tool verification, have been explored in a wide variety of research efforts. In this chapter, we discuss various techniques from each of these areas that are directly relevant to this book.
Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
Chapter 4. Verification Using Automated Theorem Provers
Abstract
An automated theorem prover is a tool that determines, automatically or semi-automatically, the validity of formulas in a particular logic. Automated theorem provers have been put to use in many applications. They have been used to solve open problems in mathematics, such as Robbin’s problem in boolean algebra [140], which was open since the 1930s, and various open problems about quasigroups [188]. They have also been used to prove interesting properties about real-world systems, properties that would have been hard, difficult or tedious to prove by hand. For example, automated theorem provers have been used to verify microprocessors [19, 20, 164], communication protocols [20], concurrent algorithms [20], and various properties of software systems [9, 58, 100, 130, 132, 164, 168].
Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
Chapter 5. Execution-Based Model Checking for High-Level Designs
Abstract
In this chapter, we present an high-level property checking approach. We begin with a general description of verification of concurrent programs, and then describe it for a high-level language called SystemC [78]. In this approach, we start with a design written in SystemC, and then use model checking techniques to verify that the design satisfies a given property such as the absence of deadlocks or assertion violations.
Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
Chapter 6. Bounded Model Checking for Concurrent Systems: Synchronous Vs. Asynchronous
Abstract
Concurrent systems are hard to verify due to complex and unintended asynchronous interactions. Exploring the state space of such a system is a daunting task. Model checking techniques that use symbolic search and partial-order reduction are gaining popularity. In this chapter, we focus primarily on bounded model checking (BMC) approaches that use decision procedures to search for bounded length counter-examples to safety properties such as data races and assertion violations in multi-threaded concurrent systems. In particular, we contrast several state-of-the-art approaches based on the synchronous and asynchronous modeling styles used in formulating the decision problems, and the sizes of the corresponding formulas.
Malay K. Ganai
Chapter 7. Translation Validation of High-Level Synthesis
Abstract
Once the important properties of the high-level components have been verified possibly using techniques presented in Chaps. 5 and 6, the translation from the high-level design to low-level RTL still needs to be proven correct, thereby also guaranteeing that the important properties of the components are preserved. In this chapter we will discuss an approach that proves that the translation from high-level design to a scheduled design is correct, for each translation that the HLS tool performs. In the next chapter we will describe another approach that will allow us to write part of these tools in a provably correct manner.
Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
Chapter 8. Parameterized Program Equivalence Checking
Abstract
In the previous chapter we discussed an approach to verify if two programs are equivalent, thereby proving that the translation (performed by an HLS tool) from high-level design to low-level design is correct. In this chapter, we discuss another approach that guarantees correctness of the translation from high-level design to low-level design, by proving the HLS tool itself correct. Unlike translation validation, this approach proves the correctness of an HLS tool once and for all, before it is ever run. In the following sections we describe in details an approach called Parametrized Equivalence Checking [120] (PEC ) that generalizes the translation validation approach discussed in the previous chapter to automatically establish the correctness of semantics preserving transformations once and for all.
Zachary Tatlock
Chapter 9. Conclusions and Future Work
Abstract
We have addressed the need for high-level verificationmethodologies that allows us to do functional verification early in the design phase and then iteratively use correct refinement steps to generate the final RTL design. We believe that by performing verification on the high-level design, where the design description is smaller in size and the design intent information is easier to extract, and then checking that all refinement steps are correct, the domain of high-level verificationcan provide strong and expressive guarantees that would have been difficult to achieve by directly analyzing the low-level RTL code.
Sudipta Kundu, Sorin Lerner, Rajesh K. Gupta
Backmatter
Metadata
Title
High-Level Verification
Authors
Sudipta Kundu
Sorin Lerner
Rajesh K. Gupta
Copyright Year
2011
Publisher
Springer New York
Electronic ISBN
978-1-4419-9359-5
Print ISBN
978-1-4419-9358-8
DOI
https://doi.org/10.1007/978-1-4419-9359-5