From 7724dfcca212ae1fd43cb095d5d85fea85c07608 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 30 Mar 2016 21:51:50 -0700 Subject: Windowing for technology mapping. --- src/aig/gia/gia.h | 23 +++- src/aig/gia/giaDfs.c | 34 ++--- src/aig/gia/giaFrames.c | 2 +- src/aig/gia/giaIf.c | 10 +- src/aig/gia/giaMan.c | 1 + src/aig/gia/giaSatLut.c | 231 +++++++++++++++++++++------------ src/aig/gia/giaSplit.c | 332 ++++++++++++++++++++++++++++++++++++------------ 7 files changed, 450 insertions(+), 183 deletions(-) (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index a6ff65f2..ef80d814 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -32,6 +32,7 @@ #include #include "misc/vec/vec.h" +#include "misc/vec/vecWec.h" #include "misc/util/utilCex.h" //////////////////////////////////////////////////////////////////////// @@ -130,7 +131,9 @@ struct Gia_Man_t_ Vec_Int_t * vFanoutNums; // static fanout Vec_Int_t * vFanout; // static fanout Vec_Int_t * vMapping; // mapping for each node + Vec_Wec_t * vMapping2; // mapping for each node Vec_Int_t * vCellMapping; // mapping for each node + void * pSatlutWinman; // windowing for SAT-based mapping Vec_Int_t * vPacking; // packing information Vec_Int_t * vConfigs; // cell configurations char * pCellStr; // cell description @@ -986,6 +989,12 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re static inline int Gia_ObjLutMuxId( Gia_Man_t * p, int Id ) { return Gia_ObjLutFanins(p, Id)[Gia_ObjLutSize(p, Id)]; } static inline int Gia_ObjLutIsMux( Gia_Man_t * p, int Id ) { return (int)(Gia_ObjLutMuxId(p, Id) < 0); } +static inline int Gia_ManHasMapping2( Gia_Man_t * p ) { return p->vMapping2 != NULL; } +static inline int Gia_ObjIsLut2( Gia_Man_t * p, int Id ) { return Vec_IntSize(Vec_WecEntry(p->vMapping2, Id)) != 0; } +static inline int Gia_ObjLutSize2( Gia_Man_t * p, int Id ) { return Vec_IntSize(Vec_WecEntry(p->vMapping2, Id)); } +static inline Vec_Int_t * Gia_ObjLutFanins2( Gia_Man_t * p, int Id ) { return Vec_WecEntry(p->vMapping2, Id); } +static inline int Gia_ObjLutFanin2( Gia_Man_t * p, int Id, int i ) { return Vec_IntEntry(Vec_WecEntry(p->vMapping2, Id), i); } + static inline int Gia_ManHasCellMapping( Gia_Man_t * p ) { return p->vCellMapping != NULL; } static inline int Gia_ObjIsCell( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, iLit) != 0; } static inline int Gia_ObjIsCellInv( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, iLit) == -1; } @@ -1002,6 +1011,15 @@ static inline int Gia_ObjCellId( Gia_Man_t * p, int iLit ) { re #define Gia_LutForEachFaninObj( p, i, pFanin, k ) \ for ( k = 0; k < Gia_ObjLutSize(p,i) && ((pFanin = Gia_ManObj(p, Gia_ObjLutFanins(p,i)[k])),1); k++ ) +#define Gia_ManForEachLut2( p, i ) \ + for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsLut2(p, i) ) {} else +#define Gia_LutForEachFanin2( p, i, iFan, k ) \ + for ( k = 0; k < Gia_ObjLutSize2(p,i) && ((iFan = Gia_ObjLutFanin2(p,i,k)),1); k++ ) +#define Gia_ManForEachLut2Vec( vIds, p, vVec, iObj, i ) \ + for ( i = 0; i < Vec_IntSize(vIds) && (vVec = Vec_WecEntry(p->vMapping2, (iObj = Vec_IntEntry(vIds, i)))); i++ ) +#define Gia_ManForEachLut2VecReverse( vIds, p, vVec, iObj, i ) \ + for ( i = Vec_IntSize(vIds)-1; i >= 0 && (vVec = Vec_WecEntry(p->vMapping2, (iObj = Vec_IntEntry(vIds, i)))); i-- ) + #define Gia_ManForEachCell( p, i ) \ for ( i = 2; i < 2*Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsCell(p, i) ) {} else #define Gia_CellForEachFanin( p, i, iFanLit, k ) \ @@ -1118,7 +1136,7 @@ extern Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs extern Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose ); /*=== giaDfs.c ============================================================*/ extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp ); -extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes ); +extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves ); extern Vec_Int_t * Gia_ManCollectNodesCis( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes ); @@ -1359,6 +1377,9 @@ extern void Gia_ManSimulateRound( Gia_ManSim_t * p ); extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerbose, int fVeryVerbose ); +/*=== giaSplit.c ============================================================*/ +extern void Gia_ManComputeOneWinStart( Gia_Man_t * p, int fReverse ); +extern int Gia_ManComputeOneWin( Gia_Man_t * p, int iPivot, Vec_Int_t ** pvRoots, Vec_Int_t ** pvNodes, Vec_Int_t ** pvLeaves, Vec_Int_t ** pvAnds ); /*=== giaStg.c ============================================================*/ extern void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates ); extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerbose ); diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c index 940eaf46..0dd0ac8e 100644 --- a/src/aig/gia/giaDfs.c +++ b/src/aig/gia/giaDfs.c @@ -96,17 +96,19 @@ void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSu SeeAlso [] ***********************************************************************/ -void Gia_ManCollectAnds_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes ) +void Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes ) { - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) return; - Gia_ObjSetTravIdCurrent(p, pObj); + Gia_ObjSetTravIdCurrentId(p, iObj); + pObj = Gia_ManObj( p, iObj ); if ( Gia_ObjIsCi(pObj) ) return; assert( Gia_ObjIsAnd(pObj) ); - Gia_ManCollectAnds_rec( p, Gia_ObjFanin0(pObj), vNodes ); - Gia_ManCollectAnds_rec( p, Gia_ObjFanin1(pObj), vNodes ); - Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); + Gia_ManCollectAnds_rec( p, Gia_ObjFaninId0(pObj, iObj), vNodes ); + Gia_ManCollectAnds_rec( p, Gia_ObjFaninId1(pObj, iObj), vNodes ); + Vec_IntPush( vNodes, iObj ); } /**Function************************************************************* @@ -120,20 +122,22 @@ void Gia_ManCollectAnds_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes SeeAlso [] ***********************************************************************/ -void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes ) +void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves ) { - Gia_Obj_t * pObj; - int i; - Vec_IntClear( vNodes ); + int i, iLeaf; // Gia_ManIncrementTravId( p ); - Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); + Gia_ObjSetTravIdCurrentId( p, 0 ); + if ( vLeaves ) + Vec_IntForEachEntry( vLeaves, iLeaf, i ) + Gia_ObjSetTravIdCurrentId( p, iLeaf ); + Vec_IntClear( vNodes ); for ( i = 0; i < nNodes; i++ ) { - pObj = Gia_ManObj( p, pNodes[i] ); + Gia_Obj_t * pObj = Gia_ManObj( p, pNodes[i] ); if ( Gia_ObjIsCo(pObj) ) - Gia_ManCollectAnds_rec( p, Gia_ObjFanin0(pObj), vNodes ); + Gia_ManCollectAnds_rec( p, Gia_ObjFaninId0(pObj, pNodes[i]), vNodes ); else - Gia_ManCollectAnds_rec( p, pObj, vNodes ); + Gia_ManCollectAnds_rec( p, pNodes[i], vNodes ); } } @@ -216,7 +220,7 @@ void Gia_ManCollectTest( Gia_Man_t * p ) Gia_ManForEachCo( p, pObj, i ) { iNode = Gia_ObjId(p, pObj); - Gia_ManCollectAnds( p, &iNode, 1, vNodes ); + Gia_ManCollectAnds( p, &iNode, 1, vNodes, NULL ); } Vec_IntFree( vNodes ); ABC_PRT( "DFS from each output", Abc_Clock() - clk ); diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c index ebe2c139..3b33e3de 100644 --- a/src/aig/gia/giaFrames.c +++ b/src/aig/gia/giaFrames.c @@ -706,7 +706,7 @@ void Gia_ManFraSupports( Gia_ManFra_t * p ) vIns = Vec_IntAlloc( 100 ); Gia_ManCollectCis( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vIns ); vAnds = Vec_IntAlloc( 100 ); - Gia_ManCollectAnds( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vAnds ); + Gia_ManCollectAnds( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vAnds, NULL ); Vec_PtrWriteEntry( p->vIns, f, vIns ); Vec_PtrWriteEntry( p->vAnds, f, vAnds ); Vec_PtrWriteEntry( p->vOuts, f, vOuts ); diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index d93390e3..f5071929 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -249,10 +249,10 @@ void Gia_ManSetRefsMapped( Gia_Man_t * p ) ABC_FREE( p->pRefs ); p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) ); Gia_ManForEachCo( p, pObj, i ) - Gia_ObjRefInc( p, Gia_ObjFanin0(pObj) ); + Gia_ObjRefIncId( p, Gia_ObjFaninId0p(p, pObj) ); Gia_ManForEachLut( p, i ) Gia_LutForEachFanin( p, i, iFan, k ) - Gia_ObjRefInc( p, Gia_ManObj(p, iFan) ); + Gia_ObjRefIncId( p, iFan ); } /**Function************************************************************* @@ -273,10 +273,10 @@ void Gia_ManSetLutRefs( Gia_Man_t * p ) ABC_FREE( p->pLutRefs ); p->pLutRefs = ABC_CALLOC( int, Gia_ManObjNum(p) ); Gia_ManForEachCo( p, pObj, i ) - Gia_ObjLutRefInc( p, Gia_ObjFanin0(pObj) ); + Gia_ObjLutRefIncId( p, Gia_ObjFaninId0p(p, pObj) ); Gia_ManForEachLut( p, i ) Gia_LutForEachFanin( p, i, iFan, k ) - Gia_ObjLutRefInc( p, Gia_ManObj(p, iFan) ); + Gia_ObjLutRefIncId( p, iFan ); } /**Function************************************************************* @@ -1568,7 +1568,7 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * // collect nodes Gia_ManIncrementTravId( pTemp ); Id = Abc_Lit2Var( iLit ); - Gia_ManCollectAnds( pTemp, &Id, 1, vCover ); + Gia_ManCollectAnds( pTemp, &Id, 1, vCover, NULL ); Vec_IntPrint( vCover ); Gia_ManForEachObjVec( vCover, pTemp, pObj, i ) Gia_ObjPrint( pTemp, pObj ); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index cba58b3c..ea25c4ab 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -113,6 +113,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_WrdFreeP( &p->vTtMemory ); Vec_PtrFreeP( &p->vTtInputs ); Vec_IntFreeP( &p->vMapping ); + Vec_WecFreeP( &p->vMapping2 ); Vec_IntFreeP( &p->vCellMapping ); Vec_IntFreeP( &p->vPacking ); Vec_IntFreeP( &p->vConfigs ); diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index 7f18a485..f985eb50 100644 --- a/src/aig/gia/giaSatLut.c +++ b/src/aig/gia/giaSatLut.c @@ -20,7 +20,6 @@ #include "gia.h" #include "sat/bsat/satStore.h" -#include "misc/vec/vecWec.h" #include "misc/util/utilNam.h" #include "map/scl/sclCon.h" @@ -40,13 +39,12 @@ struct Sbl_Man_t_ int FirstVar; // first variable to be used int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2) int nInputs; // the number of inputs - // mapping - Vec_Wec_t * vMapping; // current mapping // window Gia_Man_t * pGia; Vec_Int_t * vLeaves; // leaf nodes - Vec_Int_t * vNodes; // internal nodes - Vec_Int_t * vRoots; // driver nodes (a subset of vNodes) + Vec_Int_t * vAnds; // AND-gates + Vec_Int_t * vNodes; // internal LUTs + Vec_Int_t * vRoots; // driver nodes (a subset of vAnds) Vec_Int_t * vRootVars; // driver nodes (as SAT variables) // cuts Vec_Wrd_t * vCutsI; // input bit patterns @@ -79,55 +77,55 @@ struct Sbl_Man_t_ SeeAlso [] ***********************************************************************/ -Vec_Wec_t * Sbl_ManToMapping( Gia_Man_t * p ) -{ - Vec_Wec_t * vMapping = Vec_WecStart( Gia_ManObjNum(p) ); - int Obj, Fanin, k; - Gia_ManForEachLut( p, Obj ) - Gia_LutForEachFanin( p, Obj, Fanin, k ) - Vec_WecPush( vMapping, Obj, Fanin ); - return vMapping; -} -Vec_Int_t * Sbl_ManFromMapping( Gia_Man_t * p, Vec_Wec_t * vMap ) -{ - Vec_Int_t * vMapping, * vVec; int i, k, Obj; - vMapping = Vec_IntAlloc( Gia_ManObjNum(p) + Vec_WecSizeSize(vMap) + 2*Vec_WecSizeUsed(vMap) ); - Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 ); - Vec_WecForEachLevel( vMap, vVec, i ) - if ( Vec_IntSize(vVec) > 0 ) - { - Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) ); - Vec_IntPush( vMapping, Vec_IntSize(vVec) ); - Vec_IntForEachEntry( vVec, Obj, k ) - Vec_IntPush( vMapping, Obj ); - Vec_IntPush( vMapping, i ); - } - assert( Vec_IntSize(vMapping) < 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) ); - return vMapping; -} void Sbl_ManUpdateMapping( Sbl_Man_t * p ) { +// Gia_Obj_t * pObj; Vec_Int_t * vObj; - int i, c, b, iObj; word CutI, CutN; + int i, c, b, iObj, iTemp; assert( Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) ); - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Vec_IntClear( Vec_WecEntry(p->vMapping, iObj) ); + Vec_IntForEachEntry( p->vAnds, iObj, i ) + { + vObj = Vec_WecEntry(p->pGia->vMapping2, iObj); + Vec_IntForEachEntry( vObj, iTemp, b ) + Gia_ObjLutRefDecId( p->pGia, iTemp ); + Vec_IntClear( vObj ); + } Vec_IntForEachEntry( p->vSolCuts2, c, i ) { CutI = Vec_WrdEntry( p->vCutsI, c ); CutN = Vec_WrdEntry( p->vCutsN, c ); iObj = Vec_IntEntry( p->vCutsObj, c ); - iObj = Vec_IntEntry( p->vNodes, iObj ); - vObj = Vec_WecEntry( p->vMapping, iObj ); + iObj = Vec_IntEntry( p->vAnds, iObj ); + vObj = Vec_WecEntry( p->pGia->vMapping2, iObj ); assert( Vec_IntSize(vObj) == 0 ); for ( b = 0; b < 64; b++ ) if ( (CutI >> b) & 1 ) Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) ); for ( b = 0; b < 64; b++ ) if ( (CutN >> b) & 1 ) - Vec_IntPush( vObj, Vec_IntEntry(p->vNodes, b) ); + Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, b) ); + Vec_IntForEachEntry( vObj, iTemp, b ) + Gia_ObjLutRefIncId( p->pGia, iTemp ); } +/* + // verify + Gia_ManForEachLut2Vec( p->pGia, vObj, i ) + Vec_IntForEachEntry( vObj, iTemp, b ) + Gia_ObjLutRefDecId( p->pGia, iTemp ); + Gia_ManForEachCo( p->pGia, pObj, i ) + Gia_ObjLutRefDecId( p->pGia, Gia_ObjFaninId0p(p->pGia, pObj) ); + + for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ ) + if ( p->pGia->pLutRefs[i] ) + printf( "Object %d has %d refs\n", i, p->pGia->pLutRefs[i] ); + + Gia_ManForEachCo( p->pGia, pObj, i ) + Gia_ObjLutRefIncId( p->pGia, Gia_ObjFaninId0p(p->pGia, pObj) ); + Gia_ManForEachLut2Vec( p->pGia, vObj, i ) + Vec_IntForEachEntry( vObj, iTemp, b ) + Gia_ObjLutRefIncId( p->pGia, iTemp ); +*/ } /**Function************************************************************* @@ -147,11 +145,11 @@ static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs ) printf( "{ " ); for ( b = 0; b < 64; b++ ) if ( (CutI >> b) & 1 ) - printf( "i%d ", b + 1 ), Count++; + printf( "i%d ", b ), Count++; printf( " " ); for ( b = 0; b < 64; b++ ) if ( (CutN >> b) & 1 ) - printf( "n%d ", nInputs + b + 1 ), Count++; + printf( "n%d ", b ), Count++; printf( "};\n" ); return Count; } @@ -219,12 +217,12 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN ) int Start0 = Vec_IntEntry( p->vCutsStart, Obj ); int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj ); int i; -// printf( "Looking for:\n" ); -// Sbl_ManPrintCut( CutI, CutN, p->nInputs ); -// printf( "\n" ); + //printf( "\nLooking for:\n" ); + //Sbl_ManPrintCut( CutI, CutN, p->nInputs ); + //printf( "\n" ); for ( i = Start0; i < Limit0; i++ ) { -// Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs ); + //Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs ); if ( pCutsI[i] == CutI && pCutsN[i] == CutN ) return i; } @@ -232,9 +230,9 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN ) } int Sbl_ManComputeCuts( Sbl_Man_t * p ) { - Gia_Obj_t * pObj, * pFanin; - int i, k, Index, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes); - assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vNodes) <= 64 ); + Gia_Obj_t * pObj; Vec_Int_t * vFanins; + int i, k, Index, Fanin, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vAnds); + assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vAnds) <= 64 ); // assign leaf cuts Vec_IntClear( p->vCutsStart ); Vec_IntClear( p->vCutsObj ); @@ -251,7 +249,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p ) pObj->Value = i; } // assign internal cuts - Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i ) + Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i ) { assert( Gia_ObjIsAnd(pObj) ); assert( ~Gia_ObjFanin0(pObj)->Value ); @@ -270,27 +268,30 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p ) int Obj = Gia_ObjId(p->pGia, pObj); if ( Gia_ObjIsCi(pObj) ) continue; - assert( Gia_ObjIsLut(p->pGia, Obj) ); + assert( Gia_ObjIsLut2(p->pGia, Obj) ); assert( ~pObj->Value ); Vec_IntPush( p->vRootVars, pObj->Value - Vec_IntSize(p->vLeaves) ); } // create current solution Vec_IntClear( p->vPolar ); Vec_IntClear( p->vSolCuts ); - Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i ) + Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i ) { word CutI = 0, CutN = 0; int Obj = Gia_ObjId(p->pGia, pObj); - if ( !Gia_ObjIsLut(p->pGia, Obj) ) + if ( !Gia_ObjIsLut2(p->pGia, Obj) ) continue; assert( (int)pObj->Value == Vec_IntSize(p->vLeaves) + i ); // add node Vec_IntPush( p->vPolar, i ); Vec_IntPush( p->vSolCuts, i ); // add its cut - Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k ) + //Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k ) + vFanins = Gia_ObjLutFanins2( p->pGia, Obj ); + Vec_IntForEachEntry( vFanins, Fanin, k ) { - assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut(p->pGia, Gia_ObjId(p->pGia, pFanin)) ); + Gia_Obj_t * pFanin = Gia_ManObj( p->pGia, Fanin ); + assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut2(p->pGia, Fanin) ); assert( ~pFanin->Value ); if ( (int)pFanin->Value < Vec_IntSize(p->vLeaves) ) CutI |= ((word)1 << pFanin->Value); @@ -299,13 +300,18 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p ) } // find the new cut Index = Sbl_ManFindCut( p, Vec_IntSize(p->vLeaves) + i, CutI, CutN ); + if ( Index < 0 ) + { + printf( "Cannot find the available cut.\n" ); + continue; + } assert( Index >= 0 ); Vec_IntPush( p->vPolar, p->FirstVar+Index ); } // clean value Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i ) pObj->Value = ~0; - Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i ) + Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i ) pObj->Value = ~0; return Vec_WrdSize(p->vCutsI); } @@ -316,7 +322,7 @@ int Sbl_ManCreateCnf( Sbl_Man_t * p ) assert( p->FirstVar == sat_solver_nvars(p->pSat) ); sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WrdSize(p->vCutsI) ); //printf( "\n" ); - for ( i = 0; i < Vec_IntSize(p->vNodes); i++ ) + for ( i = 0; i < Vec_IntSize(p->vAnds); i++ ) { int Start0 = Vec_IntEntry( p->vCutsStart, Vec_IntSize(p->vLeaves) + i ); int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Vec_IntSize(p->vLeaves) + i ) - 1; @@ -380,6 +386,7 @@ Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN ) // window p->pGia = pGia; p->vLeaves = Vec_IntAlloc( 64 ); + p->vAnds = Vec_IntAlloc( 64 ); p->vNodes = Vec_IntAlloc( 64 ); p->vRoots = Vec_IntAlloc( 64 ); p->vRootVars = Vec_IntAlloc( 64 ); @@ -399,7 +406,6 @@ Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN ) p->vPolar = Vec_IntAlloc( 1000 ); // other Gia_ManFillValue( pGia ); - p->vMapping = Sbl_ManToMapping( pGia ); return p; } @@ -407,9 +413,9 @@ void Sbl_ManStop( Sbl_Man_t * p ) { sat_solver_delete( p->pSat ); Vec_IntFree( p->vCardVars ); - Vec_WecFree( p->vMapping ); // internal Vec_IntFree( p->vLeaves ); + Vec_IntFree( p->vAnds ); Vec_IntFree( p->vNodes ); Vec_IntFree( p->vRoots ); Vec_IntFree( p->vRootVars ); @@ -439,25 +445,68 @@ void Sbl_ManWindow( Sbl_Man_t * p ) Gia_ManForEachCiId( p->pGia, ObjId, i ) Vec_IntPush( p->vLeaves, ObjId ); // collect internal - Vec_IntClear( p->vNodes ); + Vec_IntClear( p->vAnds ); Gia_ManForEachAndId( p->pGia, ObjId ) - Vec_IntPush( p->vNodes, ObjId ); + Vec_IntPush( p->vAnds, ObjId ); // collect roots Vec_IntClear( p->vRoots ); Gia_ManForEachCoDriverId( p->pGia, ObjId, i ) Vec_IntPush( p->vRoots, ObjId ); } -int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose ) +int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot ) { + Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds; + int Count = Gia_ManComputeOneWin( p->pGia, iPivot, &vRoots, &vNodes, &vLeaves, &vAnds ); + if ( Count == 0 ) + return 0; + Vec_IntClear( p->vRoots ); Vec_IntAppend( p->vRoots, vRoots ); + Vec_IntClear( p->vNodes ); Vec_IntAppend( p->vNodes, vNodes ); + Vec_IntClear( p->vLeaves ); Vec_IntAppend( p->vLeaves, vLeaves ); + Vec_IntClear( p->vAnds ); Vec_IntAppend( p->vAnds, vAnds ); +//Vec_IntPrint( vRoots ); +//Vec_IntPrint( vAnds ); +//Vec_IntPrint( vLeaves ); + // recompute internal nodes +// Gia_ManIncrementTravId( p->pGia ); +// Gia_ManCollectAnds( p->pGia, Vec_IntArray(p->vRoots), Vec_IntSize(p->vRoots), p->vAnds, p->vLeaves ); + return Count; +} + +int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose ) +{ + int fKeepTrying = 1; abctime clk = Abc_Clock(), clk2; int i, LogN = 6, nVars = 1 << LogN, status, Root; Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN ); - int fKeepTrying = 1; - int StartSol; + int StartSol, Count, nConfTotal = 0; + + // compute one window + Count = Sbl_ManWindow2( p, iPivot ); + if ( Count == 0 ) + { + printf( "Obj %d: Window with less than %d inputs does not exist.\n", iPivot, 64 ); + Sbl_ManStop( p ); + return 0; + } + if ( fVerbose ) + printf( "\nObj = %6d : Leaf = %2d. LUT = %2d. AND = %2d. Root = %2d.\n", + iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vAnds), Vec_IntSize(p->vRoots) ); + if ( Vec_IntSize(p->vLeaves) > 64 || Vec_IntSize(p->vAnds) > 64 ) + { + printf( "Obj %d: Encountered window with %d inputs and %d internal nodes.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds) ); + Sbl_ManStop( p ); + return 0; + } + + if ( Vec_IntSize(p->vAnds) < 20 ) + { + if ( fVerbose ) + printf( "Skipping.\n" ); + Sbl_ManStop( p ); + return 0; + } - // derive window - Sbl_ManWindow( p ); // derive cuts Sbl_ManComputeCuts( p ); // derive SAT instance @@ -468,7 +517,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose ) if ( fVerbose ) printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n\n", - sat_solver_nclauses(p->pSat), Vec_IntSize(p->vNodes), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vNodes), + sat_solver_nclauses(p->pSat), Vec_IntSize(p->vAnds), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vAnds), sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) ); // create assumptions @@ -476,17 +525,19 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose ) Vec_IntClear( p->vAssump ); Vec_IntPush( p->vAssump, -1 ); // unused variables - for ( i = Vec_IntSize(p->vNodes); i < nVars; i++ ) + for ( i = Vec_IntSize(p->vAnds); i < nVars; i++ ) Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) ); // root variables Vec_IntForEachEntry( p->vRootVars, Root, i ) Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) ); // Vec_IntPrint( p->vAssump ); + Vec_IntClear( p->vSolCuts2 ); StartSol = Vec_IntSize(p->vSolCuts) + 1; // StartSol = 30; while ( fKeepTrying && StartSol-fKeepTrying > 0 ) { + int nConfBef, nConfAft; if ( fVerbose ) printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying ); // for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ ) @@ -494,19 +545,24 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose ) Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) ); // solve the problem clk2 = Abc_Clock(); - status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 ); + nConfBef = (int)p->pSat->stats.conflicts; + status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), nBTLimit, 0, 0, 0 ); + nConfAft = (int)p->pSat->stats.conflicts; + nConfTotal += nConfAft - nConfBef; + if ( status == l_Undef ) + break; if ( status == l_True ) { int Count = 0, LitCount = 0; if ( fVerbose ) { printf( "Inputs = %d. ANDs = %d. Total = %d. All vars = %d.\n", - Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), - Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vNodes), nVars ); - for ( i = 0; i < Vec_IntSize(p->vNodes); i++ ) + Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds), + Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vAnds), nVars ); + for ( i = 0; i < Vec_IntSize(p->vAnds); i++ ) printf( "%d", sat_solver_var_value(p->pSat, i) ); printf( "\n" ); - for ( i = 0; i < Vec_IntSize(p->vNodes); i++ ) + for ( i = 0; i < Vec_IntSize(p->vAnds); i++ ) if ( sat_solver_var_value(p->pSat, i) ) { printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) ); @@ -523,13 +579,18 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose ) if ( sat_solver_var_value(p->pSat, i) ) { if ( fVerbose ) - printf( "Cut %3d : ", Count++ ); + printf( "Cut %3d : Node = %3d Node = %6d ", Count++, Vec_IntEntry(p->vCutsObj, i-p->FirstVar), Vec_IntEntry(p->vAnds, Vec_IntEntry(p->vCutsObj, i-p->FirstVar)) ); if ( fVerbose ) LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar ); Vec_IntPush( p->vSolCuts2, i-p->FirstVar ); } if ( fVerbose ) - printf( "LitCount = %d.\n", LitCount ); + printf( "LitCount = %d.\n", LitCount ); + if ( fVerbose ) + Vec_IntPrint( p->vRootVars ); + //Vec_IntPrint( p->vRoots ); + //Vec_IntPrint( p->vAnds ); + //Vec_IntPrint( p->vLeaves ); } fKeepTrying = status == l_True ? fKeepTrying + 1 : 0; if ( fVerbose ) @@ -547,18 +608,30 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose ) } // update solution - Sbl_ManUpdateMapping( p ); - - Vec_IntFreeP( &pGia->vMapping ); - pGia->vMapping = Sbl_ManFromMapping( pGia, p->vMapping ); - + if ( Vec_IntSize(p->vSolCuts2) > 0 && Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) ) + { + Sbl_ManUpdateMapping( p ); + printf( "Object %d : Saved %d nodes. (Conf = %d.)\n", iPivot, Vec_IntSize(p->vSolCuts)-Vec_IntSize(p->vSolCuts2), nConfTotal ); + Sbl_ManStop( p ); + return 2; + } Sbl_ManStop( p ); return 1; } -void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nConfl, int fVerbose ) +void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nConfl, int fReverse, int fVerbose ) { - Sbl_ManTestSat( p, fVerbose ); + int iLut; + Gia_ManComputeOneWinStart( pGia, fReverse ); + Gia_ManForEachLut2( pGia, iLut ) + { +// if ( iLut > 259 ) +// break; + if ( Sbl_ManTestSat( pGia, nConfl, iLut, fVerbose ) != 2 ) + continue; +// break; + } + Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaSplit.c b/src/aig/gia/giaSplit.c index c2e2d448..8bb5d3c0 100644 --- a/src/aig/gia/giaSplit.c +++ b/src/aig/gia/giaSplit.c @@ -35,14 +35,16 @@ struct Spl_Man_t_ Gia_Man_t * pGia; // user AIG with nodes marked int iObj; // object ID int Limit; // limit on AIG nodes - int Count; // count of AIG nodes + int fReverse; // enable reverse search // intermediate Vec_Bit_t * vMarksCIO; // CI/CO marks Vec_Bit_t * vMarksIn; // input marks Vec_Bit_t * vMarksNo; // node marks - Vec_Int_t * vNodes; // nodes used in the window + Vec_Bit_t * vMarksAnd; // AND node marks Vec_Int_t * vRoots; // nodes pointing to Nodes + Vec_Int_t * vNodes; // nodes used in the window Vec_Int_t * vLeaves; // nodes pointed by Nodes + Vec_Int_t * vAnds; // AND nodes used in the window // temporary Vec_Int_t * vFanouts; // fanouts of the node Vec_Int_t * vCands; // candidate nodes @@ -55,7 +57,48 @@ struct Spl_Man_t_ /**Function************************************************************* - Synopsis [] + Synopsis [Transforming to the internal LUT representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Spl_ManToWecMapping( Gia_Man_t * p ) +{ + Vec_Wec_t * vMapping = Vec_WecStart( Gia_ManObjNum(p) ); + int Obj, Fanin, k; + assert( Gia_ManHasMapping(p) ); + Gia_ManForEachLut( p, Obj ) + Gia_LutForEachFanin( p, Obj, Fanin, k ) + Vec_WecPush( vMapping, Obj, Fanin ); + return vMapping; +} +Vec_Int_t * Spl_ManFromWecMapping( Gia_Man_t * p, Vec_Wec_t * vMap ) +{ + Vec_Int_t * vMapping, * vVec; int i, k, Obj; + assert( Gia_ManHasMapping2(p) ); + vMapping = Vec_IntAlloc( Gia_ManObjNum(p) + Vec_WecSizeSize(vMap) + 2*Vec_WecSizeUsed(vMap) ); + Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 ); + Vec_WecForEachLevel( vMap, vVec, i ) + if ( Vec_IntSize(vVec) > 0 ) + { + Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) ); + Vec_IntPush( vMapping, Vec_IntSize(vVec) ); + Vec_IntForEachEntry( vVec, Obj, k ) + Vec_IntPush( vMapping, Obj ); + Vec_IntPush( vMapping, i ); + } + assert( Vec_IntSize(vMapping) < 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) ); + return vMapping; +} + + +/**Function************************************************************* + + Synopsis [Creating manager.] Description [] @@ -64,45 +107,62 @@ struct Spl_Man_t_ SeeAlso [] ***********************************************************************/ -Spl_Man_t * Spl_ManAlloc( Gia_Man_t * pGia, int Limit ) +Spl_Man_t * Spl_ManAlloc( Gia_Man_t * pGia, int Limit, int fReverse ) { int i, iObj; Spl_Man_t * p = ABC_CALLOC( Spl_Man_t, 1 ); - assert( Gia_ManHasMapping(pGia) ); p->pGia = pGia; p->Limit = Limit; + p->fReverse = fReverse; // intermediate p->vMarksCIO = Vec_BitStart( Gia_ManObjNum(pGia) ); p->vMarksIn = Vec_BitStart( Gia_ManObjNum(pGia) ); p->vMarksNo = Vec_BitStart( Gia_ManObjNum(pGia) ); + p->vMarksAnd = Vec_BitStart( Gia_ManObjNum(pGia) ); p->vRoots = Vec_IntAlloc( 100 ); p->vNodes = Vec_IntAlloc( 100 ); p->vLeaves = Vec_IntAlloc( 100 ); + p->vAnds = Vec_IntAlloc( 100 ); // temporary p->vFanouts = Vec_IntAlloc( 100 ); p->vCands = Vec_IntAlloc( 100 ); p->vInputs = Vec_IntAlloc( 100 ); // mark CIs/COs + Vec_BitWriteEntry( p->vMarksCIO, 0, 1 ); Gia_ManForEachCiId( pGia, iObj, i ) Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 ); Gia_ManForEachCoId( pGia, iObj, i ) Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 ); - // prepare AIG - Gia_ManStaticFanoutStart( pGia ); - Gia_ManSetLutRefs( pGia ); + // mapping + ABC_FREE( pGia->pRefs ); Gia_ManCreateRefs( pGia ); + Gia_ManSetLutRefs( pGia ); + assert( Gia_ManHasMapping(pGia) ); + assert( !Gia_ManHasMapping2(pGia) ); + pGia->vMapping2 = Spl_ManToWecMapping( pGia ); + Vec_IntFreeP( &pGia->vMapping ); + // fanout + Gia_ManStaticFanoutStart( pGia ); return p; } void Spl_ManStop( Spl_Man_t * p ) { + // fanout Gia_ManStaticFanoutStop( p->pGia ); + // mapping + assert( !Gia_ManHasMapping(p->pGia) ); + assert( Gia_ManHasMapping2(p->pGia) ); + p->pGia->vMapping = Spl_ManFromWecMapping( p->pGia, p->pGia->vMapping2 ); + Vec_WecFreeP( &p->pGia->vMapping2 ); // intermediate Vec_BitFree( p->vMarksCIO ); Vec_BitFree( p->vMarksIn ); Vec_BitFree( p->vMarksNo ); + Vec_BitFree( p->vMarksAnd ); Vec_IntFree( p->vRoots ); Vec_IntFree( p->vNodes ); Vec_IntFree( p->vLeaves ); + Vec_IntFree( p->vAnds ); // temporary Vec_IntFree( p->vFanouts ); Vec_IntFree( p->vCands ); @@ -123,31 +183,55 @@ void Spl_ManStop( Spl_Man_t * p ) ***********************************************************************/ void Spl_ManWinFindLeavesRoots( Spl_Man_t * p ) { + Vec_Int_t * vVec; int iObj, iFan, i, k; // collect leaves +/* Vec_IntClear( p->vLeaves ); - Vec_IntForEachEntry( p->vNodes, iObj, i ) + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) { assert( Vec_BitEntry(p->vMarksNo, iObj) ); - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + Vec_IntForEachEntry( vVec, iFan, k ) if ( !Vec_BitEntry(p->vMarksNo, iFan) ) { Vec_BitWriteEntry(p->vMarksNo, iFan, 1); Vec_IntPush( p->vLeaves, iFan ); } } - Vec_IntForEachEntry( p->vLeaves, iObj, i ) - Vec_BitWriteEntry(p->vMarksNo, iObj, 0); + Vec_IntForEachEntry( p->vLeaves, iFan, i ) + Vec_BitWriteEntry(p->vMarksNo, iFan, 0); +*/ + Vec_IntClear( p->vLeaves ); + Vec_IntForEachEntry( p->vAnds, iObj, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); + assert( Vec_BitEntry(p->vMarksAnd, iObj) ); + iFan = Gia_ObjFaninId0( pObj, iObj ); + if ( !Vec_BitEntry(p->vMarksAnd, iFan) ) + { + Vec_BitWriteEntry(p->vMarksAnd, iFan, 1); + Vec_IntPush( p->vLeaves, iFan ); + } + iFan = Gia_ObjFaninId1( pObj, iObj ); + if ( !Vec_BitEntry(p->vMarksAnd, iFan) ) + { + Vec_BitWriteEntry(p->vMarksAnd, iFan, 1); + Vec_IntPush( p->vLeaves, iFan ); + } + } + Vec_IntForEachEntry( p->vLeaves, iFan, i ) + Vec_BitWriteEntry(p->vMarksAnd, iFan, 0); + // collect roots Vec_IntClear( p->vRoots ); - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) Gia_ObjLutRefDecId( p->pGia, iFan ); - Vec_IntForEachEntry( p->vNodes, iObj, i ) + Vec_IntForEachEntry( p->vAnds, iObj, i ) if ( Gia_ObjLutRefNumId(p->pGia, iObj) ) Vec_IntPush( p->vRoots, iObj ); - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) Gia_ObjLutRefIncId( p->pGia, iFan ); } @@ -170,7 +254,7 @@ void Spl_ManLutFanouts_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_B int iFanout, i; if ( Vec_BitEntry(vMarksNo, iObj) || Vec_BitEntry(vMarksCIO, iObj) ) return; - if ( Gia_ObjIsLut(p, iObj) ) + if ( Gia_ObjIsLut2(p, iObj) ) { Vec_BitWriteEntry( vMarksCIO, iObj, 1 ); Vec_IntPush( vFanouts, iObj ); @@ -182,7 +266,7 @@ void Spl_ManLutFanouts_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_B int Spl_ManLutFanouts( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_Bit_t * vMarksNo, Vec_Bit_t * vMarksCIO ) { int i, iFanout; - assert( Gia_ObjIsLut(p, iObj) ); + assert( Gia_ObjIsLut2(p, iObj) ); Vec_IntClear( vFanouts ); Gia_ObjForEachFanoutStaticId( p, iObj, iFanout, i ) Spl_ManLutFanouts_rec( p, iFanout, vFanouts, vMarksNo, vMarksCIO ); @@ -195,30 +279,7 @@ int Spl_ManLutFanouts( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_Bit_t /**Function************************************************************* - Synopsis [Compute MFFC size of one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj ) -{ - int Res, iFan, i; - assert( Gia_ObjIsLut(p, iObj) ); - Gia_LutForEachFanin( p, iObj, iFan, i ) - Gia_ObjRefIncId( p, iFan ); - Res = Gia_NodeMffcSize( p, Gia_ManObj(p, iObj) ); - Gia_LutForEachFanin( p, iObj, iFan, i ) - Gia_ObjRefDecId( p, iFan ); - return Res; -} - -/**Function************************************************************* - - Synopsis [Returns the number of fanins not beloning to the set.] + Synopsis [Returns the number of fanins beloning to the set.] Description [] @@ -229,8 +290,9 @@ int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj ) ***********************************************************************/ int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks ) { - int k, iFan, Count = 0; - Gia_LutForEachFanin( p, iObj, iFan, k ) + int i, iFan, Count = 0; + Vec_Int_t * vFanins = Gia_ObjLutFanins2(p, iObj); + Vec_IntForEachEntry( vFanins, iFan, i ) if ( Vec_BitEntry(vMarks, iFan) ) Count++; return Count; @@ -249,27 +311,46 @@ int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks ) ***********************************************************************/ int Spl_ManFindOne( Spl_Man_t * p ) { + Vec_Int_t * vVec; int nFanouts, iObj, iFan, i, k; int Res = 0, InCount, InCountMax = -1; Vec_IntClear( p->vCands ); Vec_IntClear( p->vInputs ); // deref - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) Gia_ObjLutRefDecId( p->pGia, iFan ); // consider LUT inputs - get one that has no refs - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) - if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) ) - { - if ( !Gia_ObjLutRefNumId(p->pGia, iFan) ) + if ( p->fReverse ) + { + Gia_ManForEachLut2VecReverse( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) + if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) ) { - Res = iFan; - goto finish; + if ( !Gia_ObjLutRefNumId(p->pGia, iFan) ) + { + Res = iFan; + goto finish; + } + Vec_IntPush( p->vCands, iFan ); + Vec_IntPush( p->vInputs, iFan ); } - Vec_IntPush( p->vCands, iFan ); - Vec_IntPush( p->vInputs, iFan ); - } + } + else + { + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) + if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) ) + { + if ( !Gia_ObjLutRefNumId(p->pGia, iFan) ) + { + Res = iFan; + goto finish; + } + Vec_IntPush( p->vCands, iFan ); + Vec_IntPush( p->vInputs, iFan ); + } + } // all inputs have refs - collect external nodes Vec_IntForEachEntry( p->vNodes, iObj, i ) @@ -277,7 +358,7 @@ int Spl_ManFindOne( Spl_Man_t * p ) if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 0 ) continue; assert( Gia_ObjLutRefNumId(p->pGia, iObj) > 0 ); - if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 ) + if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 ) // skip nodes with high fanout! continue; nFanouts = Spl_ManLutFanouts( p->pGia, iObj, p->vFanouts, p->vMarksNo, p->vMarksCIO ); if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 1 && nFanouts == 1 ) @@ -310,9 +391,9 @@ int Spl_ManFindOne( Spl_Man_t * p ) Res = Vec_IntEntry( p->vCands, 0 ); finish: - // deref - Vec_IntForEachEntry( p->vNodes, iObj, i ) - Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) + // ref + Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i ) + Vec_IntForEachEntry( vVec, iFan, k ) Gia_ObjLutRefIncId( p->pGia, iFan ); return Res; } @@ -321,7 +402,7 @@ finish: /**Function************************************************************* - Synopsis [] + Synopsis [Computing window for one pivot node.] Description [] @@ -330,50 +411,137 @@ finish: SeeAlso [] ***********************************************************************/ -void Spl_ManComputeOne( Spl_Man_t * p, int iPivot ) +int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj, Vec_Int_t * vTemp, Vec_Bit_t * vMarksAnd ) +{ + int iTemp, i, k = 0; + assert( Gia_ObjIsLut2(p, iObj) ); +//Vec_IntPrint( Gia_ObjLutFanins2(p, iObj) ); + Gia_ManIncrementTravId( p ); + Gia_ManCollectAnds( p, &iObj, 1, vTemp, Gia_ObjLutFanins2(p, iObj) ); + Vec_IntForEachEntry( vTemp, iTemp, i ) + if ( !Vec_BitEntry(vMarksAnd, iTemp) ) + Vec_IntWriteEntry( vTemp, k++, iTemp ); + Vec_IntShrink( vTemp, k ); + return k; +} +void Spl_ManAddNode( Spl_Man_t * p, int iPivot, Vec_Int_t * vCands ) +{ + int i, iObj; + Vec_IntPush( p->vNodes, iPivot ); + Vec_BitWriteEntry( p->vMarksNo, iPivot, 1 ); + Vec_IntAppend( p->vAnds, vCands ); + Vec_IntForEachEntry( vCands, iObj, i ) + Vec_BitWriteEntry( p->vMarksAnd, iObj, 1 ); +} +int Spl_ManComputeOne( Spl_Man_t * p, int iPivot ) { int CountAdd, iObj, i; - assert( Gia_ObjIsLut(p->pGia, iPivot) ); + assert( Gia_ObjIsLut2(p->pGia, iPivot) ); +//Gia_ManPrintCone2( p->pGia, Gia_ManObj(p->pGia, iPivot) ); // assume it was previously filled in Vec_IntForEachEntry( p->vNodes, iObj, i ) Vec_BitWriteEntry( p->vMarksNo, iObj, 0 ); + Vec_IntForEachEntry( p->vAnds, iObj, i ) + Vec_BitWriteEntry( p->vMarksAnd, iObj, 0 ); // double check that it is empty - //Gia_ManForEachLut( p->pGia, iObj ) + //Gia_ManForEachLut2( p->pGia, iObj ) // assert( !Vec_BitEntry(p->vMarksNo, iObj) ); + //Gia_ManForEachLut2( p->pGia, iObj ) + // assert( !Vec_BitEntry(p->vMarksAnd, iObj) ); + // clean arrays + Vec_IntClear( p->vNodes ); + Vec_IntClear( p->vAnds ); // add root node - Vec_IntFill( p->vNodes, 1, iPivot ); - Vec_BitWriteEntry( p->vMarksNo, iPivot, 1 ); + Spl_ManLutMffcSize( p->pGia, iPivot, p->vCands, p->vMarksAnd ); + Spl_ManAddNode( p, iPivot, p->vCands ); + if ( Vec_IntSize(p->vAnds) > p->Limit ) + return 0; //printf( "%d ", iPivot ); // add one node at a time - p->Count = Spl_ManLutMffcSize( p->pGia, iPivot ); while ( (iObj = Spl_ManFindOne(p)) ) { - assert( Gia_ObjIsLut(p->pGia, iObj) ); - CountAdd = Spl_ManLutMffcSize( p->pGia, iObj ); - if ( p->Count + CountAdd > p->Limit ) + assert( Gia_ObjIsLut2(p->pGia, iObj) ); + assert( !Vec_BitEntry(p->vMarksNo, iObj) ); + CountAdd = Spl_ManLutMffcSize( p->pGia, iObj, p->vCands, p->vMarksAnd ); + if ( Vec_IntSize(p->vAnds) + CountAdd > p->Limit ) break; - p->Count += CountAdd; - Vec_IntPush( p->vNodes, iObj ); - Vec_BitWriteEntry( p->vMarksNo, iObj, 1 ); + Spl_ManAddNode( p, iObj, p->vCands ); //printf( "+%d ", iObj ); } //printf( "\n" ); Vec_IntSort( p->vNodes, 0 ); + Vec_IntSort( p->vAnds, 0 ); + Spl_ManWinFindLeavesRoots( p ); + Vec_IntSort( p->vLeaves, 0 ); + Vec_IntSort( p->vRoots, 0 ); + return 1; } +/**Function************************************************************* + + Synopsis [External procedures.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManComputeOneWin( Gia_Man_t * pGia, int iPivot, Vec_Int_t ** pvRoots, Vec_Int_t ** pvNodes, Vec_Int_t ** pvLeaves, Vec_Int_t ** pvAnds ) +{ + Spl_Man_t * p = (Spl_Man_t *)pGia->pSatlutWinman; + assert( p != NULL ); + if ( iPivot == -1 ) + { + Spl_ManStop( p ); + pGia->pSatlutWinman = NULL; + return 0; + } + if ( !Spl_ManComputeOne( p, iPivot ) ) + { + *pvRoots = NULL; + *pvNodes = NULL; + *pvLeaves = NULL; + *pvAnds = NULL; + return 0; + } + *pvRoots = p->vRoots; + *pvNodes = p->vNodes; + *pvLeaves = p->vLeaves; + *pvAnds = p->vAnds; + // Vec_IntPrint( p->vNodes ); + return Vec_IntSize(p->vAnds); +} +void Gia_ManComputeOneWinStart( Gia_Man_t * pGia, int fReverse ) +{ + assert( pGia->pSatlutWinman == NULL ); + pGia->pSatlutWinman = Spl_ManAlloc( pGia, 64, fReverse ); +} + +/**Function************************************************************* + + Synopsis [Testing procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Spl_ManComputeOneTest( Gia_Man_t * pGia ) { - int iLut; - Spl_Man_t * p = Spl_ManAlloc( pGia, 64 ); - Gia_ManForEachLut( pGia, iLut ) + int iLut, Count; + Gia_ManComputeOneWinStart( pGia, 0 ); + Gia_ManForEachLut2( pGia, iLut ) { - Spl_ManComputeOne( p, iLut ); - Spl_ManWinFindLeavesRoots( p ); - // Vec_IntPrint( p->vNodes ); + Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds; + Count = Gia_ManComputeOneWin( pGia, iLut, &vRoots, &vNodes, &vLeaves, &vAnds ); printf( "Obj = %6d : Leaf = %2d. Node = %2d. Root = %2d. AND = %3d.\n", - iLut, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vRoots), p->Count ); + iLut, Vec_IntSize(vLeaves), Vec_IntSize(vNodes), Vec_IntSize(vRoots), Count ); } - Spl_ManStop( p ); + Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL ); } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3