Arun Chandrasekharan · Daniel Große  Rolf Drechsler Design Automation Techniques for Approximation Circuits Verifi cation, Synthesis and Test Design Automation Techniques for Approximation Circuits Arun Chandrasekharan • Daniel Große Rolf Drechsler Design Automation Techniques for Approximation Circuits Verification, Synthesis and Test 123 ArunChandrasekharan DanielGroße OneSpinSolutionsGmbH UniversityofBremenandDFKIGmbH Munich,Germany Bremen,Germany RolfDrechsler UniversityofBremenandDFKIGmbH Bremen,Germany ISBN978-3-319-98964-8 ISBN978-3-319-98965-5 (eBook) https://doi.org/10.1007/978-3-319-98965-5 LibraryofCongressControlNumber:2018952911 ©SpringerNatureSwitzerlandAG2019 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartof thematerialisconcerned,specificallytherightsoftranslation,reprinting,reuseofillustrations,recitation, broadcasting,reproductiononmicrofilmsorinanyotherphysicalway,andtransmissionorinformation storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodology nowknownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher,theauthorsandtheeditorsaresafetoassumethattheadviceandinformationinthisbook arebelievedtobetrueandaccurateatthedateofpublication.Neitherthepublishernortheauthorsor theeditorsgiveawarranty,expressorimplied,withrespecttothematerialcontainedhereinorforany errorsoromissionsthatmayhavebeenmade.Thepublisherremainsneutralwithregardtojurisdictional claimsinpublishedmapsandinstitutionalaffiliations. ThisSpringerimprintispublishedbytheregisteredcompanySpringerNatureSwitzerlandAG Theregisteredcompanyaddressis:Gewerbestrasse11,6330Cham,Switzerland To Keerthana, Nanno and Zehra Preface APPROXIMATECOMPUTINGisanoveldesignparadigmtoaddresstheperformance and energy efficiency needed for future computing systems. It is based on the observation that many applications compute their results more accurately than needed, wasting precious computational resources. Compounded to this problem, dark silicon and device scaling limits in the hardware design severely undermine thegrowingdemandforcomputationalpower.Approximatecomputingtacklesthis bydeliberatelyintroducingcontrolledinaccuraciesinthehardwareandsoftwareto improve performance. There is a huge set of applications from multi-media, data analytics,deeplearning,etc.thatcanmakeasignificantdifferenceinperformance andenergyefficiencyusingapproximatecomputing.However,despiteitspotential, thisnovelcomputationalparadigmisinitsinfancy.Thisisduetothelackofefficient design automation techniques that are synergetic to approximate computing. Our book bridgesthis gap. We explain algorithmsand methodologiesfrom automated synthesis to verification and test of an approximate computing system. All the algorithmsexplainedin this bookare implementedand thoroughlyevaluatedon a widerangeofbenchmarksandusecases.Ourmethodologiesareefficient,scalable, andsignificantlyadvancethestateoftheartoftheapproximatesystemdesign. vii Acknowledgments First andforemost,we would like to thankthemembersof the researchgroupfor computerarchitectureattheUniversityofBremen.Wedeeplyappreciatethecontin- uoussupport,theinspiringdiscussions,andthestimulatingenvironmentprovided. Next,wewouldliketothankallcoauthorsofthepaperswhichformedthestarting pointforthisbook:MathiasSoeken,UlrichKühne,andStephanEggersglüß.This bookwouldnothavebeenpossiblewithouttheiracademicknowledgeandvaluable insight. Our sincere thanks also go to Kenneth Schmitz, Saman Fröhlich, and ArighnaDebfornumerousdiscussionsandsuccessfulcollaborations. Munich,Germany ArunChandrasekharan Bremen,Germany DanielGroße Bremen,Germany RolfDrechsler July2018 ix Contents 1 Introduction .................................................................. 1 1.1 ApproximateComputingICDesignFlow............................. 4 1.2 Outline................................................................... 7 1.3 AxCSoftwareFrameworkandRelatedTools ......................... 8 2 Preliminaries ................................................................. 11 2.1 GeneralNotationandConventions..................................... 11 2.2 DataStructures:BooleanNetworks.................................... 12 2.2.1 BinaryDecisionDiagrams ..................................... 14 2.2.2 And-InverterGraphs............................................ 16 2.3 BooleanSatisfiability ................................................... 17 2.3.1 CNFandTseitinEncoding..................................... 19 2.3.2 LexicographicSAT ............................................. 19 2.3.3 ModelCounting................................................. 20 2.3.4 BoundedModelChecking...................................... 21 2.4 Post-productionTest,Faults,andATPG............................... 21 2.5 QuantifyingApproximations:ErrorMetrics........................... 22 2.5.1 Error-Rate....................................................... 23 2.5.2 Worst-CaseError ............................................... 24 2.5.3 Average-CaseError............................................. 24 2.5.4 Bit-FlipError ................................................... 24 3 ErrorMetricComputationforApproximate CombinationalCircuits ..................................................... 27 3.1 Overview ................................................................ 28 3.2 BDD-BasedMethods................................................... 29 3.2.1 Error-RateUsingBDDs........................................ 29 3.2.2 Worst-CaseErrorandBit-FlipErrorUsingBDDs............ 30 3.2.3 AlgorithmsformaxFunction .................................. 31 3.2.4 Algorithm3.2toFindmax..................................... 33 3.2.5 Average-CaseErrorUsingBDDs.............................. 34 xi xii Contents 3.3 SAT-BasedMethods .................................................... 38 3.3.1 Error-RateUsingSAT.......................................... 38 3.3.2 Worst-CaseErrorUsingSAT .................................. 39 3.3.3 Bit-FlipErrorUsingSAT....................................... 41 3.3.4 Average-CaseErrorUsingSAT................................ 41 3.4 AlgorithmicComplexityofErrorMetricComputations.............. 43 3.5 Implementation.......................................................... 43 3.5.1 ExperimentalResults........................................... 44 3.6 ConcludingRemarks.................................................... 50 4 FormalVerificationofApproximateSequentialCircuits................ 51 4.1 Overview ................................................................ 52 4.2 GeneralIdea............................................................. 53 4.2.1 SequentialApproximationMiter............................... 54 4.3 ApproximationQuestions .............................................. 55 4.3.1 Question1:WhatIstheEarliestTimeThatOneCan ExceedanAccumulatedWorst-CaseErrorofX?............. 55 4.3.2 Question2:WhatIstheMaximumWorst-CaseError?....... 56 4.3.3 Question3:WhatIstheEarliestTimeThatOneCan ReachanAccumulatedBit-FlipErrorofX?.................. 57 4.3.4 Question4:WhatIstheMaximumBit-FlipError?........... 57 4.3.5 Question5:CanOneGuaranteeThattheAverage-Case ErrorDoesNotExceedX?..................................... 57 4.4 ExperimentalResults ................................................... 57 4.4.1 ApproximatedSequentialMultiplier........................... 58 4.4.2 GeneralityandScalability...................................... 61 4.5 ConcludingRemarks.................................................... 64 5 SynthesisTechniquesforApproximationCircuits ....................... 65 5.1 Overview ................................................................ 65 5.2 ApproximateBDDMinimization...................................... 67 5.2.1 BDDApproximationOperators................................ 68 5.2.2 ExperimentalEvaluation ....................................... 70 5.3 AIG-BasedApproximationSynthesis.................................. 73 5.3.1 And-InverterGraphRewriting ................................. 73 5.3.2 Approximation-AwareRewriting.............................. 75 5.3.3 Implementation ................................................. 76 5.3.4 ExperimentalResults........................................... 78 5.4 ConcludingRemarks.................................................... 86 6 Post-ProductionTestStrategiesforApproximationCircuits ........... 87 6.1 Overview ................................................................ 87 6.2 Approximation-AwareTestMethodology ............................. 90 6.2.1 GeneralIdeaandMotivatingExample ........................ 90 6.2.2 Approximation-AwareFaultClassification.................... 92 Contents xiii 6.3 ExperimentalResults ................................................... 96 6.3.1 ResultsfortheWorst-CaseErrorMetric ...................... 97 6.3.2 ResultsfortheBit-FlipErrorMetric........................... 100 6.4 ConcludingRemarks.................................................... 102 7 ProACt:HardwareArchitectureforCross-LayerApproximate Computing.................................................................... 103 7.1 Overview ................................................................ 103 7.1.1 LiteratureReviewonApproximationArchitectures.......... 106 7.2 ProACtSystemArchitecture ........................................... 107 7.2.1 ApproximateFloatingPointUnit(AFPU) .................... 109 7.2.2 InstructionSetArchitecture(ISA)Extension ................. 110 7.2.3 ProACtProcessorArchitecture ................................ 111 7.2.4 CompilerFrameworkandSystemLibraries................... 112 7.3 ProACtEvaluation...................................................... 112 7.3.1 FPGAImplementationDetails................................. 113 7.3.2 ExperimentalResults........................................... 114 7.4 ConcludingRemarks.................................................... 118 8 ConclusionsandOutlook ................................................... 119 8.1 Outlook.................................................................. 120 References......................................................................... 123 Index............................................................................... 129