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 +++++- src/base/abc/abcDfs.c | 8 +- src/base/abci/abc.c | 158 ++++++++++++++++ src/base/abci/abcMfs.c | 2 - src/misc/tim/tim.h | 1 + src/misc/tim/timMan.c | 87 +++++++++ src/opt/sfm/sfm.h | 2 +- src/opt/sfm/sfmNtk.c | 3 +- src/opt/sfm/sfmWin.c | 36 +++- 14 files changed, 617 insertions(+), 259 deletions(-) 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************************************************************* diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index caeacb8e..4508f334 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -1460,8 +1460,6 @@ int Abc_NtkIsAcyclicWithBoxes_rec( Abc_Obj_t * pNode ) Abc_Obj_t * pFanin; int fAcyclic, i; assert( !Abc_ObjIsNet(pNode) ); - if ( Abc_ObjIsBo(pNode) ) - pNode = Abc_ObjFanin0(pNode); if ( Abc_ObjIsPi(pNode) || Abc_ObjIsLatch(pNode) || Abc_ObjIsBlackbox(pNode) ) return 1; assert( Abc_ObjIsNode(pNode) || Abc_ObjIsBox(pNode) ); @@ -1485,8 +1483,6 @@ int Abc_NtkIsAcyclicWithBoxes_rec( Abc_Obj_t * pNode ) if ( Abc_ObjIsBox(pNode) ) pFanin = Abc_ObjFanin0(pFanin); pFanin = Abc_ObjFanin0Ntk(pFanin); - // make sure there is no mixing of networks - assert( pFanin->pNtk == pNode->pNtk ); if ( Abc_ObjIsBo(pFanin) ) pFanin = Abc_ObjFanin0(pFanin); // check if the fanin is visited @@ -1523,6 +1519,8 @@ int Abc_NtkIsAcyclicWithBoxes( Abc_Ntk_t * pNtk ) Abc_NtkForEachPo( pNtk, pNode, i ) { pNode = Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode)); + if ( Abc_ObjIsBo(pNode) ) + pNode = Abc_ObjFanin0(pNode); if ( Abc_NodeIsTravIdPrevious(pNode) ) continue; // traverse the output logic cone @@ -1537,6 +1535,8 @@ int Abc_NtkIsAcyclicWithBoxes( Abc_Ntk_t * pNtk ) Abc_NtkForEachLatchInput( pNtk, pNode, i ) { pNode = Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode)); + if ( Abc_ObjIsBo(pNode) ) + pNode = Abc_ObjFanin0(pNode); if ( Abc_NodeIsTravIdPrevious(pNode) ) continue; // traverse the output logic cone diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e7bd2a6a..7b08c564 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -440,6 +440,7 @@ static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9PoXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Demiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Fadds ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1042,6 +1043,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&poxsim", Abc_CommandAbc9PoXsim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&demiter", Abc_CommandAbc9Demiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&fadds", Abc_CommandAbc9Fadds, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); @@ -36624,6 +36626,162 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Mfs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ); + Gia_Man_t * pTemp; int c; + Sfm_Par_t Pars, * pPars = &Pars; + Sfm_ParSetDefault( pPars ); + pPars->nTfoLevMax = 5; + pPars->nDepthMax = 100; + pPars->nWinSizeMax = 2000; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCNdaevwh" ) ) != EOF ) + { + switch ( c ) + { + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTfoLevMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTfoLevMax < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFanoutMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFanoutMax < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nDepthMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nDepthMax < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nWinSizeMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nWinSizeMax < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nGrowthLevel = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBTLimit < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nNodesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nNodesMax < 0 ) + goto usage; + break; + case 'd': + pPars->fRrOnly ^= 1; + break; + case 'a': + pPars->fArea ^= 1; + break; + case 'e': + pPars->fMoreEffort ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" ); + return 0; + } + if ( !Gia_ManHasMapping(pAbc->pGia) ) + { + Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has no mapping.\n" ); + return 0; + } + pTemp = Gia_ManPerformMfs( pAbc->pGia, pPars ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &mfs [-WFDMLCN ] [-daevwh]\n" ); + Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" ); + Abc_Print( -2, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax ); + Abc_Print( -2, "\t-F : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax ); + Abc_Print( -2, "\t-D : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax ); + Abc_Print( -2, "\t-M : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax ); + Abc_Print( -2, "\t-L : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); + Abc_Print( -2, "\t-C : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit ); + Abc_Print( -2, "\t-N : the max number of nodes to try (0 = all) [default = %d]\n", pPars->nNodesMax ); + Abc_Print( -2, "\t-d : toggle performing redundancy removal [default = %s]\n", pPars->fRrOnly? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); + Abc_Print( -2, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c index e6d07993..aab18ed0 100644 --- a/src/base/abci/abcMfs.c +++ b/src/base/abci/abcMfs.c @@ -270,7 +270,6 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars ) p = Abc_NtkExtractMfs( pNtk, pPars->nFirstFixed ); // perform optimization nNodes = Sfm_NtkPerform( p, pPars ); - // call the fast extract procedure if ( nNodes == 0 ) { // Abc_Print( 1, "The network is not changed by \"mfs\".\n" ); @@ -451,7 +450,6 @@ int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t pp = Abc_NtkExtractMfs2( pNtk, iPivot ); // perform optimization nNodes = Sfm_NtkPerform( pp, pPars ); - // call the fast extract procedure if ( nNodes == 0 ) { // Abc_Print( 1, "The network is not changed by \"mfs\".\n" ); diff --git a/src/misc/tim/tim.h b/src/misc/tim/tim.h index ba2b1bdb..df69ae36 100644 --- a/src/misc/tim/tim.h +++ b/src/misc/tim/tim.h @@ -130,6 +130,7 @@ extern Tim_Man_t * Tim_ManLoad( Vec_Str_t * p, int fHieOnly ); extern Tim_Man_t * Tim_ManStart( int nCis, int nCos ); extern Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay ); extern Tim_Man_t * Tim_ManTrim( Tim_Man_t * p, Vec_Int_t * vBoxPres ); +extern Tim_Man_t * Tim_ManReduce( Tim_Man_t * p, Vec_Int_t * vBoxesLeft ); extern Vec_Int_t * Tim_ManAlignTwo( Tim_Man_t * pSpec, Tim_Man_t * pImpl ); extern void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * vOutReqs ); extern float * Tim_ManGetArrTimes( Tim_Man_t * p ); diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c index c3caf4dc..8fcc8eaf 100644 --- a/src/misc/tim/timMan.c +++ b/src/misc/tim/timMan.c @@ -237,6 +237,93 @@ Tim_Man_t * Tim_ManTrim( Tim_Man_t * p, Vec_Int_t * vBoxPres ) return pNew; } +/**Function************************************************************* + + Synopsis [Trims the timing manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Tim_Man_t * Tim_ManReduce( Tim_Man_t * p, Vec_Int_t * vBoxesLeft ) +{ + Tim_Man_t * pNew; + Tim_Box_t * pBox; + Tim_Obj_t * pObj; + float * pDelayTable, * pDelayTableNew; + int i, k, iBox, nNewCis, nNewCos, nInputs, nOutputs; + if ( Vec_IntSize(vBoxesLeft) == Tim_ManBoxNum(p) ) + return Tim_ManDup( p, 0 ); + assert( Vec_IntSize(vBoxesLeft) < Tim_ManBoxNum(p) ); + // count the number of CIs and COs in the trimmed manager + nNewCis = Tim_ManPiNum(p); + nNewCos = Tim_ManPoNum(p); + Vec_IntForEachEntry( vBoxesLeft, iBox, i ) + { + pBox = Tim_ManBox( p, iBox ); + nNewCis += pBox->nOutputs; + nNewCos += pBox->nInputs; + } + assert( nNewCis < Tim_ManCiNum(p) ); + assert( nNewCos < Tim_ManCoNum(p) ); + // clear traversal IDs + Tim_ManForEachCi( p, pObj, i ) + pObj->TravId = 0; + Tim_ManForEachCo( p, pObj, i ) + pObj->TravId = 0; + // create new manager + pNew = Tim_ManStart( nNewCis, nNewCos ); + // copy box connectivity information + memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * Tim_ManPiNum(p) ); + memcpy( pNew->pCos + nNewCos - Tim_ManPoNum(p), + p->pCos + Tim_ManCoNum(p) - Tim_ManPoNum(p), + sizeof(Tim_Obj_t) * Tim_ManPoNum(p) ); + // duplicate delay tables + if ( Tim_ManDelayTableNum(p) > 0 ) + { + pNew->vDelayTables = Vec_PtrStart( Vec_PtrSize(p->vDelayTables) ); + Tim_ManForEachTable( p, pDelayTable, i ) + { + if ( pDelayTable == NULL ) + continue; + assert( i == (int)pDelayTable[0] ); + nInputs = (int)pDelayTable[1]; + nOutputs = (int)pDelayTable[2]; + pDelayTableNew = ABC_ALLOC( float, 3 + nInputs * nOutputs ); + pDelayTableNew[0] = (int)pDelayTable[0]; + pDelayTableNew[1] = (int)pDelayTable[1]; + pDelayTableNew[2] = (int)pDelayTable[2]; + for ( k = 0; k < nInputs * nOutputs; k++ ) + pDelayTableNew[3+k] = pDelayTable[3+k]; +// assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) ); + assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL ); + Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew ); + } + } + // duplicate boxes + if ( Tim_ManBoxNum(p) > 0 ) + { + int curPi = Tim_ManPiNum(p); + int curPo = 0; + pNew->vBoxes = Vec_PtrAlloc( Tim_ManBoxNum(p) ); + Vec_IntForEachEntry( vBoxesLeft, iBox, i ) + { + pBox = Tim_ManBox( p, iBox ); + Tim_ManCreateBox( pNew, curPo, pBox->nInputs, curPi, pBox->nOutputs, pBox->iDelayTable ); + Tim_ManBoxSetCopy( pNew, Tim_ManBoxNum(pNew) - 1, iBox ); + curPi += pBox->nOutputs; + curPo += pBox->nInputs; + } + curPo += Tim_ManPoNum(p); + assert( curPi == Tim_ManCiNum(pNew) ); + assert( curPo == Tim_ManCoNum(pNew) ); + } + return pNew; +} + /**Function************************************************************* Synopsis [Aligns two sets of boxes using the copy field.] diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h index c8a30030..1d97cd8b 100644 --- a/src/opt/sfm/sfm.h +++ b/src/opt/sfm/sfm.h @@ -77,7 +77,7 @@ extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i ); extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i ); extern int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i ); /*=== sfmWin.c ==========================================================*/ -extern Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p ); +extern Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft ); ABC_NAMESPACE_HEADER_END diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c index fd04e432..1ded0ede 100644 --- a/src/opt/sfm/sfmNtk.c +++ b/src/opt/sfm/sfmNtk.c @@ -54,7 +54,8 @@ void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 ); // nodes are in a topo order; POs cannot be fanins Vec_IntForEachEntry( vArray, Fanin, k ) - assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) ); +// assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) ); + assert( Fanin + nPos < Vec_WecSize(vFanins) ); // POs have one fanout if ( i + nPos >= Vec_WecSize(vFanins) ) assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 ); diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c index 9f91c936..6eab478e 100644 --- a/src/opt/sfm/sfmWin.c +++ b/src/opt/sfm/sfmWin.c @@ -125,33 +125,53 @@ static inline int Sfm_ObjIsTravIdCurrent2( Sfm_Ntk_t * p, int Id ) { return Synopsis [Collects used internal nodes in a topological order.] - Description [] + Description [Additionally considers objects in groups as a single object + and collects them in a topological order together as single entity.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes ) +void Sfm_NtkDfs_rec( Sfm_Ntk_t * p, int iNode, Vec_Int_t * vNodes, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft ) { int i, iFanin; if ( Sfm_ObjIsPi(p, iNode) ) return; if ( Sfm_ObjIsTravIdCurrent(p, iNode) ) return; - Sfm_ObjSetTravIdCurrent(p, iNode); - Sfm_ObjForEachFanin( p, iNode, iFanin, i ) - Sfm_NtkDfs_rec( p, iFanin, vNodes ); - Vec_IntPush( vNodes, iNode ); + if ( Vec_IntEntry(vGroupMap, iNode) >= 0 ) + { + int k, iGroup = Abc_Lit2Var( Vec_IntEntry(vGroupMap, iNode) ); + Vec_Int_t * vGroup = Vec_WecEntry( vGroups, iGroup ); + Vec_IntForEachEntry( vGroup, iNode, i ) + assert( Sfm_ObjIsNode(p, iNode) ); + Vec_IntForEachEntry( vGroup, iNode, i ) + Sfm_ObjSetTravIdCurrent( p, iNode ); + Vec_IntForEachEntry( vGroup, iNode, i ) + Sfm_ObjForEachFanin( p, iNode, iFanin, k ) + Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); + Vec_IntForEachEntry( vGroup, iNode, i ) + Vec_IntPush( vNodes, iNode ); + Vec_IntPush( vBoxesLeft, iGroup ); + } + else + { + Sfm_ObjSetTravIdCurrent(p, iNode); + Sfm_ObjForEachFanin( p, iNode, iFanin, i ) + Sfm_NtkDfs_rec( p, iFanin, vNodes, vGroups, vGroupMap, vBoxesLeft ); + Vec_IntPush( vNodes, iNode ); + } } -Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p ) +Vec_Int_t * Sfm_NtkDfs( Sfm_Ntk_t * p, Vec_Wec_t * vGroups, Vec_Int_t * vGroupMap, Vec_Int_t * vBoxesLeft ) { Vec_Int_t * vNodes; int i; + Vec_IntClear( vBoxesLeft ); vNodes = Vec_IntAlloc( p->nObjs ); Sfm_NtkIncrementTravId( p ); Sfm_NtkForEachPo( p, i ) - Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes ); + Sfm_NtkDfs_rec( p, Sfm_ObjFanin(p, i, 0), vNodes, vGroups, vGroupMap, vBoxesLeft ); return vNodes; } -- cgit v1.2.3