src/opt/lpk/lpkMulti.c File Reference

#include "lpkInt.h"
Include dependency graph for lpkMulti.c:

Go to the source code of this file.

Functions

void Lpk_CreateVarOrder (Kit_DsdNtk_t *pNtk, char pTable[][16])
void Lpk_CreateCommonOrder (char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose)
int Lpk_FindHighest (Kit_DsdNtk_t **ppNtks, int *piLits, int nSize, int *pPrio, int *pDecision)
If_Obj_t * Lpk_MapTreeMulti_rec (Lpk_Man_t *p, Kit_DsdNtk_t **ppNtks, int *piLits, int *piCofVar, int nCBars, If_Obj_t **ppLeaves, int nLeaves, int *pPrio)
If_Obj_t * Lpk_MapTreeMulti (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)

Function Documentation

void Lpk_CreateCommonOrder ( char  pTable[][16],
int  piCofVar[],
int  nCBars,
int  pPrios[],
int  nVars,
int  fVerbose 
)

Function*************************************************************

Synopsis [Creates commmon variable order.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file lpkMulti.c.

00085 {
00086     int Score[16] = {0}, pPres[16];
00087     int i, y, x, iVarBest, ScoreMax, PrioCount;
00088 
00089     // mark the present variables
00090     for ( i = 0; i < nVars; i++ )
00091         pPres[i] = 1;
00092     // remove cofactored variables
00093     for ( i = 0; i < nCBars; i++ )
00094         pPres[piCofVar[i]] = 0;
00095 
00096     // compute scores for each leaf
00097     for ( i = 0; i < nVars; i++ )
00098     {
00099         if ( pPres[i] == 0 )
00100             continue;
00101         for ( y = 0; y < nVars; y++ )
00102             Score[i] += pTable[i][y];
00103         for ( x = 0; x < nVars; x++ )
00104             Score[i] -= pTable[x][i];
00105     }
00106 
00107     // print the scores
00108     if ( fVerbose )
00109     {
00110         printf( "Scores: " );
00111         for ( i = 0; i < nVars; i++ )
00112             printf( "%c=%d ", 'a'+i, Score[i] );
00113         printf( "   " );
00114         printf( "Prios: " );
00115     }
00116 
00117     // derive variable priority
00118     // variables with equal score receive the same priority
00119     for ( i = 0; i < nVars; i++ )
00120         pPrios[i] = 16;
00121 
00122     // iterate until variables remain
00123     for ( PrioCount = 1; ; PrioCount++ )
00124     {
00125         // find the present variable with the highest score
00126         iVarBest = -1;
00127         ScoreMax = -100000;
00128         for ( i = 0; i < nVars; i++ )
00129         {
00130             if ( pPres[i] == 0 )
00131                 continue;
00132             if ( ScoreMax < Score[i] )
00133             {
00134                 ScoreMax = Score[i];
00135                 iVarBest = i;
00136             }
00137         }
00138         if ( iVarBest == -1 )
00139             break;
00140         // give the next priority to all vars having this score
00141         if ( fVerbose )
00142             printf( "%d=", PrioCount );
00143         for ( i = 0; i < nVars; i++ )
00144         {
00145             if ( pPres[i] == 0 )
00146                 continue;
00147             if ( Score[i] == ScoreMax )
00148             {
00149                 pPrios[i] = PrioCount;
00150                 pPres[i] = 0;
00151                 if ( fVerbose )
00152                     printf( "%c", 'a'+i );
00153             }
00154         }
00155         if ( fVerbose )
00156             printf( " " );
00157     }
00158     if ( fVerbose )
00159         printf( "\n" );
00160 }

void Lpk_CreateVarOrder ( Kit_DsdNtk_t *  pNtk,
char  pTable[][16] 
)

CFile****************************************************************

FileName [lpkMulti.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
lpkMulti.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Records variable order.]

Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]

SideEffects []

SeeAlso []

Definition at line 42 of file lpkMulti.c.

00043 {
00044     Kit_DsdObj_t * pObj;
00045     unsigned uSuppFanins, k;
00046     int Above[16], Below[16];
00047     int nAbove, nBelow, iFaninLit, i, x, y;
00048     // iterate through the nodes
00049     Kit_DsdNtkForEachObj( pNtk, pObj, i )
00050     {
00051         // collect fanin support of this node
00052         nAbove = 0;
00053         uSuppFanins = 0;
00054         Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
00055         {
00056             if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
00057                 Above[nAbove++] = Kit_DsdLit2Var(iFaninLit);
00058             else
00059                 uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
00060         }
00061         // find the below variables
00062         nBelow = 0;
00063         for ( y = 0; y < 16; y++ )
00064             if ( uSuppFanins & (1 << y) )
00065                 Below[nBelow++] = y;
00066         // create all pairs
00067         for ( x = 0; x < nAbove; x++ )
00068             for ( y = 0; y < nBelow; y++ )
00069                 pTable[Above[x]][Below[y]]++;
00070     }
00071 }

int Lpk_FindHighest ( Kit_DsdNtk_t **  ppNtks,
int *  piLits,
int  nSize,
int *  pPrio,
int *  pDecision 
)

Function*************************************************************

Synopsis [Finds components with the highest priority.]

Description [Returns the number of components selected.]

SideEffects []

SeeAlso []

Definition at line 173 of file lpkMulti.c.

00174 {
00175     Kit_DsdObj_t * pObj;
00176     unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge;
00177     int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv;
00178 
00179     // find individual support and total support 
00180     uSuppTotal = 0;
00181     for ( i = 0; i < nSize; i++ )
00182     {
00183         pTriv[i] = 1;
00184         if ( piLits[i] < 0 ) 
00185             uSupps[i] = 0;
00186         else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) )
00187             uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] );
00188         else
00189         {
00190             pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
00191             if ( pObj->Type == KIT_DSD_PRIME )
00192             {
00193                 pTriv[i] = 0;
00194                 uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] );
00195             }
00196             else
00197             {
00198                 assert( pObj->nFans == 2 );
00199                 if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) )
00200                     pTriv[i] = 0;
00201                 uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] );
00202             }
00203             uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
00204         }
00205         assert( uSupps[i] <= 0xFFFF );
00206         uSuppTotal |= uSupps[i];
00207     }
00208     if ( uSuppTotal == 0 )
00209         return 0;
00210 
00211     // find one support variable with the highest priority
00212     PrioMin = ABC_INFINITY;
00213     iVarMax = -1;
00214     for ( i = 0; i < 16; i++ )
00215         if ( uSuppTotal & (1 << i) )
00216             if ( PrioMin > pPrio[i] )
00217             {
00218                 PrioMin = pPrio[i];
00219                 iVarMax = i;
00220             }
00221     assert( iVarMax != -1 );
00222 
00223     // select components, which have this variable
00224     nComps = 0;
00225     fOneNonTriv = 0;
00226     uSuppLarge = 0;
00227     for ( i = 0; i < nSize; i++ )
00228         if ( uSupps[i] & (1<<iVarMax) )
00229         {
00230             if ( pTriv[i] || !fOneNonTriv )
00231             {
00232                 if ( !pTriv[i] )
00233                 {
00234                     uSuppLarge = uSupps[i];
00235                     fOneNonTriv = 1;
00236                 }
00237                 pDecision[i] = 1;
00238                 nComps++;
00239             }
00240             else
00241                 pDecision[i] = 0;
00242         }
00243         else
00244             pDecision[i] = 0;
00245 
00246     // add other non-trivial not-taken components whose support is contained in the current large component support
00247     if ( fOneNonTriv )
00248         for ( i = 0; i < nSize; i++ )
00249             if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 )
00250             {
00251                 pDecision[i] = 1;
00252                 nComps++;
00253             }
00254 
00255     return nComps;
00256 }

If_Obj_t* Lpk_MapTreeMulti ( Lpk_Man_t *  p,
unsigned *  pTruth,
int  nVars,
If_Obj_t **  ppLeaves 
)

Function*************************************************************

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 344 of file lpkMulti.c.

00345 {
00346     static Counter = 0;
00347     If_Obj_t * pResult;
00348     Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
00349     Kit_DsdObj_t * pRoot;
00350     int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16];
00351     int i, k, nCBars, nSize, nMemSize;
00352     unsigned * ppCofs[4][8], uSupport;
00353     char pTable[16][16] = {0};
00354     int fVerbose = p->pPars->fVeryVerbose;
00355 
00356     Counter++;
00357 //    printf( "Run %d.\n", Counter );
00358 
00359     // allocate storage for cofactors
00360     nMemSize = Kit_TruthWordNum(nVars);
00361     ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
00362     nSize = 0;
00363     for ( i = 0; i < 4; i++ )
00364     for ( k = 0; k < 8; k++ )
00365         ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
00366     assert( nSize == 32 );
00367 
00368     // find the best cofactoring variables
00369     nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
00370 //    nCBars = 2;
00371 //    piCofVar[0] = 0;
00372 //    piCofVar[1] = 1;
00373 
00374 
00375     // copy the function
00376     Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
00377 
00378     // decompose w.r.t. these variables
00379     for ( k = 0; k < nCBars; k++ )
00380     {
00381         nSize = (1 << k);
00382         for ( i = 0; i < nSize; i++ )
00383         {
00384             Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
00385             Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
00386         }
00387     }
00388     nSize = (1 << nCBars);
00389     // compute DSD networks
00390     for ( i = 0; i < nSize; i++ )
00391     {
00392         ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
00393         ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
00394         Kit_DsdNtkFree( pTemp );
00395         if ( fVerbose )
00396         {
00397             printf( "Cof%d%d: ", nCBars, i );
00398             Kit_DsdPrint( stdout, ppNtks[i] );
00399         }
00400     }
00401 
00402     // compute variable frequences
00403     for ( i = 0; i < nSize; i++ )
00404     {
00405         uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
00406         for ( k = 0; k < nVars; k++ )
00407             if ( uSupport & (1<<k) )
00408                 pFreqs[k]++;
00409     }
00410 
00411     // find common variable order
00412     for ( i = 0; i < nSize; i++ )
00413     {
00414         Kit_DsdGetSupports( ppNtks[i] );
00415         Lpk_CreateVarOrder( ppNtks[i], pTable );
00416     }
00417     Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose );
00418     // update priorities with frequences
00419     for ( i = 0; i < nVars; i++ )
00420         pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i;
00421 
00422     if ( fVerbose )
00423         printf( "After restructuring with priority:\n" );
00424 
00425     if ( Counter == 1 )
00426     {
00427         int x = 0;
00428     }
00429     // transform all networks according to the variable order
00430     for ( i = 0; i < nSize; i++ )
00431     {
00432         ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
00433         Kit_DsdNtkFree( pTemp );
00434         Kit_DsdGetSupports( ppNtks[i] );
00435         assert( ppNtks[i]->pSupps[0] <= 0xFFFF );
00436         // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
00437         Kit_DsdRotate( ppNtks[i], pFreqs );
00438         // print the resulting networks
00439         if ( fVerbose )
00440         {
00441             printf( "Cof%d%d: ", nCBars, i );
00442             Kit_DsdPrint( stdout, ppNtks[i] );
00443         }
00444     }
00445  
00446     for ( i = 0; i < nSize; i++ )
00447     {
00448         // collect the roots
00449         pRoot = Kit_DsdNtkRoot(ppNtks[i]);
00450         if ( pRoot->Type == KIT_DSD_CONST1 )
00451             piLits[i] = Kit_DsdLitIsCompl(ppNtks[i]->Root)? -2: -1;
00452         else if ( pRoot->Type == KIT_DSD_VAR )
00453             piLits[i] = Kit_DsdLitNotCond( pRoot->pFans[0], Kit_DsdLitIsCompl(ppNtks[i]->Root) );
00454         else
00455             piLits[i] = ppNtks[i]->Root;
00456     }
00457 
00458 
00459     // recursively construct AIG for mapping
00460     p->fCofactoring = 1;
00461     pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios );
00462     p->fCofactoring = 0;
00463 
00464     if ( fVerbose )
00465         printf( "\n" );
00466 
00467     // verify the transformations
00468     nSize = (1 << nCBars);
00469     for ( i = 0; i < nSize; i++ )
00470         Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] );
00471     // mux the truth tables
00472     for ( k = nCBars-1; k >= 0; k-- )
00473     {
00474         nSize = (1 << k);
00475         for ( i = 0; i < nSize; i++ )
00476             Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] );
00477     }
00478     if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) )
00479         printf( "Verification failed.\n" );
00480 
00481 
00482     // free the networks
00483     for ( i = 0; i < 8; i++ )
00484         if ( ppNtks[i] )
00485             Kit_DsdNtkFree( ppNtks[i] );
00486     free( ppCofs[0][0] );
00487 
00488     return pResult;
00489 }

If_Obj_t* Lpk_MapTreeMulti_rec ( Lpk_Man_t *  p,
Kit_DsdNtk_t **  ppNtks,
int *  piLits,
int *  piCofVar,
int  nCBars,
If_Obj_t **  ppLeaves,
int  nLeaves,
int *  pPrio 
)

Function*************************************************************

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 269 of file lpkMulti.c.

00270 {
00271     Kit_DsdObj_t * pObj;
00272     If_Obj_t * pObjsNew[4][8], * pResPrev;
00273     int piLitsNew[8], pDecision[8];
00274     int i, k, nComps, nSize;
00275 
00276     // find which of the variables is highest in the order
00277     nSize = (1 << nCBars);
00278     nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision );
00279     if ( nComps == 0 )
00280         return If_Not( If_ManConst1(p->pIfMan) );
00281 
00282     // iterate over the nodes
00283     if ( p->pPars->fVeryVerbose )
00284         printf( "Decision: " );
00285     for ( i = 0; i < nSize; i++ )
00286     {
00287         if ( pDecision[i] )
00288         {
00289             if ( p->pPars->fVeryVerbose )
00290                 printf( "%d ", i );
00291             assert( piLits[i] >= 0 );
00292             pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
00293             if ( pObj == NULL )
00294                 piLitsNew[i] = -2;
00295             else if ( pObj->Type == KIT_DSD_PRIME )
00296                 piLitsNew[i] = pObj->pFans[0];
00297             else
00298                 piLitsNew[i] = pObj->pFans[1];
00299         }
00300         else
00301             piLitsNew[i] = piLits[i];
00302     }
00303     if ( p->pPars->fVeryVerbose )
00304         printf( "\n" );
00305 
00306     // call again
00307     pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio );
00308 
00309     // create new set of nodes
00310     for ( i = 0; i < nSize; i++ )
00311     {
00312         if ( pDecision[i] )
00313             pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev );
00314         else if ( piLits[i] == -1 )
00315             pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan);
00316         else if ( piLits[i] == -2 )
00317             pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) );
00318         else
00319             pObjsNew[nCBars][i] = pResPrev;
00320     }
00321 
00322     // create MUX using these outputs
00323     for ( k = nCBars; k > 0; k-- )
00324     {
00325         nSize /= 2;
00326         for ( i = 0; i < nSize; i++ )
00327             pObjsNew[k-1][i] = If_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
00328     }
00329     assert( nSize == 1 );
00330     return pObjsNew[0][0];  
00331 }

Generated on Tue Jan 5 12:19:29 2010 for abc70930 by  doxygen 1.6.1