Skip to content

A
abc
Commit 5b3d4b7d by Alan Mishchenko
Options

Experiments with delay fault testing.

parent b541201d
Showing with 164 additions and 15 deletions
src/base/abci/abc.c
......@@ -394,6 +394,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_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -950,6 +951,7 @@ 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", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
......@@ -32438,6 +32440,72 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9FunFaTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManFaultTest( Gia_Man_t * p, int nTimeOut, int fDump, int fVerbose );
int c, nTimeOut = 0, fDump = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Tdvh" ) ) != EOF )
{
switch ( c )
{
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nTimeOut < 0 )
goto usage;
break;
case 'd':
fDump ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9FunFaTest(): There is no AIG.\n" );
return 0;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9FunFaTest(): AIG is combinational.\n" );
return 0;
}
Gia_ManFaultTest( pAbc->pGia, nTimeOut, fDump, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &funfatest [-T num] [-dvh]\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-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");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
return -1;
src/sat/bmc/bmcFault.c
......@@ -92,7 +92,7 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iThis;
int i, iCtrl, iThis;
pNew = Gia_ManStart( (2 + 3 * fUseMuxes) * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
......@@ -108,16 +108,17 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes )
pObj->Value = Gia_ObjFanin0Copy(pObj);
// add second timeframe
Gia_ManForEachRo( p, pObj, i )
pObj->Value = Gia_ObjRoToRi(pNew, pObj)->Value;
pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
{
iCtrl = Gia_ManAppendCi( pNew );
iThis = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( fUseMuxes )
pObj->Value = Gia_ManHashMux( pNew, Gia_ManAppendCi(pNew), iThis, pObj->Value );
pObj->Value = Gia_ManHashMux( pNew, iCtrl, iThis, pObj->Value );
else
pObj->Value = iThis, Gia_ManAppendCi(pNew);
pObj->Value = iThis;
}
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
......@@ -175,12 +176,66 @@ Gia_Man_t * Gia_ManFaultCofactor( Gia_Man_t * p, Vec_Int_t * vValues )
SeeAlso []
***********************************************************************/
void Gia_ManFaultTest( Gia_Man_t * p )
void Gia_ManDumpTests( Vec_Int_t * vTests, int nIter )
{
int nTimeOut = 0;
int nIterMax = 100;
int i, status;
Vec_Int_t * vLits;
FILE * pFile = fopen( "tests.txt", "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") )
for ( k = 0; k < nVars; k++ )
fprintf( pFile, "%d", Vec_IntEntry(vTests, v++) );
fclose( pFile );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime clk )
{
FILE * pTable = fopen( "fault_stats.txt", "a+" );
fprintf( pTable, "%s ", Gia_ManName(p) );
fprintf( pTable, "%d ", Gia_ManPiNum(p) );
fprintf( pTable, "%d ", Gia_ManPoNum(p) );
fprintf( pTable, "%d ", Gia_ManRegNum(p) );
fprintf( pTable, "%d ", Gia_ManAndNum(p) );
fprintf( pTable, "%d ", sat_solver_nvars(pSat) );
fprintf( pTable, "%d ", sat_solver_nclauses(pSat) );
fprintf( pTable, "%d ", sat_solver_nconflicts(pSat) );
fprintf( pTable, "%d ", nIter );
fprintf( pTable, "%.2f", 1.0*clk/CLOCKS_PER_SEC );
fprintf( pTable, "\n" );
fclose( pTable );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManFaultTest( Gia_Man_t * p, int nTimeOut, int fDump, int fVerbose )
{
int nIterMax = 1000000;
int i, Iter, status;
abctime clkTotal = Abc_Clock();
abctime clkSat = 0;
Vec_Int_t * vLits, * vTests;
sat_solver * pSat;
Gia_Obj_t * pObj;
Gia_Man_t * pC;
......@@ -190,10 +245,11 @@ void Gia_ManFaultTest( Gia_Man_t * p )
Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM ), * pCnf2;
Gia_ManStop( p0 );
Gia_ManStop( p1 );
assert( Gia_ManRegNum(p) > 0 );
// start the SAT solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars * 10 );
sat_solver_setnvars( pSat, pCnf->nVars );
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
// add timeframe clauses
for ( i = 0; i < pCnf->nClauses; i++ )
......@@ -207,17 +263,33 @@ void Gia_ManFaultTest( Gia_Man_t * p )
sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
// iterate through the test vectors
for ( i = 0; i < nIterMax; i++ )
vTests = Vec_IntAlloc( 10000 );
for ( Iter = 0; 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 );
clkSat += Abc_Clock() - clk;
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 );
}
if ( status == l_Undef )
{
printf( "Timeout reached after %d seconds.\n", nTimeOut );
if ( fVerbose )
printf( "\n" );
printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter );
break;
}
if ( status == l_False )
{
printf( "The problem is UNSAT.\n" );
if ( fVerbose )
printf( "\n" );
printf( "The problem is UNSAT after %d iterations. ", Iter );
break;
}
assert( status == l_True );
......@@ -226,11 +298,12 @@ void Gia_ManFaultTest( Gia_Man_t * p )
Gia_ManForEachPi( pM, pObj, i )
if ( i < Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p) )
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, pCnf->nVars );
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] ) )
......@@ -238,7 +311,7 @@ void Gia_ManFaultTest( Gia_Man_t * p )
// add constraint clauses
Gia_ManForEachPo( pC, pObj, i )
{
int Lit = Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pC, pObj)], 1);
int Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 1 );
if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
assert( 0 );
}
......@@ -249,11 +322,19 @@ void Gia_ManFaultTest( Gia_Man_t * p )
Cnf_DataFree( pCnf2 );
Gia_ManStop( pC );
}
// print results
// if ( status == l_False )
// Gia_ManPrintResults( p, pSat, Iter, Abc_Clock() - clkTotal );
// cleanup
Vec_IntFree( vLits );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pM );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
// dump the test suite
if ( fDump )
Gia_ManDumpTests( vTests, Iter );
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