diff options
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 24 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 49 |
3 files changed, 61 insertions, 13 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 18544a73..0efc263b 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1293,6 +1293,7 @@ extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ); extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo ); extern Gia_Man_t * Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value ); extern Gia_Man_t * Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int Value ); extern Gia_Man_t * Gia_ManDupMux( int iVar, Gia_Man_t * pCof1, Gia_Man_t * pCof0 ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 988d50a2..e05380d5 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1556,6 +1556,30 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) ); return pNew; } +Gia_Man_t * Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + assert( iPo >= 0 && iPo < Gia_ManPoNum(p) ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachCo( p, pObj, i ) + if ( !Gia_ObjIsPo(p, pObj) || i == iPo ) + Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + if ( !Gia_ObjIsPo(p, pObj) || i == iPo ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} /**Function************************************************************* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 17e255b8..96432812 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -45764,11 +45764,6 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } */ - if ( Gia_ManPoNum(pAbc->pGia) > 1 ) - { - Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" ); - return 0; - } if ( pPars->nFramesMax < 0 ) { Abc_Print( 1, "The number of starting frames should be a positive integer.\n" ); @@ -45779,14 +45774,42 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" ); return 0; } - if ( fNewAlgo ) - pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars ); - else - pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, 0 ); - pAbc->nFrames = pPars->iFrame; - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); - if ( pLogFileName ) - Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&gla" ); + if ( Gia_ManPoNum(pAbc->pGia) == 1 ) + { + if ( fNewAlgo ) + pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars ); + else + pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, 0 ); + pAbc->nFrames = pPars->iFrame; + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + if ( pLogFileName ) + Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&gla" ); + } + else // iterate over outputs + { + Gia_Obj_t * pObj; int o, Status; + Vec_Ptr_t * vSeqModelVec = Vec_PtrStart( Gia_ManPoNum(pAbc->pGia) ); + Vec_Int_t * vStatuses = Vec_IntAlloc( Gia_ManPoNum(pAbc->pGia) ); + Gia_ManForEachPo( pAbc->pGia, pObj, o ) + { + Gia_Man_t * pOne = Gia_ManDupDfsOnePo( pAbc->pGia, o ); + if ( fNewAlgo ) + Status = Gia_ManPerformGla( pOne, pPars ); + else + Status = Gia_ManPerformGlaOld( pOne, pPars, 0 ); + Vec_IntPush( vStatuses, Status ); + if ( pLogFileName ) + Abc_NtkWriteLogFile( pLogFileName, pOne->pCexSeq, Status, pPars->iFrame, "&gla" ); + if ( pOne->pCexSeq ) + Vec_PtrWriteEntry( vSeqModelVec, o, pOne->pCexSeq ); + pOne->pCexSeq = NULL; + Gia_ManStop( pOne ); + } + assert( Vec_IntSize(vStatuses) == Gia_ManPoNum(pAbc->pGia) ); + Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec ); + Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); + pAbc->nFrames = -1; + } return 0; usage: |