diff options
Diffstat (limited to 'src/aig/dar/darLib.c')
| -rw-r--r-- | src/aig/dar/darLib.c | 268 |
1 files changed, 221 insertions, 47 deletions
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c index fce6155b..c3d57b52 100644 --- a/src/aig/dar/darLib.c +++ b/src/aig/dar/darLib.c @@ -44,7 +44,7 @@ struct Dar_LibDat_t_ // library object data Aig_Obj_t * pFunc; // the corresponding AIG node if it exists int Level; // level of this node after it is constructured int TravId; // traversal ID of the library object data - unsigned char Area; // area of the node + unsigned char fMffc; // set to one if node is part of MFFC unsigned char nLats[3]; // the number of latches on the input/output stem }; @@ -54,9 +54,6 @@ struct Dar_Lib_t_ // library Dar_LibObj_t * pObjs; // the set of library objects int nObjs; // the number of objects used int iObj; // the current object - // object data - Dar_LibDat_t * pDatas; - int nDatas; // structures by class int nSubgr[222]; // the number of subgraphs by class int * pSubgr[222]; // the subgraphs for each class @@ -75,8 +72,24 @@ struct Dar_Lib_t_ // library int nNodes[222]; // the number of nodes by class int * pNodes[222]; // the nodes for each class int * pNodesMem; // memory for nodes pointers - int pNodesTotal; // the total number of nodes - // information by NPN classes + int nNodesTotal; // the total number of nodes + // prepared library + int nSubgraphs; + int nNodes0Max; + // nodes by class + int nNodes0[222]; // the number of nodes by class + int * pNodes0[222]; // the nodes for each class + int * pNodes0Mem; // memory for nodes pointers + int nNodes0Total; // the total number of nodes + // structures by class + int nSubgr0[222]; // the number of subgraphs by class + int * pSubgr0[222]; // the subgraphs for each class + int * pSubgr0Mem; // memory for subgraph pointers + int nSubgr0Total; // the total number of subgraph + // object data + Dar_LibDat_t * pDatas; + int nDatas; + // information about NPN classes char ** pPerms4; unsigned short * puCanons; char * pPhases; @@ -104,7 +117,7 @@ static inline int Dar_LibObjTruth( Dar_LibObj_t * pObj ) { return pOb SeeAlso [] ***********************************************************************/ -Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas ) +Dar_Lib_t * Dar_LibAlloc( int nObjs ) { unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 }; Dar_Lib_t * p; @@ -115,10 +128,6 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas ) p->nObjs = nObjs; p->pObjs = ALLOC( Dar_LibObj_t, nObjs ); memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs ); - // allocate datas - p->nDatas = nDatas; - p->pDatas = ALLOC( Dar_LibDat_t, nDatas ); - memset( p->pObjs, 0, sizeof(Dar_LibDat_t) * nDatas ); // allocate canonical data p->pPerms4 = Extra_Permutations( 4 ); Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap ); @@ -149,7 +158,9 @@ void Dar_LibFree( Dar_Lib_t * p ) free( p->pObjs ); free( p->pDatas ); free( p->pNodesMem ); + free( p->pNodes0Mem ); free( p->pSubgrMem ); + free( p->pSubgr0Mem ); free( p->pPriosMem ); FREE( p->pPlaceMem ); FREE( p->pScoreMem ); @@ -163,6 +174,31 @@ void Dar_LibFree( Dar_Lib_t * p ) /**Function************************************************************* + Synopsis [Returns canonical truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibReturnCanonicals( unsigned * pCanons ) +{ + int Visits[222] = {0}; + int i, k; + // find canonical truth tables + for ( i = k = 0; i < (1<<16); i++ ) + if ( !Visits[s_DarLib->pMap[i]] ) + { + Visits[s_DarLib->pMap[i]] = 1; + pCanons[k++] = ((i<<16) | i); + } + assert( k == 222 ); +} + +/**Function************************************************************* + Synopsis [Adds one AND to the library.] Description [] @@ -196,14 +232,14 @@ void Dar_LibAddNode( Dar_Lib_t * p, int Id0, int Id1, int fCompl0, int fCompl1 ) SeeAlso [] ***********************************************************************/ -void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class ) +void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect ) { if ( pObj->fTerm || (int)pObj->Num == Class ) return; pObj->Num = Class; - Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class ); - Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class ); - if ( p->pNodesMem ) + Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect ); + Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect ); + if ( fCollect ) p->pNodes[Class][ p->nNodes[Class]++ ] = pObj-p->pObjs; else p->nNodes[Class]++; @@ -239,10 +275,12 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) } // allocate memory for the roots of each class p->pSubgrMem = ALLOC( int, Vec_IntSize(vOuts) ); + p->pSubgr0Mem = ALLOC( int, Vec_IntSize(vOuts) ); p->nSubgrTotal = 0; for ( i = 0; i < 222; i++ ) { p->pSubgr[i] = p->pSubgrMem + p->nSubgrTotal; + p->pSubgr0[i] = p->pSubgr0Mem + p->nSubgrTotal; p->nSubgrTotal += p->nSubgr[i]; p->nSubgr[i] = 0; } @@ -321,18 +359,20 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) // count nodes in each class for ( i = 0; i < 222; i++ ) for ( k = 0; k < p->nSubgr[i]; k++ ) - Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i ); + Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 0 ); // count the total number of nodes - p->pNodesTotal = 0; + p->nNodesTotal = 0; for ( i = 0; i < 222; i++ ) - p->pNodesTotal += p->nNodes[i]; + p->nNodesTotal += p->nNodes[i]; // allocate memory for the nodes of each class - p->pNodesMem = ALLOC( int, p->pNodesTotal ); - p->pNodesTotal = 0; + p->pNodesMem = ALLOC( int, p->nNodesTotal ); + p->pNodes0Mem = ALLOC( int, p->nNodesTotal ); + p->nNodesTotal = 0; for ( i = 0; i < 222; i++ ) { - p->pNodes[i] = p->pNodesMem + p->pNodesTotal; - p->pNodesTotal += p->nNodes[i]; + p->pNodes[i] = p->pNodesMem + p->nNodesTotal; + p->pNodes0[i] = p->pNodes0Mem + p->nNodesTotal; + p->nNodesTotal += p->nNodes[i]; p->nNodes[i] = 0; } // create traversal IDs @@ -343,11 +383,11 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) for ( i = 0; i < 222; i++ ) { for ( k = 0; k < p->nSubgr[i]; k++ ) - Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i ); + Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 1 ); nNodesTotal += p->nNodes[i]; //printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] ); } - assert( nNodesTotal == p->pNodesTotal ); + assert( nNodesTotal == p->nNodesTotal ); // prepare the number of the PI nodes for ( i = 0; i < 4; i++ ) Dar_LibObj(p, i)->Num = i; @@ -355,6 +395,133 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) /**Function************************************************************* + Synopsis [Starts the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibCreateData( Dar_Lib_t * p, int nDatas ) +{ + if ( p->nDatas == nDatas ) + return; + FREE( p->pDatas ); + // allocate datas + p->nDatas = nDatas; + p->pDatas = ALLOC( Dar_LibDat_t, nDatas ); + memset( p->pDatas, 0, sizeof(Dar_LibDat_t) * nDatas ); +} + +/**Function************************************************************* + + Synopsis [Adds one AND to the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibSetup0_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect ) +{ + if ( pObj->fTerm || (int)pObj->Num == Class ) + return; + pObj->Num = Class; + Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect ); + Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect ); + if ( fCollect ) + p->pNodes0[Class][ p->nNodes0[Class]++ ] = pObj-p->pObjs; + else + p->nNodes0[Class]++; +} + +/**Function************************************************************* + + Synopsis [Starts the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibPrepare( int nSubgraphs ) +{ + Dar_Lib_t * p = s_DarLib; + int i, k, nNodes0Total; + if ( p->nSubgraphs == nSubgraphs ) + return; + + // favor special classes: + // 1 : F = (!d*!c*!b*!a) + // 4 : F = (!d*!c*!(b*a)) + // 12 : F = (!d*!(c*!(!b*!a))) + // 20 : F = (!d*!(c*b*a)) + + // set the subgraph counters + p->nSubgr0Total = 0; + for ( i = 0; i < 222; i++ ) + { +// if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes + if ( i == 1 ) // special classes + p->nSubgr0[i] = p->nSubgr[i]; + else + p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs ); + p->nSubgr0Total += p->nSubgr0[i]; + for ( k = 0; k < p->nSubgr0[i]; k++ ) + p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ]; + } + + // count the number of nodes + // clean node counters + for ( i = 0; i < 222; i++ ) + p->nNodes0[i] = 0; + // create traversal IDs + for ( i = 0; i < p->iObj; i++ ) + Dar_LibObj(p, i)->Num = 0xff; + // count nodes in each class + // count the total number of nodes and the largest class + p->nNodes0Total = 0; + p->nNodes0Max = 0; + for ( i = 0; i < 222; i++ ) + { + for ( k = 0; k < p->nSubgr0[i]; k++ ) + Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 ); + p->nNodes0Total += p->nNodes0[i]; + p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] ); + } + + // clean node counters + for ( i = 0; i < 222; i++ ) + p->nNodes0[i] = 0; + // create traversal IDs + for ( i = 0; i < p->iObj; i++ ) + Dar_LibObj(p, i)->Num = 0xff; + // add the nodes to storage + nNodes0Total = 0; + for ( i = 0; i < 222; i++ ) + { + for ( k = 0; k < p->nSubgr0[i]; k++ ) + Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 ); + nNodes0Total += p->nNodes0[i]; + } + assert( nNodes0Total == p->nNodes0Total ); + // prepare the number of the PI nodes + for ( i = 0; i < 4; i++ ) + Dar_LibObj(p, i)->Num = i; + + // realloc the datas + Dar_LibCreateData( p, p->nNodes0Max + 32 ); + // allocated more because Dar_LibBuildBest() sometimes requires more entries +} + +/**Function************************************************************* + Synopsis [Reads library from array.] Description [] @@ -374,7 +541,7 @@ Dar_Lib_t * Dar_LibRead() vOuts = Dar_LibReadOuts(); vPrios = Dar_LibReadPrios(); // create library - p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4, 6000 ); + p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4 ); // create nodes for ( i = 0; i < vObjs->nSize; i += 2 ) Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1, @@ -383,6 +550,7 @@ Dar_Lib_t * Dar_LibRead() Dar_LibSetup( p, vOuts, vPrios ); Vec_IntFree( vObjs ); Vec_IntFree( vOuts ); + Vec_IntFree( vPrios ); return p; } @@ -670,15 +838,20 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) Dar_LibDat_t * pData, * pData0, * pData1; Aig_Obj_t * pGhost, * pFanin0, * pFanin1; int i; - for ( i = 0; i < s_DarLib->nNodes[Class]; i++ ) + for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ ) { // get one class node, assign its temporary number and set its data - pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes[Class][i]); + pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]); pObj->Num = 4 + i; + assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 ); pData = s_DarLib->pDatas + pObj->Num; + pData->fMffc = 0; pData->pFunc = NULL; pData->TravId = 0xFFFF; + // explore the fanins + assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 ); + assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 ); pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num; pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num; pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level); @@ -704,9 +877,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class ) // clear the node if it is part of MFFC if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) ) - pData->pFunc = NULL; -//if ( Class == 7 ) -//printf( "Evaling node %d at data %d\n", pData->pFunc? pData->pFunc->Id : -1, pObj->Num ); + pData->fMffc = 1; } } @@ -729,20 +900,22 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required return 0; assert( pObj->Num > 3 ); pData = s_DarLib->pDatas + pObj->Num; - if ( pData->pFunc ) + if ( pData->pFunc && !pData->fMffc ) return 0; if ( pData->Level > Required ) return 0xff; if ( pData->TravId == Out ) - return pData->Area; + return 0; pData->TravId = Out; - Area = 1 + Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required ); + // this is a new node - get a bound on the area of its branches + nNodesSaved--; + Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1 ); if ( Area > nNodesSaved ) - return pData->Area = 0xff; - Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required ); + return 0xff; + Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1 ); if ( Area > nNodesSaved ) - return pData->Area = 0xff; - return pData->Area = Area; + return 0xff; + return Area + 1; } /**Function************************************************************* @@ -773,25 +946,27 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir Class = s_DarLib->pMap[pCut->uTruth]; Dar_LibEvalAssignNums( p, Class ); // profile outputs by their savings - p->nTotalSubgs += s_DarLib->nSubgr[Class]; - p->ClassSubgs[Class] += s_DarLib->nSubgr[Class]; - for ( Out = 0; Out < s_DarLib->nSubgr[Class]; Out++ ) + p->nTotalSubgs += s_DarLib->nSubgr0[Class]; + p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class]; + for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ ) { - pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr[Class][Out]); - nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved, Required ); + pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]); + if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot ) + continue; + nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required ); nNodesGained = nNodesSaved - nNodesAdded; if ( fTraining && nNodesGained >= 0 ) Dar_LibIncrementScore( Class, Out, nNodesGained + 1 ); - if ( nNodesGained <= 0 ) + if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) ) continue; - if ( nNodesGained < p->GainBest || - (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->GainBest) ) + if ( nNodesGained < p->GainBest || + (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) ) continue; // remember this possibility Vec_PtrClear( p->vLeavesBest ); for ( k = 0; k < (int)pCut->nLeaves; k++ ) Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc ); - p->OutBest = s_DarLib->pSubgr[Class][Out]; + p->OutBest = s_DarLib->pSubgr0[Class][Out]; p->OutNumBest = Out; p->LevelBest = s_DarLib->pDatas[pObj->Num].Level; p->GainBest = nNodesGained; @@ -845,7 +1020,6 @@ Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj ) pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 ); pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 ); pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 ); -//printf( "Adding node %d for data %d\n", pData->pFunc->Id, pObj->Num ); return pData->pFunc; } |