From 5a10c8ad01b62a6760e4cf8720800acb1fab8554 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 16 Nov 2014 23:27:21 -0800 Subject: Integrating mfs2 package to work with boxes. --- src/aig/gia/gia.h | 5 + src/aig/gia/giaDup.c | 32 ++++ src/aig/gia/giaFadds.c | 2 +- src/aig/gia/giaMan.c | 1 + src/aig/gia/giaMfs.c | 487 +++++++++++++++++++++++++------------------------ src/aig/gia/giaTim.c | 52 +++++- 6 files changed, 336 insertions(+), 243 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 8c6c2fb4..3c5d3569 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -483,6 +483,7 @@ static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj), iLit); } static inline int Gia_ObjCopyArray( Gia_Man_t * p, int iObj ) { return Vec_IntEntry(&p->vCopies, iObj); } static inline void Gia_ObjSetCopyArray( Gia_Man_t * p, int iObj, int iLit ) { Vec_IntWriteEntry(&p->vCopies, iObj, iLit); } +static inline void Gia_ManCleanCopyArray( Gia_Man_t * p ) { Vec_IntFill( &p->vCopies, Gia_ManObjNum(p), -1 ); } static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } @@ -1088,6 +1089,7 @@ extern Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop ); extern Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres ); +extern Gia_Man_t * Gia_ManDupSelectedOutputs( Gia_Man_t * p, Vec_Int_t * vOutsLeft ); extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis ); extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ); @@ -1345,6 +1347,7 @@ extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, extern Vec_Int_t * Gia_ManComputeSwitchProbs( Gia_Man_t * pGia, int nFrames, int nPref, int fProbOne ); extern Vec_Flt_t * Gia_ManPrintOutputProb( Gia_Man_t * p ); /*=== giaTim.c ===========================================================*/ +extern int Gia_ManBoxNum( Gia_Man_t * p ); extern int Gia_ManIsSeqWithBoxes( Gia_Man_t * p ); extern int Gia_ManIsNormalized( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p ); @@ -1353,7 +1356,9 @@ extern Gia_Man_t * Gia_ManDupUnshuffleInputs( Gia_Man_t * p ); extern int Gia_ManLevelWithBoxes( Gia_Man_t * p ); extern int Gia_ManLutLevelWithBoxes( Gia_Man_t * p ); extern void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres ); +extern void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBoxesLeft ); extern Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres ); +extern Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxesLeft ); extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres ); extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit, char * pFileSpec ); /*=== giaTruth.c ===========================================================*/ diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 0e1028e8..5d7a6cb3 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -252,6 +252,38 @@ Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupSelectedOutputs( Gia_Man_t * p, Vec_Int_t * vOutsLeft ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i, iOut; + assert( Gia_ManRegNum(p) == 0 ); + assert( Gia_ManPoNum(p) >= Vec_IntSize(vOutsLeft) ); + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Vec_IntForEachEntry( vOutsLeft, iOut, i ) + Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(Gia_ManPo(p, iOut)) ); + Vec_IntForEachEntry( vOutsLeft, iOut, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, iOut)) ); + return pNew; +} + /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] diff --git a/src/aig/gia/giaFadds.c b/src/aig/gia/giaFadds.c index 4e913687..7b463f42 100644 --- a/src/aig/gia/giaFadds.c +++ b/src/aig/gia/giaFadds.c @@ -538,7 +538,7 @@ Tim_Man_t * Gia_ManGenerateTim( int nPis, int nPos, int nBoxes, int nIns, int nO curPo = 0; for ( i = 0; i < nBoxes; i++ ) { - Tim_ManCreateBox( pMan, curPo, nIns, curPi, nOuts, -1 ); + Tim_ManCreateBox( pMan, curPo, nIns, curPi, nOuts, 0 ); curPi += nOuts; curPo += nIns; } diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 9fbf5844..31b7490c 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -105,6 +105,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vBarBufs ); Vec_IntFreeP( &p->vLevels ); Vec_IntFreeP( &p->vTruths ); + Vec_IntErase( &p->vCopies ); Vec_IntFreeP( &p->vTtNums ); Vec_IntFreeP( &p->vTtNodes ); Vec_WrdFreeP( &p->vTtMemory ); diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index 4f6e74a1..afd6bbd7 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -19,22 +19,15 @@ ***********************************************************************/ #include "gia.h" -#include "bool/kit/kit.h" #include "opt/sfm/sfm.h" #include "misc/tim/tim.h" ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static word s_ElemVar = ABC_CONST(0xAAAAAAAAAAAAAAAA); -static word s_ElemVar2 = ABC_CONST(0xCCCCCCCCCCCCCCCC); - -extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -50,204 +43,139 @@ extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_I SeeAlso [] ***********************************************************************/ -void Gia_ManExtractMfs_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vId2Mfs, Vec_Wec_t * vFanins, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths, Vec_Wrd_t * vTruthsTemp ) +Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) { + Gia_Obj_t * pObj, * pObjExtra; + Vec_Wec_t * vFanins; // mfs data + Vec_Str_t * vFixed; // mfs data + Vec_Str_t * vEmpty; // mfs data + Vec_Wrd_t * vTruths; // mfs data Vec_Int_t * vArray; - int i, Fanin; - Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); - assert( Gia_ObjIsLut(p, iObj) ); - if ( !~pObj->Value ) - return; - Gia_LutForEachFanin( p, iObj, Fanin, i ) - Gia_ManExtractMfs_rec( p, Fanin, vId2Mfs, vFanins, vFixed, vTruths, vTruthsTemp ); - pObj->Value = Vec_WecSize(vFanins); - vArray = Vec_WecPushLevel( vFanins ); - Vec_IntGrow( vArray, Gia_ObjLutSize(p, iObj) ); - Gia_LutForEachFanin( p, iObj, Fanin, i ) - Vec_IntPush( vArray, Gia_ManObj(p, Fanin)->Value ); - Vec_StrPush( vFixed, (char)0 ); - Vec_WrdPush( vTruths, Gia_ObjComputeTruthTable6Lut(p, iObj, vTruthsTemp) ); - Vec_IntWriteEntry( vId2Mfs, iObj, pObj->Value ); -} -void Gia_ManExtractMfs_rec2( Gia_Man_t * p, int iObj, Vec_Int_t * vId2Mfs, Vec_Wec_t * vFanins, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths ) -{ - Vec_Int_t * vArray; - Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) - return; - Gia_ObjSetTravIdCurrent(p, pObj); - assert( Gia_ObjIsAnd(pObj) ); - Gia_ManExtractMfs_rec2( p, Gia_ObjFaninId0(pObj, iObj), vId2Mfs, vFanins, vFixed, vTruths ); - Gia_ManExtractMfs_rec2( p, Gia_ObjFaninId1(pObj, iObj), vId2Mfs, vFanins, vFixed, vTruths ); - pObj->Value = Vec_WecSize(vFanins); - vArray = Vec_WecPushLevel( vFanins ); - Vec_IntGrow( vArray, 2 ); - Vec_IntPush( vArray, Gia_ObjFanin0(pObj)->Value ); - Vec_IntPush( vArray, Gia_ObjFanin1(pObj)->Value ); - Vec_StrPush( vFixed, (char)1 ); - Vec_WrdPush( vTruths, (Gia_ObjFaninC0(pObj) ? ~s_ElemVar : s_ElemVar) & (Gia_ObjFaninC1(pObj) ? ~s_ElemVar2 : s_ElemVar2) ); - Vec_IntWriteEntry( vId2Mfs, iObj, pObj->Value ); -} -Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t ** pvId2Mfs ) -{ + Vec_Int_t * vLeaves; + word uTruth, uTruthVar = ABC_CONST(0xAAAAAAAAAAAAAAAA); Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; - Vec_Int_t * vPoNodes; - Vec_Int_t * vId2Mfs; - Vec_Wec_t * vFanins; - Vec_Str_t * vFixed; - Vec_Wrd_t * vTruths, * vTruthsTemp; - Vec_Int_t * vArray; - Gia_Obj_t * pObj, * pObjBox; - int i, k, nRealPis, nRealPos, nPiNum, nPoNum, curCi, curCo; - assert( pManTime == NULL || Tim_ManCiNum(pManTime) == Gia_ManCiNum(p) ); - assert( pManTime == NULL || Tim_ManCoNum(pManTime) == Gia_ManCoNum(p) ); - // get the real number of PIs and POs - nRealPis = pManTime ? Tim_ManPiNum(pManTime) : Gia_ManCiNum(p); - nRealPos = pManTime ? Tim_ManPoNum(pManTime) : Gia_ManCoNum(p); - // create mapping from GIA into MFS - vId2Mfs = Vec_IntStartFull( Gia_ManObjNum(p) ); - // collect PO nodes - vPoNodes = Vec_IntAlloc( 1000 ); - // create the arrays - vFanins = Vec_WecAlloc( 1000 ); - vFixed = Vec_StrAlloc( 1000 ); - vTruths = Vec_WrdAlloc( 1000 ); - vTruthsTemp = Vec_WrdStart( Gia_ManObjNum(p) ); - // assign MFS ids to primary inputs - Gia_ManFillValue( p ); - for ( i = 0; i < nRealPis; i++ ) + int nBoxes = Gia_ManBoxNum(p); + int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p); + int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p); + int i, k, curCi, curCo, nBoxIns, nBoxOuts; + int Id, iFan, nMfsVars, Counter = 0; + assert( !p->pAigExtra || Gia_ManPiNum(p->pAigExtra) <= 6 ); + // prepare storage + nMfsVars = Gia_ManCiNum(p) + 1 + Gia_ManLutNum(p) + Gia_ManCoNum(p); + vFanins = Vec_WecStart( nMfsVars ); + vFixed = Vec_StrStart( nMfsVars ); + vEmpty = Vec_StrStart( nMfsVars ); + vTruths = Vec_WrdStart( nMfsVars ); + // set internal PIs + Gia_ManCleanCopyArray( p ); + Gia_ManForEachCiId( p, Id, i ) + Gia_ObjSetCopyArray( p, Id, Counter++ ); + // set constant node + Vec_StrWriteEntry( vFixed, Counter, (char)1 ); + Vec_WrdWriteEntry( vTruths, Counter, (word)0 ); + Gia_ObjSetCopyArray( p, 0, Counter++ ); + // set internal LUTs + vLeaves = Vec_IntAlloc( 6 ); + Gia_ObjComputeTruthTableStart( p, 6 ); + Gia_ManForEachLut( p, Id ) { - pObj = Gia_ManPi( p, i ); - pObj->Value = Vec_WecSize(vFanins); - Vec_WecPushLevel( vFanins ); - Vec_StrPush( vFixed, (char)0 ); - Vec_WrdPush( vTruths, (word)0 ); - Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value ); - } - // assign MFS ids to black box outputs - curCi = nRealPis; - curCo = 0; - if ( pManTime ) - for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ ) - { - if ( !Tim_ManBoxIsBlack(pManTime, i) ) + Vec_IntClear( vLeaves ); + vArray = Vec_WecEntry( vFanins, Counter ); + Vec_IntGrow( vArray, Gia_ObjLutSize(p, Id) ); + Gia_LutForEachFanin( p, Id, iFan, k ) { - // collect POs - for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ ) - { - pObj = Gia_ManPo( p, curCo + k ); - Vec_IntPush( vPoNodes, Gia_ObjId(p, pObj) ); - } - // assign values to the PIs - for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ ) - { - pObj = Gia_ManPi( p, curCi + k ); - pObj->Value = Vec_WecSize(vFanins); - Vec_WecPushLevel( vFanins ); - Vec_StrPush( vFixed, (char)1 ); - Vec_WrdPush( vTruths, (word)0 ); - Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value ); - } + assert( Gia_ObjCopyArray(p, iFan) >= 0 ); + Vec_IntPush( vArray, Gia_ObjCopyArray(p, iFan) ); + Vec_IntPush( vLeaves, iFan ); } - curCo += Tim_ManBoxInputNum(pManTime, i); - curCi += Tim_ManBoxOutputNum(pManTime, i); + assert( Vec_IntSize(vLeaves) <= 6 ); + assert( Vec_IntSize(vLeaves) == Gia_ObjLutSize(p, Id) ); + uTruth = *Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves ); + Vec_WrdWriteEntry( vTruths, Counter, uTruth ); + Gia_ObjSetCopyArray( p, Id, Counter++ ); } - // collect POs -// for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ ) - for ( i = Gia_ManCoNum(p) - nRealPos; i < Gia_ManCoNum(p); i++ ) - { - pObj = Gia_ManPo( p, i ); - Vec_IntPush( vPoNodes, Gia_ObjId(p, pObj) ); - } - curCo += nRealPos; - // verify counts - assert( curCi == Gia_ManPiNum(p) ); - assert( curCo == Gia_ManPoNum(p) ); - // remeber the end of PIs - nPiNum = Vec_WecSize(vFanins); - nPoNum = Vec_IntSize(vPoNodes); - // assign value to constant node - pObj = Gia_ManConst0(p); - Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), Vec_WecSize(vFanins) ); - pObj->Value = Vec_WecSize(vFanins); - Vec_WecPushLevel( vFanins ); - Vec_StrPush( vFixed, (char)0 ); - Vec_WrdPush( vTruths, (word)0 ); - Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value ); - // create internal nodes - curCi = nRealPis; - curCo = 0; - if ( pManTime ) - for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ ) + Gia_ObjComputeTruthTableStop( p ); + // set all POs + Gia_ManForEachCo( p, pObj, i ) { - // recursively add for box inputs - Gia_ManIncrementTravId( pBoxes ); - for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ ) + iFan = Gia_ObjFaninId0p( p, pObj ); + assert( Gia_ObjCopyArray(p, iFan) >= 0 ); + vArray = Vec_WecEntry( vFanins, Counter ); + Vec_IntFill( vArray, 1, Gia_ObjCopyArray(p, iFan) ); + if ( i < Gia_ManCoNum(p) - nRealPos ) // internal PO { - // build logic - pObj = Gia_ManPo( p, curCo + k ); - Gia_ManExtractMfs_rec( p, Gia_ObjFaninId0p(p, pObj), vId2Mfs, vFanins, vFixed, vTruths, vTruthsTemp ); - // add buffer/inverter - pObj->Value = Vec_WecSize(vFanins); - vArray = Vec_WecPushLevel( vFanins ); - Vec_IntGrow( vArray, 1 ); - assert( !~Gia_ObjFanin0(pObj)->Value ); - Vec_IntPush( vArray, Gia_ObjFanin0(pObj)->Value ); - Vec_StrPush( vFixed, (char)0 ); - Vec_WrdPush( vTruths, Gia_ObjFaninC0(pObj) ? ~s_ElemVar : s_ElemVar ); - Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value ); - // transfer to the PI - pObjBox = Gia_ManPi( pBoxes, k ); - pObjBox->Value = pObj->Value; - Gia_ObjSetTravIdCurrent( pBoxes, pObjBox ); + Vec_StrWriteEntry( vFixed, Counter, (char)1 ); + Vec_StrWriteEntry( vEmpty, Counter, (char)1 ); + uTruth = Gia_ObjFaninC0(pObj) ? ~uTruthVar: uTruthVar; + Vec_WrdWriteEntry( vTruths, Counter, uTruth ); } - if ( !Tim_ManBoxIsBlack(pManTime, i) ) + Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), Counter++ ); + } + assert( Counter == nMfsVars ); + // add functions of the boxes + if ( p->pAigExtra ) + { + Gia_ObjComputeTruthTableStart( p->pAigExtra, 6 ); + curCi = nRealPis; + curCo = 0; + for ( i = 0; i < nBoxes; i++ ) { - pObjBox = Gia_ManConst0(pBoxes); - pObjBox->Value = Vec_WecSize(vFanins); - Vec_WecPushLevel( vFanins ); - Vec_StrPush( vFixed, (char)0 ); - Vec_WrdPush( vTruths, (word)0 ); - Gia_ObjSetTravIdCurrent( pBoxes, pObjBox ); - // add internal nodes and transfer - for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ ) + assert( !Tim_ManBoxIsBlack(pManTime, i) ); + nBoxIns = Tim_ManBoxInputNum( pManTime, i ); + nBoxOuts = Tim_ManBoxOutputNum( pManTime, i ); + // collect truth table leaves + Vec_IntClear( vLeaves ); + for ( k = 0; k < nBoxIns; k++ ) + Vec_IntPush( vLeaves, Gia_ObjId(p->pAigExtra, Gia_ManCi(p->pAigExtra, k)) ); + // iterate through box outputs + for ( k = 0; k < nBoxOuts; k++ ) { - // build logic - pObjBox = Gia_ManPo( pBoxes, curCi - Tim_ManPiNum(pManTime) + k ); - Gia_ManExtractMfs_rec2( pBoxes, Gia_ObjFaninId0p(pBoxes, pObjBox), vId2Mfs, vFanins, vFixed, vTruths ); - // add buffer/inverter - vArray = Vec_WecPushLevel( vFanins ); - Vec_IntGrow( vArray, 1 ); - assert( !~Gia_ObjFanin0(pObjBox)->Value ); - Vec_IntPush( vArray, Gia_ObjFanin0(pObjBox)->Value ); - Vec_StrPush( vFixed, (char)1 ); - Vec_WrdPush( vTruths, Gia_ObjFaninC0(pObjBox) ? ~s_ElemVar : s_ElemVar ); - // transfer to the PI - pObj = Gia_ManPi( p, curCi + k ); - pObj->Value = pObjBox->Value; + // CI corresponding to the box outputs + pObj = Gia_ManCi( p, curCi + k ); + Counter = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) ); + //printf( "%d ", Counter ); + // box output in the extra manager + pObjExtra = Gia_ManCo( p->pAigExtra, curCi - nRealPis + k ); + // compute truth table + if ( Gia_ObjFaninId0p(p->pAigExtra, pObjExtra) == 0 ) + uTruth = 0; + else + uTruth = *Gia_ObjComputeTruthTableCut( p->pAigExtra, Gia_ObjFanin0(pObjExtra), vLeaves ); + uTruth = Gia_ObjFaninC0(pObjExtra) ? ~uTruth : uTruth; + Vec_WrdWriteEntry( vTruths, Counter, uTruth ); + // add box inputs (POs of the AIG) as fanins + vArray = Vec_WecEntry( vFanins, Counter ); + Vec_IntGrow( vArray, nBoxIns ); + for ( k = 0; k < nBoxIns; k++ ) + { + iFan = Gia_ObjId( p, Gia_ManCo(p, curCo + k) ); + assert( Gia_ObjCopyArray(p, iFan) >= 0 ); + Vec_IntPush( vArray, Gia_ObjCopyArray(p, iFan) ); + } + Vec_StrWriteEntry( vFixed, Counter, (char)1 ); } + // set internal POs pointing directly to internal PIs as no-delay + for ( k = 0; k < nBoxIns; k++ ) + { + pObj = Gia_ManCo( p, curCo + k ); + if ( !Gia_ObjIsCi( Gia_ObjFanin0(pObj) ) ) + continue; + Counter = Gia_ObjCopyArray( p, Gia_ObjFaninId0p(p, pObj) ); + Vec_StrWriteEntry( vEmpty, Counter, (char)1 ); + } + curCo += nBoxIns; + curCi += nBoxOuts; } - curCo += Tim_ManBoxInputNum(pManTime, i); - curCi += Tim_ManBoxOutputNum(pManTime, i); - } - // create POs with buffers - Gia_ManForEachObjVec( vPoNodes, p, pObj, i ) - { - Gia_ManExtractMfs_rec( p, Gia_ObjFaninId0p(p, pObj), vId2Mfs, vFanins, vFixed, vTruths, vTruthsTemp ); - pObj->Value = Vec_WecSize(vFanins); - // add buffer/inverter - vArray = Vec_WecPushLevel( vFanins ); - Vec_IntGrow( vArray, 1 ); - assert( !~Gia_ObjFanin0(pObj)->Value ); - Vec_IntPush( vArray, Gia_ObjFanin0(pObj)->Value ); - Vec_StrPush( vFixed, (char)0 ); - Vec_WrdPush( vTruths, Gia_ObjFaninC0(pObj) ? ~s_ElemVar : s_ElemVar ); - Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value ); + curCo += nRealPos; + Gia_ObjComputeTruthTableStop( p->pAigExtra ); + // verify counts + assert( curCi == Gia_ManCiNum(p) ); + assert( curCo == Gia_ManCoNum(p) ); + assert( curCi - nRealPis == Gia_ManCoNum(p->pAigExtra) ); } - Vec_IntFree( vPoNodes ); - Vec_WrdFree( vTruthsTemp ); - *pvId2Mfs = vId2Mfs; - return Sfm_NtkConstruct( vFanins, nPiNum, nPoNum, vFixed, NULL, vTruths ); + // finalize + Vec_IntFree( vLeaves ); + return Sfm_NtkConstruct( vFanins, nRealPis, nRealPos, vFixed, vEmpty, vTruths ); } /**Function************************************************************* @@ -261,72 +189,159 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t ** p SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, Vec_Int_t * vId2Mfs ) +Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk ) { - Gia_Man_t * pNew; - Gia_Obj_t * pObj; - Vec_Int_t * vMfsTopo, * vMfs2New, * vArray, * vCover; - int i, k, Fanin, iMfsId, iLitNew; - word * pTruth; - // collect MFS nodes in the topo order - vMfsTopo = Sfm_NtkDfs( pNtk ); - // create mapping from MFS to new GIA literals - vMfs2New = Vec_IntStartFull( Vec_IntCap(vMfsTopo) ); + extern int Gia_ManFromIfLogicCreateLut( Gia_Man_t * pNew, word * pRes, Vec_Int_t * vLeaves, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2 ); + Gia_Man_t * pNew; Gia_Obj_t * pObj; + Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; + int nBoxes = Gia_ManBoxNum(p); + int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p); + int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p); + int i, k, Id, curCi, curCo, nBoxIns, nBoxOuts, iLitNew, iMfsId, iGroup, Fanin; + int nMfsNodes = 1 + Gia_ManCiNum(p) + Gia_ManLutNum(p) + Gia_ManCoNum(p); + word * pTruth, uTruthVar = ABC_CONST(0xAAAAAAAAAAAAAAAA); + Vec_Wec_t * vGroups = Vec_WecStart( nBoxes ); + Vec_Int_t * vMfs2Gia = Vec_IntStartFull( nMfsNodes ); + Vec_Int_t * vGroupMap = Vec_IntStartFull( nMfsNodes ); + Vec_Int_t * vMfsTopo, * vCover, * vBoxesLeft; + Vec_Int_t * vArray, * vLeaves; + Vec_Int_t * vMapping, * vMapping2; + // collect nodes + curCi = nRealPis; + curCo = 0; + for ( i = 0; i < nBoxes; i++ ) + { + nBoxIns = Tim_ManBoxInputNum( pManTime, i ); + nBoxOuts = Tim_ManBoxOutputNum( pManTime, i ); + vArray = Vec_WecEntry( vGroups, i ); + for ( k = 0; k < nBoxIns; k++ ) + { + pObj = Gia_ManCo( p, curCo + k ); + iMfsId = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) ); + assert( iMfsId > 0 ); + Vec_IntPush( vArray, iMfsId ); + Vec_IntWriteEntry( vGroupMap, iMfsId, Abc_Var2Lit(i,0) ); + } + for ( k = 0; k < nBoxOuts; k++ ) + { + pObj = Gia_ManCi( p, curCi + k ); + iMfsId = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) ); + assert( iMfsId > 0 ); + Vec_IntPush( vArray, iMfsId ); + Vec_IntWriteEntry( vGroupMap, iMfsId, Abc_Var2Lit(i,1) ); + } + curCo += nBoxIns; + curCi += nBoxOuts; + } + curCo += nRealPos; + assert( curCi == Gia_ManCiNum(p) ); + assert( curCo == Gia_ManCoNum(p) ); + + // collect nodes in the given order + vBoxesLeft = Vec_IntAlloc( nBoxes ); + vMfsTopo = Sfm_NtkDfs( pNtk, vGroups, vGroupMap, vBoxesLeft ); + assert( Vec_IntSize(vBoxesLeft) <= nBoxes ); + assert( Vec_IntSize(vMfsTopo) > 0 ); + // start new GIA pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + + // start mapping + vMapping = Vec_IntStart( Gia_ManObjNum(p) ); + vMapping2 = Vec_IntStart( 1 ); + // create const LUT + Vec_IntWriteEntry( vMapping, 0, Vec_IntSize(vMapping2) ); + Vec_IntPush( vMapping2, 0 ); + Vec_IntPush( vMapping2, 0 ); + + // map constant + Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, 0), 0 ); // map primary inputs - Gia_ManForEachCi( p, pObj, i ) - { - iMfsId = Vec_IntEntry( vId2Mfs, Gia_ObjId(p, pObj) ); - assert( iMfsId >= 0 ); - Vec_IntWriteEntry( vMfs2New, iMfsId, Gia_ManAppendCi(pNew) ); - } + Gia_ManForEachCiId( p, Id, i ) + if ( i < nRealPis ) + Vec_IntWriteEntry( vMfs2Gia, Gia_ObjCopyArray(p, Id), Gia_ManAppendCi(pNew) ); // map internal nodes + vLeaves = Vec_IntAlloc( 6 ); vCover = Vec_IntAlloc( 1 << 16 ); Vec_IntForEachEntry( vMfsTopo, iMfsId, i ) { - assert( Sfm_NodeReadUsed(pNtk, iMfsId) ); pTruth = Sfm_NodeReadTruth( pNtk, iMfsId ); - if ( pTruth[0] == 0 || ~pTruth[0] == 0 ) - { - Vec_IntWriteEntry( vMfs2New, iMfsId, 0 ); - continue; - } + iGroup = Vec_IntEntry( vGroupMap, iMfsId ); vArray = Sfm_NodeReadFanins( pNtk, iMfsId ); // belongs to pNtk + Vec_IntClear( vLeaves ); Vec_IntForEachEntry( vArray, Fanin, k ) { - iLitNew = Vec_IntEntry( vMfs2New, Fanin ); - assert( iLitNew >= 0 ); - Vec_IntWriteEntry( vArray, k, iLitNew ); + iLitNew = Vec_IntEntry( vMfs2Gia, Fanin ); assert( iLitNew >= 0 ); + Vec_IntPush( vLeaves, iLitNew ); + } + if ( iGroup == -1 ) // internal node + { + assert( Sfm_NodeReadUsed(pNtk, iMfsId) ); + iLitNew = Gia_ManFromIfLogicCreateLut( pNew, pTruth, vLeaves, vCover, vMapping, vMapping2 ); } - // derive new function - iLitNew = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vArray), vCover, vArray, 0 ); - Vec_IntWriteEntry( vMfs2New, iMfsId, iLitNew ); + else if ( Abc_LitIsCompl(iGroup) ) // internal CI + iLitNew = Gia_ManAppendCi( pNew ); + else // internal CO + { + iLitNew = Gia_ManAppendCo( pNew, Abc_LitNotCond(Vec_IntEntry(vLeaves, 0), pTruth[0] == ~uTruthVar) ); + //printf("Group = %d. po = %d\n", iGroup>>1, iMfsId ); + } + Vec_IntWriteEntry( vMfs2Gia, iMfsId, iLitNew ); } Vec_IntFree( vCover ); - // map output nodes + Vec_IntFree( vLeaves ); + + // map primary outputs Gia_ManForEachCo( p, pObj, i ) { - iMfsId = Vec_IntEntry( vId2Mfs, Gia_ObjId(p, pObj) ); - assert( iMfsId >= 0 ); - vArray = Sfm_NodeReadFanins( pNtk, iMfsId ); // belongs to pNtk - assert( Vec_IntSize(vArray) == 1 ); - // get the fanin - iLitNew = Vec_IntEntry( vMfs2New, Vec_IntEntry(vArray, 0) ); + if ( i < Gia_ManCoNum(p) - nRealPos ) // internal COs + { + iMfsId = Gia_ObjCopyArray( p, Gia_ObjId(p, pObj) ); + iGroup = Vec_IntEntry( vGroupMap, iMfsId ); + if ( Vec_IntFind(vMfsTopo, iGroup) >= 0 ) + { + iLitNew = Vec_IntEntry( vMfs2Gia, iMfsId ); + assert( iLitNew >= 0 ); + } + continue; + } + iLitNew = Vec_IntEntry( vMfs2Gia, Gia_ObjCopyArray(p, Gia_ObjFaninId0p(p, pObj)) ); assert( iLitNew >= 0 ); - // create CO - pTruth = Sfm_NodeReadTruth( pNtk, iMfsId ); - assert( pTruth[0] == s_ElemVar || ~pTruth[0] == s_ElemVar ); - Gia_ManAppendCo( pNew, Abc_LitNotCond(iLitNew, (int)(pTruth[0] != s_ElemVar)) ); + Gia_ManAppendCo( pNew, Abc_LitNotCond(iLitNew, Gia_ObjFaninC0(pObj)) ); } - Vec_IntFree( vMfs2New ); + + // finish mapping + if ( Vec_IntSize(vMapping) > Gia_ManObjNum(pNew) ) + Vec_IntShrink( vMapping, Gia_ManObjNum(pNew) ); + else + Vec_IntFillExtra( vMapping, Gia_ManObjNum(pNew), 0 ); + assert( Vec_IntSize(vMapping) == Gia_ManObjNum(pNew) ); + Vec_IntForEachEntry( vMapping, iLitNew, i ) + if ( iLitNew > 0 ) + Vec_IntAddToEntry( vMapping, i, Gia_ManObjNum(pNew) ); + Vec_IntAppend( vMapping, vMapping2 ); + Vec_IntFree( vMapping2 ); + assert( pNew->vMapping == NULL ); + pNew->vMapping = vMapping; + + // create new timing manager and extra AIG + if ( pManTime ) + pNew->pManTime = Gia_ManUpdateTimMan2( p, vBoxesLeft ); + // update extra STG + if ( p->pAigExtra ) + pNew->pAigExtra = Gia_ManUpdateExtraAig2( p->pManTime, p->pAigExtra, vBoxesLeft ); + + // cleanup + Vec_WecFree( vGroups ); Vec_IntFree( vMfsTopo ); + Vec_IntFree( vGroupMap ); + Vec_IntFree( vMfs2Gia ); + Vec_IntFree( vBoxesLeft ); return pNew; } - /**Function************************************************************* Synopsis [] @@ -341,7 +356,6 @@ Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, Vec_Int_t * vId2M Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) { Sfm_Ntk_t * pNtk; - Vec_Int_t * vId2Mfs; Gia_Man_t * pNew; int nFaninMax, nNodes; assert( Gia_ManRegNum(p) == 0 ); @@ -359,32 +373,29 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) return NULL; } // collect information - pNtk = Gia_ManExtractMfs( p, p->pAigExtra, &vId2Mfs ); + pNtk = Gia_ManExtractMfs( p ); // perform optimization nNodes = Sfm_NtkPerform( pNtk, pPars ); - // call the fast extract procedure if ( nNodes == 0 ) { Abc_Print( 1, "The network is not changed by \"&mfs\".\n" ); pNew = Gia_ManDup( p ); pNew->vMapping = Vec_IntDup( p->vMapping ); + Gia_ManTransferTiming( pNew, p ); } else { - pNew = Gia_ManInsertMfs( p, pNtk, vId2Mfs ); + pNew = Gia_ManInsertMfs( p, pNtk ); if( pPars->fVerbose ) Abc_Print( 1, "The network has %d nodes changed by \"&mfs\".\n", nNodes ); } - Vec_IntFree( vId2Mfs ); Sfm_NtkFree( pNtk ); return pNew; } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - ABC_NAMESPACE_IMPL_END diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 156f67b1..c9d55ffc 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -33,6 +33,22 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Returns the number of boxes in the AIG with boxes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManBoxNum( Gia_Man_t * p ) +{ + return p->pManTime ? Tim_ManBoxNum((Tim_Man_t *)p->pManTime) : 0; +} + /**Function************************************************************* Synopsis [Returns one if this is a seq AIG with non-trivial boxes.] @@ -598,9 +614,16 @@ void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres ) { Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; assert( pManTime != NULL ); - assert( Tim_ManBoxNum(pManTime) == Vec_IntSize(vBoxPres) ); + assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) ); return Tim_ManTrim( pManTime, vBoxPres ); } +void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBoxesLeft ) +{ + Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; + assert( pManTime != NULL ); + assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) ); + return Tim_ManReduce( pManTime, vBoxesLeft ); +} /**Function************************************************************* @@ -615,7 +638,7 @@ void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres ) ***********************************************************************/ Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxPres ) { - Gia_Man_t * pNew = NULL; + Gia_Man_t * pNew; Tim_Man_t * pManTime = (Tim_Man_t *)pTime; Vec_Int_t * vOutPres = Vec_IntAlloc( 100 ); int i, k, curPo = 0; @@ -628,11 +651,32 @@ Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * p, Vec_Int_t * vBox curPo += Tim_ManBoxOutputNum(pManTime, i); } assert( curPo == Gia_ManCoNum(p) ); -// if ( Vec_IntSize(vOutPres) > 0 ) - pNew = Gia_ManDupOutputVec( p, vOutPres ); + pNew = Gia_ManDupOutputVec( p, vOutPres ); Vec_IntFree( vOutPres ); return pNew; } +Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxesLeft ) +{ + Gia_Man_t * pNew; + Tim_Man_t * pManTime = (Tim_Man_t *)pTime; + int nRealPis = Tim_ManPiNum(pManTime); + Vec_Int_t * vOutsLeft; + int i, k, iBox, iOutFirst; + if ( Vec_IntSize(vBoxesLeft) == Tim_ManBoxNum(pManTime) ) + return Gia_ManDup( p ); + assert( Vec_IntSize(vBoxesLeft) < Tim_ManBoxNum(pManTime) ); + assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - nRealPis ); + vOutsLeft = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vBoxesLeft, iBox, i ) + { + iOutFirst = Tim_ManBoxOutputFirst(pManTime, iBox) - nRealPis; + for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, iBox); k++ ) + Vec_IntPush( vOutsLeft, iOutFirst + k ); + } + pNew = Gia_ManDupSelectedOutputs( p, vOutsLeft ); + Vec_IntFree( vOutsLeft ); + return pNew; +} /**Function************************************************************* -- cgit v1.2.3