基于多項(xiàng)式符號(hào)代數(shù)的電路形式驗(yàn)證.pdf

1、北京交通大學(xué)碩士學(xué)位論文基于多項(xiàng)式符號(hào)代數(shù)的電路形式驗(yàn)證姓名：閆碩申請學(xué)位級(jí)別：碩士專業(yè)：計(jì)算機(jī)科學(xué)與技術(shù)指導(dǎo)教師：吳盡昭201106ABSTRACTABSTRACT：IIlmodemwodd，tlleICiIldus包叮deVelopsr印idlyMore肌dInoreelec加Ilicproductscometoourlife謝thprofoulldinnuenceAstllesize，c印abilit)r鋤d缸lctionalco

2、mplexit)，ofintegratedcircuitdesigei11creaSing，t11esizeofcircuitst11emselvesbecomessmaUerAmdt_he矗lnctionalverificationh弱beenthemaillbottleneckill廿le￡lesignprocessThditionalVerificationmemodsalwaysb嬲eonsimulation，theyc鋤ots

3、upporttoday’s缸emendouSVerificationdemaI】ld伊aduallyInstead，newt班)eofmethcIdsuch嬲fo徹alverificationhaSbeenpaidmorea：ttentionsiIlacademicco塒mu】【li鑼andindus圩y、ⅣorldExiStillgflo鋤alv耐ficationtcchniquesarcmostlyfitforVerificatio

4、noflowlevelcon仃ol—dominatedcircuits111eyaredi伍cultt0satis每theverificationrequnmemoflligh—leveldatadominatedplaIlsWithahardworkscientiStsdevelopanewt11eo搿calledpolynomialsymbolicalgebra，whichcanbeaVe巧effectiVetecllIliquef

5、orrepresentationandcomputationofinte鏟ate(1circuitdesignsWhat’smore，itsuccess如llyoVercomessome、veal(pointsofthetraditionalfomlalVerificationmemodstoacerrtainde伊eeThereseachesoft11isthesisareasfollows：1Forthemainstre鋤forII

6、lalverificationm屺齜ds，thisthesisdoesanir卜depthsmd孔Whjchincludese)【poulldingthemaillprirlciplesalldmeansofmeseInethodsandspecifyingmecoInp撕sona11danalysisbe鉚eenthem2111isthesisbaSedonWu一＆ttandGroebnerbaSis西ves竹lefollo、杭ngr

7、esearchiIl缸lctionalequivalenceVerificationofhi曲一leveldatapaths：firstly，、Ⅳecallmodeldat印achsathi曲erleVelsofabs仃actiondirectly砸derthetheo巧ofPSA111egeneralfomofⅡlepolyIlomialsetrepresentationsofhigh19VeldatapathsandⅡlememod

8、toconStruCt“arcpresentedThen，staning缸’m也ecommonzerosofp01)momialset，mefurlctiomlequiValenceoflli曲一level缸印athsisdefinedFunllernlore，anewe虢ctivefhnctionalequiValenceVerificationalgo打t11lTf：masedonPSAiscreatedAnditscorrectl