第八章功能验证

第八章,功能验证,Outlines,WhatisVerification?ProblemandTrendofFunctionVerificationHW/SWCo-verificationEmulatorbasedco-verificationESLdesigntoolbasedco-verificationAssertionBasedVerification(ABV),WhatisVerification?,Designconceptverification(functionalityverification)Doesthebehavioralideaworkasexpected?DesignimplementationverificationDoesthephysicaldesignbehaveasexpected?DesignperformanceverificationHowfastthechipcanoperatecorrectly?Howmuchpowerthechipconsumes?FaultsimulationWilltheselectedtestvectorcoverdesignandmanufacturingfaults?SiliconchiptestingDoesthesiliconchipworkandoperateasexpected?,ProblemofFunctionVerification,FunctionalityVerificationhasbeenover60%(even70%)ofdesigncycleformillionsgatesdesign.30%-70%manpowerforverificationCPUtimeincreasesexponentiallyinbigdesign,ProblemofFunctionVerification-cont.,MostoftheverificationtimeisspentdoingdebugHardware/softwareinteractionsAnalog/digitalinteractionsTestbenchsICdesignfocusonRTLverificationonlySoftwaredevelopmentafterICisreadyVerificationcanneverfinished!(example:achipfromCLcompany,ARM+DSPBasedPortableAudioDecoder,spend3yrsdesign,tapeout6times,butneveronproduction),TrendofFunctionVerification,NewmethodologiesandbettertoolsUnderstandsystemcontextHardware/softwareco-verificationLocaterootcauseofproblemseasilyAssertionbasedverification,Outlines,WhatisVerification?ProblemandTrendofFunctionVerificationHW/SWCo-verificationEmulatorbasedco-verificationESLdesigntoolbasedco-verificationAssertionBasedVerification(ABV)Methodology,Hardware/SoftwareCo-verification,SystemcomponentsNotjustHardwareRTOSSoftwareAnalogEnvironmentVerificationofcompletesystembothHW/SW,Hardware/SoftwareCo-verification,HW/SWco-verificationisamethodologythatenablestheexecutionofembeddedsystemsoftwareonasimulatedrepresentationofthesystemhardwareEmulatorbasedco-verification(emulation)ESLbasedco-verification,Emulation,EmulationisamethodofmodelingthedesigninhardwareEmulationdominatedbyFPGA-basedsystem,Co-Emulation,Integratingsimulationandemulationenvironmentsforco-verification.Providinganin-circuitverificationenvironment.Providingasystem-leveltestingenvironment.Providingasystemprototyping.,Co-verificationwithESLDesigntool,DoneinearlydesignstageMoreflexibleLessexpensive,Outlines,WhatisVerification?ProblemandTrendofFunctionalVerificationHW/SWCo-verificationEmulatorbasedco-verificationESLdesigntoolbasedco-verificationAssertionBasedVerification(ABV)MethodologyWhatisassertionAssertioninsimulationAssertioninformalverification,AssertionBasedVerification(ABV),Whyneedassertionbasedverification?Whatisassertionbasedverification?,CurrentPracticesofFunctionVerification,HDLsimulationwhereengineerswrite“reactivetestbenches”Checkwaveform,codecoverage,thenwritemorepatternsInputgenerationManual(verificationengineersthinkoftestcases)UsuallyorblocklevelverificationPseudo-randomNeedauto-testbenchtool,needtohaveaccuratemodelatabstractlevelNeedinputconstraintstolimittolegalvectorsNormallyforchiplevelverificationMixed(somerandomparameters)Needtowritealotofvectorstogetenough“coverage”!,CurrentPracticescont.,Lowcontrollability(cantgenerateenoughvectors).Lowobservability(internalerrorsmightnotpropagateduringtest).Doesntfacilitatereuse.,TrendofFunctionVerification,SmartersimulationProperties,Acceleratedsimulator,coveragetoolStaticformalverificationStartfromresetstate,lookingforproofDynamicformalverification(ormodelchecking,propertychecking,hybridformalverification)Startfromsimulationresult,provewhetherapropertyisholdunderthesimulation.LookingforcounterexamplesAssertionbasedverificationmethodologyAssertionsarestatementsabouthowthedesignisintendedtobehaveattheRTLlevelorhigherabstractionlevelsimulationbasedverificationFormalverificationwithadvancedhybridformaltool,Assertion-BasedVerification(ABV),Convergenceofdesignandverificationtocreateanimproveddesign-for-verificationmethodology.,Assertion,Assertionisaprecisedescriptionofwhatbehaviorisexpectedwhenagiveninputispresentedtodesign.usedasmonitors/checkerlookingforbadbehaviorduringverificationusedtocreateanalertfordesiredbehavior,AssertionBasedVerification(AVB),Assertionsmustbewrittenindesigncode(ClikesystemabstractionmodelorRTL)ortestbench(Establishassertions)asanenablerofmuchmoreefficientverification,simplifiedanalysis,andthesynergisticuseofsimulationandformalverificationmethods.,AssertioninsimulationCanbeusedasmonitor,coverageanalysistoolAssertioninformalverification(modelchecking)Canbeusedtowriteconstraintsofinputsandtowritethepropertyofthedesign,AssertionLanguagesinIndustry,Anassertionlanguage:standardassertionformatandgoodtoolsupportOpenVeraAssertionsLanguage(OVA)(Synopsys)PropertySpecificationLanguage(PSL)(IBM,basedonSugar)AcceleraOpenVerificationLibrary(OVL)SystemVerilogCorSystemC,Example:PropertiesWritteninOVL,Designspec:Afterrequestcondition(req)isasserted,anacknowledge(ack)mustoccurafter3andbefore7clockcycleshaveoccurred.Implementation:UsingOpenVerificationLibrary(OVL)showstheverificationofusingassert_framemoduleinVerilog,Example:PropertiesWritteninOVA,RTLfor8-bitcounter:modulecounter_8bit(rst,clk,cnt);inputrst,clk;output7:0cnt;reg7:0counter;always(rstorposedgeclk)if(rst)counter=8b0;elsecounter=counter+1;assigncnt=counterendmodule,Testbenchtocheckcounteroverflow:unitcounter_checker(logicclk,logic7:0counter);clocknegedge(clk)evente_overflow:(cnt=8hff)#1(cnt=8h00);asserta_overflow:check(e_overflow);endunitbindmodulecounter_8bit:counter_checker(clk,cnt);,Writeabstract(behaviorlevel)Assertion,AssertionimplementedinC/SystemC:SystemleveldesignAssertionimplementedinRTL:DesignengineerscanembedassertioncallsinlinewiththeirRTLdesign.Theassertionsdonotgetsynthesized.Assertionimplementedintestbench:instantiateassertioncallsinatestbench.Standardprotocol:suchAMBA,SDRAM,theremaybeexistsacheckertypeslibrary(availableassertion),justuseit.,Whatneedtobewrittenas“assertion”?,Whatneedtobewrittenas“assertion”?assertionsaboutthepropertiesaccordingtothespec.assertionsaboutthecornercase.assertionsaboutanyworrycasethatmaydisobeythedesignintentConstrainsforassertionareimportantRestricttheinputvectorstoberealisticconstrainsattheblocklevelinterface,alsocanbereusedbyotherconnectedblocks,orasassertionsinthechiplevelWithoutconstraints,aformalenginewillreportfalseerrorsinsteadofdesignbugs.,AssertionUsedinSimulation,Assertionsusedinsimulation:Assertionswereusedtoimproveobservability,whichmeanstheabilitytoobservebugsoncetheyaretriggeredbyasimulationvector.ItllspeedbuggingWithoutassertions,testvectorshadtobemuchlongertoensurethattriggeredbugswerepropagatedtoobservableoutputs,elsetheerrorsremainedundetected.Whenmanuallygeneratingthesimulationvector,thereisnoneedofinputconstraininthewholeflow,otherwisetheconstrainisratherimportant.,AssertionUsedinFormalVerification,ModelCheckingDynamicFormalVerification(HybridAnalysis)Usedatbehaviorallevelaftersimulationisverifiedandthedebugismodified.StartswithfullDUTstatestakenfromnormalsimulationtraces(“seeds”),hencetheterm“dynamic”.,Givenaseed,foreachassertionitusesanultra-fastboundedmodelcheckingalgorithmtoexhaustivelysearchforcounterexamplesthatcanbeproducedwithinafewcyclesstartingfromtheseed.,DynamicFormalverification,Pros&Cons,Pros:ProvidinginternaltestpointsinthedesignSimplifyingthediagnosisanddetectionofbugsbylocalizingtheoccurrenceofasuspectedbugtoanassertionmonitorAllowingdesignerstoverifythesame