WIXLIB

How to Verify an AirplaneValidation of Microprocessorsl Introductionl Functional ValidationvSimulation-based ValidationvFormal VerificationAerodynamics (Bernoulli's Equation)l Hybrid Methods (Simulation Formal)vTest Generation using Model CheckingvTest Generation using Concolic Testingl ConclusionCDA 4102/5155 – Fall 2021Copyright 2021 Prabhat Mishra1122Embedded SystemsThe Mystery Of Flight 447AutomobilesMedicallAirspeed sensor unit did not workNeeded to maintain speed and altitudeu Likely ice formation on the tip of the senoruHandheldAirplanesMilitarylWhy heating device did not workuPrinciple of super-cooled water (pure water)lCrash was attributed to pilot error3Entertainment341

Example: BMW 745iExample: Digital CameraMemoryControllersInterfacel 2, 000, 000 LOCl Windows CE OSSoftwarel 53 8-bit µP(Application Programs)Coprocessorsl 11 32-bit µPProcessorl 7 16-bit µPASICl Multiple NetworksConvertersAnalogl Buggy!DigitalAnalog56Ariane Rocket ExplosionElectronic Devices in AutomobileslJune 4, 1996: Ariane 5 rocket explosion.lCost: 7 billion (des), 500 million rocket.lSoftware error in the inertial reference system.uA64 bit floating point number relating to thehorizontal velocity of the rocket with respect to theplatform was converted to a 16 bit signed integer.The number did not fit, and conversion failed.8782

Intel FDIV BugThe MARS Pathfinder ProblemlRare scenario when floating-point division failslDec 1994 / Jan 1995lCost: 475 millionl A few days into the mission, not long afterPathfinder started gathering meteorologicaldata, the spacecraft began experiencing totalsystem resets, each resulting in losses of data.lThe press reported these failures in termssuch as "software glitches" and "the computerwas trying to do too many things at once".” 9910Verification ComplexityStatisticsUp to 70% effort (time and resources)spent on validation and verificationAdder2 32-bit inputs è232 x 232 264 input vectors 1.8 x 1020Adder è1111ALU èProcessor è Systems12123

Design ComplexityUse of Silicon PowerSource: Intel1314Technology and DemandTime-to-Market#of transistors are doubling every 2 years 1 yearTechnologyDemandExplorationPlanning3-4 yearsDevelopmentProductionProduct TimelineCommunication, multimedia, entertainment, networkingDesign complexity è verification complexity15164

Functional Validation of ProcessorsMythical Man-MonthlFunctional validation is a major 516190Pre-silicon logic bugs per generationTeam237855Months until completionIndividual102030Number of designers25000( Source: Tom Schubert, Intel, DAC 2003)182443pipelined complex microarchitectures8002240PentiumPentium ProPentium 4Next ?40lLogic bugs increase at 3-4 times/generationuBugsincrease (exponential) is linear with designcomplexity growth.1718Pentium 4 Bugs BreakdownNorth America Re-spin StatisticsSource: Bob Bentley, HLDVT 20021st Silicon Success100%48%199944%200239%2004Source: 2002 Collett International Research and SynopsysMicro-architectural complexity is a major contributor19205

North America Re-spin StatisticsDesign Validation Complexity48%199944%Engineer Years1st Silicon 110B201995100M20041M10M100MSimulation Vectors20000?BillionsLogic GatesSource: 2002 Collett International Research and Synopsys71% SOC re-spins are due to logic bugsSource: Synopsys2122OverviewlSpecification: capture the design conceptusing SystemC or HDL at appropriate level ofabstraction e.g., behavioral, structural, RTL, uuValidation of Microprocessorsl Introductionl Functional ValidationDesign Verification: is this what I want?lImplementation: Use synthesis tool (or handwritten) to generate lower level of abstractionImplementation Verification: does implementationsatisfies the specification?Simulation: validate the design model using testsu Formal Methods: prove properties or equivalenceuvSimulation-based ValidationvFormal Verificationl Hybrid Methods (Simulation Formal)lVerification Techniques2322vTest Generation using Model CheckingvTest Generation using Concolic Testingl Conclusion24246

SimulationclockComb.LogicStateLoading / Compilation TimeAbstractionStateSimulation elerationCompiled SimulationInterpretive Simulation(transistor level)Performance25Simulation Performance26Validation TechniqueslInterpretive SimulationuLine-by-linesimulation of the HDL codeq Can be functional or cycle-accuratelCompiled SimulationuGenerateC/C equivalent of each line of the HDLcode, compile the equivalent code along withsimulation kernel.Interpretive ISA Simulationl ( ) Simplel ( )Flexibleu Can handle selfl (-)lAccelerationSlowInstructionequivalent code and distribute amongvarious computation nodes e.g., IKOS boxmodifying ationuUsereconfigurable fabric for better performanceand enable validation in the presence of OS etc.27Run TimeEg. SimpleScalar287

Static Compiled Simulationl ( ) DoingTargetApplicationBinarySimulationCompilerul ( )uValidation of Microprocessorsas much as possible at compile timeE.g. No decode at run timel Functional ValidationGenerates fast optimized codeUtilizing compiler optimizationsCompile time overhead & limitation(-) Staticl (-)luCan not handle self modifying codeHostApplicationBinaryCompile TimeExecuteHostvSimulation-based ValidationvFormal Verificationl Hybrid Methods (Simulation Formal)DecodedProgramCodeGenerationl IntroductionE.g:[Zhu95][Braun01]Run TimevTest Generation using Model CheckingvTest Generation using Concolic Testingl Conclusion302930Formal VerificationWhat is Theorem Proving?l Solving by combinatorial enumeration and searchl Given RuleslTheorem ProvinguProve a theorem about the system correctnessl Model CheckinguCheck whether design satisfies a propertyl Equivalence CheckinguSimulate the design using symbolic inputs31Find a satisfiable assignment: parent(X,Y), male(X).mother(X,Y): parent(X,Y), female(X).usibling(X,Y): parent(Z,X), parent(Z,Y).ugrandparent(X,Y): parent(X,Z), parent(Z,Y).uuncle(X,Y)u: parent(Z,Y), sibling(X,Z), male(X).male(john), male(sam), male(joe), male(bill), female(sue),female(ellen), parent(sam, john), parent(ellen, john), parent(ellen, joe),parent(sam, joe), parent(sue, bill), parent(al, sam), parent(sue, ellen).l Queryl Satisfiability (SAT) Solvingufather(X,Y)ul FactsCheck whether two designs are equivalentl Symbolic Simulationuuu uncle(bill,john)?john)?u uncle(sue,31yes.fail.328

Use of Theorem ProvingFormal VerificationlTheorem ProvinglDrive Rules from SpecificationlState the Theorem about the correctness ofthe ImplementationlProve the TheoremlExplore the use of PVS theorem proveruuProve a theorem about the system correctnessl Model CheckinguCheck whether design satisfies a propertyl Equivalence Checkinghttp://pvs.csl.sri.com/uCheck whether two designs are equivalentl Symbolic SimulationuSimulate the design using symbolic inputsl Satisfiability (SAT) Solvingu3333Find a satisfiable assignment3434Model CheckingFormal VerificationlTheorem ProvingModel(System em Property)Yes, if model satisfiesthe specificationNo, Counterexampleul Model Checkingumodel satisfied enough system propertiesu Study counterexamples, pinpoint the source of the error,correct the model, and try againl Explore the use of SMV model checkeru http://www.kenmcmil.com/smv.htmluCheck whether two designs are equivalentl Symbolic SimulationuSimulate the design using symbolic inputsl Satisfiability (SAT) Solvinguu http://www.cs.cmu.edu/ modelcheck/smv.html35Check whether design satisfies a propertyl Equivalence Checkingl Increase confidence in the correctness of the model:u TheProve a theorem about the system correctnessFind a satisfiable assignment36369

What is Satisfiability (SAT)?Use of SAT for VerificationlModel the design in CNFlModel the property in CNFlCheck the satisfiability of the overall CNFlExplore the use of zChaff SAT solverGiven a propositional formula in CNF,find if there exists an assignment toBoolean variables that makes theformula true:literalsuhttp://www.princeton.edu/ chaff/zchaff.htmlw1 (b Ú c)clausesw2 ( a Ú d)w3 ( b Ú d)j w1 Ù w2 Ù w3SATisfyingassignment!A {a 0, b 1, c 0, d 1}383738Formal VerificationSimulationln-input NAND gate requires 2n vectorslTheorem ProvinguProve a theorem about the system correctnessInputsl Model CheckinguCheck whether design satisfies a propertyl Equivalence CheckinguCheck whether two designs are equivalentSimulate the design using symbolic inputsl Satisfiability (SAT) Solvingu39Find a satisfiable assignment00111011101lTernary simulation requires n 1 vectorsl Symbolic SimulationuOutput00X1X01110394010

Symbolic SimulationProperty Checking: An ExampleCA0BX1X01110Antecedentl PowerPC Memory Management Unitl Three blocks and many sub-blocksuuuConsequentl Each sub-block uses RAMAB( 0, X ) 1Segment registersBlock Address Translation (BAT)Translation Lookaside Buffer (TLB)CuConsequent: (C is (a &b) from 1 to 2)Entry 1data1paeavalid0always @ (wrClk or wrEn or dIn or wrAddr)beginif (wrClk & wrEn) ram[wrAddr] dIn;endLRUValid 1Antecedent: (A is a from 0 to 1) and (B is b from 0 to 1)data0Entry 0assign out (rdClk & rdEn) ? ram[rdAddr] : 32’b0;l Property for writeuvsidValid 0lRequires only 1 vectorl Property for readvalid1TLBl Same property can be used for all sub-blocksu41Name mapping needed42Property Checking: Experimentsl TLB miss detectionuuuuuuassign input assign out0 assign out1 assign hit0 assign hit1 assign miss ( {1'b1, vsid[0:23], ea[4:9],ea[10:13] } );( {valid0, data0[0:23], data0[24:29], data0[54:57]} );( {valid1, data1[0:23], data1[24:29], data1[54:57]} );( input out0 );( input out1 ); ( hit0 hit1 );Formal VerificationlTheorem Provingul Model CheckinguvsidEntry 0data0Entry 1data1LRUValid 1Valid 0valid0uvalid1TLBl Applicable to BAT array miss detectionl Simple extension for associativity nCheck whether two designs are equivalentl Symbolic SimulationuSimulate the design using symbolic inputsl Satisfiability (SAT) Solvingu43Check whether design satisfies a propertyl Equivalence CheckingpaeaProve a theorem about the system correctnessFind a satisfiable assignment444411

Equivalence Checking: An ExampleEquivalence Checkingl Traditional Equivalence Checkersl Equivalence Checking using SAT SolversInputsSpecificationOutputl Reference: generated from ADL specificationl Implementation: 32-bit RISC DLX (eda.org)l Equivalence Checker: Synopsys Formalityl Experimentsu Identified a bugu Validation time:XORImplementationin computation of overflow397 secondsl Limitationu reference model generation needs to be guidedq to maintain structure similar to the implementationl Works well between industrial RTL andgate-level designs (why?).454546Simulation-based ValidationValidation of Microprocessorsl IntroductionTestGenerationl Functional ValidationvSimulation-based ValidationvFormal VerificationTestsTestTestTestSimulation(DUT)Pass /FailCoverageAnalysisl Hybrid Methods (Simulation Formal)vTest Generation using Model CheckingvTest Generation using Concolic TestinglSimulation-based validation is widely usedUses billions to trillions of random testsu Still no guarantee of covering important scenariosul Conclusion47474812