资源描述：
《pii-7 implication of assertion graphs in gste》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、PII-7ImplicationofAssertionGraphsinGSTE11GuowuYang,JinYang,WilliamN.N.Hung,andXiaoyuSongDepartmentofElectrical&ComputerEngineering,PortlandStateUniversity,OR,USA1IntelCorporation,Hillsboro,OR,USAAbstract-Weaddresstheproblemofimplicationofassertionassertiongraphs,thu
2、savoidingthereachabilitycomputationgraphsthatoccuringeneralizedsymbolictrajectoryevaluationinGSTEandsidestepthebiggestpotentialcauseforthe(GSTE).GSTEhasdemonstrateditspowerfulcapacityinBDDexplosionproblem.Wehavesuccessfullyappliedbothformalverificationofdigitalsyste
3、ms.Assertiongraphsareusedmodel-basedimplicationandlanguage-basedimplicationonforpropertyandmodelspecifications.Wepresentanovelrealindustrialcircuits.implicationtechniqueforassertiongraphs.ItreliesondirectBooleanreasoningoneachedge(andvertex)ofanassertiongraph,thusav
4、oidingthereachabilitycomputationinGSTE.II.PreliminariesWehavesuccessfullyappliedbothmodel-basedandlanguage-basedimplicationsonrealindustrialcircuits.Weintroducesomebasicdefinitionsinthissection.SomeExperimentalresultsdemonstratethepromisingperformanceofthemweregiven
5、in[1,2].Weassumeanon-emptysetofofourapproach.finitestates,denotedbyS.ArelationΤ⊆S×Sisatransitionrelationif∀s∈S,∃s’∈S,(s,s’)∈T,whereSisanon-emptysetoffinitestates.ThemodelMinducedbythetransitionI.IntroductionrelationTisthepair(pre,post)where:(1)thepre-imagetransforme
6、rpre:2S→2Sisdefinedas:pre(Q)={s
7、∃s’∈Q,(s,SymbolicTrajectoryEvaluation(STE)[1]isthemains’)∈T}forallQ∈2S;and(2)thepost-imagetransformeralternativetosymbolicmodelchecking(SMC).ComparedSSpost:2→2isdefinedas:post(Q)={s’
8、∃s∈Q,(s,s’)∈T}withSMC,whichusuallyrequiresabstracti
9、on[7],STEhasSforallQ∈2.LetM=(pre,post)beadirectedgraphM=(S,T).theadvantageofbeingappliedtoverylargecircuitsdirectly.WeusepreandposttorepresenttwofunctionsbasedonM.TheSTEtheoryconsistsofasimplespecificationlanguage,Notethatpre(s)=pre({s}),post(s)=post({s}),foralls∈S.
10、Ifasimulation-basedmodelcheckingalgorithm,andaforalls∈S,post(s)isdefinedandnonempty,thenMismappingofthealgorithmtoacoarseabstractdomain.Th
