diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-01 11:53:08 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-01 11:53:08 -0700 |
commit | 7b8863466eacfd6b63159600e62816f830acece6 (patch) | |
tree | 121788940097c38fa8b7530835c38be46f5e9a2a | |
parent | 41e94c474a26ac18cbe75572066411dd9ece81d0 (diff) | |
download | abc-7b8863466eacfd6b63159600e62816f830acece6.tar.gz abc-7b8863466eacfd6b63159600e62816f830acece6.tar.bz2 abc-7b8863466eacfd6b63159600e62816f830acece6.zip |
Adding switch to handle only single faults.
-rw-r--r-- | src/aig/gia/giaCCof.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaFalse.c | 4 | ||||
-rw-r--r-- | src/base/abci/abc.c | 14 | ||||
-rw-r--r-- | src/map/if/ifSelect.c | 2 | ||||
-rw-r--r-- | src/proof/int2/int2Bmc.c | 2 | ||||
-rw-r--r-- | src/sat/bmc/bmcFault.c | 96 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.h | 8 |
7 files changed, 104 insertions, 24 deletions
diff --git a/src/aig/gia/giaCCof.c b/src/aig/gia/giaCCof.c index 71a6547d..19cdf9e6 100644 --- a/src/aig/gia/giaCCof.c +++ b/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) ); } diff --git a/src/aig/gia/giaFalse.c b/src/aig/gia/giaFalse.c index c7a5a638..c918559f 100644 --- a/src/aig/gia/giaFalse.c +++ b/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 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c9c4c587..acdfb9f8 100644 --- a/src/base/abci/abc.c +++ b/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" ); diff --git a/src/map/if/ifSelect.c b/src/map/if/ifSelect.c index 78557583..21e3be72 100644 --- a/src/map/if/ifSelect.c +++ b/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]; diff --git a/src/proof/int2/int2Bmc.c b/src/proof/int2/int2Bmc.c index cd7f1a74..641bfb84 100644 --- a/src/proof/int2/int2Bmc.c +++ b/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 diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index b4a540a4..8f7d8c9b 100644 --- a/src/sat/bmc/bmcFault.c +++ b/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 ) { diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 1003d54a..fb19490c 100644 --- a/src/sat/bsat/satSolver.h +++ b/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 ); |