Skip to content

A
abc
Commit c6663b04 by Alan Mishchenko
Options

Experiments with stuck-at fault testing.

parent 6f17c44e
Showing with 168 additions and 40 deletions
src/base/abci/abc.c
......@@ -32857,8 +32857,9 @@ usage:
***********************************************************************/
int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, int fDump, int fVerbose );
extern void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int nTimeOut, int fDump, int fVerbose );
int c, Algo = 0, fComplVars = 0, nTimeOut = 0, fDump = 0, fVerbose = 0;
char * pFileName = NULL;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ATcdvh" ) ) != EOF )
{
......@@ -32901,6 +32902,20 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
// get the file name
if ( argc == globalUtilOptind + 1 )
{
FILE * pFile;
pFileName = argv[globalUtilOptind];
pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
{
Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName );
return 0;
}
fclose( pFile );
}
// check other conditions
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9FFTest(): There is no AIG.\n" );
......@@ -32911,11 +32926,11 @@ 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, Algo, fComplVars, nTimeOut, fDump, fVerbose );
Gia_ManFaultTest( pAbc->pGia, pFileName, Algo, fComplVars, nTimeOut, fDump, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &fftest [-AT num] [-cdvh]\n" );
Abc_Print( -2, "usage: &fftest [-AT num] [-cdvh] <file>\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 0: algorithm is not selected\n" );
......@@ -32927,6 +32942,7 @@ usage:
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");
Abc_Print( -2, "\t<file> : (optional) file name with input test patterns\n");
return 1;
}
src/sat/bmc/bmcFault.c
......@@ -254,9 +254,9 @@ Gia_Man_t * Gia_ManFaultCofactor( Gia_Man_t * p, Vec_Int_t * vValues )
SeeAlso []
***********************************************************************/
void Gia_ManDumpTests( Vec_Int_t * vTests, int nIter )
void Gia_ManDumpTests( Vec_Int_t * vTests, int nIter, char * pFileName )
{
FILE * pFile = fopen( "tests.txt", "wb" );
FILE * pFile = fopen( pFileName, "wb" );
int i, k, v, nVars = Vec_IntSize(vTests) / nIter;
assert( Vec_IntSize(vTests) % nIter == 0 );
for ( v = i = 0; i < nIter; i++, fprintf(pFile, "\n") )
......@@ -307,35 +307,136 @@ void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime c
SeeAlso []
***********************************************************************/
void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, int fDump, int fVerbose )
void Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Vec_Int_t * vLits, int nFuncVars )
{
Gia_Man_t * pC;
Cnf_Dat_t * pCnf2;
Gia_Obj_t * pObj;
int i, Lit;
// derive the cofactor
pC = Gia_ManFaultCofactor( pM, vLits );
// derive new CNF
pCnf2 = Cnf_DeriveGiaRemapped( pC );
Cnf_DataLiftGia( pCnf2, pC, sat_solver_nvars(pSat) );
// add timeframe clauses
for ( i = 0; i < pCnf2->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf2->pClauses[i], pCnf2->pClauses[i+1] ) )
assert( 0 );
// add constraint clauses
Gia_ManForEachPo( pC, pObj, i )
{
Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 1 );
if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
assert( 0 );
}
// add connection clauses
Gia_ManForEachPi( pM, pObj, i )
if ( i >= nFuncVars )
sat_solver_add_buffer( pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)], pCnf2->pVarNums[Gia_ObjId(pC, Gia_ManPi(pC, i))], 0 );
Cnf_DataFree( pCnf2 );
Gia_ManStop( pC );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName )
{
FILE * pFile = fopen( pFileName, "rb" );
Vec_Int_t * vTests; int c;
if ( pFile == NULL )
{
printf( "Cannot open input file \"%s\".\n", pFileName );
return NULL;
}
vTests = Vec_IntAlloc( 10000 );
while ( (c = fgetc(pFile)) != EOF )
{
if ( c == ' ' || c == '\t' || c == '\r' || c == '\n' )
continue;
if ( c != '0' && c != '1' )
{
printf( "Wring symbol (%c) in the input file.\n", c );
Vec_IntFreeP( &vTests );
break;
}
Vec_IntPush( vTests, c - '0' );
}
fclose( pFile );
return vTests;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int nTimeOut, int fDump, int fVerbose )
{
int nIterMax = 1000000;
int i, Iter, status, nFuncVars = -1;
abctime clkTotal = Abc_Clock();
abctime clkSat = 0;
abctime clkSat = 0, clkTotal = Abc_Clock();
Vec_Int_t * vLits, * vTests;
sat_solver * pSat;
Gia_Man_t * p0, * p1, * pM;
Gia_Obj_t * pObj;
Gia_Man_t * pC, * p0, * p1, * pM;
Cnf_Dat_t * pCnf, * pCnf2;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
// select algorithm
if ( Algo == 1 )
nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
else if ( Algo == 2 )
nFuncVars = Gia_ManCiNum(p);
else if ( Algo == 3 )
nFuncVars = Gia_ManCiNum(p);
else
{
printf( "Unregnized algorithm (%d).\n", Algo );
return;
}
// collect test patterns from file
if ( pFileName )
vTests = Gia_ManGetTestPatterns( pFileName );
else
vTests = Vec_IntAlloc( 10000 );
if ( vTests == NULL )
return;
if ( Vec_IntSize(vTests) % nFuncVars != 0 )
{
printf( "The number of symbols in the input patterns (%d) does not divide evenly on the number of test variables (%d).\n", Vec_IntSize(vTests), nFuncVars );
Vec_IntFree( vTests );
return;
}
// 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 );
}
......@@ -366,9 +467,36 @@ void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, in
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 available test-patterns
if ( Vec_IntSize(vTests) > 0 )
{
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 );
for ( Iter = 0; Iter < nTests; Iter++ )
{
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;
// get pattern
Vec_IntClear( vLits );
for ( i = 0; i < nFuncVars; i++ )
Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) );
Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars );
if ( fVerbose )
{
printf( "Iter%6d : ", Iter );
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 );
}
}
}
// iterate through the test vectors
vTests = Vec_IntAlloc( 10000 );
for ( Iter = 0; Iter < nIterMax; Iter++ )
for ( Iter = Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ )
{
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 );
......@@ -379,7 +507,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, in
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_PrintTime( 1, "Time", clkSat );
ABC_PRTr( "Solver time", clkSat );
}
if ( status == l_Undef )
......@@ -403,28 +531,8 @@ void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, in
if ( i < nFuncVars )
Vec_IntPush( vLits, sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) );
Vec_IntAppend( vTests, vLits );
// derive the cofactor
pC = Gia_ManFaultCofactor( pM, vLits );
// derive new CNF
pCnf2 = Cnf_DeriveGiaRemapped( pC );
Cnf_DataLiftGia( pCnf2, pC, sat_solver_nvars(pSat) );
// add timeframe clauses
for ( i = 0; i < pCnf2->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf2->pClauses[i], pCnf2->pClauses[i+1] ) )
assert( 0 );
// add constraint clauses
Gia_ManForEachPo( pC, pObj, i )
{
int Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 1 );
if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
assert( 0 );
}
// add connection clauses
Gia_ManForEachPi( pM, pObj, i )
if ( i >= nFuncVars )
sat_solver_add_buffer( pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)], pCnf2->pVarNums[Gia_ObjId(pC, Gia_ManPi(pC, i))], 0 );
Cnf_DataFree( pCnf2 );
Gia_ManStop( pC );
// add constraint
Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars );
}
// print results
// if ( status == l_False )
......@@ -437,7 +545,11 @@ void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, in
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
// dump the test suite
if ( fDump )
Gia_ManDumpTests( vTests, Iter );
{
char * pFileName = "tests.txt";
Gia_ManDumpTests( vTests, Iter, pFileName );
printf( "Dumping %d computed test patterns into file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pFileName );
}
Vec_IntFree( vTests );
}
......
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