欢迎来到天天文库
浏览记录
ID:36619834
大小:2.10 MB
页数:61页
时间:2019-05-13
《基于吴方法的高层次模型检验方法研究》由会员上传分享,免费在线阅读,更多相关内容在学术论文-天天文库。
1、分类号:UDC:密级:编号:工学硕士学位论文基于吴方法的高层次模型检验方法研究硕士研究生:杨志指导老师:马光胜教授学位级别:工学硕士专业:计算机应用技术所在单位:计算机科学与技术学院论文提交日期:2008年1月论文答辩日期:2008年1月学位授予单位:哈尔滨工程大学Abstract舡thesizeandfunctionalcomplexityofintegratedcircuitsincrease,designverificationbecomesamoreandmoreimportantaspectofthede
2、signtlow‘ClassicalsimulationmethodcannotmeetwiththetremendousverificatlondemandofcomplexICdesigns.Becauseofthis,formalverificationreceivesmoreandmoreattentionsfromacademiccirclesasanimportantassistant·As0neofimportantformalverification‘techniques,modelchecking
3、ISwidelvusedintheindustrialpracticebecauseofthetraitofhighdegreeofautomationandstrongability.ExistingmodelcheckingmethodsaremostlYbasedonbit.1eveltechniquessuchasBDDorSAT,whichmainlyaimatlowleVelcontr01dominateddesigns.However,currentchipsemphasistheabilitieso
4、fsignalprocessing,datacommunication,picture/multimediaprocessingandoperatlon·Avarietvofcommunicationunits,rangingfromarithmeticoperationmodulestOdatapathsareembeddedonasignalchip.ExistingmodelcheckingtechniquesarehardtOsatis“theverificationrequirementofhighlev
5、eldatadominateddeslgns·Inthispaper,anovelmodelcheckingapproachforthehighleveldesignvefificationisproposed.WeconducttheresearchfromtWOaspects:theexPresslonmodelandtheverificationalgorithm.Intheapproach,functionsofcircultcom‘ponentsarerepresentedbypolynomialequa
6、tions,andhighleveltemporall091cf0衄ulaearedirectlyappliedtothisrepresentation.Wu’smethodformechanlcaltheoremprovingisthenappliedintheframeworkofmodelchecking·Firstly,circuitisunrolledoveYtimeframestoobtainasetofpolynomialequatlons·Secondly,temporallogicformulaw
7、hichdescribesthepropertyistranslatedtOanothersetofpolynomialequationsaccordingtoboundedsemantics·Letthefirstsetofpolynomialequationsbe.thehypothesisandthesecondsetofpoIYnomlale口uationsbetheconclusion,thentheoriginalmodelcheckingproblemISreducedtothetaskoftheor
8、emprovingwhichcanbesolvedbyWu’smethodefficiently.Aseriesofexperimentshavebeendoneinordertovalidatetheproposedapproach.ExperimentalresultsdemonstratethatthenewapproachachleVestne哈尔滨
此文档下载收益归作者所有