From bc6c0837a18e21b4fbcb6e43c8328f42614e9277 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 17 Apr 2015 17:00:31 +0900 Subject: Adding support for dumping faults not detected by a given test-set in &fftest (switch -n). --- src/base/abci/abc.c | 10 +++- src/sat/bmc/bmc.h | 1 + src/sat/bmc/bmcFault.c | 130 ++++++++++++++++++++++++++++++++++++++++--------- 3 files changed, 117 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8b96bba1..7249e676 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10890,6 +10890,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Tab_DecomposeTest(); //Tab_DecomposeTest(); + extern void Cnf_AddCardinConstrTest(); + Cnf_AddCardinConstrTest(); } return 0; usage: @@ -36342,7 +36344,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, "ATNKSGkbsfdeuvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ATNKSGkbsfdeunvh" ) ) != EOF ) { switch ( c ) { @@ -36429,6 +36431,9 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'u': pPars->fDumpUntest ^= 1; break; + case 'n': + pPars->fDumpNewFaults ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -36507,7 +36512,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fftest [-ATNK num] [-kbsfdeuvh] [-G file] [-S str]\n" ); + Abc_Print( -2, "usage: &fftest [-ATNK num] [-kbsfdeunvh] [-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" ); @@ -36525,6 +36530,7 @@ usage: 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" ); Abc_Print( -2, "\t-u : toggles dumping untestable faults into \"untest.txt\" [default = %s]\n", pPars->fDumpUntest? "yes": "no" ); + Abc_Print( -2, "\t-n : toggles dumping faults not detected by a given test set [default = %s]\n", pPars->fDumpNewFaults? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : (optional) file name with input test patterns\n\n"); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 14ffec12..b0a9210d 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -137,6 +137,7 @@ struct Bmc_ParFf_t_ int fDump; int fDumpDelay; int fDumpUntest; + int fDumpNewFaults; int fVerbose; }; diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index e91c76ac..4665bbad 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -836,7 +836,7 @@ void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime c SeeAlso [] ***********************************************************************/ -int Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Vec_Int_t * vLits, int nFuncVars ) +int Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Vec_Int_t * vLits, int nFuncVars, int fAddOr, Gia_Man_t * pGiaCnf ) { Gia_Man_t * pC;//, * pTemp; Cnf_Dat_t * pCnf2; @@ -844,14 +844,6 @@ int Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Vec int i, Lit; // derive the cofactor pC = Gia_ManFaultCofactor( pM, vLits ); - // try synthesis -// printf( "\n" ); -// Gia_ManPrintStats( pC, NULL ); -// pC = Gia_ManAigSyn2( pTemp = pC, 0, 1, 0, 100, 0, 0, 0 ); -// Gia_ManStop( pTemp ); -// Gia_ManPrintStats( pC, NULL ); -//Gia_AigerWrite( pC, "fftest_cof.aig", 0, 0 ); -//printf( "Dumped cofactor circuit into file \"%s\".\n", "fftest_cof.aig" ); // derive new CNF pCnf2 = Cnf_DeriveGiaRemapped( pC ); Cnf_DataLiftGia( pCnf2, pC, sat_solver_nvars(pSat) ); @@ -864,20 +856,40 @@ int Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Vec return 0; } // add constraint clauses - Gia_ManForEachPo( pC, pObj, i ) + if ( fAddOr ) { - Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 1 ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + // add one OR gate to assert difference of at least one output of the miter + Vec_Int_t * vOrGate = Vec_IntAlloc( Gia_ManPoNum(pC) ); + Gia_ManForEachPo( pC, pObj, i ) { - Cnf_DataFree( pCnf2 ); - Gia_ManStop( pC ); - return 0; + Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 0 ); + Vec_IntPush( vOrGate, Lit ); + } + if ( !sat_solver_addclause( pSat, Vec_IntArray(vOrGate), Vec_IntArray(vOrGate) + Vec_IntSize(vOrGate) ) ) + assert( 0 ); + Vec_IntFree( vOrGate ); + } + else + { + // add negative literals to assert equality of all outputs of the miter + Gia_ManForEachPo( pC, pObj, i ) + { + Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 1 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + { + Cnf_DataFree( pCnf2 ); + Gia_ManStop( pC ); + return 0; + } } } // add connection clauses - Gia_ManForEachPi( pM, pObj, i ) - if ( i >= nFuncVars ) - sat_solver_add_buffer( pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)], pCnf2->pVarNums[Gia_ObjId(pC, Gia_ManPi(pC, i))], 0 ); + if ( pGiaCnf ) + { + Gia_ManForEachPi( pGiaCnf, pObj, i ) + if ( i >= nFuncVars ) + sat_solver_add_buffer( pSat, pCnf->pVarNums[Gia_ObjId(pGiaCnf, pObj)], pCnf2->pVarNums[Gia_ObjId(pC, Gia_ManPi(pC, i))], 0 ); + } Cnf_DataFree( pCnf2 ); Gia_ManStop( pC ); return 1; @@ -1053,6 +1065,69 @@ int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vMap, return nUnsats; } +/**Function************************************************************* + + Synopsis [Dump faults detected by the new test, which are not detected by previous tests.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFaultDumpNewFaults( Gia_Man_t * pM, int nFuncVars, Vec_Int_t * vTests, Vec_Int_t * vTestNew, Bmc_ParFf_t * pPars ) +{ + char * pFileName = "newfaults.txt"; + abctime clk; + Gia_Man_t * pC; + Cnf_Dat_t * pCnf2; + sat_solver * pSat; + Vec_Int_t * vLits; + int i, Iter, IterMax, nNewFaults; + + // derive the cofactor + pC = Gia_ManFaultCofactor( pM, vTestNew ); + // derive new CNF + pCnf2 = Cnf_DeriveGiaRemapped( pC ); + + // create SAT solver + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, 1 ); + sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); + // create the first cofactor + Gia_ManFaultAddOne( pM, NULL, pSat, vTestNew, nFuncVars, 1, NULL ); + + // add other test patterns + assert( Vec_IntSize(vTests) % nFuncVars == 0 ); + IterMax = Vec_IntSize(vTests) / nFuncVars; + vLits = Vec_IntAlloc( nFuncVars ); + for ( Iter = 0; Iter < IterMax; Iter++ ) + { + // get pattern + Vec_IntClear( vLits ); + for ( i = 0; i < nFuncVars; i++ ) + Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) ); + // the resulting problem cannot be UNSAT, because the new test is guaranteed + // to detect something that the given test set does not detect + if ( !Gia_ManFaultAddOne( pM, pCnf2, pSat, vLits, nFuncVars, 0, pC ) ) + assert( 0 ); + } + Vec_IntFree( vLits ); + + // dump the new faults + clk = Abc_Clock(); + nNewFaults = Gia_ManDumpUntests( pC, pCnf2, pSat, nFuncVars, pFileName, pPars->fVerbose ); + printf( "Dumped %d new multiple faults into file \"%s\". ", nNewFaults, pFileName ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + // cleanup + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf2 ); + Gia_ManStop( pC ); + return 1; +} + /**Function************************************************************* Synopsis [Generate miter, CNF and solver.] @@ -1174,7 +1249,7 @@ int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int Vec_IntClear( vLits ); for ( i = 0; i < nFuncVars; i++ ) Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) ); - if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ) ) + if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars, 0, pM ) ) { if ( pPars->fVerbose ) printf( "\n" ); @@ -1214,7 +1289,7 @@ int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int // initialize simple pattern Vec_IntFill( vLits, nFuncVars, Iter ); Vec_IntAppend( vTests, vLits ); - if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ) ) + if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars, 0, pM ) ) { if ( pPars->fVerbose ) printf( "\n" ); @@ -1369,9 +1444,19 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars ) Gia_ManForEachPi( pM, pObj, i ) if ( i < nFuncVars ) Vec_IntPush( vLits, sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) ); + // if the user selected to generate new faults detected by this test (vLits) + // and not detected by the given test set (vTests), we compute the new faults here and quit + if ( pPars->fDumpNewFaults ) + { + if ( Vec_IntSize(vTests) == 0 ) + printf( "The input test patterns are not given.\n" ); + else + Gia_ManFaultDumpNewFaults( pM, nFuncVars, vTests, vLits, pPars ); + goto finish_all; + } Vec_IntAppend( vTests, vLits ); // add constraint - if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ) ) + if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars, 0, pM ) ) { if ( pPars->fVerbose ) printf( "\n" ); @@ -1472,7 +1557,7 @@ finish: Vec_IntClear( vLits ); for ( i = 0; i < nFuncVars; i++ ) Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter2*nFuncVars + i) ); - if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ) ) + if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars, 0, pM ) ) { printf( "The problem is UNSAT after adding %d tests.\n", Iter2 ); goto finish; @@ -1512,6 +1597,7 @@ finish: Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } } +finish_all: sat_solver_delete( pSat ); Cnf_DataFree( pCnf ); Gia_ManStop( pM ); -- cgit v1.2.3