Post-Silicon and Runtime Verification for Modern Processors Ilya Wagner • Valeria Bertacco Post-Silicon and Runtime Verification for Modern Processors Ilya Wagner Valeria Bertacco Platform Validation Engineering Group Department of Electrical Engineering Intel Corporation and Computer Science Hillsboro, Oregon University of Michigan USA Ann Arbor, Michigan [email protected] USA [email protected] ISBN 978-1-4419-8033-5 e-ISBN 978-1-4419-8034-2 DOI 10.1007/978-1-4419-8034-2 Springer New York Dordrecht Heidelberg London © 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) To mynieceEllie,who showed me themiracleof learning. Ilya Wagner To allmystudents,who make working inthefieldof verificationsucharewarding experience. ValeriaBertacco Preface The growingcomplexityof modernprocessordesignsandtheir shrinkingproduc- tionschedulescauseanincreasingnumberoferrorstoescapeintoreleasedproducts. Many of these escaped bugs can have dramatic effects on the security and stabil- ityofconsumersystems,underminetheimageofthemanufacturingcompanyand cause substantial financial grief. Moreover, recent trends towards multi-core pro- cessor chips, with complexmemorysubsystems and sometimes non-deterministic communicationdelays,furtherexacerbatetheproblemwithmoresubtle,yetmore devastating, escaped bugs. This worsening situation calls for high-efficiency and high-coverage verification methodologies for systems under development, a goal that is unachievable with today’s pre-silicon simulation and formal validation so- lutions. In light of this, functional post-silicon validation and runtime verification are becomingvitally importantcomponentsof a modernmicroprocessordevelop- ment process. Post-silicon validation leverages orders of magnitude performance improvementsoverpre-siliconsimulationwhileprovidingveryhighcoverage.Run- timeverificationsolutionsaugmentthehardwarewithon-chipmonitorsandcheck- ing modulesthatcan detecterroneousexecutionsin systems deployedin the field andrecoverfromthemdynamically. The purpose of this book is to present and discuss the state of the art in post- siliconandruntimeverificationtechniques:twoveryrecentandfastgrowingtrends in the world of microprocessordesign and verification. The first part of this book beginswithahigh-leveloverviewofthevariousverificationactivitiesthataproces- sorissubjectedtoasitmovesthroughitslife-cycle,fromarchitecturalconception to silicon deployment. When a chip is being designed, and before early hardware prototypesaremanufactured,theverificationlandscapeisdominatedbytwo main groupsoftechniques:simulation-basedvalidationandformalverification.Simula- tionsolutionsleverageamodelofthedesign’sstructure,oftenwritteninspecialized hardwareprogramminglanguages,andvalidateadesignbyprovidinginputstimuli tothemodelandevaluatingitsresponsestothosestimuli.Formaltechniques,onthe otherhand,treatadesignasamathematicaldescriptionofitsfunctionalityandfo- cusonprovingawiderangeofpropertiesofitsfunctionalbehavior.Unfortunately, these two categories of validation methods are becoming increasingly inadequate vii viii Preface incopingwiththecomplexityofmodernmulti-coresystems.Thisisexactlywhere post-siliconandruntimevalidationtechniques,theprimaryscopeofthisbook,can lendamuchneededhand. Throughoutthebookwepresentarangeofrecentsolutionsinthesetwodomains, designedspecificallytoidentifyfunctionalbugslocatedindifferentcomponentsof amodernprocessor,fromindividualcomputationalcorestothememorysubsystem andon-chipfabricsforinter-corecommunication.Wetransitionintothesecondpart ofthebookbypresentingmainstreampost-siliconvalidationandtestactivitiesthat are currently being deployed in industrial development environments and outline important performance bottlenecks of these techniques. We then present Reversi, ourproposedmethodologyto alleviatethese bottlenecksin processorcores.Basic principlesof inter-corecommunicationthroughsharedmemoryare overviewedin the followingchapter,whichalso detailsnewapproachestovalidationofcommu- nicationinvariantsin silicon prototypes.We concludethediscussionof functional post-siliconvalidationwithanovelechnique,targetedspecificallytomodernmulti- cores,calledDacota. The recently proposed approaches to validation that we collected in part two of this book have an enormouspotential to improveverification performanceand coverage;however,therestillisachancethatcomplexandsubtleerrorsevadethem andescapeintoend-usersiliconsystems.Runtimesolutions,thefocusofthethird part of this work, are designed to address these situations and to guarantee that a processor performs correctly even in presence of escaped design bugs without degrading user experience. To better analyze these techniques we investigate the taxonomy of escaped bugs reported for some of the processor designs available today,andwealsoclassifyruntimeapproachesintotwomajorgroups:checker-and patching-based.Intheremainderofpartthreewedetailseveralruntimeverification methodswithinbothcategories,firstrelatingtoindividualcoresandthentomulti- core systems. We conclude the book with a glance towards the future, discussing moderntrendsinprocessorarchitectureandsilicontechnology,andtheirpotential impactsontheverificationofupcomingdesigns. Acknowledgements Wewouldliketoacknowledgeseveralpeoplethatmadethewritingofthisbookpos- sible.First,andforemost,weexpressourgratitudetoourcolleagues,whoworked withusontheresearchpresentedinthisbook.Inparticular,wewouldliketothank ProfessorToddAustin,whowasavitalmemberofourruntimeverificationresearch andprovidedcriticaladviceinmanyotherprojects.AndrewDeOriohascontributed immenselyto our post-siliconvalidationresearch andhashelpedus greatlyin the experimentalevaluationsofseveralothertechniques.BothToddandAndrewhave also worked tirelessly on the original development of these works and provided valuableinsightsonthepresentationofthematerialinthismanuscript. We would also like to thank many students working in the Advanced Com- puter Architecture Lab, and, especially, all those who have devoted their research to hardware verification: Kai-hui Chang, Stephen Plaza, Andrea Pellegrini, De- bapriya Chatterjee, Rawan Abdel-Khalek have worked particularly closely to us amongmanyothers.Everydaytheseindividualsarerelentlesslyadvancingthethe- oryandthepracticeofthisexcitingandchallengingfield.Wealsoacknowledgeall ofthefacultyandstaffattheComputerScienceandEngineeringDepartmentofThe UniversityofMichigan,aswellasallengineersandresearchersinacademiaandin- dustry who provided us with valuable feedback on our work at conferences and workshops, reviewed and critiqued our papers and published their findings, upon whichmuchofourresearchwasbuilt.Thesearetrulythegiants,onwhoseshoul- derswestand. Wealsothankourfamilies,whofaithfullysupportedusthroughouttheyearsof research that led to the publicationof this book.Each and everyone of them was constantlyreadytooffertechnicaladviceoraheartwarmingconsolationindifficult times, andcelebratethemomentsofoursuccesses. Indeed,withouttheirtrustand encouragementthiswritingwouldbeabsolutelyimpossible. Finally,wewouldliketoacknowledgeoureditors,Mr.AlexGreene,Ms.Ciara VincentandMs. KatelynChinfromSpringer,whoworkedcloselywithusonthis publicationwithtrulyangelicpatience.Timeandagain,theyencouragedustocon- tinuewritingandgaveusvaluableadviceonmanyaspectsofthisbook. ix