Design and Verification of Microprocessor Systems for High-Assurance Applications

Design and Verification of Microprocessor Systems for High-Assurance Applications Edited by: David S. Hardin This book examines several leading-edge design and verification technologies that have been successfully applied to microprocessor systems  f

  • PDF / 4,933,471 Bytes
  • 439 Pages / 439.37 x 666.142 pts Page_size
  • 67 Downloads / 219 Views

DOWNLOAD

REPORT


David S. Hardin Editor

Design and Verification of Microprocessor Systems for High-Assurance Applications

123

Editor David S. Hardin Rockwell Collins, Inc. 400 Collins Road NE. Cedar Rapids IA 52498 USA [email protected]

ISBN 978-1-4419-1538-2 e-ISBN 978-1-4419-1539-9 DOI 10.1007/978-1-4419-1539-9 Springer New York Dordrecht Heidelberg London Library of Congress Control Number: 2010921140 c Springer Science+Business Media, LLC 2010  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)

For my grandmother, Wilma Smith, who taught me the value of books before I was able to read.

Preface

Microprocessors are the workhorses of modern high-assurance systems. New cars typically utilize dozens of microprocessors, managing vital functions such as braking, ignition, traction control, and air bags. Most of the critical functions on modern aircraft, including flight control, engine control, flight management, and pilot displays, are microprocessor based. Medical devices, transportation systems, power grids, communications infrastructure, defense systems, and numerous other highconfidence applications are all dependent on microprocessor control. Over the last 30 years, the microprocessors deployed in high-assurance systems have increased in sophistication from simple 8-bit chips with less than 10,000 transistors to 32- and 64-bit chips with millions of transistors, pipelining, floating point, specialized functional units (e.g., for cryptography), memory management, cache management, and so on. The system software for these systems has likewise increased from simple interrupt handlers to full-fledged operating systems capable of supporting multiple concurrent applications with space and time partitioning. Finally, the application logic on these microprocessor systems has increased from a few hundred lines of assembly code to millions of lines of high-level language code. The means of expressing the application design has changed as well, progressing from schematics and assembly code to high-level languages for both hardware and software. Indeed, many high-assurance applications are now developed using model-based development languages, with the final source code (which may be a mixture of programming language and hardware description language source