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-23 00:13:03 +09:00
parent fee0da2310
commit ed1a925c61
2 changed files with 285 additions and 144 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

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

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

@ -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*************************************************************
@ -789,6 +770,26 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName )
return vTests;
}
/**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 []
@ -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 );
}