src/aig/csw/cswInt.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "aig.h"
#include "dar.h"
#include "kit.h"
#include "csw.h"
Include dependency graph for cswInt.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  Csw_Cut_t_
struct  Csw_Man_t_

Defines

#define Csw_ObjForEachCut(p, pObj, pCut, i)   for ( i = 0, pCut = Csw_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Csw_CutNext(pCut) )
#define Csw_CutForEachLeaf(p, pCut, pLeaf, i)   for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )

Typedefs

typedef struct Csw_Man_t_ Csw_Man_t
typedef struct Csw_Cut_t_ Csw_Cut_t

Functions

static int Csw_CutLeaveNum (Csw_Cut_t *pCut)
static int * Csw_CutLeaves (Csw_Cut_t *pCut)
static unsigned * Csw_CutTruth (Csw_Cut_t *pCut)
static Csw_Cut_t * Csw_CutNext (Csw_Cut_t *pCut)
static int Csw_ObjRefs (Csw_Man_t *p, Aig_Obj_t *pObj)
static void Csw_ObjAddRefs (Csw_Man_t *p, Aig_Obj_t *pObj, int nRefs)
static Csw_Cut_t * Csw_ObjCuts (Csw_Man_t *p, Aig_Obj_t *pObj)
static void Csw_ObjSetCuts (Csw_Man_t *p, Aig_Obj_t *pObj, Csw_Cut_t *pCuts)
static Aig_Obj_t * Csw_ObjEquiv (Csw_Man_t *p, Aig_Obj_t *pObj)
static void Csw_ObjSetEquiv (Csw_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pEquiv)
static Aig_Obj_t * Csw_ObjChild0Equiv (Csw_Man_t *p, Aig_Obj_t *pObj)
static Aig_Obj_t * Csw_ObjChild1Equiv (Csw_Man_t *p, Aig_Obj_t *pObj)
Csw_Cut_t * Csw_ObjPrepareCuts (Csw_Man_t *p, Aig_Obj_t *pObj, int fTriv)
Aig_Obj_t * Csw_ObjSweep (Csw_Man_t *p, Aig_Obj_t *pObj, int fTriv)
Csw_Man_t * Csw_ManStart (Aig_Man_t *pMan, int nCutsMax, int nLeafMax, int fVerbose)
void Csw_ManStop (Csw_Man_t *p)
int Csw_TableCountCuts (Csw_Man_t *p)
void Csw_TableCutInsert (Csw_Man_t *p, Csw_Cut_t *pCut)
Aig_Obj_t * Csw_TableCutLookup (Csw_Man_t *p, Csw_Cut_t *pCut)

Define Documentation

#define Csw_CutForEachLeaf ( p,
pCut,
pLeaf,
i   )     for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )

Definition at line 130 of file cswInt.h.

#define Csw_ObjForEachCut ( p,
pObj,
pCut,
i   )     for ( i = 0, pCut = Csw_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Csw_CutNext(pCut) )

MACRO DEFINITIONS /// ITERATORS ///

Definition at line 127 of file cswInt.h.

Typedef Documentation

typedef struct Csw_Cut_t_ Csw_Cut_t

Definition at line 52 of file cswInt.h.

typedef struct Csw_Man_t_ Csw_Man_t

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

FileName [cswInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Cut sweeping.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - July 11, 2007.]

Revision [

Id
cswInt.h,v 1.00 2007/07/11 00:00:00 alanmi Exp

] INCLUDES /// PARAMETERS /// BASIC TYPES ///

Definition at line 51 of file cswInt.h.

Function Documentation

static int Csw_CutLeaveNum ( Csw_Cut_t *  pCut  )  [inline, static]

Definition at line 101 of file cswInt.h.

00101 { return pCut->nFanins;                                   }

static int* Csw_CutLeaves ( Csw_Cut_t *  pCut  )  [inline, static]

Definition at line 102 of file cswInt.h.

00102 { return pCut->pFanins;                                   }

static Csw_Cut_t* Csw_CutNext ( Csw_Cut_t *  pCut  )  [inline, static]

Definition at line 104 of file cswInt.h.

00104 { return (Csw_Cut_t *)(((char *)pCut) + pCut->nCutSize);  }

static unsigned* Csw_CutTruth ( Csw_Cut_t *  pCut  )  [inline, static]

Definition at line 103 of file cswInt.h.

00103 { return (unsigned *)(pCut->pFanins + pCut->nLeafMax);    }

Csw_Man_t* Csw_ManStart ( Aig_Man_t *  pMan,
int  nCutsMax,
int  nLeafMax,
int  fVerbose 
)

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

FileName [cswMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Cut sweeping.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - July 11, 2007.]

Revision [

Id
cswMan.c,v 1.00 2007/07/11 00:00:00 alanmi Exp

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

Synopsis [Starts the cut sweeping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file cswMan.c.

00043 {
00044     Csw_Man_t * p;
00045     Aig_Obj_t * pObj;
00046     int i;
00047     assert( nCutsMax >= 2  );
00048     assert( nLeafMax <= 16 );
00049     // allocate the fraiging manager
00050     p = ALLOC( Csw_Man_t, 1 );
00051     memset( p, 0, sizeof(Csw_Man_t) );
00052     p->nCutsMax = nCutsMax;
00053     p->nLeafMax = nLeafMax;
00054     p->fVerbose = fVerbose;
00055     p->pManAig  = pMan;
00056     // create the new manager
00057     p->pManRes  = Aig_ManStartFrom( pMan );
00058     assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManRes) );
00059     // allocate room for cuts and equivalent nodes
00060     p->pnRefs   = ALLOC( int, Aig_ManObjNumMax(pMan) );
00061     p->pEquiv   = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pMan) );
00062     p->pCuts    = ALLOC( Csw_Cut_t *, Aig_ManObjNumMax(pMan) );
00063     memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pMan) );
00064     memset( p->pnRefs, 0, sizeof(int) * Aig_ManObjNumMax(pMan) );
00065     // allocate memory manager
00066     p->nTruthWords = Aig_TruthWordNum(nLeafMax);
00067     p->nCutSize = sizeof(Csw_Cut_t) + sizeof(int) * nLeafMax + sizeof(unsigned) * p->nTruthWords;
00068     p->pMemCuts = Aig_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
00069     // allocate hash table for cuts
00070     p->nTableSize = Aig_PrimeCudd( Aig_ManNodeNum(pMan) * p->nCutsMax / 2 );
00071     p->pTable = ALLOC( Csw_Cut_t *, p->nTableSize );
00072     memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
00073     // set the pointers to the available fraig nodes
00074     Csw_ObjSetEquiv( p, Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManRes) );
00075     Aig_ManForEachPi( p->pManAig, pObj, i )
00076         Csw_ObjSetEquiv( p, pObj, Aig_ManPi(p->pManRes, i) );
00077     // room for temporary truth tables
00078     p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords );
00079     p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
00080     p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
00081     p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
00082     return p;
00083 }

void Csw_ManStop ( Csw_Man_t *  p  ) 

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

Synopsis [Stops the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file cswMan.c.

00097 {
00098     if ( p->fVerbose )
00099     {
00100         int nNodesBeg = Aig_ManNodeNum(p->pManAig);
00101         int nNodesEnd = Aig_ManNodeNum(p->pManRes);
00102         printf( "Beg = %7d.  End = %7d.  (%6.2f %%)  Try = %7d.  Cuts = %8d.\n", 
00103             nNodesBeg, nNodesEnd, 100.0*(nNodesBeg-nNodesEnd)/nNodesBeg,
00104             p->nNodesTried, Csw_TableCountCuts( p ) );
00105         printf( "Triv0 = %6d.  Triv1 = %6d.  Triv2 = %6d.  Cut-replace = %6d.\n", 
00106             p->nNodesTriv0, p->nNodesTriv1, p->nNodesTriv2, p->nNodesCuts );
00107         PRTP( "Cuts    ", p->timeCuts,     p->timeTotal );
00108         PRTP( "Hashing ", p->timeHash,     p->timeTotal );
00109         PRTP( "Other   ", p->timeOther,    p->timeTotal );
00110         PRTP( "TOTAL   ", p->timeTotal,    p->timeTotal );
00111     }
00112     free( p->puTemp[0] );
00113     Aig_MmFixedStop( p->pMemCuts, 0 );
00114     free( p->pnRefs );
00115     free( p->pEquiv );
00116     free( p->pCuts );
00117     free( p->pTable );
00118     free( p );
00119 }

static void Csw_ObjAddRefs ( Csw_Man_t *  p,
Aig_Obj_t *  pObj,
int  nRefs 
) [inline, static]

Definition at line 107 of file cswInt.h.

00107 { p->pnRefs[pObj->Id] += nRefs; }

static Aig_Obj_t* Csw_ObjChild0Equiv ( Csw_Man_t *  p,
Aig_Obj_t *  pObj 
) [inline, static]

Definition at line 115 of file cswInt.h.

00115 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL;  }

static Aig_Obj_t* Csw_ObjChild1Equiv ( Csw_Man_t *  p,
Aig_Obj_t *  pObj 
) [inline, static]

Definition at line 116 of file cswInt.h.

00116 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL;  }

static Csw_Cut_t* Csw_ObjCuts ( Csw_Man_t *  p,
Aig_Obj_t *  pObj 
) [inline, static]

Definition at line 109 of file cswInt.h.

00109 { return p->pCuts[pObj->Id];    }

static Aig_Obj_t* Csw_ObjEquiv ( Csw_Man_t *  p,
Aig_Obj_t *  pObj 
) [inline, static]

Definition at line 112 of file cswInt.h.

00112 { return p->pEquiv[pObj->Id];   }

Csw_Cut_t* Csw_ObjPrepareCuts ( Csw_Man_t *  p,
Aig_Obj_t *  pObj,
int  fTriv 
)

FUNCTION DECLARATIONS ///

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 450 of file cswCut.c.

00451 {
00452     Csw_Cut_t * pCutSet, * pCut;
00453     int i;
00454     // create the cutset of the node
00455     pCutSet = (Csw_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
00456     Csw_ObjSetCuts( p, pObj, pCutSet );
00457     Csw_ObjForEachCut( p, pObj, pCut, i )
00458     {
00459         pCut->nFanins = 0;
00460         pCut->iNode = pObj->Id;
00461         pCut->nCutSize = p->nCutSize;
00462         pCut->nLeafMax = p->nLeafMax;
00463     }
00464     // add unit cut if needed
00465     if ( fTriv )
00466     {
00467         pCut = pCutSet;
00468         pCut->Cost = 0;
00469         pCut->iNode = pObj->Id;
00470         pCut->nFanins = 1;
00471         pCut->pFanins[0] = pObj->Id;
00472         pCut->uSign = Aig_ObjCutSign( pObj->Id );
00473         memset( Csw_CutTruth(pCut), 0xAA, sizeof(unsigned) * p->nTruthWords );
00474     }
00475     return pCutSet;
00476 }

static int Csw_ObjRefs ( Csw_Man_t *  p,
Aig_Obj_t *  pObj 
) [inline, static]

Definition at line 106 of file cswInt.h.

00106 { return p->pnRefs[pObj->Id];   }

static void Csw_ObjSetCuts ( Csw_Man_t *  p,
Aig_Obj_t *  pObj,
Csw_Cut_t *  pCuts 
) [inline, static]

Definition at line 110 of file cswInt.h.

00110 { p->pCuts[pObj->Id] = pCuts;   }

static void Csw_ObjSetEquiv ( Csw_Man_t *  p,
Aig_Obj_t *  pObj,
Aig_Obj_t *  pEquiv 
) [inline, static]

Definition at line 113 of file cswInt.h.

00113 { p->pEquiv[pObj->Id] = pEquiv; }

Aig_Obj_t* Csw_ObjSweep ( Csw_Man_t *  p,
Aig_Obj_t *  pObj,
int  fTriv 
)

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

Synopsis [Derives cuts for one node and sweeps this node.]

Description []

SideEffects []

SeeAlso []

Definition at line 489 of file cswCut.c.

00490 {
00491     int fUseResub = 1;
00492     Csw_Cut_t * pCut0, * pCut1, * pCut, * pCutSet;
00493     Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj);
00494     Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
00495     Aig_Obj_t * pObjNew;
00496     unsigned * pTruth;
00497     int i, k, nVars, nFanins, iVar, clk;
00498 
00499     assert( !Aig_IsComplement(pObj) );
00500     if ( !Aig_ObjIsNode(pObj) )
00501         return pObj;
00502     if ( Csw_ObjCuts(p, pObj) )
00503         return pObj;
00504     // the node is not processed yet
00505     assert( Csw_ObjCuts(p, pObj) == NULL );
00506     assert( Aig_ObjIsNode(pObj) );
00507 
00508     // set up the first cut
00509     pCutSet = Csw_ObjPrepareCuts( p, pObj, fTriv );
00510 
00511     // compute pair-wise cut combinations while checking table
00512     Csw_ObjForEachCut( p, pFanin0, pCut0, i )
00513     if ( pCut0->nFanins > 0 )
00514     Csw_ObjForEachCut( p, pFanin1, pCut1, k )
00515     if ( pCut1->nFanins > 0 )
00516     {
00517         // make sure K-feasible cut exists
00518         if ( Kit_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->nLeafMax )
00519             continue;
00520         // get the next cut of this node
00521         pCut = Csw_CutFindFree( p, pObj );
00522 clk = clock();
00523         // assemble the new cut
00524         if ( !Csw_CutMerge( p, pCut0, pCut1, pCut ) )
00525         {
00526             assert( pCut->nFanins == 0 );
00527             continue;
00528         }
00529         // check containment
00530         if ( Csw_CutFilter( p, pObj, pCut ) )
00531         {
00532             assert( pCut->nFanins == 0 );
00533             continue;
00534         }
00535         // create its truth table
00536         pTruth = Csw_CutComputeTruth( p, pCut, pCut0, pCut1, Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
00537         // support minimize the truth table
00538         nFanins = pCut->nFanins;
00539 //        nVars = Csw_CutSupportMinimize( p, pCut ); // leads to quality degradation
00540         nVars = Kit_TruthSupportSize( pTruth, p->nLeafMax );
00541 p->timeCuts += clock() - clk;
00542 
00543         // check for trivial truth tables
00544         if ( nVars == 0 )
00545         {
00546             p->nNodesTriv0++;
00547             return Aig_NotCond( Aig_ManConst1(p->pManRes), !(pTruth[0] & 1) );
00548         }
00549         if ( nVars == 1 )
00550         {
00551             p->nNodesTriv1++;
00552             iVar = Kit_WordFindFirstBit( Kit_TruthSupport(pTruth, p->nLeafMax) );
00553             assert( iVar < pCut->nFanins );
00554             return Aig_NotCond( Aig_ManObj(p->pManRes, pCut->pFanins[iVar]), (pTruth[0] & 1) );
00555         }
00556         if ( nVars == 2 && nFanins > 2 && fUseResub )
00557         {
00558             if ( pObjNew = Csw_ObjTwoVarCut( p, pCut ) )
00559             {
00560                 p->nNodesTriv2++;
00561                 return pObjNew;
00562             }
00563         }
00564 
00565         // check if an equivalent node with the same cut exists
00566 clk = clock();
00567         pObjNew = pCut->nFanins > 2 ? Csw_TableCutLookup( p, pCut ) : NULL;
00568 p->timeHash += clock() - clk;
00569         if ( pObjNew )
00570         {
00571             p->nNodesCuts++;
00572             return pObjNew;
00573         }
00574 
00575         // assign the cost
00576         pCut->Cost = Csw_CutFindCost( p, pCut );
00577         assert( pCut->nFanins > 0 );
00578         assert( pCut->Cost > 0 );
00579     }
00580     p->nNodesTried++;
00581 
00582     // load the resulting cuts into the table
00583 clk = clock();
00584     Csw_ObjForEachCut( p, pObj, pCut, i )
00585     {
00586         if ( pCut->nFanins > 2 )
00587         {
00588             assert( pCut->Cost > 0 );
00589             Csw_TableCutInsert( p, pCut );
00590         }
00591     }
00592 p->timeHash += clock() - clk;
00593 
00594     // return the node if could not replace it
00595     return pObj;
00596 }

int Csw_TableCountCuts ( Csw_Man_t *  p  ) 

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

Synopsis [Returns the total number of cuts in the table.]

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file cswTable.c.

00080 {
00081     Csw_Cut_t * pEnt;
00082     int i, Counter = 0;
00083     for ( i = 0; i < p->nTableSize; i++ )
00084         for ( pEnt = p->pTable[i]; pEnt; pEnt = pEnt->pNext )
00085             Counter++;
00086     return Counter;
00087 }

void Csw_TableCutInsert ( Csw_Man_t *  p,
Csw_Cut_t *  pCut 
)

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

Synopsis [Adds the cut to the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file cswTable.c.

00101 {
00102     int iEntry = Csw_CutHash(pCut) % p->nTableSize;
00103     pCut->pNext = p->pTable[iEntry];
00104     p->pTable[iEntry] = pCut;
00105 }

Aig_Obj_t* Csw_TableCutLookup ( Csw_Man_t *  p,
Csw_Cut_t *  pCut 
)

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

Synopsis [Returns an equivalent node if it exists.]

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file cswTable.c.

00119 {
00120     Aig_Obj_t * pRes = NULL;
00121     Csw_Cut_t * pEnt;
00122     unsigned * pTruthNew, * pTruthOld;
00123     int iEntry = Csw_CutHash(pCut) % p->nTableSize;
00124     for ( pEnt = p->pTable[iEntry]; pEnt; pEnt = pEnt->pNext )
00125     {
00126         if ( pEnt->nFanins != pCut->nFanins )
00127             continue;
00128         if ( pEnt->uSign != pCut->uSign )
00129             continue;
00130         if ( memcmp( pEnt->pFanins, pCut->pFanins, sizeof(int) * pCut->nFanins ) )
00131             continue;
00132         pTruthOld = Csw_CutTruth(pEnt);
00133         pTruthNew = Csw_CutTruth(pCut);
00134         if ( (pTruthOld[0] & 1) == (pTruthNew[0] & 1) )
00135         {
00136             if ( Kit_TruthIsEqual( pTruthOld, pTruthNew, pCut->nFanins ) )
00137             {
00138                 pRes = Aig_ManObj( p->pManRes, pEnt->iNode );
00139                 assert( pRes->fPhase == Aig_ManObj( p->pManRes, pCut->iNode )->fPhase );
00140                 break;
00141             }
00142         }
00143         else
00144         {
00145             if ( Kit_TruthIsOpposite( pTruthOld, pTruthNew, pCut->nFanins ) )
00146             {
00147                 pRes = Aig_Not( Aig_ManObj( p->pManRes, pEnt->iNode ) );
00148                 assert( Aig_Regular(pRes)->fPhase != Aig_ManObj( p->pManRes, pCut->iNode )->fPhase );
00149                 break;
00150             }
00151         }
00152     }
00153     return pRes;
00154 }

Generated on Tue Jan 5 12:18:16 2010 for abc70930 by  doxygen 1.6.1