diff options
Diffstat (limited to 'src/opt/dar/darLib.c')
| -rw-r--r-- | src/opt/dar/darLib.c | 1339 |
1 files changed, 1339 insertions, 0 deletions
diff --git a/src/opt/dar/darLib.c b/src/opt/dar/darLib.c new file mode 100644 index 00000000..2d047404 --- /dev/null +++ b/src/opt/dar/darLib.c @@ -0,0 +1,1339 @@ +/**CFile**************************************************************** + + FileName [darLib.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting.] + + Synopsis [Library of AIG subgraphs used for rewriting.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: darLib.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "darInt.h" +#include "src/aig/gia/gia.h" +#include "dar.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Dar_Lib_t_ Dar_Lib_t; +typedef struct Dar_LibObj_t_ Dar_LibObj_t; +typedef struct Dar_LibDat_t_ Dar_LibDat_t; + +struct Dar_LibObj_t_ // library object (2 words) +{ + unsigned Fan0 : 16; // the first fanin + unsigned Fan1 : 16; // the second fanin + unsigned fCompl0 : 1; // the first compl attribute + unsigned fCompl1 : 1; // the second compl attribute + unsigned fPhase : 1; // the phase of the node + unsigned fTerm : 1; // indicates a PI + unsigned Num : 28; // internal use +}; + +struct Dar_LibDat_t_ // library object data +{ + union { + Aig_Obj_t * pFunc; // the corresponding AIG node if it exists + int iGunc; }; // 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 + float dProb; // probability of the node being 1 + 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 +}; + +struct Dar_Lib_t_ // library +{ + // objects + Dar_LibObj_t * pObjs; // the set of library objects + int nObjs; // the number of objects used + int iObj; // the current object + // structures by class + int nSubgr[222]; // the number of subgraphs by class + int * pSubgr[222]; // the subgraphs for each class + int * pSubgrMem; // memory for subgraph pointers + int nSubgrTotal; // the total number of subgraph + // structure priorities + int * pPriosMem; // memory for priority of structures + int * pPrios[222]; // pointers to the priority numbers + // structure places in the priorities + int * pPlaceMem; // memory for places of structures in the priority lists + int * pPlace[222]; // pointers to the places numbers + // structure scores + int * pScoreMem; // memory for scores of structures + int * pScore[222]; // pointers to the scores numbers + // nodes by class + int nNodes[222]; // the number of nodes by class + int * pNodes[222]; // the nodes for each class + int * pNodesMem; // memory for nodes pointers + 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; + char * pPerms; + unsigned char * pMap; +}; + +static Dar_Lib_t * s_DarLib = NULL; + +static inline Dar_LibObj_t * Dar_LibObj( Dar_Lib_t * p, int Id ) { return p->pObjs + Id; } +static inline int Dar_LibObjTruth( Dar_LibObj_t * pObj ) { return pObj->Num < (0xFFFF & ~pObj->Num) ? pObj->Num : (0xFFFF & ~pObj->Num); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dar_Lib_t * Dar_LibAlloc( int nObjs ) +{ + unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 }; + Dar_Lib_t * p; + int i;//, clk = clock(); + p = ABC_ALLOC( Dar_Lib_t, 1 ); + memset( p, 0, sizeof(Dar_Lib_t) ); + // allocate objects + p->nObjs = nObjs; + p->pObjs = ABC_ALLOC( Dar_LibObj_t, nObjs ); + memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs ); + // allocate canonical data + p->pPerms4 = Dar_Permutations( 4 ); + Dar_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap ); + // start the elementary objects + p->iObj = 4; + for ( i = 0; i < 4; i++ ) + { + p->pObjs[i].fTerm = 1; + p->pObjs[i].Num = uTruths[i]; + } +// ABC_PRT( "Library start", clock() - clk ); + return p; +} + +/**Function************************************************************* + + Synopsis [Frees the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibFree( Dar_Lib_t * p ) +{ + ABC_FREE( p->pObjs ); + ABC_FREE( p->pDatas ); + ABC_FREE( p->pNodesMem ); + ABC_FREE( p->pNodes0Mem ); + ABC_FREE( p->pSubgrMem ); + ABC_FREE( p->pSubgr0Mem ); + ABC_FREE( p->pPriosMem ); + ABC_FREE( p->pPlaceMem ); + ABC_FREE( p->pScoreMem ); + ABC_FREE( p->pPerms4 ); + ABC_FREE( p->puCanons ); + ABC_FREE( p->pPhases ); + ABC_FREE( p->pPerms ); + ABC_FREE( p->pMap ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Returns canonical truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_LibReturnClass( unsigned uTruth ) +{ + return s_DarLib->pMap[uTruth & 0xffff]; +} + + +/**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 [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibAddNode( Dar_Lib_t * p, int Id0, int Id1, int fCompl0, int fCompl1 ) +{ + Dar_LibObj_t * pFan0 = Dar_LibObj( p, Id0 ); + Dar_LibObj_t * pFan1 = Dar_LibObj( p, Id1 ); + Dar_LibObj_t * pObj = p->pObjs + p->iObj++; + pObj->Fan0 = Id0; + pObj->Fan1 = Id1; + pObj->fCompl0 = fCompl0; + pObj->fCompl1 = fCompl1; + pObj->fPhase = (fCompl0 ^ pFan0->fPhase) & (fCompl1 ^ pFan1->fPhase); + pObj->Num = 0xFFFF & (fCompl0? ~pFan0->Num : pFan0->Num) & (fCompl1? ~pFan1->Num : pFan1->Num); +} + +/**Function************************************************************* + + Synopsis [Adds one AND to the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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, 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]++; +} + +/**Function************************************************************* + + Synopsis [Adds one AND to the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios ) +{ + int fTraining = 0; + Dar_LibObj_t * pObj; + int nNodesTotal, uTruth, Class, Out, i, k; + assert( p->iObj == p->nObjs ); + + // count the number of representatives of each class + for ( i = 0; i < 222; i++ ) + p->nSubgr[i] = p->nNodes[i] = 0; + Vec_IntForEachEntry( vOuts, Out, i ) + { + pObj = Dar_LibObj( p, Out ); + uTruth = Dar_LibObjTruth( pObj ); + Class = p->pMap[uTruth]; + p->nSubgr[Class]++; + } + // allocate memory for the roots of each class + p->pSubgrMem = ABC_ALLOC( int, Vec_IntSize(vOuts) ); + p->pSubgr0Mem = ABC_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; + } + assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); + // add the outputs to storage + Vec_IntForEachEntry( vOuts, Out, i ) + { + pObj = Dar_LibObj( p, Out ); + uTruth = Dar_LibObjTruth( pObj ); + Class = p->pMap[uTruth]; + p->pSubgr[Class][ p->nSubgr[Class]++ ] = Out; + } + + if ( fTraining ) + { + // allocate memory for the priority of roots of each class + p->pPriosMem = ABC_ALLOC( int, Vec_IntSize(vOuts) ); + p->nSubgrTotal = 0; + for ( i = 0; i < 222; i++ ) + { + p->pPrios[i] = p->pPriosMem + p->nSubgrTotal; + p->nSubgrTotal += p->nSubgr[i]; + for ( k = 0; k < p->nSubgr[i]; k++ ) + p->pPrios[i][k] = k; + + } + assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); + + // allocate memory for the priority of roots of each class + p->pPlaceMem = ABC_ALLOC( int, Vec_IntSize(vOuts) ); + p->nSubgrTotal = 0; + for ( i = 0; i < 222; i++ ) + { + p->pPlace[i] = p->pPlaceMem + p->nSubgrTotal; + p->nSubgrTotal += p->nSubgr[i]; + for ( k = 0; k < p->nSubgr[i]; k++ ) + p->pPlace[i][k] = k; + + } + assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); + + // allocate memory for the priority of roots of each class + p->pScoreMem = ABC_ALLOC( int, Vec_IntSize(vOuts) ); + p->nSubgrTotal = 0; + for ( i = 0; i < 222; i++ ) + { + p->pScore[i] = p->pScoreMem + p->nSubgrTotal; + p->nSubgrTotal += p->nSubgr[i]; + for ( k = 0; k < p->nSubgr[i]; k++ ) + p->pScore[i][k] = 0; + + } + assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); + } + else + { + int Counter = 0; + // allocate memory for the priority of roots of each class + p->pPriosMem = ABC_ALLOC( int, Vec_IntSize(vOuts) ); + p->nSubgrTotal = 0; + for ( i = 0; i < 222; i++ ) + { + p->pPrios[i] = p->pPriosMem + p->nSubgrTotal; + p->nSubgrTotal += p->nSubgr[i]; + for ( k = 0; k < p->nSubgr[i]; k++ ) + p->pPrios[i][k] = Vec_IntEntry(vPrios, Counter++); + + } + assert( p->nSubgrTotal == Vec_IntSize(vOuts) ); + assert( Counter == Vec_IntSize(vPrios) ); + } + + // create traversal IDs + for ( i = 0; i < p->iObj; i++ ) + Dar_LibObj(p, i)->Num = 0xff; + // 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, 0 ); + // count the total number of nodes + p->nNodesTotal = 0; + for ( i = 0; i < 222; i++ ) + p->nNodesTotal += p->nNodes[i]; + // allocate memory for the nodes of each class + p->pNodesMem = ABC_ALLOC( int, p->nNodesTotal ); + p->pNodes0Mem = ABC_ALLOC( int, p->nNodesTotal ); + p->nNodesTotal = 0; + for ( i = 0; i < 222; 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 + for ( i = 0; i < p->iObj; i++ ) + Dar_LibObj(p, i)->Num = 0xff; + // add the nodes to storage + nNodesTotal = 0; + 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, 1 ); + nNodesTotal += p->nNodes[i]; +//printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] ); + } + assert( nNodesTotal == p->nNodesTotal ); + // prepare the number of the PI nodes + for ( i = 0; i < 4; i++ ) + Dar_LibObj(p, i)->Num = i; +} + +/**Function************************************************************* + + Synopsis [Starts the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibCreateData( Dar_Lib_t * p, int nDatas ) +{ + if ( p->nDatas == nDatas ) + return; + ABC_FREE( p->pDatas ); + // allocate datas + p->nDatas = nDatas; + p->pDatas = ABC_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] = Abc_MinInt( 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 = Abc_MaxInt( 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 [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dar_Lib_t * Dar_LibRead() +{ + Vec_Int_t * vObjs, * vOuts, * vPrios; + Dar_Lib_t * p; + int i; + // read nodes and outputs + vObjs = Dar_LibReadNodes(); + vOuts = Dar_LibReadOuts(); + vPrios = Dar_LibReadPrios(); + // create library + 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, + vObjs->pArray[i] & 1, vObjs->pArray[i+1] & 1 ); + // create outputs + Dar_LibSetup( p, vOuts, vPrios ); + Vec_IntFree( vObjs ); + Vec_IntFree( vOuts ); + Vec_IntFree( vPrios ); + return p; +} + +/**Function************************************************************* + + Synopsis [Starts the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibStart() +{ +// int clk = clock(); + assert( s_DarLib == NULL ); + s_DarLib = Dar_LibRead(); +// printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal ); +// ABC_PRT( "Time", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [Stops the library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibStop() +{ + assert( s_DarLib != NULL ); + Dar_LibFree( s_DarLib ); + s_DarLib = NULL; +} + +/**Function************************************************************* + + Synopsis [Updates the score of the class and adjusts the priority of this class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibIncrementScore( int Class, int Out, int Gain ) +{ + int * pPrios = s_DarLib->pPrios[Class]; // pPrios[i] = Out + int * pPlace = s_DarLib->pPlace[Class]; // pPlace[Out] = i + int * pScore = s_DarLib->pScore[Class]; // score of Out + int Out2; + assert( Class >= 0 && Class < 222 ); + assert( Out >= 0 && Out < s_DarLib->nSubgr[Class] ); + assert( pPlace[pPrios[Out]] == Out ); + // increment the score + pScore[Out] += Gain; + // move the out in the order + while ( pPlace[Out] > 0 && pScore[Out] > pScore[ pPrios[pPlace[Out]-1] ] ) + { + // get the previous output in the priority list + Out2 = pPrios[pPlace[Out]-1]; + // swap Out and Out2 + pPlace[Out]--; + pPlace[Out2]++; + pPrios[pPlace[Out]] = Out; + pPrios[pPlace[Out2]] = Out2; + } +} + +/**Function************************************************************* + + Synopsis [Prints out the priorities into the file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibDumpPriorities() +{ + int i, k, Out, Out2, Counter = 0, Printed = 0; + printf( "\nOutput priorities (total = %d):\n", s_DarLib->nSubgrTotal ); + for ( i = 0; i < 222; i++ ) + { +// printf( "Class%d: ", i ); + for ( k = 0; k < s_DarLib->nSubgr[i]; k++ ) + { + Out = s_DarLib->pPrios[i][k]; + Out2 = k == 0 ? Out : s_DarLib->pPrios[i][k-1]; + assert( s_DarLib->pScore[i][Out2] >= s_DarLib->pScore[i][Out] ); +// printf( "%d(%d), ", Out, s_DarLib->pScore[i][Out] ); + printf( "%d, ", Out ); + Printed++; + if ( ++Counter == 15 ) + { + printf( "\n" ); + Counter = 0; + } + } + } + printf( "\n" ); + assert( Printed == s_DarLib->nSubgrTotal ); +} + + +/**Function************************************************************* + + Synopsis [Matches the cut with its canonical form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_LibCutMatch( Dar_Man_t * p, Dar_Cut_t * pCut ) +{ + Aig_Obj_t * pFanin; + unsigned uPhase; + char * pPerm; + int i; + assert( pCut->nLeaves == 4 ); + // get the fanin permutation + uPhase = s_DarLib->pPhases[pCut->uTruth]; + pPerm = s_DarLib->pPerms4[ (int)s_DarLib->pPerms[pCut->uTruth] ]; + // collect fanins with the corresponding permutation/phase + for ( i = 0; i < (int)pCut->nLeaves; i++ ) + { + pFanin = Aig_ManObj( p->pAig, pCut->pLeaves[ (int)pPerm[i] ] ); + if ( pFanin == NULL ) + { + p->nCutsBad++; + return 0; + } + pFanin = Aig_NotCond(pFanin, ((uPhase >> i) & 1) ); + s_DarLib->pDatas[i].pFunc = pFanin; + s_DarLib->pDatas[i].Level = Aig_Regular(pFanin)->Level; + // copy the propability of node being one + if ( p->pPars->fPower ) + { + float Prob = Abc_Int2Float( Vec_IntEntry( p->pAig->vProbs, Aig_ObjId(Aig_Regular(pFanin)) ) ); + s_DarLib->pDatas[i].dProb = Aig_IsComplement(pFanin)? 1.0-Prob : Prob; + } + } + p->nCutsGood++; + return 1; +} + + + +/**Function************************************************************* + + Synopsis [Marks the MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves, float * pPower ) +{ + int i, nNodes; + // mark the cut leaves + for ( i = 0; i < nLeaves; i++ ) + Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++; + // label MFFC with current ID + nNodes = Aig_NodeMffcLabel( p, pRoot, pPower ); + // unmark the cut leaves + for ( i = 0; i < nLeaves; i++ ) + Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--; + return nNodes; +} + +/**Function************************************************************* + + Synopsis [Evaluates one cut.] + + Description [Returns the best gain.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibObjPrint_rec( Dar_LibObj_t * pObj ) +{ + if ( pObj->fTerm ) + { + printf( "%c", 'a' + (int)(pObj - s_DarLib->pObjs) ); + return; + } + printf( "(" ); + Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan0) ); + if ( pObj->fCompl0 ) + printf( "\'" ); + Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan1) ); + if ( pObj->fCompl0 ) + printf( "\'" ); + printf( ")" ); +} + + +/**Function************************************************************* + + Synopsis [Assigns numbers to the nodes of one class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot ) +{ + Dar_LibObj_t * pObj; + Dar_LibDat_t * pData, * pData0, * pData1; + Aig_Obj_t * pFanin0, * pFanin1; + int 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->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 + Abc_MaxInt(pData0->Level, pData1->Level); + if ( pData0->pFunc == NULL || pData1->pFunc == NULL ) + continue; + pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 ); + pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 ); + if ( Aig_Regular(pFanin0) == pRoot || Aig_Regular(pFanin1) == pRoot ) + continue; + pData->pFunc = Aig_TableLookupTwo( p->pAig, pFanin0, pFanin1 ); + if ( pData->pFunc ) + { + // update the level to be more accurate + pData->Level = Aig_Regular(pData->pFunc)->Level; + // mark the node if it is part of MFFC + pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, Aig_Regular(pData->pFunc)); + // assign the probability + if ( p->pPars->fPower ) + { + float Prob = Abc_Int2Float( Vec_IntEntry( p->pAig->vProbs, Aig_ObjId(Aig_Regular(pData->pFunc)) ) ); + pData->dProb = Aig_IsComplement(pData->pFunc)? 1.0-Prob : Prob; + } + } + } +} + +/**Function************************************************************* + + Synopsis [Evaluates one cut.] + + Description [Returns the best gain.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required, float * pPower ) +{ + Dar_LibDat_t * pData; + float Power0, Power1; + int Area; + if ( pPower ) + *pPower = (float)0.0; + pData = s_DarLib->pDatas + pObj->Num; + if ( pData->TravId == Out ) + return 0; + pData->TravId = Out; + if ( pObj->fTerm ) + { + if ( pPower ) + *pPower = pData->dProb; + return 0; + } + assert( pObj->Num > 3 ); + if ( pData->Level > Required ) + return 0xff; + if ( pData->pFunc && !pData->fMffc ) + { + if ( pPower ) + *pPower = pData->dProb; + return 0; + } + // 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, pPower? &Power0 : NULL ); + if ( Area > nNodesSaved ) + return 0xff; + Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1, pPower? &Power1 : NULL ); + if ( Area > nNodesSaved ) + return 0xff; + if ( pPower ) + { + Dar_LibDat_t * pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num; + Dar_LibDat_t * pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num; + pData->dProb = (pObj->fCompl0? 1.0 - pData0->dProb : pData0->dProb)* + (pObj->fCompl1? 1.0 - pData1->dProb : pData1->dProb); + *pPower = Power0 + 2.0 * pData0->dProb * (1.0 - pData0->dProb) + + Power1 + 2.0 * pData1->dProb * (1.0 - pData1->dProb); + } + return Area + 1; +} + +/**Function************************************************************* + + Synopsis [Evaluates one cut.] + + Description [Returns the best gain.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required, int * pnMffcSize ) +{ + int fTraining = 0; + float PowerSaved, PowerAdded; + Dar_LibObj_t * pObj; + int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk; + clk = clock(); + if ( pCut->nLeaves != 4 ) + return; + // check if the cut exits and assigns leaves and their levels + if ( !Dar_LibCutMatch(p, pCut) ) + return; + // mark MFFC of the node + nNodesSaved = Dar_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves, p->pPars->fPower? &PowerSaved : NULL ); + // evaluate the cut + Class = s_DarLib->pMap[pCut->uTruth]; + Dar_LibEvalAssignNums( p, Class, pRoot ); + // profile outputs by their savings + 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->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, p->pPars->fPower? &PowerAdded : NULL ); + nNodesGained = nNodesSaved - nNodesAdded; + if ( p->pPars->fPower && PowerSaved < PowerAdded ) + continue; + if ( fTraining && nNodesGained >= 0 ) + Dar_LibIncrementScore( Class, Out, nNodesGained + 1 ); + if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) ) + continue; + 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->pSubgr0[Class][Out]; + p->OutNumBest = Out; + p->LevelBest = s_DarLib->pDatas[pObj->Num].Level; + p->GainBest = nNodesGained; + p->ClassBest = Class; + assert( p->LevelBest <= Required ); + *pnMffcSize = nNodesSaved; + } +clk = clock() - clk; +p->ClassTimes[Class] += clk; +p->timeEval += clk; +} + +/**Function************************************************************* + + Synopsis [Clears the fields of the nodes used in this cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_LibBuildClear_rec( Dar_LibObj_t * pObj, int * pCounter ) +{ + if ( pObj->fTerm ) + return; + pObj->Num = (*pCounter)++; + s_DarLib->pDatas[ pObj->Num ].pFunc = NULL; + Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0), pCounter ); + Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1), pCounter ); +} + +/**Function************************************************************* + + Synopsis [Reconstructs the best cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj ) +{ + Aig_Obj_t * pFanin0, * pFanin1; + Dar_LibDat_t * pData = s_DarLib->pDatas + pObj->Num; + if ( pData->pFunc ) + return pData->pFunc; + pFanin0 = Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan0) ); + pFanin1 = Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan1) ); + pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 ); + pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 ); + pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 ); +// assert( pData->Level == (int)Aig_Regular(pData->pFunc)->Level ); + return pData->pFunc; +} + +/**Function************************************************************* + + Synopsis [Reconstructs the best cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p ) +{ + int i, Counter = 4; + for ( i = 0; i < Vec_PtrSize(p->vLeavesBest); i++ ) + s_DarLib->pDatas[i].pFunc = (Aig_Obj_t *)Vec_PtrEntry( p->vLeavesBest, i ); + Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, p->OutBest), &Counter ); + return Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, p->OutBest) ); +} + + + + + + +/**Function************************************************************* + + Synopsis [Matches the cut with its canonical form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar2_LibCutMatch( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth ) +{ + unsigned uPhase; + char * pPerm; + int i; + assert( Vec_IntSize(vCutLits) == 4 ); + // get the fanin permutation + uPhase = s_DarLib->pPhases[uTruth]; + pPerm = s_DarLib->pPerms4[ (int)s_DarLib->pPerms[uTruth] ]; + // collect fanins with the corresponding permutation/phase + for ( i = 0; i < Vec_IntSize(vCutLits); i++ ) + { +// pFanin = Gia_ManObj( p, pCut->pLeaves[ (int)pPerm[i] ] ); +// pFanin = Gia_ManObj( p, Vec_IntEntry( vCutLits, (int)pPerm[i] ) ); +// pFanin = Gia_ObjFromLit( p, Vec_IntEntry( vCutLits, (int)pPerm[i] ) ); + s_DarLib->pDatas[i].iGunc = Abc_LitNotCond( Vec_IntEntry(vCutLits, (int)pPerm[i]), ((uPhase >> i) & 1) ); + s_DarLib->pDatas[i].Level = Gia_ObjLevel( p, Gia_Regular(Gia_ObjFromLit(p, s_DarLib->pDatas[i].iGunc)) ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Assigns numbers to the nodes of one class.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar2_LibEvalAssignNums( Gia_Man_t * p, int Class ) +{ + Dar_LibObj_t * pObj; + Dar_LibDat_t * pData, * pData0, * pData1; + int iFanin0, iFanin1, i, iLit; + 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->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->iGunc = -1; + 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 + Abc_MaxInt(pData0->Level, pData1->Level); + if ( pData0->iGunc == -1 || pData1->iGunc == -1 ) + continue; + iFanin0 = Abc_LitNotCond( pData0->iGunc, pObj->fCompl0 ); + iFanin1 = Abc_LitNotCond( pData1->iGunc, pObj->fCompl1 ); + // compute the resulting literal + if ( iFanin0 == 0 || iFanin1 == 0 || iFanin0 == Abc_LitNot(iFanin1) ) + iLit = 0; + else if ( iFanin0 == 1 || iFanin0 == iFanin1 ) + iLit = iFanin1; + else if ( iFanin1 == 1 ) + iLit = iFanin0; + else + { + iLit = Gia_ManHashLookup( p, Gia_ObjFromLit(p, iFanin0), Gia_ObjFromLit(p, iFanin1) ); + if ( iLit == 0 ) + iLit = -1; + } + pData->iGunc = iLit; + if ( pData->iGunc >= 0 ) + { + // update the level to be more accurate + pData->Level = Gia_ObjLevel( p, Gia_Regular(Gia_ObjFromLit(p, pData->iGunc)) ); + // mark the node if it is part of MFFC +// pData->fMffc = Gia_ObjIsTravIdCurrentArray(p, Gia_Regular(pData->pGunc)); + } + } +} + +/**Function************************************************************* + + Synopsis [Evaluates one cut.] + + Description [Returns the best gain.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar2_LibEval_rec( Dar_LibObj_t * pObj, int Out ) +{ + Dar_LibDat_t * pData; + int Area; + pData = s_DarLib->pDatas + pObj->Num; + if ( pData->TravId == Out ) + return 0; + pData->TravId = Out; + if ( pObj->fTerm ) + return 0; + assert( pObj->Num > 3 ); + if ( pData->iGunc >= 0 )//&& !pData->fMffc ) + return 0; + // this is a new node - get a bound on the area of its branches +// nNodesSaved--; + Area = Dar2_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out ); +// if ( Area > nNodesSaved ) +// return 0xff; + Area += Dar2_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out ); +// if ( Area > nNodesSaved ) +// return 0xff; + return Area + 1; +} + +/**Function************************************************************* + + Synopsis [Evaluates one cut.] + + Description [Returns the best gain.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar2_LibEval( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t * vLeavesBest2 ) +{ + int p_OutBest = -1; + int p_OutNumBest = -1; + int p_LevelBest = 1000000; + int p_GainBest = -1000000; + int p_ClassBest = -1; + int fTraining = 0; + Dar_LibObj_t * pObj; + int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk; + clk = clock(); + assert( Vec_IntSize(vCutLits) == 4 ); + assert( (uTruth >> 16) == 0 ); + // check if the cut exits and assigns leaves and their levels + if ( !Dar2_LibCutMatch(p, vCutLits, uTruth) ) + return -1; + // mark MFFC of the node +// nNodesSaved = Dar2_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves, p->pPars->fPower? &PowerSaved : NULL ); + nNodesSaved = 0; + // evaluate the cut + Class = s_DarLib->pMap[uTruth]; + Dar2_LibEvalAssignNums( p, Class ); + // profile outputs by their savings +// 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->pSubgr0[Class][Out]); +// nNodesAdded = Dar2_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required, p->pPars->fPower? &PowerAdded : NULL ); + nNodesAdded = Dar2_LibEval_rec( pObj, Out ); + nNodesGained = nNodesSaved - nNodesAdded; + if ( fKeepLevel ) + { + if ( s_DarLib->pDatas[pObj->Num].Level > p_LevelBest || + (s_DarLib->pDatas[pObj->Num].Level == p_LevelBest && nNodesGained <= p_GainBest) ) + continue; + } + else + { + if ( nNodesGained < p_GainBest || + (nNodesGained == p_GainBest && s_DarLib->pDatas[pObj->Num].Level >= p_LevelBest) ) + continue; + } + // remember this possibility + Vec_IntClear( vLeavesBest2 ); + for ( k = 0; k < Vec_IntSize(vCutLits); k++ ) + Vec_IntPush( vLeavesBest2, s_DarLib->pDatas[k].iGunc ); + p_OutBest = s_DarLib->pSubgr0[Class][Out]; + p_OutNumBest = Out; + p_LevelBest = s_DarLib->pDatas[pObj->Num].Level; + p_GainBest = nNodesGained; + p_ClassBest = Class; +// assert( p_LevelBest <= Required ); + } +//clk = clock() - clk; +//p->ClassTimes[Class] += clk; +//p->timeEval += clk; + assert( p_OutBest != -1 ); + return p_OutBest; +} + +/**Function************************************************************* + + Synopsis [Clears the fields of the nodes used i this cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar2_LibBuildClear_rec( Dar_LibObj_t * pObj, int * pCounter ) +{ + if ( pObj->fTerm ) + return; + pObj->Num = (*pCounter)++; + s_DarLib->pDatas[ pObj->Num ].iGunc = -1; + Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0), pCounter ); + Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1), pCounter ); +} + +/**Function************************************************************* + + Synopsis [Reconstructs the best cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar2_LibBuildBest_rec( Gia_Man_t * p, Dar_LibObj_t * pObj ) +{ + Gia_Obj_t * pNode; + Dar_LibDat_t * pData; + int iFanin0, iFanin1; + pData = s_DarLib->pDatas + pObj->Num; + if ( pData->iGunc >= 0 ) + return pData->iGunc; + iFanin0 = Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan0) ); + iFanin1 = Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan1) ); + iFanin0 = Abc_LitNotCond( iFanin0, pObj->fCompl0 ); + iFanin1 = Abc_LitNotCond( iFanin1, pObj->fCompl1 ); + pData->iGunc = Gia_ManHashAnd( p, iFanin0, iFanin1 ); + pNode = Gia_ManObj( p, Abc_Lit2Var(pData->iGunc) ); + if ( Gia_ObjIsAnd( pNode ) ) + Gia_ObjSetAndLevel( p, pNode ); + Gia_ObjSetPhase( pNode ); + return pData->iGunc; +} + +/**Function************************************************************* + + Synopsis [Reconstructs the best cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar2_LibBuildBest( Gia_Man_t * p, Vec_Int_t * vLeavesBest2, int OutBest ) +{ + int i, iLeaf, Counter = 4; + assert( Vec_IntSize(vLeavesBest2) == 4 ); + Vec_IntForEachEntry( vLeavesBest2, iLeaf, i ) + s_DarLib->pDatas[i].iGunc = iLeaf; + Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, OutBest), &Counter ); + return Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, OutBest) ); +} + +/**Function************************************************************* + + Synopsis [Evaluate and build the new node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_LibEvalBuild( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t * vLeavesBest2 ) +{ + int OutBest = Dar2_LibEval( p, vCutLits, uTruth, fKeepLevel, vLeavesBest2 ); + return Dar2_LibBuildBest( p, vLeavesBest2, OutBest ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |