diff options
| -rw-r--r-- | src/aig/gia/giaFalse.c | 187 | ||||
| -rw-r--r-- | src/aig/gia/giaUtil.c | 24 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 84 |
3 files changed, 228 insertions, 67 deletions
diff --git a/src/aig/gia/giaFalse.c b/src/aig/gia/giaFalse.c index c4548ef4..c7a5a638 100644 --- a/src/aig/gia/giaFalse.c +++ b/src/aig/gia/giaFalse.c @@ -20,6 +20,7 @@ #include "gia.h" #include "misc/vec/vecQue.h" +#include "misc/vec/vecWec.h" #include "sat/bsat/satStore.h" ABC_NAMESPACE_IMPL_START @@ -35,7 +36,7 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* - Synopsis [Compute slacks measured using the number of AIG levels.] + Synopsis [Reconstruct the AIG after detecting false paths.] Description [] @@ -44,17 +45,60 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_ManComputeSlacks( Gia_Man_t * p ) +void Gia_ManFalseRebuildOne( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vHook, int fVerbose, int fVeryVerbose ) { + Gia_Obj_t * pObj, * pPrev = NULL; + int i, iObjValue, iPrevValue = -1; + if ( fVerbose ) + { + printf( "Eliminating path: " ); + Vec_IntPrint( vHook ); + } + Gia_ManForEachObjVec( vHook, p, pObj, i ) + { + if ( fVeryVerbose ) + Gia_ObjPrint( p, pObj ); + iObjValue = pObj->Value; + pObj->Value = i ? Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj)) : 0; + if ( pPrev ) + pPrev->Value = iPrevValue; + iPrevValue = iObjValue; + pPrev = pObj; + } +} +Gia_Man_t * Gia_ManFalseRebuild( Gia_Man_t * p, Vec_Wec_t * vHooks, int fVerbose, int fVeryVerbose ) +{ + Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; - int i, nLevels = Gia_ManLevelNum( p ); - Vec_Int_t * vLevelR = Gia_ManReverseLevel( p ); - Vec_Int_t * vSlacks = Vec_IntAlloc( Gia_ManObjNum(p) ); - Gia_ManForEachObj( p, pObj, i ) - Vec_IntPush( vSlacks, nLevels - Gia_ObjLevelId(p, i) - Vec_IntEntry(vLevelR, i) ); - assert( Vec_IntSize(vSlacks) == Gia_ManObjNum(p) ); - Vec_IntFree( vLevelR ); - return vSlacks; + int i, Counter = 0; + pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) / 3 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManHashAlloc( pNew ); + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Vec_WecLevelSize(vHooks, i) > 0 ) + { + if ( fVerbose ) + printf( "Path %d : ", Counter++ ); + Gia_ManFalseRebuildOne( pNew, p, Vec_WecEntry(vHooks, i), fVerbose, fVeryVerbose ); + } + else + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; } /**Function************************************************************* @@ -68,26 +112,25 @@ Vec_Int_t * Gia_ManComputeSlacks( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManCollectPath_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSlacks, Vec_Int_t * vPath ) +void Gia_ManCollectPath_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPath ) { if ( Gia_ObjIsAnd(pObj) ) { - int Slack = Vec_IntEntry(vSlacks, Gia_ObjId(p, pObj)); - int Slack0 = Vec_IntEntry(vSlacks, Gia_ObjFaninId0p(p, pObj)); - int Slack1 = Vec_IntEntry(vSlacks, Gia_ObjFaninId1p(p, pObj)); - assert( Slack == Slack0 || Slack == Slack1 ); - if ( Slack == Slack0 ) - Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vSlacks, vPath ); - else - Gia_ManCollectPath_rec( p, Gia_ObjFanin1(pObj), vSlacks, vPath ); + if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) > Gia_ObjLevel(p, Gia_ObjFanin1(pObj)) ) + Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vPath ); + else if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) < Gia_ObjLevel(p, Gia_ObjFanin1(pObj)) ) + Gia_ManCollectPath_rec( p, Gia_ObjFanin1(pObj), vPath ); +// else if ( rand() & 1 ) +// Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vPath ); + else + Gia_ManCollectPath_rec( p, Gia_ObjFanin1(pObj), vPath ); } Vec_IntPush( vPath, Gia_ObjId(p, pObj) ); } -Vec_Int_t * Gia_ManCollectPath( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSlacks ) +Vec_Int_t * Gia_ManCollectPath( Gia_Man_t * p, Gia_Obj_t * pObj ) { Vec_Int_t * vPath = Vec_IntAlloc( p->nLevels ); - assert( Gia_ObjIsCo(pObj) ); - Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vSlacks, vPath ); + Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vPath ); return vPath; } @@ -102,19 +145,22 @@ Vec_Int_t * Gia_ManCollectPath( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSl SeeAlso [] ***********************************************************************/ -void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Int_t * vSlacks ) +void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vHooks, int fVerbose, int fVeryVerbose ) { sat_solver * pSat; - Gia_Obj_t * pObj = Gia_ManCo( p, iOut ); + Gia_Obj_t * pObj; + Gia_Obj_t * pPivot = Gia_ManCo( p, iOut ); Vec_Int_t * vLits = Vec_IntAlloc( p->nLevels ); - Vec_Int_t * vPath = Gia_ManCollectPath( p, pObj, vSlacks ); - int i, Shift[2], status, nLits, * pLits; + Vec_Int_t * vPath = Gia_ManCollectPath( p, pPivot ); + int nLits = 0, * pLits = NULL; + int i, Shift[2], status; abctime clkStart = Abc_Clock(); // collect objects and assign SAT variables - int iFanin = Gia_ObjFaninId0p( p, pObj ); + int iFanin = Gia_ObjFaninId0p( p, pPivot ); Vec_Int_t * vObjs = Gia_ManCollectNodesCis( p, &iFanin, 1 ); Gia_ManForEachObjVec( vObjs, p, pObj, i ) pObj->Value = Vec_IntSize(vObjs) - 1 - i; + assert( Gia_ObjIsCo(pPivot) ); // create SAT solver pSat = sat_solver_new(); sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); @@ -139,74 +185,85 @@ void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Int_t * vS Gia_ObjFanin0(pObj)->Value + Shift[1], Gia_ObjFanin1(pObj)->Value + Shift[1], Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) ); } - printf( "PO %6d : ", iOut ); // 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 ); - if ( status == l_Undef ) - printf( "Timeout reached after %d seconds. ", nTimeOut ); - else if ( status == l_True ) - printf( "There is no false path. " ); - else + if ( status == l_False ) { - assert( status == l_False ); - // call analize_final + int iBeg, iEnd; nLits = sat_solver_final( pSat, &pLits ); - printf( "False path contains %d nodes (out of %d): ", nLits, Vec_IntSize(vLits) ); - printf( "top = %d ", Vec_IntEntry(vPath, Abc_Lit2Var(pLits[0])) ); - for ( i = 0; i < nLits; i++ ) - printf( "%d ", Abc_Lit2Var(pLits[i]) ); - printf( " " ); + iBeg = Abc_Lit2Var(pLits[nLits-1]); + iEnd = Abc_Lit2Var(pLits[0]); + if ( iEnd - iBeg < 20 ) + { + // check if nodes on the path are already used + for ( i = iBeg; i <= iEnd; i++ ) + if ( Vec_WecLevelSize(vHooks, Vec_IntEntry(vPath, i)) > 0 ) + break; + if ( i > iEnd ) + { + Vec_Int_t * vHook = Vec_WecEntry(vHooks, Vec_IntEntry(vPath, iEnd)); + for ( i = iBeg; i <= iEnd; i++ ) + Vec_IntPush( vHook, Vec_IntEntry(vPath, i) ); + } + } + } + if ( fVerbose ) + { + printf( "PO %6d : Level = %3d ", iOut, Gia_ObjLevel(p, pPivot) ); + if ( status == l_Undef ) + printf( "Timeout reached after %d seconds. ", nTimeOut ); + else if ( status == l_True ) + printf( "There is no false path. " ); + else + { + printf( "False path contains %d nodes (out of %d): ", nLits, Vec_IntSize(vLits) ); + printf( "top = %d ", Vec_IntEntry(vPath, Abc_Lit2Var(pLits[0])) ); + if ( fVeryVerbose ) + for ( i = 0; i < nLits; i++ ) + printf( "%d ", Abc_Lit2Var(pLits[i]) ); + printf( " " ); + } + Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); } - Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); sat_solver_delete( pSat ); Vec_IntFree( vObjs ); Vec_IntFree( vPath ); Vec_IntFree( vLits ); } -void Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut ) +Gia_Man_t * Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose ) { + Gia_Man_t * pNew; + Vec_Wec_t * vHooks; Vec_Que_t * vPrio; Vec_Flt_t * vWeights; - Vec_Int_t * vSlacks; Gia_Obj_t * pObj; int i; - vSlacks = Gia_ManComputeSlacks(p); -//Vec_IntPrint( vSlacks ); + srand( 111 ); + Gia_ManLevelNum( p ); // create PO weights vWeights = Vec_FltAlloc( Gia_ManCoNum(p) ); Gia_ManForEachCo( p, pObj, i ) - Vec_FltPush( vWeights, p->nLevels - Vec_IntEntry(vSlacks, Gia_ObjId(p, pObj)) ); + Vec_FltPush( vWeights, Gia_ObjLevel(p, pObj) ); // put POs into the queue vPrio = Vec_QueAlloc( Gia_ManCoNum(p) ); Vec_QueSetPriority( vPrio, Vec_FltArrayP(vWeights) ); Gia_ManForEachCo( p, pObj, i ) Vec_QuePush( vPrio, i ); // work on each PO in the queue + vHooks = Vec_WecStart( Gia_ManObjNum(p) ); while ( Vec_QueTopPriority(vPrio) >= p->nLevels - nSlackMax ) - Gia_ManCheckFalseOne( p, Vec_QuePop(vPrio), nTimeOut, vSlacks ); + Gia_ManCheckFalseOne( p, Vec_QuePop(vPrio), nTimeOut, vHooks, fVerbose, fVeryVerbose ); + if ( fVerbose ) + printf( "Collected %d non-overlapping false paths.\n", Vec_WecSizeUsed(vHooks) ); + // reconstruct the AIG + pNew = Gia_ManFalseRebuild( p, vHooks, fVerbose, fVeryVerbose ); // cleanup - Vec_IntFree( vSlacks ); + Vec_WecFree( vHooks ); Vec_FltFree( vWeights ); Vec_QueFree( vPrio ); + return pNew; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax ) -{ - Gia_ManCheckFalse( p, nSlackMax, 0 ); -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index f3edca36..34bda9bb 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -621,6 +621,30 @@ Vec_Int_t * Gia_ManRequiredLevel( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Compute slacks measured using the number of AIG levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManComputeSlacks( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, nLevels = Gia_ManLevelNum( p ); + Vec_Int_t * vLevelR = Gia_ManReverseLevel( p ); + Vec_Int_t * vSlacks = Vec_IntAlloc( Gia_ManObjNum(p) ); + Gia_ManForEachObj( p, pObj, i ) + Vec_IntPush( vSlacks, nLevels - Gia_ObjLevelId(p, i) - Vec_IntEntry(vLevelR, i) ); + assert( Vec_IntSize(vSlacks) == Gia_ManObjNum(p) ); + Vec_IntFree( vLevelR ); + return vSlacks; +} + +/**Function************************************************************* + Synopsis [Assigns levels.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3da41636..0681f28e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -355,6 +355,7 @@ static int Abc_CommandAbc9Balance ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Syn2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Syn3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Syn4 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9False ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Miter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Miter2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Append ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -920,6 +921,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&syn2", Abc_CommandAbc9Syn2, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&syn3", Abc_CommandAbc9Syn3, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&syn4", Abc_CommandAbc9Syn4, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&false", Abc_CommandAbc9False, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&miter", Abc_CommandAbc9Miter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&miter2", Abc_CommandAbc9Miter2, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&append", Abc_CommandAbc9Append, 0 ); @@ -27790,6 +27792,84 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9False( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose ); + Gia_Man_t * pTemp; + int nSlackMax = 0; + int nTimeOut = 0; + int c, fVerbose = 0; + int fVeryVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "STvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by a char string.\n" ); + goto usage; + } + nSlackMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSlackMax < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by a char string.\n" ); + goto usage; + } + nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9False(): There is no AIG.\n" ); + return 1; + } + pTemp = Gia_ManCheckFalse( pAbc->pGia, nSlackMax, nTimeOut, fVerbose, fVeryVerbose ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &false [-ST num] [-vwh]\n" ); + Abc_Print( -2, "\t detecting and elimintation false paths\n" ); + Abc_Print( -2, "\t-S num : maximum slack to idetify false paths [default = %d]\n", nSlackMax ); + Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeOut ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pFile; @@ -34003,7 +34083,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern Gia_Man_t * Llb_ReachableStatesGia( Gia_Man_t * p ); // extern Gia_Man_t * Unm_ManTest( Gia_Man_t * pGia ); // extern void Agi_ManTest( Gia_Man_t * pGia ); - extern void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax ); +// extern void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF ) @@ -34083,7 +34163,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Agi_ManTest( pAbc->pGia ); // Gia_ManResubTest( pAbc->pGia ); // Jf_ManTestCnf( pAbc->pGia ); - Gia_ManCheckFalseTest( pAbc->pGia, nFrames ); +// Gia_ManCheckFalseTest( pAbc->pGia, nFrames ); return 0; usage: Abc_Print( -2, "usage: &test [-F num] [-svh]\n" ); |