Embedded Systems and Software Validation The Morgan Kaufmann Series in Systems on Silicon Series Editor: Wayne Wolf, Georgia Institute of Technology The Designer’s Guide to VHDL, Second Edition Peter J. Ashenden The System Designer’s Guide to VHDL-AMS Peter J. Ashenden, Gregory D. Peterson, and Darrell A. Teegarden Modeling Embedded Systems and SoCs Axel Jantsch ASIC and FPGA Verification: A Guide to Component Modeling Richard Munden Multiprocessor Systems-on-Chips Edited by Ahmed Amine Jerraya and Wayne Wolf Functional Verification Bruce Wile, John Goss, and Wolfgang Roesner Customizable and Configurable Embedded Processors Edited by Paolo Ienne and Rainer Leupers Networks-on-Chips: Technology and Tools Edited by Giovanni De Micheli and Luca Benini VLSI Test Principles & Architectures Edited by Laung-Terng Wang, Cheng-Wen Wu, and Xiaoqing Wen Designing SoCs with Configured Processors Steve Leibson ESL Design and Verification Grant Martin, Andrew Piziali, and Brian Bailey Aspect-Oriented Programming with e David Robinson Reconfigurable Computing: The Theory and Practice of FPGA-Based Computation Edited by Scott Hauck and André DeHon System-on-Chip Test Architectures Edited by Laung-Terng Wang, Charles Stroud, and Nur Touba Verification Techniques for System-Level Design Masahiro Fujita, Indradeep Ghosh, and Mukul Prasad VHDL-2008: Just the New Stuff Peter J. Ashenden and Jim Lewis On-Chip Communication Architectures: System on Chip Interconnect Sudeep Pasricha and Nikil Dutt Embedded DSP Processor Design: Application Specific Instruction Set Processors Dake Liu Processor Description Languages: Applications and Methodologies Edited by Prabhat Mishra and Nikil Dutt Three-dimensional Integrated Circuit Design Vasilis F. Pavlidis and Eby G. Friedman Electronic Design Automation: Synthesis, Verification, and Test Edited by Laung-Terng Wang, Kwang-Ting (Tim) Cheng, Yao-Wen Chang Embedded Systems and Software Validation Abhik Roychoudhury Embedded Systems and Software Validation Abhik Roychoudhury Department of Computer Science National University of Singapore AMSTERDAM • BOSTON • HEIDELBERG • LONDON NEWYORK • OXFORD • PARIS • SAN DIEGO SAN FRANCISCO • SINGAPORE • SYDNEY • TOKYO Morgan Kaufmann Publishers is an imprint of Elsevier Morgan Kaufmann Publishers is an imprint of Elsevier 30 Corporate Drive, Suite 400, Burlington, MA 01803, USA This book is printed on acid-free paper. ⃝⬁ Copyright © 2009 by Elsevier Inc. All rights reserved. No part of this publication may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocopy, recording, or any information storage and retrieval system, without permission in writing from the publisher. Permissions may be sought directly from Elsevier’s Science & Technology Rights Department in Oxford, UK: phone: (+44) 1865 843830, fax: (+44) 1865 853333, E-mail: To Jishnu This page intentionally left blank Contents Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ix Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . xi CHAPTER 1 Introduction 1 CHAPTER 2 Model Validation 7 2.1 Platform versus System Behavior . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2 Criteria for Design Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.3 Informal Requirements: A Case Study . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.1 The Requirements Document . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3.2 Simplification of the Informal Requirements . . . . . . . . . . . . 14 2.4 Common Modeling Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.4.1 Finite-State Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.4.2 Communicating FSMs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.4.3 Message Sequence Chart–Based Models . . . . . . . . . . . . . . . . 27 2.5 Remarks about Modeling Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2.6 Model Simulations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2.6.1 FSM Simulations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 2.6.2 Simulating MSC-Based System Models . . . . . . . . . . . . . . . . . 46 2.7 Model-Based Testing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 2.8 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 2.8.1 Property Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 2.8.2 Checking Procedure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 2.9 The SPIN Validation Tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 2.10 The SMVValidation Tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 2.11 Case Study: Air-Traffic Controller . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 2.12 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 2.13 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 CHAPTER 3 Communication Validation 95 3.1 Common Incompatibilities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 3.1.1 Sending/Receiving Signals in Different Order. . . . . . . . . . . 99 3.1.2 Handling a Different Signal Alphabet . . . . . . . . . . . . . . . . . . . . 100 3.1.3 Mismatch in Data Format . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 3.1.4 Mismatch in Data Rates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 3.2 Converter Synthesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 3.2.1 Representing Native Protocols and Converters . . . . . . . . . . 106 3.2.2 Basic Ideas for Converter Synthesis . . . . . . . . . . . . . . . . . . . . . . 108 3.2.3 Various Strategies for Protocol Conversion . . . . . . . . . . . . . . 115 vii viii Contents 3.2.4 Avoiding No-Progress Cycles. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 3.2.5 Speculative Transmission to Avoid Deadlocks. . . . . . . . . . . 118 3.3 Changing a Working Design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 3.4 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 3.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 CHAPTER 4 Performance Validation 125 4.1 The Conventional Abstraction of Time . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 4.2 Predicting Execution Time of a Program. . . . . . . . . . . . . . . . . . . . . . . . . 131 4.2.1 WCET Calculation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 4.2.2 Modeling of Microarchitecture . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 4.3 Interference within a Processing Element . . . . . . . . . . . . . . . . . . . . . . . . 154 4.3.1 Interrupts from Environment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 4.3.2 Contention and Preemption . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157 4.3.3 Sharing a Processor Cache . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161 4.4 System-Level Communication Analysis . . . . . . . . . . . . . . . . . . . . . . . . . 165 4.5 Designing Systems with Predictable Timing . . . . . . . . . . . . . . . . . . . . . 169 4.5.1 Scratchpad Memories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169 4.5.2 Time-Triggered Communication . . . . . . . . . . . . . . . . . . . . . . . . . 174 4.6 Emerging Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176 4.7 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177 4.8 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177 CHAPTER 5 Functionality Validation 181 5.1 Dynamic or Trace-Based Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184 5.1.1 Dynamic Slicing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 5.1.2 Fault Localization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 5.1.3 Directed Testing Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203 5.2 Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207 5.2.1 Predicate Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211 5.2.2 Software Checking via Predicate Abstraction. . . . . . . . . . . . 218 5.2.3 Combining Formal Verification with Testing . . . . . . . . . . . . 225 5.3 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229 5.4 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 230 Bibliography 233 Index 241 Acknowledgments This book owes a lot to all my students, colleagues, and co-workers. It is by working with them over the past decade that I have discovered the issues and challenges in the field of embedded systems validation. So, first and foremost, I must thank them all. I have written this book off and on, in the course of my teaching and research work at the National University of Singapore (NUS). Funding from a University Research Council project at NUS is gratefully acknowledged. A leave from NUS in 2007 to the Indian Institute of Science (IISc) infused in me the energy to start writing the book. The calm environs of the IISc campus helped set the mood for writing this book. The support of Elsevier staff was instrumental in ensuring that the book has proceeded on schedule. Finally, playingwithmy5-year-old son Jishnu allowedme to absorb the pressures of writing the book in the midst of various deadlines and commitments. Thanks, Jishnu! Singapore 19 January 2009 ix