基于GSTE驗(yàn)證的細(xì)化問題的研究.pdf

1、㈤龜占科技女管碩士學(xué)位論文MASTERDlSSERTATlON論文題目接于GsrE驗(yàn)證的紐I化問趔n“Nf究學(xué)科專業(yè)指導(dǎo)教師作者姓名班學(xué)號l算機(jī)應(yīng)川技術(shù)雷航教授鄖德生200520604012AbstractAbstractWiththeincreasingcomplexityandtighttime—tomarkerschedulesoftoday’Sdigital，verificationisbecomingmoreandmoredi

2、fficultThereportinInternationaltechnologyroadmapforSemiconductor2003haspointedoutthatverificationhasbeenthebottleneckintheICdesignflowExtensivesimulation，thetraditionalapproachisnolongeradequatebecauseitistootimeconsumin

3、ganditgivesnoabsoluteguaranteesaboutthecorrectnessofthedesignFormalverificationmethodsareappliedtoactuallyconstructamathematicalproofforthecorrectnessofthedesign。Soitcanimprovetheverification’Scorrectnessandassuremarketr

4、equirementInadditionformalverificationasoneofcomplementaryapproaches，hasbeenputforwardtosolvetheseproblemsWithlotsofpreviousworkonformalverificationonlargedigitalICdesignstudyandextendGSTEmethodwhichisoneofthecurrentlymo

5、stimportantformalverificationmethodsdeeplytoreducethefalsenegativefurtherandimprovethecorrectnessbyusingGSTEmethodinintegratecircuitverificationOnstudymethods，thepaperintroducesthebasictheoryandtechnologyofSTEverificatio

6、nalgorithmandanalyzesthestrongpointandshortageindetail。ForextendingSTEverificationspecificationusinggraphicaltheoryintroducingtheconceptofassertiongraphandimplementassertionbasedverificationalgorithm，thepaperanalyzesthem

7、indetailThenimportconceptoftheGSTEandcomparetheadvantagesandweaknessesbetweenSTEandGSTEGSTEinheritstheabstractbehaviorofSTEItmeansittakeswiththefalsenegativeproblems弧epaperanalyzesthereasonthatmakesthefalsenegativeproble

8、msandputsforwardanimprovedalgorithmonGSTE’SSMCalgorithmAtlastuseFORTEtoverifytheimprovedalgorithm。TheresultshowstheimprovedalgorithmmakeprogressinreducingthefalsenegativeandcheckingfaultIfsomeoneisnotfamiliarwiththecircu

9、it，theycanusetheimprovedalgorithmofGSETtoveritythecircuitcorrectnessForothers。訊eyCanextendtheloopbyhandsAtthesametime，fortheautomationoftheverificationtool，bringforwardawaynamedautomaticinsertionoffaulttolerantWenoticeth