diff options
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigBmc.c | 94 | ||||
-rw-r--r-- | src/aig/saig/saigInter.c | 8 |
3 files changed, 101 insertions, 3 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index f0eb7099..b9b7de40 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -76,7 +76,7 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /*=== saigBmc.c ==========================================================*/ -extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose, int * piFrame ); +extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame ); /*=== saigCone.c ==========================================================*/ extern void Saig_ManPrintCones( Aig_Man_t * p ); /*=== saigInter.c ==========================================================*/ diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 3a6aa611..f6a42c8b 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -82,6 +82,90 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) /**Function************************************************************* + Synopsis [Returns the number of internal nodes that are not counted yet.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + if ( !Aig_ObjIsNode(pObj) ) + return 0; + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return 0; + Aig_ObjSetTravIdCurrent(p, pObj); + return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + + Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Create timeframes of the manager for BMC.] + + Description [The resulting manager is combinational. The primary inputs + corresponding to register outputs are ordered first. POs correspond to + the property outputs in each time-frame. + The unrolling is stopped as soon as the number of nodes in the frames + exceeds the given maximum size.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax ) +{ + Aig_Man_t * pFrames; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo; + int i, f, Counter = 0; + assert( Saig_ManRegNum(pAig) > 0 ); + pFrames = Aig_ManStart( nSizeMax ); + Aig_ManIncrementTravId( pFrames ); + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); + // create variables for register outputs + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_ManConst0( pFrames ); + // add timeframes + Counter = 0; + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + { + pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) ); + if ( Counter >= nSizeMax ) + { + Aig_ManCleanup( pFrames ); + return pFrames; + } + } + if ( f == nFrames - 1 ) + break; + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Aig_ObjChild0Copy(pObj); + // transfer to register outputs + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + pObjLo->pData = pObjLi->pData; + } + Aig_ManCleanup( pFrames ); + return pFrames; +} + +/**Function************************************************************* + Synopsis [Performs BMC for the given AIG.] Description [] @@ -91,7 +175,7 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) SeeAlso [] ***********************************************************************/ -int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) +int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame ) { sat_solver * pSat; Cnf_Dat_t * pCnf; @@ -101,7 +185,13 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fRewri *piFrame = -1; // derive the timeframes clk = clock(); - pFrames = Saig_ManFramesBmc( pAig, nFrames ); + if ( nSizeMax > 0 ) + { + pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax ); + nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); + } + else + pFrames = Saig_ManFramesBmc( pAig, nFrames ); if ( fVerbose ) { printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index c3bb0875..3adcc568 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -566,6 +566,14 @@ p->timeCnf += clock() - clk; // iterate the interpolation procedure for ( i = 0; ; i++ ) { + if ( p->nFrames + i >= 100 ) + { + if ( fVerbose ) + printf( "Reached limit (%d) on the number of timeframes.\n", 100 ); + p->timeTotal = clock() - clkTotal; + Saig_ManagerFree( p ); + return -1; + } // perform interplation clk = clock(); RetValue = Saig_PerformOneStep( p ); |