luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding symbolic fault representation in &fftest.

This commit is contained in:
Alan Mishchenko 2014-05-14 20:28:55 +09:00
parent 26c92f161a
commit 911b801f20
3 changed files with 341 additions and 76 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

91
src/base/abci/abc.c
View File

@ -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;
}

15
src/sat/bmc/bmc.h
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

311
src/sat/bmc/bmcFault.c
View File

@ -30,10 +30,38 @@ 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.]
@ -322,6 +350,183 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
return pNew;
}
/**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 []
@ -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 );