资源描述:
《EQUIPE Parallel Equivalence Checking with GP-GPUs用GPGPU并行等价性检查》由会员上传分享,免费在线阅读,更多相关内容在学术论文-天天文库。
1、EQUIPE:ParallelEquivalenceCheckingwithGP-GPUsDebapriyaChatterjee,ValeriaBertaccoDepartmentofComputerScienceandEngineering,UniversityofMichigan{dchatt,valeria}@umich.eduAbstractCombinationalequivalencechecking(CEC)isamain-relatedcomputation,butalsoalgorithmswithahighdegreeofstreamapplicatio
2、ninElectronicDesignAutomationusedtodetermineparallelismandinvolvingalargeamountoflocalizedcomputation.theequivalencebetweentwocombinationalnetlists.ToolsperformingTothisend,severalvendorshaverecentlydevelopedgeneralpur-CECarewidelydeployedinthedesignflowtodeterminethecor-rectnessofsynthesis
3、transformationsandoptimizations.Oneoftheposeprogramminginterfacesthatenableuserstodevelopsoftwaremainlimitationsofthesetoolsistheirscalability,asindustrialscaleapplicationstargetingtheirGP-GPUs(forinstance,NVIDIAanddesignsdemandtime-consumingcomputation.InthisworkweproposeAMD).Whileparalle
4、lsolutionsforBDDcomputationsandSATEQUIPE,anovelcombinationalequivalencecheckingsolution,whichsolvershaveexperiencedonlymixedsuccesssofar,reachingaleveragesthemassiveparallelismofmoderngeneralpurposegraphiclimitedamountofspeedupoversingle-threadedexecution,otherprocessingunits.EQUIPEreduces
5、theneedforhard-to-parallelizeengines,suchasBDDsandSAT,bytakingadvantageofalgorithmscomponentsinCECarepronetoaggressiveparallelization.Thesewell-suitedtoconcurrentimplementation.Wefoundexperimentallythatincludesignature-basedanalysisandstructuraltechniques,whichEQUIPEoutperformscommercialCE
6、Ctoolsbyanorderofmagnitude,constituteapreponderantfractionofthecomputation,particularlyonaverage,andstate-of-the-artresearchCECsolutionsbyuptoawhenthenetlistsarederivedfromoneanotherbysynthesistrans-factorofthree,onawiderangeofindustry-strengthdesigns.formations,oftenappliedlocally.Whenthe
7、selattercomponentsI.INTRODUCTIONcanoperateeffectively,theneedforBDDandSATenginesisCombinationalequivalencechecking(CEC)isoneofthemostmuchreduced,thuslimitingthefractionofcomputationspentonpopularformalmethodsinthecontextofdigitalcircuitdesign.Thesequentialtask