src/opt/lpk/lpkSets.c File Reference

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

Go to the source code of this file.

Data Structures

struct  Lpk_Set_t_

Typedefs

typedef struct Lpk_Set_t_ Lpk_Set_t

Functions

unsigned Lpk_ComputeSets_rec (Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets)
unsigned Lpk_ComputeSets (Kit_DsdNtk_t *p, Vec_Int_t *vSets)
static void Lpk_PrintSetOne (int uSupport)
static void Lpk_PrintSets (Vec_Int_t *vSets)
void Lpk_ComposeSets (Vec_Int_t *vSets0, Vec_Int_t *vSets1, int nVars, int iCofVar, Lpk_Set_t *pStore, int *pSize, int nSizeLimit)
void Lpk_MapSuppPrintSet (Lpk_Set_t *pSet, int i)
unsigned Lpk_MapSuppRedDecSelect (Lpk_Man_t *p, unsigned *pTruth, int nVars, int *piVar, int *piVarReused)

Typedef Documentation

typedef struct Lpk_Set_t_ Lpk_Set_t

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

FileName [lpkSets.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
lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 27 of file lpkSets.c.

Function Documentation

void Lpk_ComposeSets ( Vec_Int_t *  vSets0,
Vec_Int_t *  vSets1,
int  nVars,
int  iCofVar,
Lpk_Set_t *  pStore,
int *  pSize,
int  nSizeLimit 
)

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

Synopsis [Computes maximal support reducing bound-sets.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file lpkSets.c.

00188 {
00189     static int nTravId = 0;            // the number of the times this is visited
00190     static int TravId[1<<16] = {0};    // last visited
00191     static char SRed[1<<16];           // best support reduction
00192     static char Over[1<<16];           // best overlaps
00193     static unsigned Parents[1<<16];    // best set of parents
00194     static unsigned short Used[1<<16]; // storage for used subsets
00195     int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s;
00196     unsigned Entry, Entry0, Entry1;
00197     unsigned uSupp, uSupp0, uSupp1, uSuppTotal;
00198     Lpk_Set_t * pEntry;
00199 
00200     if ( nTravId == (1 << 30) )
00201         memset( TravId, 0, sizeof(int) * (1 << 16) );
00202 
00203     // collect support reducing subsets
00204     nUsed = 0;
00205     nTravId++;
00206     uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar);
00207     Vec_IntForEachEntry( vSets0, Entry0, i )
00208     Vec_IntForEachEntry( vSets1, Entry1, k )
00209     {
00210         uSupp0 = (Entry0 & 0xFFFF);
00211         uSupp1 = (Entry1 & 0xFFFF);
00212         // skip trivial
00213         if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal )
00214             continue;
00215         if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) )
00216             continue;
00217         // get the entry
00218         Entry = Entry0 | Entry1;
00219         uSupp = Entry & 0xFFFF;
00220         // set the bound set size
00221         nSuppSize = Kit_WordCountOnes( uSupp );
00222         // get the number of overlapping vars
00223         nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) );
00224         // get the support reduction
00225         nSuppRed  = nSuppSize - 1 - nSuppOver;
00226         // only consider support-reducing subsets
00227         if ( nSuppRed <= 0 )
00228             continue;
00229         // check if this support is already used
00230         if ( TravId[uSupp] < nTravId )
00231         {
00232             Used[nUsed++] = uSupp;
00233 
00234             TravId[uSupp] = nTravId;
00235             SRed[uSupp] = nSuppRed;
00236             Over[uSupp] = nSuppOver;
00237             Parents[uSupp] = (k << 16) | i;
00238         }
00239         else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed )
00240         {
00241             TravId[uSupp] = nTravId;
00242             SRed[uSupp] = nSuppRed;
00243             Over[uSupp] = nSuppOver;
00244             Parents[uSupp] = (k << 16) | i;
00245         }
00246     }
00247 
00248     // find the minimum overlap
00249     nMinOver = 1000;
00250     for ( s = 0; s < nUsed; s++ )
00251         if ( nMinOver > Over[Used[s]] )
00252             nMinOver = Over[Used[s]];
00253 
00254 
00255     // collect the accumulated ones
00256     for ( s = 0; s < nUsed; s++ )
00257         if ( Over[Used[s]] == nMinOver )
00258         {
00259             // save the entry
00260             if ( *pSize == nSizeLimit )
00261                 return;
00262             pEntry = pStore + (*pSize)++;
00263 
00264             i = Parents[Used[s]] & 0xFFFF;
00265             k = Parents[Used[s]] >> 16;
00266 
00267             pEntry->uSubset0 = Vec_IntEntry(vSets0, i);
00268             pEntry->uSubset1 = Vec_IntEntry(vSets1, k);
00269             Entry  = pEntry->uSubset0 | pEntry->uSubset1;
00270 
00271             // record the cofactoring variable
00272             pEntry->iVar = iCofVar;
00273             // set the bound set size
00274             pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF );
00275             // get the number of overlapping vars
00276             pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
00277             // get the support reduction
00278             pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
00279             assert( pEntry->SRed > 0 );
00280         }
00281 }

unsigned Lpk_ComputeSets ( Kit_DsdNtk_t *  p,
Vec_Int_t *  vSets 
)

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

Synopsis [Computes the set of subsets of decomposable variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file lpkSets.c.

00106 {
00107     unsigned uSupport, Entry;
00108     int Number, i;
00109     assert( p->nVars <= 16 );
00110     Vec_IntClear( vSets );
00111     Vec_IntPush( vSets, 0 );
00112     if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
00113         return 0;
00114     if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
00115     {
00116         uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
00117         Vec_IntPush( vSets, uSupport );
00118         return uSupport;
00119     }
00120     uSupport = Lpk_ComputeSets_rec( p, p->Root, vSets );
00121     assert( (uSupport & 0xFFFF0000) == 0 );
00122     Vec_IntPush( vSets, uSupport );
00123     // set the remaining variables
00124     Vec_IntForEachEntry( vSets, Number, i )
00125     {
00126         Entry = Number;
00127         Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
00128     }
00129     return uSupport;
00130 }

unsigned Lpk_ComputeSets_rec ( Kit_DsdNtk_t *  p,
int  iLit,
Vec_Int_t *  vSets 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Recursively computes decomposable subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file lpkSets.c.

00054 {
00055     unsigned i, iLitFanin, uSupport, uSuppCur;
00056     Kit_DsdObj_t * pObj;
00057     // consider the case of simple gate
00058     pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
00059     if ( pObj == NULL )
00060         return (1 << Kit_DsdLit2Var(iLit));
00061     if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
00062     {
00063         unsigned uSupps[16], Limit, s;
00064         uSupport = 0;
00065         Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
00066         {
00067             uSupps[i] = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
00068             uSupport |= uSupps[i];
00069         }
00070         // create all subsets, except empty and full
00071         Limit = (1 << pObj->nFans) - 1;
00072         for ( s = 1; s < Limit; s++ )
00073         {
00074             uSuppCur = 0;
00075             for ( i = 0; i < pObj->nFans; i++ )
00076                 if ( s & (1 << i) )
00077                     uSuppCur |= uSupps[i];
00078             Vec_IntPush( vSets, uSuppCur );
00079         }
00080         return uSupport;
00081     }
00082     assert( pObj->Type == KIT_DSD_PRIME );
00083     // get the cumulative support of all fanins
00084     uSupport = 0;
00085     Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
00086     {
00087         uSuppCur  = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
00088         uSupport |= uSuppCur;
00089         Vec_IntPush( vSets, uSuppCur );
00090     }
00091     return uSupport;
00092 }

void Lpk_MapSuppPrintSet ( Lpk_Set_t *  pSet,
int  i 
)

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

Synopsis [Prints one set.]

Description []

SideEffects []

SeeAlso []

Definition at line 294 of file lpkSets.c.

00295 {
00296     unsigned Entry;
00297     Entry = pSet->uSubset0 | pSet->uSubset1;
00298     printf( "%2d : ", i );
00299     printf( "Var = %c  ",  'a' + pSet->iVar );
00300     printf( "Size = %2d  ", pSet->Size );
00301     printf( "Over = %2d  ", pSet->Over );
00302     printf( "SRed = %2d  ", pSet->SRed );
00303     Lpk_PrintSetOne( Entry );
00304     printf( "              " );
00305     Lpk_PrintSetOne( Entry >> 16 );
00306     printf( "\n" );
00307 }

unsigned Lpk_MapSuppRedDecSelect ( Lpk_Man_t *  p,
unsigned *  pTruth,
int  nVars,
int *  piVar,
int *  piVarReused 
)

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

Synopsis [Evaluates the cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 320 of file lpkSets.c.

00321 {
00322     static int nStoreSize = 256;
00323     static Lpk_Set_t pStore[256], * pSet, * pSetBest;
00324     Kit_DsdNtk_t * ppNtks[2], * pTemp;
00325     Vec_Int_t * vSets0 = p->vSets[0];
00326     Vec_Int_t * vSets1 = p->vSets[1];
00327     unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
00328     unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
00329     int nSets, i, SizeMax;//, SRedMax;
00330     unsigned Entry;
00331     int fVerbose = p->pPars->fVeryVerbose;
00332 //    int fVerbose = 0;
00333 
00334     // collect decomposable subsets for each pair of cofactors
00335     if ( fVerbose )
00336     {
00337         printf( "\nExploring support-reducing bound-sets of function:\n" );
00338         Kit_DsdPrintFromTruth( pTruth, nVars );
00339     }
00340     nSets = 0;
00341     for ( i = 0; i < nVars; i++ )
00342     {
00343         if ( fVerbose )
00344         printf( "Evaluating variable %c:\n", 'a'+i );
00345         // evaluate the cofactor pair
00346         Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
00347         Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
00348         // decompose and expand
00349         ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
00350         ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
00351         ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );      Kit_DsdNtkFree( pTemp );
00352         ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );      Kit_DsdNtkFree( pTemp );
00353         if ( fVerbose )
00354         Kit_DsdPrint( stdout, ppNtks[0] );
00355         if ( fVerbose )
00356         Kit_DsdPrint( stdout, ppNtks[1] );
00357         // compute subsets
00358         Lpk_ComputeSets( ppNtks[0], vSets0 );
00359         Lpk_ComputeSets( ppNtks[1], vSets1 );
00360         // print subsets
00361         if ( fVerbose )
00362         Lpk_PrintSets( vSets0 );
00363         if ( fVerbose )
00364         Lpk_PrintSets( vSets1 );
00365         // free the networks
00366         Kit_DsdNtkFree( ppNtks[0] );
00367         Kit_DsdNtkFree( ppNtks[1] );
00368         // evaluate the pair
00369         Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize );
00370     }
00371 
00372     // print the results
00373     if ( fVerbose )
00374     printf( "\n" );
00375     if ( fVerbose )
00376     for ( i = 0; i < nSets; i++ )
00377         Lpk_MapSuppPrintSet( pStore + i, i );
00378 
00379     // choose the best subset
00380     SizeMax = 0;
00381     pSetBest = NULL;
00382     for ( i = 0; i < nSets; i++ )
00383     {
00384         pSet = pStore + i;
00385         if ( pSet->Size > p->pPars->nLutSize - 1 )
00386             continue;
00387         if ( SizeMax < pSet->Size )
00388         {
00389             pSetBest = pSet;
00390             SizeMax = pSet->Size;
00391         }
00392     }
00393 /*
00394     // if the best is not choosen, select the one with largest reduction
00395     SRedMax = 0;
00396     if ( pSetBest == NULL )
00397     {
00398         for ( i = 0; i < nSets; i++ )
00399         {
00400             pSet = pStore + i;
00401             if ( SRedMax < pSet->SRed )
00402             {
00403                 pSetBest = pSet;
00404                 SRedMax = pSet->SRed;
00405             }
00406         }
00407     }
00408 */
00409     if ( pSetBest == NULL )
00410     {
00411         if ( fVerbose )
00412         printf( "Could not select a subset.\n" );
00413         return 0;
00414     }
00415     else
00416     {
00417         if ( fVerbose )
00418         printf( "Selected the following subset:\n" );
00419         if ( fVerbose )
00420         Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
00421     }
00422 
00423     // prepare the return result
00424     // get the remaining variables
00425     Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16));
00426     // get the variables to be removed
00427     Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry;
00428     // make sure there are some - otherwise it is not supp-red
00429     assert( Entry );
00430     // remember the first such variable
00431     *piVarReused = Kit_WordFindFirstBit( Entry );
00432     *piVar = pSetBest->iVar;
00433     return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF);
00434 }

static void Lpk_PrintSetOne ( int  uSupport  )  [static]

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

Synopsis [Prints the sets of subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file lpkSets.c.

00144 {
00145     unsigned k;
00146     for ( k = 0; k < 16; k++ )
00147         if ( uSupport & (1<<k) )
00148             printf( "%c", 'a'+k );
00149     printf( " " );
00150 }

static void Lpk_PrintSets ( Vec_Int_t *  vSets  )  [static]

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

Synopsis [Prints the sets of subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file lpkSets.c.

00163 {
00164     unsigned uSupport;
00165     int Number, i;
00166     printf( "Subsets(%d): ", Vec_IntSize(vSets) );
00167     Vec_IntForEachEntry( vSets, Number, i )
00168     {
00169         uSupport = Number;
00170         Lpk_PrintSetOne( uSupport );
00171     }
00172     printf( "\n" );
00173 }

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