资源描述：
《word level symbolic model checking a new approach for verifying arithmetic circuits》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、WordLevelSymbolicModelCheckingANewapproachforVerifyingArithmeticCircuitsE.ClarkeX.ZhaoMay,1995CMU-CS-95-161SchoolofComputerScienceCarnegieMellonUniversityPittsburgh,PA15213ThisresearchwassponsoredinpartbytheNationalScienceFoundationunderGrantNo.CCR-9217549,bytheSemiconductorResearchCorp
2、orationunderContractNo.94-DJ-294,andbytheWrightLaboratory,AeronauticalSystemsCenter,AirForceMaterielCommand,USAF,andtheAdvancedResearchProjectsAgency(ARPA)underGrantNo.F33615-93-1-1330.TheUSGovernmentisauthorizedtoreproduceanddistributereprintsforGovernmentpurposes,notwithstandinganycop
3、yrightnotationthereon.Viewsandconclusionscontainedinthisdocumentarethoseoftheauthorsandshouldnotbeinterpretedasrepresentingtheocialpolicies,eitherexpressedorimplied,ofWrightLaboratoryortheUnitedStatesGovernment.Keywords:automaticveri cation,temporallogic,modelchecking,binarydecisiondi-
4、agrams,multi-terminalbinarydecisiondiagrams,binarymomentdiagrams,hybriddecisiondiagrams,wordlevelproperties,arithmeticcircuit,Pentium,divisioncircuitAbstractThehighly-publicizeddivisionerrorinthePentiumhasemphasizedtheimportanceofformalveri cationofarithmeticoperations.Symbolicmodelchec
5、kingtechniquesbasedonbinarydecisiondiagrams(BDDs)havebeensuccessfulinverifyingcontrollogic.However,lackofproperrepresentationforfunctionsthatmapbooleanvectorsintointegershaspreventedthistechniquefrombeingusedforverifyingarithmeticcircuits.Wehaveusedhybriddecisiondiagramstorepresentthein
6、tegerfunctionsthatoccurinthearithmeticcircuitveri cation.Forthestatevariablescorrespondingtodatabits,ourrepresentationbehaveslikeabinarymomentdiagram(BMD)whileforthestatevariablescorrespondingtocontrolsignals,itbehaveslikeamulti-terminalBDD(MTBDD).Byusingthisrepresentation,weareabletoha
7、ndlecircuitswithbothcontrollogicandwidedatapaths.WehaveextendedthesymbolicmodelcheckingsystemSMVsothatitcanalsohandlepropertiesinvolvingrelationshipsamongdatawords.IntheoriginalSMVsystem,atomicformulascouldonlycontainstatevariables.Intheextendedsystem,weallowatomicfor-mulastobe
