摘要
ThispaperexploitsBooleansatisfiabilityprobleminequivalencecheckingandmodelcheckingrespectively.Acombinationalequivalencecheckingmethodbasedonincrementalsatisfiabilityispresented.Thismethodchoosesthecandidateequivalentpairswithsomenewtechniques,andusesincrementalsatisfiabilityalgorithmtoimproveitsperformance.Bysubstitutingtheinternalequivalentpairsandconvertingtheequivalencerelationsintoconjunctivenormalform(CNF)formulas,thisapproachcanavoidthefalsenegatives,andreducethesearchspaceofSATprocedure.ExperimentalresultsonISCAS'85benchmarkcircuitsshowthat,thepresentedapproachisfasterandmorerobustthanthoseexistedinliterature.Thispaperalsopresentsanalgorithmforextractingofunsatisfiablecore,whichhasanimportantapplicationinabstractionandrefinementformodelcheckingtoalleviatethestatespaceexplosionbottleneck.Theerrorofapproximateextractionisanalyzedbymeansofsimulation.Ananalysisrevealsthataninterestingphenomenonoccurs,withtheincreasingdensityoftheformula,theaverageerroroftheextractionisdecreasing.AnexactextractionapproachforMUsubformula,referredtoaspre-assignmentalgorithm,isproposed.Boththeoreticalanalysisandexperimentalresultsshowthatitismoreefficient.
出版日期
2005年01月11日（中国期刊网平台首次上网日期，不代表论文的发表时间）
