From ca87c1a6a09a7357931432e47c0b0edd4cb29c20 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 15 Aug 2017 11:36:15 +0700 Subject: Unfold several timeframes at the same time in &bmcs. --- src/base/abci/abc.c | 18 ++++- src/sat/bmc/bmcBmcS.c | 191 +++++++++++++++++++++++++++----------------------- 2 files changed, 118 insertions(+), 91 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6ef02a06..0e4f25f7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -39991,7 +39991,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) memset( pPars, 0, sizeof(Bmc_AndPar_t) ); pPars->nStart = 0; // starting timeframe pPars->nFramesMax = 0; // maximum number of timeframes - pPars->nFramesAdd = 0; // the number of additional frames + pPars->nFramesAdd = 1; // the number of additional frames pPars->nConfLimit = 0; // maximum number of conflicts at a node pPars->nTimeOut = 0; // timeout in seconds pPars->nLutSize = 0; // max LUT size for CNF computation @@ -40009,7 +40009,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pFuncOnFrameDone = pAbc->pFuncOnFrameDone; // frame done callback Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PCFTvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PCFATvwh" ) ) != EOF ) { switch ( c ) { @@ -40046,6 +40046,17 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nFramesMax < 0 ) goto usage; break; + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesAdd < 0 ) + goto usage; + break; case 'T': if ( globalUtilOptind >= argc ) { @@ -40080,11 +40091,12 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &bmcs [-PCFT num] [-vwh]\n" ); + Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-vwh]\n" ); Abc_Print( -2, "\t performs bounded model checking\n" ); Abc_Print( -2, "\t-P num : the number of parallel solvers [default = %d]\n", pPars->nProcs ); Abc_Print( -2, "\t-C num : the SAT solver conflict limit [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax ); + Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd ); Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 9df478df..4b15a81d 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -453,25 +453,27 @@ int Bmcs_ManCollect_rec( Bmcs_Man_t * p, int iObj ) Gia_ObjSetCopyArray( p->pFrames, iObj, iLitClean ); return iLitClean; } -Gia_Man_t * Bmcs_ManUnfold( Bmcs_Man_t * p, int f ) +Gia_Man_t * Bmcs_ManUnfold( Bmcs_Man_t * p, int f, int nFramesAdd ) { Gia_Man_t * pNew = NULL; Gia_Obj_t * pObj; - int i, iLitFrame, iLitClean, fTrivial = 1; - int nFrameObjs = Gia_ManObjNum(p->pFrames); - int * pCopies; - // unfold this timeframe - Vec_PtrPush( &p->vGia2Fr, ABC_FALLOC(int, Gia_ManObjNum(p->pGia)) ); - assert( Vec_PtrSize(&p->vGia2Fr) == f+1 ); - pCopies = Bmcs_ManCopies( p, f ); - //memset( pCopies, 0xFF, sizeof(int)*Gia_ManObjNum(p->pGia) ); - pCopies[0] = 0; + int i, k, iLitFrame, iLitClean, fTrivial = 1; + int * pCopies, nFrameObjs = Gia_ManObjNum(p->pFrames); assert( Gia_ManPoNum(p->pFrames) == f * Gia_ManPoNum(p->pGia) ); - Gia_ManForEachPo( p->pGia, pObj, i ) + for ( k = 0; k < nFramesAdd; k++ ) { - iLitFrame = Bmcs_ManUnfold_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); - iLitFrame = Abc_LitNotCond( iLitFrame, Gia_ObjFaninC0(pObj) ); - pCopies[Gia_ObjId(p->pGia, pObj)] = Gia_ManAppendCo( p->pFrames, iLitFrame ); - fTrivial &= (iLitFrame == 0); + // unfold this timeframe + Vec_PtrPush( &p->vGia2Fr, ABC_FALLOC(int, Gia_ManObjNum(p->pGia)) ); + assert( Vec_PtrSize(&p->vGia2Fr) == f+k+1 ); + pCopies = Bmcs_ManCopies( p, f+k ); + //memset( pCopies, 0xFF, sizeof(int)*Gia_ManObjNum(p->pGia) ); + pCopies[0] = 0; + Gia_ManForEachPo( p->pGia, pObj, i ) + { + iLitFrame = Bmcs_ManUnfold_rec( p, Gia_ObjFaninId0p(p->pGia, pObj), f+k ); + iLitFrame = Abc_LitNotCond( iLitFrame, Gia_ObjFaninC0(pObj) ); + pCopies[Gia_ObjId(p->pGia, pObj)] = Gia_ManAppendCo( p->pFrames, iLitFrame ); + fTrivial &= (iLitFrame == 0); + } } if ( fTrivial ) return NULL; @@ -482,9 +484,10 @@ Gia_Man_t * Bmcs_ManUnfold( Bmcs_Man_t * p, int f ) Gia_ManStopP( &p->pClean ); p->pClean = Gia_ManStart( Gia_ManObjNum(p->pFrames) - nFrameObjs + 1000 ); Gia_ObjSetCopyArray( p->pFrames, 0, 0 ); + for ( k = 0; k < nFramesAdd; k++ ) for ( i = 0; i < Gia_ManPoNum(p->pGia); i++ ) { - pObj = Gia_ManCo( p->pFrames, f * Gia_ManPoNum(p->pGia) + i ); + pObj = Gia_ManCo( p->pFrames, (f+k) * Gia_ManPoNum(p->pGia) + i ); iLitClean = Bmcs_ManCollect_rec( p, Gia_ObjFaninId0p(p->pFrames, pObj) ); iLitClean = Abc_LitNotCond( iLitClean, Gia_ObjFaninC0(pObj) ); iLitClean = Gia_ManAppendCo( p->pClean, iLitClean ); @@ -496,9 +499,9 @@ Gia_Man_t * Bmcs_ManUnfold( Bmcs_Man_t * p, int f ) Gia_ObjSetCopyArray( p->pFrames, pObj->Value, -1 ); return pNew; } -Cnf_Dat_t * Bmcs_ManAddNewCnf( Bmcs_Man_t * p, int f ) +Cnf_Dat_t * Bmcs_ManAddNewCnf( Bmcs_Man_t * p, int f, int nFramesAdd ) { - Gia_Man_t * pNew = Bmcs_ManUnfold( p, f ); + Gia_Man_t * pNew = Bmcs_ManUnfold( p, f, nFramesAdd ); Cnf_Dat_t * pCnf; Gia_Obj_t * pObj; int i, iVar, * pMap; @@ -577,64 +580,70 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { abctime clkStart = Abc_Clock(); Bmcs_Man_t * p = Bmcs_ManStart( pGia, pPars ); - int f, i = Gia_ManPoNum(pGia), status, RetValue = -1, nClauses = 0; + int f, k, i = Gia_ManPoNum(pGia), status, RetValue = -1, nClauses = 0; Abc_CexFreeP( &pGia->pCexSeq ); - for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ ) + for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f += pPars->nFramesAdd ) { - Cnf_Dat_t * pCnf = Bmcs_ManAddNewCnf( p, f ); + Cnf_Dat_t * pCnf = Bmcs_ManAddNewCnf( p, f, pPars->nFramesAdd ); if ( pCnf == NULL ) { Bmcs_ManPrintFrame( p, f, nClauses, -1, clkStart ); if( pPars->pFuncOnFrameDone) + for ( k = 0; k < pPars->nFramesAdd; k++ ) for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) - pPars->pFuncOnFrameDone(f, i, 0); + pPars->pFuncOnFrameDone(f+k, i, 0); continue; } nClauses += pCnf->nClauses; Bmcs_ManAddCnf( p->pSats[0], pCnf ); Cnf_DataFree( pCnf ); - assert( Gia_ManPoNum(p->pFrames) == (f + 1) * Gia_ManPoNum(pGia) ); - for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) + assert( Gia_ManPoNum(p->pFrames) == (f + pPars->nFramesAdd) * Gia_ManPoNum(pGia) ); + for ( k = 0; k < pPars->nFramesAdd; k++ ) { - int iObj = Gia_ObjId( p->pFrames, Gia_ManCo(p->pFrames, f * Gia_ManPoNum(pGia) + i) ); - int iLit = Abc_Var2Lit( Vec_IntEntry(&p->vFr2Sat, iObj), 0 ); - if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut ) - break; - satoko_assump_push( p->pSats[0], iLit ); - status = satoko_solve( p->pSats[0] ); - satoko_assump_pop( p->pSats[0] ); - if ( status == SATOKO_UNSAT ) - { - if ( i == Gia_ManPoNum(pGia)-1 ) - Bmcs_ManPrintFrame( p, f, nClauses, -1, clkStart ); - if( pPars->pFuncOnFrameDone) - pPars->pFuncOnFrameDone(f, i, 0); - continue; - } - if ( status == SATOKO_SAT ) + for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) { - RetValue = 0; - pPars->iFrame = f; - pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f, 0 ); - pPars->nFailOuts++; - if ( !pPars->fNotVerbose ) + int iObj = Gia_ObjId( p->pFrames, Gia_ManCo(p->pFrames, (f+k) * Gia_ManPoNum(pGia) + i) ); + int iLit = Abc_Var2Lit( Vec_IntEntry(&p->vFr2Sat, iObj), 0 ); + if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut ) + break; + satoko_assump_push( p->pSats[0], iLit ); + status = satoko_solve( p->pSats[0] ); + satoko_assump_pop( p->pSats[0] ); + if ( status == SATOKO_UNSAT ) + { + if ( i == Gia_ManPoNum(pGia)-1 ) + Bmcs_ManPrintFrame( p, f+k, nClauses, -1, clkStart ); + if( pPars->pFuncOnFrameDone) + pPars->pFuncOnFrameDone(f+k, i, 0); + continue; + } + if ( status == SATOKO_SAT ) { - int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); - Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs). ", - nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Gia_ManPoNum(pGia) ); - fflush( stdout ); + RetValue = 0; + pPars->iFrame = f+k; + pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, 0 ); + pPars->nFailOuts++; + if ( !pPars->fNotVerbose ) + { + int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); + Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs). ", + nOutDigits, i, f+k, nOutDigits, pPars->nFailOuts, nOutDigits, Gia_ManPoNum(pGia) ); + fflush( stdout ); + } + if( pPars->pFuncOnFrameDone) + pPars->pFuncOnFrameDone(f+k, i, 1); } - if( pPars->pFuncOnFrameDone) - pPars->pFuncOnFrameDone(f, i, 1); + break; } - break; + if ( i < Gia_ManPoNum(pGia) || f+k == pPars->nFramesMax-1 ) + break; } - if ( i < Gia_ManPoNum(pGia) ) + if ( k < pPars->nFramesAdd ) break; } Bmcs_ManStop( p ); if ( RetValue == -1 && !pPars->fNotVerbose ) - printf( "No output failed in %d frames. ", f ); + printf( "No output failed in %d frames. ", f + (k < pPars->nFramesAdd ? k+1 : 0) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); return RetValue; } @@ -746,7 +755,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pthread_t WorkerThread[PAR_THR_MAX]; Par_ThData_t ThData[PAR_THR_MAX]; Bmcs_Man_t * p = Bmcs_ManStart( pGia, pPars ); - int f, i = Gia_ManPoNum(pGia), status, RetValue = -1, nClauses = 0, Solver = 0; + int f, k, i = Gia_ManPoNum(pGia), status, RetValue = -1, nClauses = 0, Solver = 0; Abc_CexFreeP( &pGia->pCexSeq ); // start threads for ( i = 0; i < pPars->nProcs; i++ ) @@ -759,15 +768,16 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) status = pthread_create( WorkerThread + i, NULL, Bmcs_ManWorkerThread, (void *)(ThData + i) ); assert( status == 0 ); } // solve properties in each timeframe - for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ ) + for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f += pPars->nFramesAdd ) { - Cnf_Dat_t * pCnf = Bmcs_ManAddNewCnf( p, f ); + Cnf_Dat_t * pCnf = Bmcs_ManAddNewCnf( p, f, pPars->nFramesAdd ); if ( pCnf == NULL ) { Bmcs_ManPrintFrame( p, f, nClauses, 0, clkStart ); if( pPars->pFuncOnFrameDone ) + for ( k = 0; k < pPars->nFramesAdd; k++ ) for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) - pPars->pFuncOnFrameDone(f, i, 0); + pPars->pFuncOnFrameDone(f+k, i, 0); continue; } // load CNF into solvers @@ -776,41 +786,46 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) Bmcs_ManAddCnf( p->pSats[i], pCnf ); Cnf_DataFree( pCnf ); // solve outputs - assert( Gia_ManPoNum(p->pFrames) == (f + 1) * Gia_ManPoNum(pGia) ); - for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) + assert( Gia_ManPoNum(p->pFrames) == (f + pPars->nFramesAdd) * Gia_ManPoNum(pGia) ); + for ( k = 0; k < pPars->nFramesAdd; k++ ) { - int iObj = Gia_ObjId( p->pFrames, Gia_ManCo(p->pFrames, f * Gia_ManPoNum(pGia) + i) ); - int iLit = Abc_Var2Lit( Vec_IntEntry(&p->vFr2Sat, iObj), 0 ); - if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut ) - break; - status = Bmcs_ManPerform_Solve( p, iLit, WorkerThread, ThData, pPars->nProcs, &Solver ); - if ( status == SATOKO_UNSAT ) - { - if ( i == Gia_ManPoNum(pGia)-1 ) - Bmcs_ManPrintFrame( p, f, nClauses, Solver, clkStart ); - if( pPars->pFuncOnFrameDone ) - pPars->pFuncOnFrameDone(f, i, 0); - continue; - } - if ( status == SATOKO_SAT ) + for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) { - RetValue = 0; - pPars->iFrame = f; - pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f, Solver ); - pPars->nFailOuts++; - if ( !pPars->fNotVerbose ) + int iObj = Gia_ObjId( p->pFrames, Gia_ManCo(p->pFrames, (f+k) * Gia_ManPoNum(pGia) + i) ); + int iLit = Abc_Var2Lit( Vec_IntEntry(&p->vFr2Sat, iObj), 0 ); + if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut ) + break; + status = Bmcs_ManPerform_Solve( p, iLit, WorkerThread, ThData, pPars->nProcs, &Solver ); + if ( status == SATOKO_UNSAT ) { - int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); - Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs). ", - nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Gia_ManPoNum(pGia) ); - fflush( stdout ); + if ( i == Gia_ManPoNum(pGia)-1 ) + Bmcs_ManPrintFrame( p, f+k, nClauses, Solver, clkStart ); + if( pPars->pFuncOnFrameDone ) + pPars->pFuncOnFrameDone(f+k, i, 0); + continue; } - if( pPars->pFuncOnFrameDone ) - pPars->pFuncOnFrameDone(f, i, 1); + if ( status == SATOKO_SAT ) + { + RetValue = 0; + pPars->iFrame = f+k; + pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, Solver ); + pPars->nFailOuts++; + if ( !pPars->fNotVerbose ) + { + int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); + Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs). ", + nOutDigits, i, f+k, nOutDigits, pPars->nFailOuts, nOutDigits, Gia_ManPoNum(pGia) ); + fflush( stdout ); + } + if( pPars->pFuncOnFrameDone ) + pPars->pFuncOnFrameDone(f+k, i, 1); + } + break; } - break; + if ( i < Gia_ManPoNum(pGia) || f+k == pPars->nFramesMax-1 ) + break; } - if ( i < Gia_ManPoNum(pGia) ) + if ( k < pPars->nFramesAdd ) break; } // stop threads @@ -822,7 +837,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) } Bmcs_ManStop( p ); if ( RetValue == -1 && !pPars->fNotVerbose ) - printf( "No output failed in %d frames. ", f ); + printf( "No output failed in %d frames. ", f + (k < pPars->nFramesAdd ? k+1 : 0) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); return RetValue; } -- cgit v1.2.3