diff options
| -rw-r--r-- | src/base/abci/abc.c | 115 | ||||
| -rw-r--r-- | src/sat/bmc/bmcFault.c | 314 |
2 files changed, 285 insertions, 144 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1c7e1156..83fd0933 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -33250,12 +33250,14 @@ usage: int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_ParFfSetDefault( Bmc_ParFf_t * p ); - extern void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ); + extern void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ); Bmc_ParFf_t Pars, * pPars = &Pars; + char * pFileName = NULL; + Gia_Man_t * pGold = NULL; int c; Gia_ParFfSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ATScsbduvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ATSGsbduvh" ) ) != EOF ) { switch ( c ) { @@ -33290,8 +33292,14 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pFormStr = argv[globalUtilOptind]; globalUtilOptind++; break; - case 'c': - pPars->fComplVars ^= 1; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by string.\n" ); + goto usage; + } + pFileName = argv[globalUtilOptind]; + globalUtilOptind++; break; case 's': pPars->fStartPats ^= 1; @@ -33348,43 +33356,74 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9FFTest(): For delay testing, AIG should be sequential.\n" ); return 0; } - Gia_ManFaultTest( pAbc->pGia, pPars ); + // check if the file is valid + if ( pFileName ) + { + FILE * pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9FFTest(): File name \"%s\" with golden model is invalid.\n", pFileName ); + return 0; + } + fclose( pFile ); + pGold = Gia_AigerRead( pFileName, 0, 0 ); + if ( pGold == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9FFTest(): Cannot read file \"%s\" with golden model.\n", pFileName ); + return 0; + } + if ( Gia_ManPiNum(pAbc->pGia) != Gia_ManPiNum(pGold) ) + { + Gia_ManStop( pGold ); + Abc_Print( -1, "Abc_CommandAbc9FFTest(): Old model and gold model have different number of PIs.\n" ); + return 0; + } + if ( Gia_ManPoNum(pAbc->pGia) != Gia_ManPoNum(pGold) ) + { + Gia_ManStop( pGold ); + Abc_Print( -1, "Abc_CommandAbc9FFTest(): Old model and gold model have different number of POs.\n" ); + return 0; + } + printf( "Entered spec AIG from file \"%s\".\n", pFileName ); + } + Gia_ManFaultTest( pAbc->pGia, pGold ? pGold : pAbc->pGia, pPars ); + Gia_ManStopP( &pGold ); return 0; usage: - Abc_Print( -2, "usage: &fftest [-AT num] [-csbduvh] <file> [-S str]\n" ); - Abc_Print( -2, "\t performs functional fault test generation\n" ); - Abc_Print( -2, "\t-A num : selects fault model for all gates [default = %d]\n", pPars->Algo ); - Abc_Print( -2, "\t 0: fault model is not selected (use -S str)\n" ); - Abc_Print( -2, "\t 1: delay fault testing for sequential circuits\n" ); - Abc_Print( -2, "\t 2: traditional stuck-at fault: -S (((a&b)&~p)|q)\n" ); - Abc_Print( -2, "\t 3: complement fault: -S ((a&b)^p)\n" ); - Abc_Print( -2, "\t 4: functionally observable fault\n" ); - Abc_Print( -2, "\t-T num : specifies approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-c : toggles complementing control variables [default = %s]\n", pPars->fComplVars? "active-high": "active-low" ); - Abc_Print( -2, "\t-s : toggles starting with the all-0 and all-1 patterns [default = %s]\n", pPars->fStartPats? "yes": "no" ); - Abc_Print( -2, "\t-b : toggles testing for single faults only [default = %s]\n", pPars->fBasic? "yes": "no" ); - Abc_Print( -2, "\t-d : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", pPars->fDump? "yes": "no" ); - Abc_Print( -2, "\t-u : toggles dumping untestable faults into \"untest.txt\" [default = %s]\n", pPars->fDumpUntest? "yes": "no" ); - Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); - Abc_Print( -2, "\t<file> : (optional) file name with input test patterns\n\n"); - Abc_Print( -2, "\t-S str : (optional) string representing the fault model\n"); - Abc_Print( -2, "\t The following notations are used:\n"); - Abc_Print( -2, "\t Functional variables: {a,b} (both a and b are always present)\n"); - Abc_Print( -2, "\t Parameter variables: {p,q,r,s,t,u,v,w} (any number from 1 to 8)\n"); - Abc_Print( -2, "\t Boolean operators: AND(&), OR(|), XOR(^), MUX(?:), NOT(~)\n"); - Abc_Print( -2, "\t Parantheses should be used around each operator. Spaces not allowed.\n"); - Abc_Print( -2, "\t Complement (~) is only allowed before variables (use DeMorgan law).\n"); - Abc_Print( -2, "\t Examples:\n"); - Abc_Print( -2, "\t (((a&b)&~p)|q) stuck-at-0/1 at the output\n"); - Abc_Print( -2, "\t (((a&~p)|q)&b) stuck-at-0/1 at input a\n"); - Abc_Print( -2, "\t (((a|p)&(b|q))&~r) stuck-at-1 at the inputs and stuck-at-0 at the output\n"); - Abc_Print( -2, "\t (((a&~p)&(b&~q))|r) stuck-at-0 at the inputs and stuck-at-1 at the output\n"); - Abc_Print( -2, "\t ((a&b)^p) complement at the output\n"); - Abc_Print( -2, "\t (((a^p)&(b^q))^r) complement at the inputs and at the output\n"); - Abc_Print( -2, "\t (a?(b?~s:r):(b?q:p)) functionally observable fault at the output\n"); - Abc_Print( -2, "\t (p?(a|b):(a&b)) replace AND by OR\n"); + Abc_Print( -2, "usage: &fftest [-AT num] [-sbduvh] <file> [-G file] [-S str]\n" ); + Abc_Print( -2, "\t performs functional fault test generation\n" ); + Abc_Print( -2, "\t-A num : selects fault model for all gates [default = %d]\n", pPars->Algo ); + Abc_Print( -2, "\t 0: fault model is not selected (use -S str)\n" ); + Abc_Print( -2, "\t 1: delay fault testing for sequential circuits\n" ); + Abc_Print( -2, "\t 2: traditional stuck-at fault: -S (((a&b)&~p)|q)\n" ); + Abc_Print( -2, "\t 3: complement fault: -S ((a&b)^p)\n" ); + Abc_Print( -2, "\t 4: functionally observable fault\n" ); + Abc_Print( -2, "\t-T num : specifies approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut ); + Abc_Print( -2, "\t-s : toggles starting with the all-0 and all-1 patterns [default = %s]\n", pPars->fStartPats? "yes": "no" ); + Abc_Print( -2, "\t-b : toggles testing for single faults only [default = %s]\n", pPars->fBasic? "yes": "no" ); + Abc_Print( -2, "\t-d : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", pPars->fDump? "yes": "no" ); + Abc_Print( -2, "\t-u : toggles dumping untestable faults into \"untest.txt\" [default = %s]\n", pPars->fDumpUntest? "yes": "no" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t<file> : (optional) file name with input test patterns\n\n"); + Abc_Print( -2, "\t-G file : (optional) file name with the golden model\n\n"); + Abc_Print( -2, "\t-S str : (optional) string representing the fault model\n"); + Abc_Print( -2, "\t The following notations are used:\n"); + Abc_Print( -2, "\t Functional variables: {a,b} (both a and b are always present)\n"); + Abc_Print( -2, "\t Parameter variables: {p,q,r,s,t,u,v,w} (any number from 1 to 8)\n"); + Abc_Print( -2, "\t Boolean operators: AND(&), OR(|), XOR(^), MUX(?:), NOT(~)\n"); + Abc_Print( -2, "\t Parantheses should be used around each operator. Spaces not allowed.\n"); + Abc_Print( -2, "\t Complement (~) is only allowed before variables (use DeMorgan law).\n"); + Abc_Print( -2, "\t Examples:\n"); + Abc_Print( -2, "\t (((a&b)&~p)|q) stuck-at-0/1 at the output\n"); + Abc_Print( -2, "\t (((a&~p)|q)&b) stuck-at-0/1 at input a\n"); + Abc_Print( -2, "\t (((a|p)&(b|q))&~r) stuck-at-1 at the inputs and stuck-at-0 at the output\n"); + Abc_Print( -2, "\t (((a&~p)&(b&~q))|r) stuck-at-0 at the inputs and stuck-at-1 at the output\n"); + Abc_Print( -2, "\t ((a&b)^p) complement at the output\n"); + Abc_Print( -2, "\t (((a^p)&(b^q))^r) complement at the inputs and at the output\n"); + Abc_Print( -2, "\t (a?(b?~s:r):(b?q:p)) functionally observable fault at the output\n"); + Abc_Print( -2, "\t (p?(a|b):(a&b)) replace AND by OR\n"); return 1; } diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index c52b5033..fd33a338 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -53,7 +53,6 @@ void Gia_ParFfSetDefault( Bmc_ParFf_t * p ) memset( p, 0, sizeof(Bmc_ParFf_t) ); p->pFileName = NULL; p->Algo = 0; - p->fComplVars = 0; p->fStartPats = 0; p->nTimeOut = 0; p->fBasic = 0; @@ -177,7 +176,7 @@ static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPl SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fComplVars ) +Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; @@ -202,7 +201,7 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fComplVars ) pObj->Value = Gia_ManAppendCi( pNew ); Gia_ManForEachAnd( p, pObj, i ) { - iCtrl = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); + iCtrl = Gia_ManAppendCi(pNew); iThis = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( fUseMuxes ) pObj->Value = Gia_ManHashMux( pNew, iCtrl, pObj->Value, iThis ); @@ -228,12 +227,12 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fComplVars ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars ) +Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; - int i, iCtrl0, iCtrl1; - pNew = Gia_ManStart( (1 + 2 * fUseFaults) * Gia_ManObjNum(p) ); + int i; + pNew = Gia_ManStart( 3 * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; @@ -242,13 +241,8 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars Gia_ManForEachAnd( p, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - iCtrl0 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); - iCtrl1 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); - if ( fUseFaults ) - { - pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(iCtrl0), pObj->Value ); - pObj->Value = Gia_ManHashOr( pNew, iCtrl1, pObj->Value ); - } + pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(Gia_ManAppendCi(pNew)), pObj->Value ); + pObj->Value = Gia_ManHashOr( pNew, Gia_ManAppendCi(pNew), pObj->Value ); } Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); @@ -269,12 +263,12 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars ) +Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; - int i, iCtrl0; - pNew = Gia_ManStart( (1 + 3 * fUseFaults) * Gia_ManObjNum(p) ); + int i; + pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; @@ -283,9 +277,7 @@ Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars ) Gia_ManForEachAnd( p, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - iCtrl0 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); - if ( fUseFaults ) - pObj->Value = Gia_ManHashXor( pNew, iCtrl0, pObj->Value ); + pObj->Value = Gia_ManHashXor( pNew, Gia_ManAppendCi(pNew), pObj->Value ); } Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); @@ -306,12 +298,12 @@ Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars ) +Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB; - pNew = Gia_ManStart( (1 + 8 * fUseFaults) * Gia_ManObjNum(p) ); + pNew = Gia_ManStart( 9 * Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; @@ -319,26 +311,21 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars ) pObj->Value = Gia_ManAppendCi( pNew ); Gia_ManForEachAnd( p, pObj, i ) { - iCtrl0 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); - iCtrl1 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); - iCtrl2 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); - iCtrl3 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); - if ( fUseFaults ) - { - if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) - iCtrl0 = Abc_LitNot(iCtrl0); - else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) - iCtrl1 = Abc_LitNot(iCtrl1); - else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) - iCtrl2 = Abc_LitNot(iCtrl2); - else //if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) - iCtrl3 = Abc_LitNot(iCtrl3); - iMuxA = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl1, iCtrl0 ); - iMuxB = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl3, iCtrl2 ); - pObj->Value = Gia_ManHashMux( pNew, Gia_ObjFanin1(pObj)->Value, iMuxB, iMuxA ); - } - else - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + iCtrl0 = Gia_ManAppendCi(pNew); + iCtrl1 = Gia_ManAppendCi(pNew); + iCtrl2 = Gia_ManAppendCi(pNew); + iCtrl3 = Gia_ManAppendCi(pNew); + if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) + iCtrl0 = Abc_LitNot(iCtrl0); + else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) + iCtrl1 = Abc_LitNot(iCtrl1); + else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) + iCtrl2 = Abc_LitNot(iCtrl2); + else //if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) + iCtrl3 = Abc_LitNot(iCtrl3); + iMuxA = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl1, iCtrl0 ); + iMuxB = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl3, iCtrl2 ); + pObj->Value = Gia_ManHashMux( pNew, Gia_ObjFanin1(pObj)->Value, iMuxB, iMuxA ); } Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); @@ -516,7 +503,7 @@ int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pStr, { return Gia_ManRealizeFormula_rec( p, pVars, pPars, pStr, pStr + strlen(pStr), nPars ); } -Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, char * pForm ) +Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm ) { char pStr[100]; Gia_Man_t * pNew, * pTemp; @@ -536,15 +523,10 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, Gia_ManForEachAnd( p, pObj, i ) { for ( k = 0; k < nPars; k++ ) - iCtrl[k] = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); - if ( fUseFaults ) - { - iFans[0] = Gia_ObjFanin0Copy(pObj); - iFans[1] = Gia_ObjFanin1Copy(pObj); - pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars ); - } - else - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + iCtrl[k] = Gia_ManAppendCi(pNew); + iFans[0] = Gia_ObjFanin0Copy(pObj); + iFans[1] = Gia_ObjFanin1Copy(pObj); + pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars ); } Gia_ManForEachCo( p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); @@ -701,23 +683,21 @@ void Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Ve SeeAlso [] ***********************************************************************/ -int Gia_ManDumpUntests( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, int nFuncVars, int LitRoot, char * pFileName, int fVerbose ) +int Gia_ManDumpUntests( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, int nFuncVars, char * pFileName, int fVerbose ) { FILE * pFile = fopen( pFileName, "wb" ); Vec_Int_t * vLits; Gia_Obj_t * pObj; int nItersMax = 10000; int i, nIters, status, Value, Count = 0; - assert( LitRoot > 1 ); vLits = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars ); for ( nIters = 0; nIters < nItersMax; nIters++ ) { - status = sat_solver_solve( pSat, &LitRoot, &LitRoot+1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_Undef ) - { printf( "Timeout reached after dumping %d untestable faults.\n", nIters ); + if ( status == l_Undef ) break; - } if ( status == l_False ) break; // collect literals @@ -745,11 +725,12 @@ int Gia_ManDumpUntests( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, int fprintf( pFile, "\n" ); } // add this clause - sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) ) + break; } Vec_IntFree( vLits ); fclose( pFile ); - return nIters-1; + return nIters; } /**Function************************************************************* @@ -791,6 +772,26 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName ) /**Function************************************************************* + Synopsis [Derive the second AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDeriveDup( Gia_Man_t * p, int nPisNew ) +{ + int i; + Gia_Man_t * pNew = Gia_ManDup(p); + for ( i = 0; i < nPisNew; i++ ) + Gia_ManAppendCi( pNew ); + return pNew; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -800,10 +801,10 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName ) SeeAlso [] ***********************************************************************/ -void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) +void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) { int nIterMax = 1000000, nVars, nPars; - int i, Iter, LitRoot, status, nFuncVars = -1; + int i, Iter, Iter2, status, nFuncVars = -1; abctime clkSat = 0, clkTotal = Abc_Clock(); Vec_Int_t * vLits, * vTests; Gia_Man_t * p0 = NULL, * p1 = NULL, * pM; @@ -859,31 +860,21 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) // select algorithm if ( pPars->Algo == 0 ) - { - p0 = Gia_ManFormulaUnfold( p, 0, pPars->fComplVars, pPars->pFormStr ); - p1 = Gia_ManFormulaUnfold( p, 1, pPars->fComplVars, pPars->pFormStr ); - } + p1 = Gia_ManFormulaUnfold( p, pPars->pFormStr ); else if ( pPars->Algo == 1 ) { assert( Gia_ManRegNum(p) > 0 ); - p0 = Gia_ManFaultUnfold( p, 0, pPars->fComplVars ); - p1 = Gia_ManFaultUnfold( p, 1, pPars->fComplVars ); + p0 = Gia_ManFaultUnfold( pG, 0 ); + p1 = Gia_ManFaultUnfold( p, 1 ); } else if ( pPars->Algo == 2 ) - { - p0 = Gia_ManStuckAtUnfold( p, 0, pPars->fComplVars ); - p1 = Gia_ManStuckAtUnfold( p, 1, pPars->fComplVars ); - } + p1 = Gia_ManStuckAtUnfold( p ); else if ( pPars->Algo == 3 ) - { - p0 = Gia_ManFlipUnfold( p, 0, pPars->fComplVars ); - p1 = Gia_ManFlipUnfold( p, 1, pPars->fComplVars ); - } + p1 = Gia_ManFlipUnfold( p ); else if ( pPars->Algo == 4 ) - { - p0 = Gia_ManFOFUnfold( p, 0, pPars->fComplVars ); - p1 = Gia_ManFOFUnfold( p, 1, pPars->fComplVars ); - } + p1 = Gia_ManFOFUnfold( p ); + if ( pPars->Algo != 1 ) + p0 = Gia_ManDeriveDup( pG, Gia_ManCiNum(p1) - Gia_ManCiNum(pG) ); // Gia_AigerWrite( p1, "newfault.aig", 0, 0 ); // printf( "Dumped circuit with fault parameters into file \"newfault.aig\".\n" ); @@ -895,9 +886,8 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) // start the SAT solver pSat = sat_solver_new(); - sat_solver_setnvars( pSat, pCnf->nVars + (pPars->fDumpUntest ? 1 : 0) ); + sat_solver_setnvars( pSat, pCnf->nVars ); sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); - LitRoot = pPars->fDumpUntest ? Abc_Var2Lit( pCnf->nVars, 1 ) : 0; // add timeframe clauses for ( i = 0; i < pCnf->nClauses; i++ ) if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) @@ -905,13 +895,11 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) // add one large OR clause vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); - if ( LitRoot ) - Vec_IntPush( vLits, Abc_LitNot(LitRoot) ); Gia_ManForEachCo( pM, pObj, i ) Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) ); sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); - // add cadinality constraint + // add cardinality constraint if ( pPars->fBasic ) { Vec_IntClear( vLits ); @@ -930,8 +918,22 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) for ( Iter = 0; Iter < nTests; Iter++ ) { abctime clk = Abc_Clock(); - status = sat_solver_solve( pSat, LitRoot ? &LitRoot : NULL, LitRoot ? &LitRoot+1 : NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); clkSat += Abc_Clock() - clk; + if ( status == l_Undef ) + { + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "Timeout reached after %d seconds and adding %d tests.\n", pPars->nTimeOut, Iter ); + goto finish; + } + if ( status == l_False ) + { + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "The problem is UNSAT after adding %d tests.\n", Iter ); + goto finish; + } // get pattern Vec_IntClear( vLits ); for ( i = 0; i < nFuncVars; i++ ) @@ -952,20 +954,20 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) { for ( Iter = 0; Iter < 2; Iter++ ) { - status = sat_solver_solve( pSat, LitRoot ? &LitRoot : NULL, LitRoot ? &LitRoot+1 : NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_Undef ) { if ( pPars->fVerbose ) printf( "\n" ); - printf( "Timeout reached after %d seconds and %d iterations. ", pPars->nTimeOut, Iter ); - break; + printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter ); + goto finish; } if ( status == l_False ) { if ( pPars->fVerbose ) printf( "\n" ); - printf( "The problem is UNSAT after %d iterations. ", Iter ); - break; + printf( "The problem is UNSAT after %d iterations.\n", Iter ); + goto finish; } // initialize simple pattern Vec_IntFill( vLits, nFuncVars, Iter ); @@ -978,7 +980,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) for ( Iter = pPars->fStartPats ? 2 : Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ ) { abctime clk = Abc_Clock(); - status = sat_solver_solve( pSat, LitRoot ? &LitRoot : NULL, LitRoot ? &LitRoot+1 : NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); clkSat += Abc_Clock() - clk; if ( pPars->fVerbose ) { @@ -993,8 +995,8 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) { if ( pPars->fVerbose ) printf( "\n" ); - printf( "Timeout reached after %d seconds and %d iterations. ", pPars->nTimeOut, Iter ); - break; + printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter ); + goto finish; } if ( status == l_False ) { @@ -1017,20 +1019,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) // if ( status == l_False ) // Gia_ManPrintResults( p, pSat, Iter, Abc_Clock() - clkTotal ); // cleanup - Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); - // dump untestable faults - if ( pPars->fDumpUntest ) - { - abctime clk = Abc_Clock(); - char * pFileName = "untest.txt"; - int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, Abc_LitNot(LitRoot), pFileName, pPars->fVerbose ); - printf( "Dumping %d untestable multiple faults into file \"%s\". ", nUntests, pFileName ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - } - Vec_IntFree( vLits ); - Cnf_DataFree( pCnf ); - Gia_ManStop( pM ); - sat_solver_delete( pSat ); + Abc_PrintTime( 1, "Testing runtime", Abc_Clock() - clkTotal ); // dump the test suite if ( pPars->fDump ) { @@ -1038,7 +1027,120 @@ void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) Gia_ManDumpTests( vTests, Iter, pFileName ); printf( "Dumping %d computed test patterns into file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pFileName ); } + + // compute untestable faults + if ( p != pG || pPars->fDumpUntest ) + { + abctime clkTotal = Abc_Clock(); + // restart the SAT solver + sat_solver_delete( pSat ); + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnf->nVars ); + sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); + // add timeframe clauses + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + assert( 0 ); + // add constraint to rule out no fault +// if ( p == pG ) + { + Vec_IntClear( vLits ); + Gia_ManForEachPi( pM, pObj, i ) + if ( i >= nFuncVars ) + Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) ); + sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + } + // add cardinality constraint + if ( pPars->fBasic ) + { + Vec_IntClear( vLits ); + Gia_ManForEachPi( pM, pObj, i ) + if ( i >= nFuncVars ) + Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ); + Cnf_AddCardinConstr( pSat, vLits ); + } + // add output clauses + Gia_ManForEachCo( pM, pObj, i ) + { + int Lit = Abc_Var2Lit( pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1 ); + sat_solver_addclause( pSat, &Lit, &Lit + 1 ); + } + // simplify the SAT solver + status = sat_solver_simplify( pSat ); + assert( status ); + + // add test patterns + assert( Vec_IntSize(vTests) == Iter * nFuncVars ); + for ( Iter2 = 0; ; Iter2++ ) + { + abctime clk = Abc_Clock(); + status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + clkSat += Abc_Clock() - clk; + if ( pPars->fVerbose ) + { + printf( "Iter%6d : ", Iter2 ); + printf( "Var =%10d ", sat_solver_nvars(pSat) ); + printf( "Clause =%10d ", sat_solver_nclauses(pSat) ); + printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) ); + //Abc_PrintTime( 1, "Time", clkSat ); + ABC_PRTr( "Solver time", clkSat ); + } + if ( status == l_Undef ) + { + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter2 ); + goto finish; + } + if ( Iter2 == Iter ) + break; + assert( status == l_True ); + // get pattern + Vec_IntClear( vLits ); + for ( i = 0; i < nFuncVars; i++ ) + Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter2*nFuncVars + i) ); + Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ); + } + assert( Iter2 == Iter ); + if ( pPars->fVerbose ) + printf( "\n" ); + if ( p == pG ) + { + if ( status == l_True ) + printf( "There are untestable faults. " ); + else if ( status == l_False ) + printf( "There is no untestable faults. " ); + else assert( 0 ); + Abc_PrintTime( 1, "Fault computation runtime", Abc_Clock() - clkTotal ); + } + else + { + if ( status == l_True ) + printf( "The circuit is rectifiable. " ); + else if ( status == l_False ) + printf( "The circuit is not rectifiable (or equivalent to the golden one). " ); + else assert( 0 ); + Abc_PrintTime( 1, "Rectification runtime", Abc_Clock() - clkTotal ); + } + // dump untestable faults + if ( pPars->fDumpUntest && status == l_True ) + { + abctime clk = Abc_Clock(); + char * pFileName = "untest.txt"; + int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, pFileName, pPars->fVerbose ); + if ( p == pG ) + printf( "Dumped %d untestable multiple faults into file \"%s\". ", nUntests, pFileName ); + else + printf( "Dumped %d ways of rectifying the circuit into file \"%s\". ", nUntests, pFileName ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + } +finish: + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + Gia_ManStop( pM ); Vec_IntFree( vTests ); + Vec_IntFree( vLits ); } |