基于吴方法的高层次模型检验方法研究

基于吴方法的高层次模型检验方法研究

ID:36619834

大小:2.10 MB

页数:61页

时间:2019-05-13

基于吴方法的高层次模型检验方法研究_第1页
基于吴方法的高层次模型检验方法研究_第2页
基于吴方法的高层次模型检验方法研究_第3页
基于吴方法的高层次模型检验方法研究_第4页
基于吴方法的高层次模型检验方法研究_第5页
资源描述:

《基于吴方法的高层次模型检验方法研究》由会员上传分享,免费在线阅读,更多相关内容在学术论文-天天文库

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哈尔滨

当前文档最多预览五页,下载文档查看全文

此文档下载收益归作者所有

当前文档最多预览五页,下载文档查看全文
温馨提示:
1. 部分包含数学公式或PPT动画的文件,查看预览时可能会显示错乱或异常,文件下载后无此问题,请放心下载。
2. 本文档由用户上传,版权归属用户,天天文库负责整理代发布。如果您对本文档版权有争议请及时联系客服。
3. 下载前请仔细阅读文档内容,确认文档内容符合您的需求后进行下载,若出现内容与标题不符可向本站投诉处理。
4. 下载文档时可能由于网络波动等原因无法下载或下载错误,付费完成后未能成功下载的用户请联系客服处理。