资源描述：
《the formal specification and verification of the fm9001 microprocessor》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、AnOverviewoftheFormalSpeci cationandVeri cationoftheFM9001MicroprocessorBishopC.BrockandWarrenA.Hunt,Jr.brock@cli.com,hunt@cli.comFall,1994Theuseofmathematicallogicformodelingandreasoningabouthardwaredesignspromisesassuranceofcircuitcorrectnessbeyondwhatisavailablefromcurr
2、entstate-of-practicetechniques.Thedevelopmentanduseofformaltech-niquesinhardwaredesignisspreading[5,13,16,19,20,25,28,36,45].Thisapproachtocircuitvalidationisknowngenerallyashardwareveri cation.Cir-cuitswiththecomplexityofmicroprocessors[5,30,35,46]havebeengivenmathematica
3、lspeci cations,andtheirdesignshavebeenprovedtoimplementtheirspeci cations.Yet,thetransferofhardwareveri cationtechniquestocommercialengineeringpracticehasbeenhamperedbysuchfactorsastheuseofnon-standardnotations,inaccessibilityofthetools,andthesigni cantmath-ematicalsophist
4、icationrequiredtousetheseapproaches.Inaddition,formaltechniqueshavebeendirectedatonlyselectedaspectsofthedesignprocess.Im-portanthardwarecharacteristicssuchastestabilityandI/Obehaviorhavebeenlargelyneglectedbytheformalhardwaremodelingandveri cationcommunity.Wehaveattempted
5、toaddresssomeoftheseissuesbyconsideringtheformalspeci cation,veri cation,andphysicalimplementationoftheFM9001micropro-cessor.TheFM9001isageneral-purpose32-bitmicroprocessorwhosegate-levelnetlistdesignimplementationwasdevelopedusingatheorem-provingenviron-mentinconjunctionw
6、ithatraditionalCADsystem.Thebehavioralspeci ca-tionfortheFM9001,thede nitionofthehardwaredescriptionlanguage(HDL)usedtorepresentthedesignoftheFM9001,thesimulatorfortheHDL,andtheveri cationoftheFM9001wereallcarriedoutusingtheBoyer-Mooretheorem-provingsystemNqthm[9].TheFM900
7、1netlistwasmechanicallytranslatedtoLSILogic'sNetlistDescriptionLanguageandimplementedbyLSILogic,Inc.,asaCMOSgate-array.Rigoroustestinghasnotuncoveredanysituationwherethemanufactureddevicefailstomeetitsspeci cation.TheFM9001alsoservesasthetargetfortheveri edassembler,Piton[
8、42],whichinturnservesasthetargetoftheveri ed-Gypsycompiler[49].Thisdocumentpresentsthede
