Skip to content

A
abc
Commit 7b886346 by Alan Mishchenko
Options

Adding switch to handle only single faults.

parent 41e94c47
Showing with 104 additions and 24 deletions
src/aig/gia/giaCCof.c
......@@ -128,7 +128,7 @@ void Gia_ManCofExtendSolver( Ccf_Man_t * p )
Gia_ObjFaninId0(pObj, i),
Gia_ObjFaninId1(pObj, i),
Gia_ObjFaninC0(pObj),
Gia_ObjFaninC1(pObj) );
Gia_ObjFaninC1(pObj), 0 );
}
sat_solver_setnvars( p->pSat, Gia_ManObjNum(p->pFrames) );
}
......
src/aig/gia/giaFalse.c
......@@ -180,10 +180,10 @@ void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vH
continue;
sat_solver_add_and( pSat, pObj->Value + Shift[0],
Gia_ObjFanin0(pObj)->Value + Shift[0], Gia_ObjFanin1(pObj)->Value + Shift[0],
Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) );
Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
sat_solver_add_and( pSat, pObj->Value + Shift[1],
Gia_ObjFanin0(pObj)->Value + Shift[1], Gia_ObjFanin1(pObj)->Value + Shift[1],
Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) );
Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
}
// call the SAT solver
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
......
src/base/abci/abc.c
......@@ -32880,11 +32880,11 @@ usage:
***********************************************************************/
int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int fStartPats, int nTimeOut, int fDump, int fDumpUntest, int fVerbose );
int c, Algo = 0, fComplVars = 0, fStartPats = 0, nTimeOut = 0, fDump = 0, fDumpUntest = 0, fVerbose = 0;
extern void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int fStartPats, int nTimeOut, int fBasic, int fDump, int fDumpUntest, int fVerbose );
int c, Algo = 0, fComplVars = 0, fStartPats = 0, nTimeOut = 0, fBasic = 0, fDump = 0, fDumpUntest = 0, fVerbose = 0;
char * pFileName = NULL;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ATcsduvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ATcsbduvh" ) ) != EOF )
{
switch ( c )
{
......@@ -32916,6 +32916,9 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
fStartPats ^= 1;
break;
case 'b':
fBasic ^= 1;
break;
case 'd':
fDump ^= 1;
break;
......@@ -32955,11 +32958,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, pFileName, Algo, fComplVars, fStartPats, nTimeOut, fDump, fDumpUntest, fVerbose );
Gia_ManFaultTest( pAbc->pGia, pFileName, Algo, fComplVars, fStartPats, nTimeOut, fBasic, fDump, fDumpUntest, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &fftest [-AT num] [-csduvh] <file>\n" );
Abc_Print( -2, "usage: &fftest [-AT num] [-csbduvh] <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" );
......@@ -32970,6 +32973,7 @@ usage:
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-s : toggles starting with the all-0 and all-1 patterns [default = %s]\n", fStartPats? "yes": "no" );
Abc_Print( -2, "\t-b : toggles testing for single faults only [default = %s]\n", fBasic? "yes": "no" );
Abc_Print( -2, "\t-d : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", fDump? "yes": "no" );
Abc_Print( -2, "\t-u : toggles dumping untestable faults into \"untest.txt\" [default = %s]\n", fDumpUntest? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
src/map/if/ifSelect.c
......@@ -455,7 +455,7 @@ int If_ManNodeShapeSat( If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vShape
assert( Vec_IntSize(vFanins) > 0 );
sat_solver_add_choice( pSat, If_ObjSatVar(pObj), vFanins ); // external
assert( If_ObjSatVar(pObj) > 0 );
// sat_solver_add_and( pSat, If_ObjSatVar(pObj)+1, If_ObjSatVar(pObj->pFanin0), If_ObjSatVar(pObj->pFanin1), 0, 0 );
// sat_solver_add_and( pSat, If_ObjSatVar(pObj)+1, If_ObjSatVar(pObj->pFanin0), If_ObjSatVar(pObj->pFanin1), 0, 0, 0 );
if ( If_ObjSatVar(pObj->pFanin0) > 0 && If_ObjSatVar(pObj->pFanin1) > 0 )
{
int Lits[2];
......
src/proof/int2/int2Bmc.c
......@@ -293,7 +293,7 @@ void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos )
if ( Entry < Gia_ManObjNum(pFrames) )
{
assert( !Abc_LitIsCompl(iLit) );
sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) );
sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), 0 );
}
}
else
......
src/sat/bmc/bmcFault.c
......@@ -36,6 +36,67 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis [Add constraint that no more than 1 variable is 1.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Cnf_AddCardinConstr( sat_solver * p, Vec_Int_t * vVars )
{
int i, k, pLits[2], iVar, nVars = sat_solver_nvars(p);
Vec_IntForEachEntry( vVars, iVar, i )
assert( iVar >= 0 && iVar < nVars );
iVar = nVars;
sat_solver_setnvars( p, nVars + Vec_IntSize(vVars) - 1 );
while ( Vec_IntSize(vVars) > 1 )
{
for ( k = i = 0; i < Vec_IntSize(vVars)/2; i++ )
{
pLits[0] = Abc_Var2Lit( Vec_IntEntry(vVars, 2*i), 1 );
pLits[1] = Abc_Var2Lit( Vec_IntEntry(vVars, 2*i+1), 1 );
sat_solver_addclause( p, pLits, pLits + 2 );
sat_solver_add_and( p, iVar, Vec_IntEntry(vVars, 2*i), Vec_IntEntry(vVars, 2*i+1), 1, 1, 1 );
Vec_IntWriteEntry( vVars, k++, iVar++ );
}
if ( Vec_IntSize(vVars) & 1 )
Vec_IntWriteEntry( vVars, k++, Vec_IntEntryLast(vVars) );
Vec_IntShrink( vVars, k );
}
return iVar;
}
void Cnf_AddCardinConstrTest()
{
int i, status, nVars = 7;
Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
sat_solver * pSat = sat_solver_new();
sat_solver_setnvars( pSat, nVars );
Cnf_AddCardinConstr( pSat, vVars );
while ( 1 )
{
status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
if ( status != l_True )
break;
Vec_IntClear( vVars );
for ( i = 0; i < nVars; i++ )
{
Vec_IntPush( vVars, Abc_Var2Lit(i, sat_solver_var_value(pSat, i)) );
printf( "%d", sat_solver_var_value(pSat, i) );
}
printf( "\n" );
status = sat_solver_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) );
if ( status == 0 )
break;
}
sat_solver_delete( pSat );
Vec_IntFree( vVars );
}
/**Function*************************************************************
Synopsis []
Description []
......@@ -503,7 +564,7 @@ Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName )
SeeAlso []
***********************************************************************/
void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int fStartPats, int nTimeOut, int fDump, int fDumpUntest, int fVerbose )
void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars, int fStartPats, int nTimeOut, int fBasic, int fDump, int fDumpUntest, int fVerbose )
{
int nIterMax = 1000000;
int i, Iter, LitRoot, status, nFuncVars = -1;
......@@ -516,19 +577,29 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
// select algorithm
if ( Algo == 1 )
nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
printf( "FFTEST is computing test patterns for %sdelay faults...\n", fBasic ? "single " : "" );
else if ( Algo == 2 )
nFuncVars = Gia_ManCiNum(p);
printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", fBasic ? "single " : "" );
else if ( Algo == 3 )
nFuncVars = Gia_ManCiNum(p);
printf( "FFTEST is computing test patterns for %scomplement faults...\n", fBasic ? "single " : "" );
else if ( Algo == 4 )
nFuncVars = Gia_ManCiNum(p);
printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", fBasic ? "single " : "" );
else
{
printf( "Unregnized algorithm (%d).\n", Algo );
return;
}
// 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 if ( Algo == 4 )
nFuncVars = Gia_ManCiNum(p);
// collect test patterns from file
if ( pFileName )
vTests = Gia_ManGetTestPatterns( pFileName );
......@@ -565,11 +636,6 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
p0 = Gia_ManFOFUnfold( p, 0, fComplVars );
p1 = Gia_ManFOFUnfold( p, 1, fComplVars );
}
else
{
printf( "Unregnized algorithm (%d).\n", Algo );
return;
}
// create miter
pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
......@@ -595,6 +661,16 @@ void Gia_ManFaultTest( Gia_Man_t * p, char * pFileName, int Algo, int fComplVars
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 cadinality constraint
if ( fBasic )
{
Vec_IntClear( vLits );
Gia_ManForEachPi( pM, pObj, i )
if ( i >= nFuncVars )
Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
Cnf_AddCardinConstr( pSat, vLits );
}
// add available test-patterns
if ( Vec_IntSize(vTests) > 0 )
{
......
src/sat/bsat/satSolver.h
......@@ -315,22 +315,22 @@ static inline int sat_solver_add_buffer_enable( sat_solver * pSat, int iVarA, in
assert( Cid );
return 2;
}
static inline int sat_solver_add_and( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
static inline int sat_solver_add_and( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
{
lit Lits[3];
int Cid;
Lits[0] = toLitCond( iVar, 1 );
Lits[0] = toLitCond( iVar, !fCompl );
Lits[1] = toLitCond( iVar0, fCompl0 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( Cid );
Lits[0] = toLitCond( iVar, 1 );
Lits[0] = toLitCond( iVar, !fCompl );
Lits[1] = toLitCond( iVar1, fCompl1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( Cid );
Lits[0] = toLitCond( iVar, 0 );
Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar0, !fCompl0 );
Lits[2] = toLitCond( iVar1, !fCompl1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
......
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