An Efficient Approach for Error Diagnosis in HDL DesignOutlineOutlineHDL Design ValidationProblem DescriptionSome DefinitionError SpaceBack-tracing OperationBack-tracing TerminationBack-tracing TerminationOutlineFlowOutlineError Space ReductionError Space ReductionError Space ReductionError Space ReductionError Space ReductionError Space Reduction Rule IError Space Reduction Rule IError Space Reduction Rule IError Space ReductionError Space ReductionError Space ReductionError Space ReductionError Space Reduction Rule IIError Space Reduction Rule IIError Space Reduction Rule IIIError Space Reduction Rule IIIOutlineExperimental ResultsSummaryOutlineConclusionsAn Efficient Approach for Error An Efficient Approach for Error Diagnosis in HDL DesignDiagnosis in HDL DesignNCTU EENCTU EECheChe--HuaHuaShih Shih JingJing--Yang Yang JouJouOutlineOutlinePreliminariesPreliminariesFlowFlowError Space ReductionError Space ReductionExperimental ResultsExperimental ResultsConclusionsConclusionsOutlineOutlinePreliminariesPreliminariesFlowFlowError Space ReductionError Space ReductionExperimental ResultsExperimental ResultsConclusionsConclusionsHDL Design ValidationHDL Design ValidationDesign Spec.Design Spec.HDL CodingHDL CodingDebugHDL SimulationHDL SimulationIs Function Correct?Is Function Correct?NYFinishFinishProblem DescriptionProblem DescriptionGivenGiven¾¾An implementation in HDLAn implementation in HDL¾¾An erroneous test case, which can differentiate An erroneous test case, which can differentiate the implementation and the design specificationthe implementation and the design specificationObjectiveObjectiveProvide a small set of error candidates for Provide a small set of error candidates for designers to locate the error source rapidlydesigners to locate the error source rapidlySome DefinitionSome DefinitionA primary output (PO) whose simulation A primary output (PO) whose simulation value is the same as the expected one is value is the same as the expected one is called a called a Correct PO Correct PO ((CPOCPO););otherwise it is otherwise it is called an called an Erroneous PO Erroneous PO ((EPOEPO))ErrorError--Observed Clock CycleObserved Clock Cycle((EOCEOC) :) :The simulation cycle in which the values of The simulation cycle in which the values of POs are different from the expected onesPOs are different from the expected onesError SpaceError SpaceError Space: A set of error candidatesError Space: A set of error candidatesA statement could be an error candidate of the A statement could be an error candidate of the EPO, ifEPO, if¾¾It was executed, and It was executed, and ¾¾It could affect the EPOIt could affect the EPOError space obtained by our approach is Error space obtained by our approach is constructed by backconstructed by back--tracing the executed tracing the executed statements from the EPOstatements from the EPOBackBack--tracing Operationtracing Operationop3op1 op2BTS(A) BTS(B) BTS(C) BTS(D)G(EPO)EFABCDAll statementsExecuted statementsHDL code:…….A=….B=….C=….D=….E=A op1 B;F=C op2 D;G=E op3 F;BTS(V): The set of executed statements that are backBTS(V): The set of executed statements that are back--traced from variable Vtraced from variable VError space of the above example:Error space of the above example:““G=E op3 FG=E op3 F””, , ““F=C op2 DF=C op2 D””, , ““E=A op1 BE=A op1 B””, BTS(D), BTS(C),, BTS(D), BTS(C),BTS(B),BTS(A)BTS(B),BTS(A)BackBack--tracing Terminationtracing TerminationError space obtained by backError space obtained by back--tracing from tracing from the EPO may expand exponentiallythe EPO may expand exponentiallyÎÎTerminate the backTerminate the back--tracing operations tracing operations earlier can greatly reduced the error spaceearlier can greatly reduced the error spaceEPOBackBack--tracing Terminationtracing TerminationError space without any error in it is Error space without any error in it is uselessuselessWe assure that at least one error is We assure that at least one error is remained in the error space After remained in the error space After terminating some backterminating some back--tracing operations tracing operationsOutlineOutlinePreliminariesPreliminariesFlowFlowError Space ReductionError Space ReductionExperimental ResultsExperimental ResultsConclusionsConclusionsFlowFlowN=EOCN=EOCInclude the back-traced statements into error space at the N-th clock cycleInclude the back-traced statements into error space at the N-th clock cycleN=N-1Apply rules to terminate back-tracingApply rules to terminate back-tracingAny back-tracing path?Any back-tracing path?YesNoDisplay the error spaceDisplay the error spaceOutlineOutlinePreliminariesPreliminariesFlowFlowError Space ReductionError Space ReductionExperimental ResultsExperimental ResultsConclusionsConclusionsError Space ReductionError Space ReductionReversible statementReversible statement: : A statement whose rightA statement whose right--hand side variable (RV) can be hand side variable (RV) can be computed by knowing the value of its leftcomputed by knowing the value of its left--hand side hand side variable (LV)variable (LV)ex: C=~A ,C=A ,C=A+2ex: C=~A ,C=A ,C=A+2Reversible pathReversible path: : A path that only consists of reversible statementsA path that only consists of reversible statementsex: ex: ““B=A+1; C=~B; D=C;B=A+1; C=~B; D=C;””,,A to D is a reversible pathA to D is a reversible pathError Space ReductionError Space ReductionLemma 1Lemma 1¾¾Given a reversible path ending with a POGiven a reversible path ending with a PO¾¾If If ¾¾PO value is correct, andPO value is correct, and¾¾All statements on the reversible path are correctAll statements on the reversible path are correct¾¾ThenThen¾¾The value of any variable on the reversible path is The value of any variable on the reversible path is correctcorrectError Space ReductionError Space Reduction11s−s1, s2, and s3 are three reversible statementsis the inverse function of s1v1s1v2)1(12vsv=)2(111vsv=−s2)2(23vsv=)3(221vsv=−v3)3(3vsPO=)(331POsv=−s3POError Space ReductionError Space ReductionTheorem 1Theorem 1¾¾Given a reversible path ending with a POGiven a reversible path ending with a PO¾¾IfIf¾¾The PO value is correct, andThe PO value is correct,