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

Adding switch &fftest -N <num> to detect fixed vars after each <num> iterations.

This commit is contained in:
Alan Mishchenko 2014-10-25 17:07:38 -07:00
parent 96c9792f33
commit f93ede121d
3 changed files with 78 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -35635,7 +35635,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_ParFfSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ATSGsbduvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ATNSGsbduvh" ) ) != EOF )
{
switch ( c )
{
@ -35661,6 +35661,17 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nTimeOut < 0 )
goto usage;
break;
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
pPars->nIterCheck = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nIterCheck < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
@ -35769,7 +35780,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &fftest [-AT num] [-sbduvh] <file> [-G file] [-S str]\n" );
Abc_Print( -2, "usage: &fftest [-ATN 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" );
@ -35778,6 +35789,7 @@ usage:
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-N num : specifies iteration to check for fixed parameters [default = %d]\n", pPars->nIterCheck );
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" );

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

@ -129,6 +129,7 @@ struct Bmc_ParFf_t_
int fComplVars;
int fStartPats;
int nTimeOut;
int nIterCheck;
int fBasic;
int fDump;
int fDumpUntest;

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

@ -55,6 +55,7 @@ void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
p->Algo = 0;
p->fStartPats = 0;
p->nTimeOut = 0;
p->nIterCheck = 0;
p->fBasic = 0;
p->fDump = 0;
p->fDumpUntest = 0;
@ -791,6 +792,54 @@ Gia_Man_t * Gia_ManDeriveDup( Gia_Man_t * p, int nPisNew )
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vLits, int Iter )
{
int status, i, v, iVar, Lit;
int nUnsats = 0, nRuns = 0;
abctime clk = Abc_Clock();
Vec_IntFill( vLits, Vec_IntSize(vPars), 0 );
for ( v = 0; v < Vec_IntSize(vPars); v++ )
{
if ( Vec_IntEntry(vLits, v) )
continue;
nRuns++;
Lit = Abc_Var2Lit( Vec_IntEntry(vPars, v), 0 );
status = sat_solver_solve( pSat, &Lit, &Lit+1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
{
//printf( "Var %d timed out\n", v );
continue;
}
if ( status == l_False )
{
nUnsats++;
//printf( "Var %d is UNSAT\n", v );
Lit = Abc_LitNot(Lit);
//status = sat_solver_addclause( pSat, &Lit, &Lit+1 );
//assert( status );
continue;
}
Vec_IntForEachEntry( vPars, iVar, i )
if ( !Vec_IntEntry(vLits, i) && sat_solver_var_value(pSat, iVar) )
Vec_IntWriteEntry( vLits, i, 1 );
assert( Vec_IntEntry(vLits, v) == 1 );
}
printf( "Iteration %3d has determined %5d (out of %5d) parameters after %6d SAT calls. ", Iter, nUnsats, Vec_IntSize(vPars), nRuns );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return nUnsats;
}
/**Function*************************************************************
Synopsis []
@ -807,7 +856,7 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
int nIterMax = 1000000, nVars, nPars;
int i, Iter, Iter2, status, nFuncVars = -1;
abctime clkSat = 0, clkTotal = Abc_Clock();
Vec_Int_t * vLits, * vTests;
Vec_Int_t * vLits, * vTests, * vPars = NULL;
Gia_Man_t * p0 = NULL, * p1 = NULL, * pM;
Gia_Obj_t * pObj;
Cnf_Dat_t * pCnf;
@ -1015,6 +1064,18 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
Vec_IntAppend( vTests, vLits );
// add constraint
Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars );
// collect parameter variables
if ( pPars->nIterCheck && vPars == NULL )
{
vPars = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars );
Gia_ManForEachPi( pM, pObj, i )
if ( i >= nFuncVars )
Vec_IntPush( vPars, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
assert( Vec_IntSize(vPars) == Gia_ManPiNum(pM) - nFuncVars );
}
// derive unit parameter variables
if ( pPars->nIterCheck && !(Iter % pPars->nIterCheck) )
Gia_ManFaultAnalyze( pSat, vPars, vLits, Iter );
}
finish:
// print results
@ -1142,6 +1203,7 @@ finish:
Gia_ManStop( pM );
Vec_IntFree( vTests );
Vec_IntFree( vLits );
Vec_IntFreeP( &vPars );
}