基于布尔可满足性的电路设计错误诊断算法pdf

18920069JOURNALOFCOMPUTER2AIDEDDESIGN&COMPUTERGRAPHICSVol118,No19Sep1,2006:2005-09-30;:2006-01-19:(90207002)(201203)(wuyang@fudan1edu1cn),,1,,;,,1,,,1;;TN47MultipleDesignErrorDiagnosisUsingBooleanSatisfiabilityWuYangTangPushan(StateKeyLaboratoryofASIC&System,MicroelectronicsDepartment,FudanUniversity,Shanghai201203)AbstractAnoveldesignerrordiagnosisalgorithmforcombinationalcircuitsispresented1Itcanperformmodel2freelogicerrorlocationbycombiningtraditionalsimulation2basedapproachwithaSATsolver1Anin2crementalSAT2baseddiagnosismethodisproposed1Weimprovedtheresolutionandaccuracyofdiagnosisbyrankingandscreeningsatsolutionswithstructuralinformationofcircuits1Anumberofheuristicsarepro2posedthatkeepthemethodsmemoryandrun2timeefficient1Experimentalresultsshowthatusingformaltechniquestodirectsimulationcapturesthemaincharacteristicsoferrorlocationandimprovestheeffective2nessandefficiencyofdesignerrordiagnosis1Keywordsdesignerrordiagnosis;Booleansatisfiability;electronicsdesignautomation01,,,,1,,1,,[1],1(designerrordiagnosis,DED),1(hardwaredis2creptionlanguage,HDL),11,,,,1,,,,1DED[2][3][4]31,,,;,;,1DED,[5]1Abadir[6],,1(model2free),,[728]1NP[9],(satisfiability,SAT)DED[10],SAT1,,110,DPLL(DavisPutnamLogemannandLoveland)SAT[11212]1SAT[13][14][15]SAT,,,DED,1,,1SAT;,111RTL,;,AND,OR,XOR,BUFF,NOT,NAND,NORXNOR1,11CV,,1[16],[17]1,1Model2free,,11,,,21,V11X={x1,x2,,xm},S={s1,s2,,sn},CY={y1,y2,,yn},siyi(1in)1S(X)={s1(X),s2(X),,sn(X)}Y(X)={y1(X),y2(X),,yn(X)}111v,vyi(v)si(v),1in,v;,121ve,vyi(ve)si(ve),1in,yi;,1ve,YEO(ve)CO(ve)2131(stembranch)1,111141,;,1,V1,151,1483120060,;1,P11,;,1,100%12SAT211SAT,,,SAT1AB,11A,2,1,:sel0,za;sel1,za1B,3,1,:sel0,za;sel1,zb11AB,(conjunctivenormalform,CNF):A(sel+…a+z)(sel+a+€z)(sel+a+z)(sel+…a+€z);B(sel+…a+z)(sel+a+…z)(sel+…b+z)(sel+b+…z)1b,,1,zb,ba1AB4,12,CNFB1,ACNF,B,1ve1,,2AB,1CNF,ve1CNF1:,;112AB,,1,,CNF1SAT,,1,12A,(1,0,1),GNAND,101GA,CNF(a+x1)(a+x2)(…a+x1+x2)(sel+…a+z)(sel+a+…z)(sel+a+z)(sel+…a+…z)(y+z)(y+x3)(…y+…z+x3)(x1)(x2)(x3)(y)14,3G,4A,3H,41y114,sel11212,N,N(1NN),131,58319:,Ve={ve1,ve2,,vek}1ve1,1,A1[18]A,,,,,SAT1CNFCNF,CNF1N(1NN),CNFSAT1,CNF1L={l1,l2,,lN}1ve1,1|L|=N,2,,,1|L|=N,,|L|N,ve1,13ve2,ve3,,A,|L|N1B,ve2ve11,,VN1,,,1,Model2free,SAT,,1213SAT,SAT,VLSI1SAT,Zchaff[11],BerkMin[12],CNF,1DED,SAT,SAT161SAT,()SAT1,NP,,1:,1DPLL,(Booleanconstraintpropa2gation,BCP)Zchaff,[11]1,,SAT,1,,,1,1SAT,,Restart,,1683120063311Diagnosis(SetofNodesL,SetofTestVectorsV,intN)beginRandomSimulationandGroupTestVectorsPPgetsortederroneousvectorsveforeach(erroneousvectorveive)letP:Setof(SetofNodesL)PPPissuspiciousnodessetCriticalPathTracePPgetPforeach(nodePiP)insertmoduleAonPiGenerateCNFformulafromSubcircuitGenerateCNFformulafrominput,outputlvGenerateCNFformulafromerrorcardinalityconstrainslwSatsolve(CNFformula)lxletS:Setof(SetofNodesPandQ)PPSissatsolutionslyGroupandSortSlzletSa:SetofSolutionsSwithcardinality=Nl{letSb:SetofSolutionsSwithcardinalityNl|foreach(solutionSaiSa)l}foreach(erroneousvectorveive)l~if(errorsimulatin(Sai)=true)thenreturnSaimuelsebreakmvletQ:Setof(SetofNodesL)PPQissuspiciousnodessetmwQ:=Q+nodeinSbmxforeach(nodeQiQ)myinsertmoduleBonQimzendLV1(),AB(1,Q,A)(),CNF,(lv)1CNFSAT(lw)1N,2:NN12,211(ly),(l|mu)1,SAT,,,,,,;,SATN,,2N-1,1,12,(s1,s2),(0,1),(0,0),(1,0),(1,1),,,,11,SAT12B(mvmy),131211,EO(ve)CO(ve)21,,1,,A,SAT111SAT,12111,,,1112ab,ba,ab1a,b12,,178319:31SAT1,AB,,,BCP1AB,,1B,(sel+…b)141SAT,1SAT,CNF,,CNF1SAT,,1SAT,,1,,,,141414SunBlade1000900MHzUltraSPARCIII2GBSo2laris8,ISCAS851,1131,,1,1,3:1);2);3)11DEDCPUPsSATPsPsPsPsSATPsPsPsC432100111767010006901000080100400200112000010037801000320151500C499100114033010005501000220100833200113633010135301001540100688C880100124167010001101000250100900200123732010000201002362118167C1355100136300010016401000670102000200136733012173701002670101439C1908100150867010007401000560101567200151212010000101003150181767C2670100169367010000301000860100367200170767012279701005510124633C3540100198933010000101001670100700201100667010182601004860104727C5315101148700010030301002170101267201155985010014201012570138565C6288101172733010017801008780104167201180591011606201011490109467C75521021161330100807010014201080002021173000100003010119301134001ISCAS8550132000,10,20,21:1SAT=SATP1SAT,121,,1,88312006,12,1,100%12[10]P%P%[10]P%P%C432255250997,502241599C49955842599148,1511661399C88086742599296,35533399C135599691111991292,1323100154C190831342599313,280012401851C26703877110099500,387725099C3540126461617991714,4545101099C53151150250991475,42773231199C628854952099545,14461661399C7552106471371799528,11094721198DED,1,,11[10],,[10],,,NSolution,1PNSolution12,,501311DED,[3][10],13:CriticalPathTrace,,13s[3]3[10]3[3]3[10]3C432501160112167501630163500C49912115001148661331750114321C880701270125067821042141899C13551611640138300731780138172C190817016201524341671411132979C267043016601697342151860195400C35406011940199633137241981105394C53158411321149967141211801194552C6288608190117690032441681631190058C7552205818521241331168341592130700:3,[10]98319:4341121434PsC43211401330113400C49911