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

Adding support for cardinality constraints in &fftest (switches -K and -k).

This commit is contained in:
Alan Mishchenko 2015-04-16 20:58:23 +09:00
parent 4b2205ce6e
commit cd4807ea04
3 changed files with 84 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -36342,7 +36342,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, "ATNSGsbfdeuvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ATNKSGkbsfdeuvh" ) ) != EOF )
{
switch ( c )
{
@ -36379,6 +36379,17 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nIterCheck < 0 )
goto usage;
break;
case 'K':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
pPars->nCardConstr = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nCardConstr <= 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
@ -36397,12 +36408,15 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
pFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 's':
pPars->fStartPats ^= 1;
case 'k':
pPars->fNonStrict ^= 1;
break;
case 'b':
pPars->fBasic ^= 1;
break;
case 's':
pPars->fStartPats ^= 1;
break;
case 'f':
pPars->fFfOnly ^= 1;
break;
@ -36493,7 +36507,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &fftest [-ATN num] [-sbfdeuvh] <file> [-G file] [-S str]\n" );
Abc_Print( -2, "usage: &fftest [-ATNK num] [-kbsfdeuvh] <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" );
@ -36503,8 +36517,10 @@ usage:
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-K num : specifies cardinality constraint (num > 0) [default = unused]\n" );
Abc_Print( -2, "\t-k : toggles non-strict cardinality (n <= K, instead of n == K) [default = %s]\n",pPars->fNonStrict? "yes": "no" );
Abc_Print( -2, "\t-b : toggles testing for single faults (the same as \"-K 1\") [default = %s]\n", pPars->fBasic? "yes": "no" );
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-f : toggles faults at flop inputs only with \"-A 1\" and \"-S str\" [default = %s]\n", pPars->fFfOnly? "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-e : toggles dumping test pattern pairs (delay faults only) [default = %s]\n", pPars->fDumpDelay? "yes": "no" );

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

@ -130,6 +130,8 @@ struct Bmc_ParFf_t_
int fStartPats;
int nTimeOut;
int nIterCheck;
int nCardConstr;
int fNonStrict;
int fBasic;
int fFfOnly;
int fDump;

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

@ -63,6 +63,56 @@ void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
p->fVerbose = 0;
}
/**Function*************************************************************
Synopsis [Adds a general cardinality constraint in terms of vVars.]
Description [Strict is "exactly K out of N". Non-strict is
"less or equal than K out of N".]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cnf_AddCardinVar( int Level, int Base, Vec_Int_t * vVars, int k )
{
return Level ? Base + k : Vec_IntEntry( vVars, k );
}
static inline void Cnf_AddCardinConstrGeneral( sat_solver * p, Vec_Int_t * vVars, int K, int fStrict )
{
int i, k, iCur, iNext, iVar, Lit;
int nVars = sat_solver_nvars(p);
int nBits = Vec_IntSize(vVars);
Vec_IntForEachEntry( vVars, iVar, i )
assert( iVar >= 0 && iVar < nVars );
sat_solver_setnvars( p, nVars + nBits * nBits );
for ( i = 0; i < nBits; i++ )
{
iCur = nVars + nBits * (i-1);
iNext = nVars + nBits * i;
if ( i & 1 )
sat_solver_add_buffer( p, iNext, Cnf_AddCardinVar(i, iCur, vVars, 0), 0 );
for ( k = i & 1; k + 1 < nBits; k += 2 )
{
sat_solver_add_and( p, iNext+k , Cnf_AddCardinVar(i, iCur, vVars, k), Cnf_AddCardinVar(i, iCur, vVars, k+1), 1, 1, 1 );
sat_solver_add_and( p, iNext+k+1, Cnf_AddCardinVar(i, iCur, vVars, k), Cnf_AddCardinVar(i, iCur, vVars, k+1), 0, 0, 0 );
}
if ( k == nBits - 1 )
sat_solver_add_buffer( p, iNext + nBits-1, Cnf_AddCardinVar(i, iCur, vVars, nBits-1), 0 );
}
// add final constraint
assert( K > 0 && K < nBits );
Lit = Abc_Var2Lit( nVars + nBits * (nBits - 1) + K, 1 );
if ( !sat_solver_addclause( p, &Lit, &Lit+1 ) )
assert( 0 );
if ( fStrict )
{
Lit = Abc_Var2Lit( nVars + nBits * (nBits - 1) + K - 1, 0 );
if ( !sat_solver_addclause( p, &Lit, &Lit+1 ) )
assert( 0 );
}
}
/**Function*************************************************************
Synopsis [Add constraint that no more than 1 variable is 1.]
@ -99,17 +149,19 @@ static inline int Cnf_AddCardinConstr( sat_solver * p, Vec_Int_t * vVars )
}
void Cnf_AddCardinConstrTest()
{
int i, status, nVars = 7;
int i, status, Count = 1, nVars = 6;
Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
sat_solver * pSat = sat_solver_new();
sat_solver_setnvars( pSat, nVars );
Cnf_AddCardinConstr( pSat, vVars );
//Cnf_AddCardinConstrGeneral( pSat, vVars, 1, 1 );
while ( 1 )
{
status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
if ( status != l_True )
break;
Vec_IntClear( vVars );
printf( "%3d : ", Count++ );
for ( i = 0; i < nVars; i++ )
{
Vec_IntPush( vVars, Abc_Var2Lit(i, sat_solver_var_value(pSat, i)) );
@ -1078,6 +1130,14 @@ int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int
Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
Cnf_AddCardinConstr( pSat, vLits );
}
else if ( pPars->nCardConstr )
{
Vec_IntClear( vLits );
Gia_ManForEachPi( pM, pObj, i )
if ( i >= nFuncVars )
Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
Cnf_AddCardinConstrGeneral( pSat, vLits, pPars->nCardConstr, !pPars->fNonStrict );
}
// add available test-patterns
if ( Vec_IntSize(vTests) > 0 )