High-Level Verification Methods and Tools for Verification of System

This book looks at the problem of design verification with a view towards speeding up the process of verification by developing methods that apply to levels of abstraction above RTL or synchronous logic descriptions. Typically such descriptions capture de

  • PDF / 3,315,493 Bytes
  • 175 Pages / 439 x 666 pts Page_size
  • 111 Downloads / 249 Views

DOWNLOAD

REPORT


Sudipta Kundu



Sorin Lerner



Rajesh K. Gupta

High-Level Verification Methods and Tools for Verification of System-Level Designs

With Chapter 6 contributed by Malay K. Ganai and Chapter 8 contributed by Zachary Tatlock

123

Sudipta Kundu Synopsys Inc. NW Thorncroft Dr. 2174 97124 Hillsboro USA [email protected]

Rajesh K. Gupta Department of Computer Science and Engineering University of California, San Diego Gillman Drive 9500 92093-0404 La Jolla USA [email protected]

Sorin Lerner Department of Computer Science and Engineering University of California, San Diego Gillman Drive 9500 92093-0404 La Jolla USA [email protected]

ISBN 978-1-4419-9358-8 e-ISBN 978-1-4419-9359-5 DOI 10.1007/978-1-4419-9359-5 Springer New York Dordrecht Heidelberg London Library of Congress Control Number: 2011928550 c Springer Science+Business Media, LLC 2011  All rights reserved. This work may not be translated or copied in whole or in part without the written permission of the publisher (Springer Science+Business Media, LLC, 233 Spring Street, New York, NY 10013, USA), except for brief excerpts in connection with reviews or scholarly analysis. Use in connection with any form of information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed is forbidden. The use in this publication of trade names, trademarks, service marks, and similar terms, even if they are not identified as such, is not to be taken as an expression of opinion as to whether or not they are subject to proprietary rights. Printed on acid-free paper Springer is part of Springer Science+Business Media (www.springer.com)

Preface

Given the growing size and heterogeneity of Systems on Chip (SOC), the design process from initial specification to chip fabrication has become increasingly complex. The 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 has been on traditional testing techniques such as random testing and scenario-based testing. This book focuses on the rapidly growing area of high-level verification. We envision 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. In this book, we discuss 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 fall into two categories: (a) methods for verifying properties of high-level designs and (b) meth