Skip to content

A
abc
Commit b13e6588 by Alan Mishchenko
Options

Experiments with stuck-at fault testing.

parent 1aa6751a
Showing with 105 additions and 31 deletions
src/base/abci/abc.c
......@@ -399,7 +399,7 @@ static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9FunFaTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9FFTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Inse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Maxi ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -966,10 +966,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&icheck", Abc_CommandAbc9ICheck, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&funfatest", Abc_CommandAbc9FunFaTest, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&fftest", Abc_CommandAbc9FFTest, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&inse", Abc_CommandAbc9Inse, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&maxi", Abc_CommandAbc9Maxi, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmci", Abc_CommandAbc9Bmci, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&maxi", Abc_CommandAbc9Maxi, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmci", Abc_CommandAbc9Bmci, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
......@@ -32855,15 +32855,26 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9FunFaTest( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManFaultTest( Gia_Man_t * p, int fStuckAt, int fComplVars, int nTimeOut, int fDump, int fVerbose );
int c, fStuckAt = 0, fComplVars = 0, nTimeOut = 0, fDump = 0, fVerbose = 0;
extern void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, int fDump, int fVerbose );
int c, Algo = 0, fComplVars = 0, nTimeOut = 0, fDump = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Tscdvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ATcdvh" ) ) != EOF )
{
switch ( c )
{
case 'A':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
goto usage;
}
Algo = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( Algo < 1 || Algo > 3 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
......@@ -32875,9 +32886,6 @@ int Abc_CommandAbc9FunFaTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nTimeOut < 0 )
goto usage;
break;
case 's':
fStuckAt ^= 1;
break;
case 'c':
fComplVars ^= 1;
break;
......@@ -32895,23 +32903,27 @@ int Abc_CommandAbc9FunFaTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9FunFaTest(): There is no AIG.\n" );
Abc_Print( -1, "Abc_CommandAbc9FFTest(): There is no AIG.\n" );
return 0;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
if ( Gia_ManRegNum(pAbc->pGia) == 0 && Algo == 1 )
{
Abc_Print( -1, "Abc_CommandAbc9FunFaTest(): AIG is combinational.\n" );
Abc_Print( -1, "Abc_CommandAbc9FFTest(): For delay testing, AIG should be sequential.\n" );
return 0;
}
Gia_ManFaultTest( pAbc->pGia, fStuckAt, fComplVars, nTimeOut, fDump, fVerbose );
Gia_ManFaultTest( pAbc->pGia, Algo, fComplVars, nTimeOut, fDump, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &funfatest [-T num] [-scdvh]\n" );
Abc_Print( -2, "usage: &fftest [-AT num] [-cdvh]\n" );
Abc_Print( -2, "\t performs functional fault test generation\n" );
Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-s : toggles generating tests for stuck-at faults [default = %s]\n", fStuckAt? "yes": "no" );
Abc_Print( -2, "\t-c : toggles complementing control variables [default = %s]\n", fComplVars? "yes": "no" );
Abc_Print( -2, "\t-A num : selects test generation algorithm [default = %d]\n", 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-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-d : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", fDump? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
src/sat/bmc/bmcFault.c
......@@ -116,7 +116,7 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fComplVars )
iCtrl = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
iThis = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( fUseMuxes )
pObj->Value = Gia_ManHashMux( pNew, iCtrl, iThis, pObj->Value );
pObj->Value = Gia_ManHashMux( pNew, iCtrl, pObj->Value, iThis );
else
pObj->Value = iThis;
}
......@@ -157,8 +157,8 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars
iCtrl1 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
if ( fUseFaults )
{
pObj->Value = Gia_ManHashAnd( pNew, iCtrl0, pObj->Value );
pObj->Value = Gia_ManHashOr( pNew, Abc_LitNot(iCtrl1), pObj->Value );
pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(iCtrl0), pObj->Value );
pObj->Value = Gia_ManHashOr( pNew, iCtrl1, pObj->Value );
}
}
Gia_ManForEachCo( p, pObj, i )
......@@ -180,6 +180,43 @@ 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 * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iCtrl0;
pNew = Gia_ManStart( 3 * 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 )
{
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 );
}
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) + Gia_ManAndNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManFaultCofactor( Gia_Man_t * p, Vec_Int_t * vValues )
{
Gia_Man_t * pNew, * pTemp;
......@@ -270,24 +307,49 @@ void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime c
SeeAlso []
***********************************************************************/
void Gia_ManFaultTest( Gia_Man_t * p, int fStuckAt, int fComplVars, int nTimeOut, int fDump, int fVerbose )
void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, int fDump, int fVerbose )
{
int nIterMax = 1000000;
int i, Iter, status;
int i, Iter, status, nFuncVars = -1;
abctime clkTotal = Abc_Clock();
abctime clkSat = 0;
int nFuncVars = fStuckAt ? Gia_ManCiNum(p) : Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
Vec_Int_t * vLits, * vTests;
sat_solver * pSat;
Gia_Obj_t * pObj;
Gia_Man_t * pC;
Gia_Man_t * p0 = fStuckAt ? Gia_ManStuckAtUnfold(p, 0, fComplVars) : Gia_ManFaultUnfold(p, 0, fComplVars);
Gia_Man_t * p1 = fStuckAt ? Gia_ManStuckAtUnfold(p, 1, fComplVars) : Gia_ManFaultUnfold(p, 1, fComplVars);
Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM ), * pCnf2;
Gia_Man_t * pC, * p0, * p1, * pM;
Cnf_Dat_t * pCnf, * pCnf2;
// select algorithm
if ( Algo == 1 )
{
assert( Gia_ManRegNum(p) > 0 );
nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
p0 = Gia_ManFaultUnfold( p, 0, fComplVars );
p1 = Gia_ManFaultUnfold( p, 1, fComplVars );
}
else if ( Algo == 2 )
{
nFuncVars = Gia_ManCiNum(p);
p0 = Gia_ManStuckAtUnfold( p, 0, fComplVars );
p1 = Gia_ManStuckAtUnfold( p, 1, fComplVars );
}
else if ( Algo == 3 )
{
nFuncVars = Gia_ManCiNum(p);
p0 = Gia_ManFlipUnfold( p, 0, fComplVars );
p1 = Gia_ManFlipUnfold( p, 1, fComplVars );
}
else
{
printf( "Unregnized algorithm (%d).\n", Algo );
return;
}
// create miter
pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
pCnf = Cnf_DeriveGiaRemapped( pM );
Gia_ManStop( p0 );
Gia_ManStop( p1 );
assert( Gia_ManRegNum(p) > 0 );
// start the SAT solver
pSat = sat_solver_new();
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment