基于布爾可滿足性的電路設計錯誤診斷.pdf

1、‘yla2_2乏了0後旦大學博士學位論文學校代“j：10246學≈：031021026基于布爾可滿足性的電路設計錯誤診斷院專姓系：信息科學與工程學院微電子系業(yè)：微電子與固體電子學名：吳洋指導教師：唐璞山教授完成日期：2006年9月20日AbstractAstoday’sVLSIdesignsgrowinscaleandcomplexity，e腫rsbecomemore讎quemanddi硒cuhtotrackinmedesignproc

2、essofiIIte疊Tatedcircuits，ManysophisticatedverificationaIgorit壬Imsatldtcclllliquesexistmatensuretheconcclnessofadesi2Itandanswerwhethcfcircuitimplementationisequivalemwithdesignst’ecificationVbrificationincludescircuitsim

3、ulationandfbnnalvefificationwhichiIlfo咖ofpropertycheckingandequivalencecheckingA11mesememodsonlydetecttheexistenceofdesilmenors，but∞uIdnottellfeasonswhyt11etwocircui￡sundercheckingarenotequivalemUnfortunatelyalthoughveri

4、ficationtoolsbecomemoree茄ciemaIldautomatic，designerrordiagmOsisa11dcorrectionofdigitalcircuitsstillremainsatimeconsumin譬’resOurceintensiveandmanuallyconductedprocedure111isthesisismainlyaboutSATbaseddesignerrordiagnosis，

5、anddescribeshowtolocatetIlesourceofeⅡorsinanerroneousimplementationofdesignspecmcationAlsoanoveldesignefrordiagnosismethodforcombinationalcircuitsisp坤sented0urapproachdoesnotincorporaleanerrormodeland，thus，issuitableforg

6、eneraltypesofdesignerrorsItcapturesthecircuit’slogicerrorbyanon—defe徹inisticbe量laviorofthecomponentundermodelfrceconditionnisthesisblliI出ahyb“dsemi—fomaltecIlIli口uecombinedwitlltraditiomlsimulationbasedappmachandmultiple

7、SATsolVingtechniqueFirstitdiagnosebyaSATsolVingprocedure，thenasmallsuspiciouslistisobtainedforlightenburdenoflocalerforsimuIationwithJosslessanypotentialsolutionS，0nlythesignaJsthatcancorrecteverygivenerroneousinputvecto

8、rSarecoIlsideredasapotentialerrorsourceAniIlcrementalSArb髂eddiagnosismethodisproposed，whichdecomposesmultipIeerrordiagnosisi“tosub—problemswithsmallerrorcardina“ty’sotlatadimcuhprobIemistmllsfo衄edtoeasyonesOurapproachisS

9、A：rbasedConsideringmedi行brenceofenors7cardinalityreIatedtoeveryinputtestvector，、vetransformthediagnosisproblemtoaSATproblembyinseningextrastrictorrelaxlogicaImodulesinl[ocircuittobnndaconstraineddiagnosisconfigurationWeu

10、seamodinedSATsolver嬲acomputerenginetoapplytocircu“diagnosisfield，Wealsoimprovedtheresolution甜1daccuracyofdiagnosisbyr銣噍in譬andscreenin疊satsolutionswthstnlctmIinfomationofcirc“ts，Anumberofhe嘶sticsareproposedthatkeepthememo

11、d’smemory徹dnlntimeemcientExperimentsshowthatduetoSArbaseddia髓osisguaranteestoret啪aco玎ection，sousingfonnaltectlIliquestodircctsimulationcaptllfessi鯽訪cantcllamctcristics卸dimprovesthee矗色ctivcness柚demciencyofmeproblemofdia蛐o