diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-05-14 20:28:55 +0900 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-05-14 20:28:55 +0900 |
commit | 911b801f204d9a8371749253fbfb44e03df66412 (patch) | |
tree | e0ac6b3bb6bb3cdd77a8243e9bf8fc20587bd6b6 /src | |
parent | 26c92f161a95ab3b30991174e79dd99f19b1c86f (diff) | |
download | abc-911b801f204d9a8371749253fbfb44e03df66412.tar.gz abc-911b801f204d9a8371749253fbfb44e03df66412.tar.bz2 abc-911b801f204d9a8371749253fbfb44e03df66412.zip |
Adding symbolic fault representation in &fftest.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 91 | ||||
-rw-r--r-- | src/sat/bmc/bmc.h | 15 | ||||
-rw-r--r-- | src/sat/bmc/bmcFault.c | 311 |
3 files changed, 341 insertions, 76 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index de32646c..79409b49 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -33144,11 +33144,13 @@ usage: ***********************************************************************/ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int fStartPats, int nTimeOut, int fBasic, int fDump, int fDumpUntest, int fVerbose ); - int c, Algo = 0, fComplVars = 0, fStartPats = 0, nTimeOut = 0, fBasic = 0, fDump = 0, fDumpUntest = 0, fVerbose = 0; - char * pFileName = NULL; + extern void Gia_ParFfSetDefault( Bmc_ParFf_t * p ); + extern void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ); + Bmc_ParFf_t Pars, * pPars = &Pars; + int c; + Gia_ParFfSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ATcsbduvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ATScsbduvh" ) ) != EOF ) { switch ( c ) { @@ -33158,9 +33160,9 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); goto usage; } - Algo = atoi(argv[globalUtilOptind]); + pPars->Algo = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( Algo < 1 || Algo > 4 ) + if ( pPars->Algo < 0 || pPars->Algo > 4 ) goto usage; break; case 'T': @@ -33169,28 +33171,37 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); goto usage; } - nTimeOut = atoi(argv[globalUtilOptind]); + pPars->nTimeOut = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nTimeOut < 0 ) + if ( pPars->nTimeOut < 0 ) goto usage; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by string.\n" ); + goto usage; + } + pPars->pFormStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'c': - fComplVars ^= 1; + pPars->fComplVars ^= 1; break; case 's': - fStartPats ^= 1; + pPars->fStartPats ^= 1; break; case 'b': - fBasic ^= 1; + pPars->fBasic ^= 1; break; case 'd': - fDump ^= 1; + pPars->fDump ^= 1; break; case 'u': - fDumpUntest ^= 1; + pPars->fDumpUntest ^= 1; break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; case 'h': goto usage; @@ -33198,15 +33209,25 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } + if ( pPars->Algo == 0 && pPars->pFormStr == NULL ) + { + Abc_Print( -1, "Formula string (-S <str>) should be selected when algorithm is 0 (-A 0).\n" ); + return 0; + } + if ( pPars->Algo != 0 && pPars->pFormStr != NULL ) + { + Abc_Print( -1, "Algorithm should be 0 (-A 0) when formula string is selected (-S <str>).\n" ); + return 0; + } // get the file name if ( argc == globalUtilOptind + 1 ) { FILE * pFile; - pFileName = argv[globalUtilOptind]; - pFile = fopen( pFileName, "r" ); + pPars->pFileName = argv[globalUtilOptind]; + pFile = fopen( pPars->pFileName, "r" ); if ( pFile == NULL ) { - Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName ); + Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pPars->pFileName ); return 0; } fclose( pFile ); @@ -33217,32 +33238,44 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9FFTest(): There is no AIG.\n" ); return 0; } - if ( Gia_ManRegNum(pAbc->pGia) == 0 && Algo == 1 ) + if ( Gia_ManRegNum(pAbc->pGia) == 0 && pPars->Algo == 1 ) { Abc_Print( -1, "Abc_CommandAbc9FFTest(): For delay testing, AIG should be sequential.\n" ); return 0; } - Gia_ManFaultTest( pAbc->pGia, pFileName, Algo, fComplVars, fStartPats, nTimeOut, fBasic, fDump, fDumpUntest, fVerbose ); + Gia_ManFaultTest( pAbc->pGia, pPars ); return 0; usage: - Abc_Print( -2, "usage: &fftest [-AT num] [-csbduvh] <file>\n" ); + 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 test generation algorithm [default = %d]\n", Algo ); + Abc_Print( -2, "\t-A num : selects test generation algorithm [default = %d]\n", pPars->Algo ); Abc_Print( -2, "\t 0: algorithm is not selected\n" ); Abc_Print( -2, "\t 1: delay fault testing for sequential circuits\n" ); Abc_Print( -2, "\t 2: traditional stuck-at testing\n" ); Abc_Print( -2, "\t 3: complement fault testing\n" ); Abc_Print( -2, "\t 4: functionally observable fault testing\n" ); - Abc_Print( -2, "\t-T num : specifies approximate runtime limit in seconds [default = %d]\n", nTimeOut ); - Abc_Print( -2, "\t-c : toggles complementing control variables [default = %s]\n", fComplVars? "active-high": "active-low" ); - Abc_Print( -2, "\t-s : toggles starting with the all-0 and all-1 patterns [default = %s]\n", fStartPats? "yes": "no" ); - Abc_Print( -2, "\t-b : toggles testing for single faults only [default = %s]\n", fBasic? "yes": "no" ); - Abc_Print( -2, "\t-d : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", fDump? "yes": "no" ); - Abc_Print( -2, "\t-u : toggles dumping untestable faults into \"untest.txt\" [default = %s]\n", fDumpUntest? "yes": "no" ); - Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + 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"); + 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} or {a,b}\n"); + Abc_Print( -2, "\t Parameter variables: {p,q,r,s,...}\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 are not allowed.\n"); + Abc_Print( -2, "\t Examples:\n"); + Abc_Print( -2, "\t ((a&~p)|q) stuck-at-0/1 model\n"); + Abc_Print( -2, "\t (a^p) complement model\n"); + Abc_Print( -2, "\t (a?(b?~s:r):(b?q:p)) functional observability fault model\n"); + Abc_Print( -2, "\t (p^((q^a)&(r^b)) complement at the inputs/output\n"); + Abc_Print( -2, "\t (p?(a|b):(a&b)) replace AND by OR\n"); return 1; } diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 558b2d62..dd8d36eb 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -120,6 +120,21 @@ struct Bmc_MulPar_t_ int fVeryVerbose; }; +typedef struct Bmc_ParFf_t_ Bmc_ParFf_t; +struct Bmc_ParFf_t_ +{ + char * pFileName; + char * pFormStr; + int Algo; + int fComplVars; + int fStartPats; + int nTimeOut; + int fBasic; + int fDump; + int fDumpUntest; + int fVerbose; +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index 6c1bf81b..7d400d03 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -30,12 +30,40 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define FFTEST_MAX_VARS 2 +#define FFTEST_MAX_PARS 8 + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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; + p->fDump = 0; + p->fDumpUntest = 0; + p->fVerbose = 0; +} + +/**Function************************************************************* + Synopsis [Add constraint that no more than 1 variable is 1.] Description [] @@ -324,6 +352,183 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars ) /**Function************************************************************* + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_FormStrCount( char * pStr, int * pnVars, int * pnPars ) +{ + int i; + if ( pStr[0] != '(' ) + { + printf( "The first symbol should be the opening paranthesis \"(\".\n" ); + return 1; + } + if ( pStr[strlen(pStr)-1] != ')' ) + { + printf( "The last symbol should be the closing paranthesis \")\".\n" ); + return 1; + } + *pnVars = 0; + *pnPars = 0; + for ( i = 0; pStr[i]; i++ ) + { + if ( pStr[i] >= 'a' && pStr[i] <= 'b' ) + *pnVars = Abc_MaxInt( *pnVars, pStr[i] - 'a' + 1 ); + else if ( pStr[i] >= 'p' && pStr[i] <= 's' ) + *pnPars = Abc_MaxInt( *pnPars, pStr[i] - 'p' + 1 ); + else if ( pStr[i] == '(' || pStr[i] == ')' ) + {} + else if ( pStr[i] == '&' || pStr[i] == '|' || pStr[i] == '^' ) + {} + else if ( pStr[i] == '?' || pStr[i] == ':' || pStr[i] == '~' ) + {} + else + { + printf( "Unknown symbol (%c) in the formula (%s)\n", pStr[i], pStr ); + return 1; + } + } + if ( *pnVars < 1 && *pnVars > FFTEST_MAX_VARS ) + { printf( "Illigal number of primary inputs (%d)\n", *pnVars ); return 1; } + if ( *pnPars < 1 && *pnPars > FFTEST_MAX_PARS ) + { printf( "Illigal number of primary inputs (%d)\n", *pnPars ); return 1; } + return 0; +} + +/**Function************************************************************* + + Synopsis [Implements fault model formula using functional/parameter vars.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Gia_ManFormulaEndToken( char * pForm ) +{ + int Counter = 0; + char * pThis; + for ( pThis = pForm; *pThis; pThis++ ) + { + if ( *pThis == '~' ) + continue; + if ( *pThis == '(' ) + Counter++; + else if ( *pThis == ')' ) + Counter--; + if ( Counter == 0 ) + return pThis + 1; + } + assert( 0 ); + return NULL; +} +int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * pBeg, char * pEnd, int nVars, int nPars ) +{ + int iFans[3], Oper = -1; + char * pEndNew; + if ( pBeg[0] == '~' ) + return Abc_LitNot( Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd, nVars, nPars ) ); + if ( pBeg + 1 == pEnd ) + { + if ( pBeg[0] >= 'a' && pBeg[0] <= 'b' ) + return pVars[pBeg[0] - 'a']; + if ( pBeg[0] >= 'p' && pBeg[0] <= 's' ) + return pPars[pBeg[0] - 'p']; + assert( 0 ); + return -1; + } + if ( pBeg[0] == '(' ) + { + pEndNew = Gia_ManFormulaEndToken( pBeg ); + if ( pEndNew == pEnd ) + { + assert( pBeg[0] == '(' ); + assert( pBeg[pEnd-pBeg-1] == ')' ); + return Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd - 1, nVars, nPars ); + } + } + // get first part + pEndNew = Gia_ManFormulaEndToken( pBeg ); + iFans[0] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nVars, nPars ); + Oper = pEndNew[0]; + // get second part + pBeg = pEndNew + 1; + pEndNew = Gia_ManFormulaEndToken( pBeg ); + iFans[1] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nVars, nPars ); + // derive the formula + if ( Oper == '&' ) + return Gia_ManHashAnd( p, iFans[0], iFans[1] ); + if ( Oper == '|' ) + return Gia_ManHashOr( p, iFans[0], iFans[1] ); + if ( Oper == '^' ) + return Gia_ManHashXor( p, iFans[0], iFans[1] ); + // get third part + assert( Oper == '?' ); + assert( pEndNew[0] == ':' ); + pBeg = pEndNew + 1; + pEndNew = Gia_ManFormulaEndToken( pBeg ); + iFans[2] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nVars, nPars ); + return Gia_ManHashMux( p, iFans[0], iFans[1], iFans[2] ); +} +int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pForm, int nVars, int nPars ) +{ + return Gia_ManRealizeFormula_rec( p, pVars, pPars, pForm, pForm + strlen(pForm), nVars, nPars ); +} +Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars, char * pForm ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, k, iCtrl[FFTEST_MAX_PARS], iFans[FFTEST_MAX_VARS]; + int nVars, nPars; + Gia_FormStrCount( pForm, &nVars, &nPars ); + pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + { + for ( k = 0; k < nPars; k++ ) + iCtrl[k] = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars ); + if ( fUseFaults ) + { + if ( nVars == 1 ) + { + iFans[0] = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pForm, 1, nPars ); + } + else if ( nVars == 2 ) + { + iFans[0] = Gia_ObjFanin0Copy(pObj); + iFans[1] = Gia_ObjFanin1Copy(pObj); + pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pForm, 2, nPars ); + } + else assert( 0 ); + } + else + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + nPars * Gia_ManAndNum(p) ); +// if ( fUseFaults ) +// Gia_AigerWrite( pNew, "newfault.aig", 0, 0 ); + return pNew; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -564,9 +769,9 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName ) SeeAlso [] ***********************************************************************/ -void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int fStartPats, int nTimeOut, int fBasic, int fDump, int fDumpUntest, int fVerbose ) +void Gia_ManFaultTest( Gia_Man_t * p, Bmc_ParFf_t * pPars ) { - int nIterMax = 1000000; + int nIterMax = 1000000, nVars, nPars; int i, Iter, LitRoot, status, nFuncVars = -1; abctime clkSat = 0, clkTotal = Abc_Clock(); Vec_Int_t * vLits, * vTests; @@ -575,34 +780,41 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars Cnf_Dat_t * pCnf; sat_solver * pSat; + if ( pPars->Algo == 0 && Gia_FormStrCount( pPars->pFormStr, &nVars, &nPars ) ) + return; + // select algorithm - if ( Algo == 1 ) - printf( "FFTEST is computing test patterns for %sdelay faults...\n", fBasic ? "single " : "" ); - else if ( Algo == 2 ) - printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", fBasic ? "single " : "" ); - else if ( Algo == 3 ) - printf( "FFTEST is computing test patterns for %scomplement faults...\n", fBasic ? "single " : "" ); - else if ( Algo == 4 ) - printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", fBasic ? "single " : "" ); + if ( pPars->Algo == 0 ) + printf( "FFTEST is computing test patterns for fault model \"%s\"...\n", pPars->pFormStr ); + else if ( pPars->Algo == 1 ) + printf( "FFTEST is computing test patterns for %sdelay faults...\n", pPars->fBasic ? "single " : "" ); + else if ( pPars->Algo == 2 ) + printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", pPars->fBasic ? "single " : "" ); + else if ( pPars->Algo == 3 ) + printf( "FFTEST is computing test patterns for %scomplement faults...\n", pPars->fBasic ? "single " : "" ); + else if ( pPars->Algo == 4 ) + printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" ); else { - printf( "Unregnized algorithm (%d).\n", Algo ); + printf( "Unregnized algorithm (%d).\n", pPars->Algo ); return; } // select algorithm - if ( Algo == 1 ) + if ( pPars->Algo == 0 ) + nFuncVars = Gia_ManCiNum(p); + else if ( pPars->Algo == 1 ) nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p); - else if ( Algo == 2 ) + else if ( pPars->Algo == 2 ) nFuncVars = Gia_ManCiNum(p); - else if ( Algo == 3 ) + else if ( pPars->Algo == 3 ) nFuncVars = Gia_ManCiNum(p); - else if ( Algo == 4 ) + else if ( pPars->Algo == 4 ) nFuncVars = Gia_ManCiNum(p); // collect test patterns from file - if ( pFileName ) - vTests = Gia_ManGetTestPatterns( pFileName ); + if ( pPars->pFileName ) + vTests = Gia_ManGetTestPatterns( pPars->pFileName ); else vTests = Vec_IntAlloc( 10000 ); if ( vTests == NULL ) @@ -615,26 +827,31 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars } // select algorithm - if ( Algo == 1 ) + if ( pPars->Algo == 0 ) + { + p0 = Gia_ManFormulaUnfold( p, 0, pPars->fComplVars, pPars->pFormStr ); + p1 = Gia_ManFormulaUnfold( p, 1, pPars->fComplVars, pPars->pFormStr ); + } + else if ( pPars->Algo == 1 ) { assert( Gia_ManRegNum(p) > 0 ); - p0 = Gia_ManFaultUnfold( p, 0, fComplVars ); - p1 = Gia_ManFaultUnfold( p, 1, fComplVars ); + p0 = Gia_ManFaultUnfold( p, 0, pPars->fComplVars ); + p1 = Gia_ManFaultUnfold( p, 1, pPars->fComplVars ); } - else if ( Algo == 2 ) + else if ( pPars->Algo == 2 ) { - p0 = Gia_ManStuckAtUnfold( p, 0, fComplVars ); - p1 = Gia_ManStuckAtUnfold( p, 1, fComplVars ); + p0 = Gia_ManStuckAtUnfold( p, 0, pPars->fComplVars ); + p1 = Gia_ManStuckAtUnfold( p, 1, pPars->fComplVars ); } - else if ( Algo == 3 ) + else if ( pPars->Algo == 3 ) { - p0 = Gia_ManFlipUnfold( p, 0, fComplVars ); - p1 = Gia_ManFlipUnfold( p, 1, fComplVars ); + p0 = Gia_ManFlipUnfold( p, 0, pPars->fComplVars ); + p1 = Gia_ManFlipUnfold( p, 1, pPars->fComplVars ); } - else if ( Algo == 4 ) + else if ( pPars->Algo == 4 ) { - p0 = Gia_ManFOFUnfold( p, 0, fComplVars ); - p1 = Gia_ManFOFUnfold( p, 1, fComplVars ); + p0 = Gia_ManFOFUnfold( p, 0, pPars->fComplVars ); + p1 = Gia_ManFOFUnfold( p, 1, pPars->fComplVars ); } // create miter @@ -645,9 +862,9 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars // start the SAT solver pSat = sat_solver_new(); - sat_solver_setnvars( pSat, pCnf->nVars + (fDumpUntest ? 1 : 0) ); - sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); - LitRoot = fDumpUntest ? Abc_Var2Lit( pCnf->nVars, 1 ) : 0; + sat_solver_setnvars( pSat, pCnf->nVars + (pPars->fDumpUntest ? 1 : 0) ); + 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] ) ) @@ -662,7 +879,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); // add cadinality constraint - if ( fBasic ) + if ( pPars->fBasic ) { Vec_IntClear( vLits ); Gia_ManForEachPi( pM, pObj, i ) @@ -676,7 +893,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars { int nTests = Vec_IntSize(vTests) / nFuncVars; assert( Vec_IntSize(vTests) % nFuncVars == 0 ); - printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pFileName ); + printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pPars->pFileName ); for ( Iter = 0; Iter < nTests; Iter++ ) { abctime clk = Abc_Clock(); @@ -687,7 +904,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars for ( i = 0; i < nFuncVars; i++ ) Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) ); Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ); - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "Iter%6d : ", Iter ); printf( "Var =%10d ", sat_solver_nvars(pSat) ); @@ -698,21 +915,21 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars } } } - else if ( fStartPats ) + else if ( pPars->fStartPats ) { 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 ); if ( status == l_Undef ) { - if ( fVerbose ) + if ( pPars->fVerbose ) printf( "\n" ); - printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter ); + printf( "Timeout reached after %d seconds and %d iterations. ", pPars->nTimeOut, Iter ); break; } if ( status == l_False ) { - if ( fVerbose ) + if ( pPars->fVerbose ) printf( "\n" ); printf( "The problem is UNSAT after %d iterations. ", Iter ); break; @@ -725,12 +942,12 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars } // iterate through the test vectors - for ( Iter = fStartPats ? 2 : Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ ) + 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 ); clkSat += Abc_Clock() - clk; - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "Iter%6d : ", Iter ); printf( "Var =%10d ", sat_solver_nvars(pSat) ); @@ -741,14 +958,14 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars } if ( status == l_Undef ) { - if ( fVerbose ) + if ( pPars->fVerbose ) printf( "\n" ); - printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter ); + printf( "Timeout reached after %d seconds and %d iterations. ", pPars->nTimeOut, Iter ); break; } if ( status == l_False ) { - if ( fVerbose ) + if ( pPars->fVerbose ) printf( "\n" ); printf( "The problem is UNSAT after %d iterations. ", Iter ); break; @@ -769,11 +986,11 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars // cleanup Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); // dump untestable faults - if ( fDumpUntest ) + if ( pPars->fDumpUntest ) { abctime clk = Abc_Clock(); char * pFileName = "untest.txt"; - int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, Abc_LitNot(LitRoot), pFileName, fVerbose ); + 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 ); } @@ -782,7 +999,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars Gia_ManStop( pM ); sat_solver_delete( pSat ); // dump the test suite - if ( fDump ) + if ( pPars->fDump ) { char * pFileName = "tests.txt"; Gia_ManDumpTests( vTests, Iter, pFileName ); |