src/aig/hop/hop.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
Include dependency graph for hop.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  Hop_Obj_t_
struct  Hop_Man_t_

Defines

#define AIG_MIN(a, b)   (((a) < (b))? (a) : (b))
#define AIG_MAX(a, b)   (((a) > (b))? (a) : (b))
#define Hop_ManForEachPi(p, pObj, i)   Vec_PtrForEachEntry( p->vPis, pObj, i )
#define Hop_ManForEachPo(p, pObj, i)   Vec_PtrForEachEntry( p->vPos, pObj, i )
#define Hop_ManForEachNode(p, pObj, i)

Typedefs

typedef struct Hop_Man_t_ Hop_Man_t
typedef struct Hop_Obj_t_ Hop_Obj_t
typedef int Hop_Edge_t

Enumerations

enum  Hop_Type_t {
  AIG_NONE, AIG_CONST1, AIG_PI, AIG_PO,
  AIG_AND, AIG_EXOR, AIG_VOID
}

Functions

static int Hop_BitWordNum (int nBits)
static int Hop_TruthWordNum (int nVars)
static int Hop_InfoHasBit (unsigned *p, int i)
static void Hop_InfoSetBit (unsigned *p, int i)
static void Hop_InfoXorBit (unsigned *p, int i)
static int Hop_Base2Log (unsigned n)
static int Hop_Base10Log (unsigned n)
static Hop_Obj_t * Hop_Regular (Hop_Obj_t *p)
static Hop_Obj_t * Hop_Not (Hop_Obj_t *p)
static Hop_Obj_t * Hop_NotCond (Hop_Obj_t *p, int c)
static int Hop_IsComplement (Hop_Obj_t *p)
static Hop_Obj_t * Hop_ManConst0 (Hop_Man_t *p)
static Hop_Obj_t * Hop_ManConst1 (Hop_Man_t *p)
static Hop_Obj_t * Hop_ManGhost (Hop_Man_t *p)
static Hop_Obj_t * Hop_ManPi (Hop_Man_t *p, int i)
static Hop_Obj_t * Hop_ManPo (Hop_Man_t *p, int i)
static Hop_Obj_t * Hop_ManObj (Hop_Man_t *p, int i)
static Hop_Edge_t Hop_EdgeCreate (int Id, int fCompl)
static int Hop_EdgeId (Hop_Edge_t Edge)
static int Hop_EdgeIsComplement (Hop_Edge_t Edge)
static Hop_Edge_t Hop_EdgeRegular (Hop_Edge_t Edge)
static Hop_Edge_t Hop_EdgeNot (Hop_Edge_t Edge)
static Hop_Edge_t Hop_EdgeNotCond (Hop_Edge_t Edge, int fCond)
static int Hop_ManPiNum (Hop_Man_t *p)
static int Hop_ManPoNum (Hop_Man_t *p)
static int Hop_ManAndNum (Hop_Man_t *p)
static int Hop_ManExorNum (Hop_Man_t *p)
static int Hop_ManNodeNum (Hop_Man_t *p)
static int Hop_ManGetCost (Hop_Man_t *p)
static int Hop_ManObjNum (Hop_Man_t *p)
static Hop_Type_t Hop_ObjType (Hop_Obj_t *pObj)
static int Hop_ObjIsNone (Hop_Obj_t *pObj)
static int Hop_ObjIsConst1 (Hop_Obj_t *pObj)
static int Hop_ObjIsPi (Hop_Obj_t *pObj)
static int Hop_ObjIsPo (Hop_Obj_t *pObj)
static int Hop_ObjIsAnd (Hop_Obj_t *pObj)
static int Hop_ObjIsExor (Hop_Obj_t *pObj)
static int Hop_ObjIsNode (Hop_Obj_t *pObj)
static int Hop_ObjIsTerm (Hop_Obj_t *pObj)
static int Hop_ObjIsHash (Hop_Obj_t *pObj)
static int Hop_ObjIsMarkA (Hop_Obj_t *pObj)
static void Hop_ObjSetMarkA (Hop_Obj_t *pObj)
static void Hop_ObjClearMarkA (Hop_Obj_t *pObj)
static void Hop_ObjSetTravId (Hop_Obj_t *pObj, int TravId)
static void Hop_ObjSetTravIdCurrent (Hop_Man_t *p, Hop_Obj_t *pObj)
static void Hop_ObjSetTravIdPrevious (Hop_Man_t *p, Hop_Obj_t *pObj)
static int Hop_ObjIsTravIdCurrent (Hop_Man_t *p, Hop_Obj_t *pObj)
static int Hop_ObjIsTravIdPrevious (Hop_Man_t *p, Hop_Obj_t *pObj)
static int Hop_ObjTravId (Hop_Obj_t *pObj)
static int Hop_ObjPhase (Hop_Obj_t *pObj)
static int Hop_ObjRefs (Hop_Obj_t *pObj)
static void Hop_ObjRef (Hop_Obj_t *pObj)
static void Hop_ObjDeref (Hop_Obj_t *pObj)
static void Hop_ObjClearRef (Hop_Obj_t *pObj)
static int Hop_ObjFaninC0 (Hop_Obj_t *pObj)
static int Hop_ObjFaninC1 (Hop_Obj_t *pObj)
static Hop_Obj_t * Hop_ObjFanin0 (Hop_Obj_t *pObj)
static Hop_Obj_t * Hop_ObjFanin1 (Hop_Obj_t *pObj)
static Hop_Obj_t * Hop_ObjChild0 (Hop_Obj_t *pObj)
static Hop_Obj_t * Hop_ObjChild1 (Hop_Obj_t *pObj)
static Hop_Obj_t * Hop_ObjChild0Copy (Hop_Obj_t *pObj)
static Hop_Obj_t * Hop_ObjChild1Copy (Hop_Obj_t *pObj)
static int Hop_ObjLevel (Hop_Obj_t *pObj)
static int Hop_ObjLevelNew (Hop_Obj_t *pObj)
static int Hop_ObjFaninPhase (Hop_Obj_t *pObj)
static void Hop_ObjClean (Hop_Obj_t *pObj)
static int Hop_ObjWhatFanin (Hop_Obj_t *pObj, Hop_Obj_t *pFanin)
static int Hop_ObjFanoutC (Hop_Obj_t *pObj, Hop_Obj_t *pFanout)
static Hop_Obj_t * Hop_ObjCreateGhost (Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1, Hop_Type_t Type)
static Hop_Obj_t * Hop_ManFetchMemory (Hop_Man_t *p)
static void Hop_ManRecycleMemory (Hop_Man_t *p, Hop_Obj_t *pEntry)
Hop_Man_t * Hop_ManBalance (Hop_Man_t *p, int fUpdateLevel)
Hop_Obj_t * Hop_NodeBalanceBuildSuper (Hop_Man_t *p, Vec_Ptr_t *vSuper, Hop_Type_t Type, int fUpdateLevel)
int Hop_ManCheck (Hop_Man_t *p)
Vec_Ptr_t * Hop_ManDfs (Hop_Man_t *p)
Vec_Ptr_t * Hop_ManDfsNode (Hop_Man_t *p, Hop_Obj_t *pNode)
int Hop_ManCountLevels (Hop_Man_t *p)
void Hop_ManCreateRefs (Hop_Man_t *p)
int Hop_DagSize (Hop_Obj_t *pObj)
void Hop_ConeUnmark_rec (Hop_Obj_t *pObj)
Hop_Obj_t * Hop_Transfer (Hop_Man_t *pSour, Hop_Man_t *pDest, Hop_Obj_t *pObj, int nVars)
Hop_Obj_t * Hop_Compose (Hop_Man_t *p, Hop_Obj_t *pRoot, Hop_Obj_t *pFunc, int iVar)
Hop_Man_t * Hop_ManStart ()
Hop_Man_t * Hop_ManDup (Hop_Man_t *p)
void Hop_ManStop (Hop_Man_t *p)
int Hop_ManCleanup (Hop_Man_t *p)
void Hop_ManPrintStats (Hop_Man_t *p)
void Hop_ManStartMemory (Hop_Man_t *p)
void Hop_ManStopMemory (Hop_Man_t *p)
Hop_Obj_t * Hop_ObjCreatePi (Hop_Man_t *p)
Hop_Obj_t * Hop_ObjCreatePo (Hop_Man_t *p, Hop_Obj_t *pDriver)
Hop_Obj_t * Hop_ObjCreate (Hop_Man_t *p, Hop_Obj_t *pGhost)
void Hop_ObjConnect (Hop_Man_t *p, Hop_Obj_t *pObj, Hop_Obj_t *pFan0, Hop_Obj_t *pFan1)
void Hop_ObjDisconnect (Hop_Man_t *p, Hop_Obj_t *pObj)
void Hop_ObjDelete (Hop_Man_t *p, Hop_Obj_t *pObj)
void Hop_ObjDelete_rec (Hop_Man_t *p, Hop_Obj_t *pObj)
Hop_Obj_t * Hop_ObjRepr (Hop_Obj_t *pObj)
void Hop_ObjCreateChoice (Hop_Obj_t *pOld, Hop_Obj_t *pNew)
Hop_Obj_t * Hop_IthVar (Hop_Man_t *p, int i)
Hop_Obj_t * Hop_Oper (Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1, Hop_Type_t Type)
Hop_Obj_t * Hop_And (Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Hop_Obj_t * Hop_Or (Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Hop_Obj_t * Hop_Exor (Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Hop_Obj_t * Hop_Mux (Hop_Man_t *p, Hop_Obj_t *pC, Hop_Obj_t *p1, Hop_Obj_t *p0)
Hop_Obj_t * Hop_Maj (Hop_Man_t *p, Hop_Obj_t *pA, Hop_Obj_t *pB, Hop_Obj_t *pC)
Hop_Obj_t * Hop_Miter (Hop_Man_t *p, Vec_Ptr_t *vPairs)
Hop_Obj_t * Hop_CreateAnd (Hop_Man_t *p, int nVars)
Hop_Obj_t * Hop_CreateOr (Hop_Man_t *p, int nVars)
Hop_Obj_t * Hop_CreateExor (Hop_Man_t *p, int nVars)
Hop_Obj_t * Hop_TableLookup (Hop_Man_t *p, Hop_Obj_t *pGhost)
void Hop_TableInsert (Hop_Man_t *p, Hop_Obj_t *pObj)
void Hop_TableDelete (Hop_Man_t *p, Hop_Obj_t *pObj)
int Hop_TableCountEntries (Hop_Man_t *p)
void Hop_TableProfile (Hop_Man_t *p)
void Hop_ManIncrementTravId (Hop_Man_t *p)
void Hop_ManCleanData (Hop_Man_t *p)
void Hop_ObjCleanData_rec (Hop_Obj_t *pObj)
void Hop_ObjCollectMulti (Hop_Obj_t *pFunc, Vec_Ptr_t *vSuper)
int Hop_ObjIsMuxType (Hop_Obj_t *pObj)
int Hop_ObjRecognizeExor (Hop_Obj_t *pObj, Hop_Obj_t **ppFan0, Hop_Obj_t **ppFan1)
Hop_Obj_t * Hop_ObjRecognizeMux (Hop_Obj_t *pObj, Hop_Obj_t **ppObjT, Hop_Obj_t **ppObjE)
void Hop_ObjPrintEqn (FILE *pFile, Hop_Obj_t *pObj, Vec_Vec_t *vLevels, int Level)
void Hop_ObjPrintVerilog (FILE *pFile, Hop_Obj_t *pObj, Vec_Vec_t *vLevels, int Level)
void Hop_ObjPrintVerbose (Hop_Obj_t *pObj, int fHaig)
void Hop_ManPrintVerbose (Hop_Man_t *p, int fHaig)
void Hop_ManDumpBlif (Hop_Man_t *p, char *pFileName)

Define Documentation

#define AIG_MAX ( a,
b   )     (((a) > (b))? (a) : (b))

Definition at line 113 of file hop.h.

#define AIG_MIN ( a,
b   )     (((a) < (b))? (a) : (b))

MACRO DEFINITIONS ///

Definition at line 112 of file hop.h.

#define Hop_ManForEachNode ( p,
pObj,
i   ) 
Value:
for ( i = 0; i < p->nTableSize; i++ )                                       \
        if ( ((pObj) = p->pTable[i]) == NULL ) {} else

Definition at line 265 of file hop.h.

#define Hop_ManForEachPi ( p,
pObj,
i   )     Vec_PtrForEachEntry( p->vPis, pObj, i )

ITERATORS ///

Definition at line 259 of file hop.h.

#define Hop_ManForEachPo ( p,
pObj,
i   )     Vec_PtrForEachEntry( p->vPos, pObj, i )

Definition at line 262 of file hop.h.

Typedef Documentation

typedef int Hop_Edge_t

Definition at line 50 of file hop.h.

typedef struct Hop_Man_t_ Hop_Man_t

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

FileName [hop.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Minimalistic And-Inverter Graph package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
hop.h,v 1.00 2006/05/11 00:00:00 alanmi Exp

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

Definition at line 48 of file hop.h.

typedef struct Hop_Obj_t_ Hop_Obj_t

Definition at line 49 of file hop.h.

Enumeration Type Documentation

enum Hop_Type_t
Enumerator:
AIG_NONE 
AIG_CONST1 
AIG_PI 
AIG_PO 
AIG_AND 
AIG_EXOR 
AIG_VOID 

Definition at line 53 of file hop.h.

00053              { 
00054     AIG_NONE,                        // 0: non-existent object
00055     AIG_CONST1,                      // 1: constant 1 
00056     AIG_PI,                          // 2: primary input
00057     AIG_PO,                          // 3: primary output
00058     AIG_AND,                         // 4: AND node
00059     AIG_EXOR,                        // 5: EXOR node
00060     AIG_VOID                         // 6: unused object
00061 } Hop_Type_t;

Function Documentation

Hop_Obj_t* Hop_And ( Hop_Man_t *  p,
Hop_Obj_t *  p0,
Hop_Obj_t *  p1 
)

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

Synopsis [Performs canonicization step.]

Description [The argument nodes can be complemented.]

SideEffects []

SeeAlso []

Definition at line 101 of file hopOper.c.

00102 {
00103     Hop_Obj_t * pGhost, * pResult;
00104 //    Hop_Obj_t * pFan0, * pFan1;
00105     // check trivial cases
00106     if ( p0 == p1 )
00107         return p0;
00108     if ( p0 == Hop_Not(p1) )
00109         return Hop_Not(p->pConst1);
00110     if ( Hop_Regular(p0) == p->pConst1 )
00111         return p0 == p->pConst1 ? p1 : Hop_Not(p->pConst1);
00112     if ( Hop_Regular(p1) == p->pConst1 )
00113         return p1 == p->pConst1 ? p0 : Hop_Not(p->pConst1);
00114     // check if it can be an EXOR gate
00115 //    if ( Hop_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
00116 //        return Hop_Exor( p, pFan0, pFan1 );
00117     // check the table
00118     pGhost = Hop_ObjCreateGhost( p, p0, p1, AIG_AND );
00119     if ( pResult = Hop_TableLookup( p, pGhost ) )
00120         return pResult;
00121     return Hop_ObjCreate( p, pGhost );
00122 }

static int Hop_Base10Log ( unsigned  n  )  [inline, static]

Definition at line 125 of file hop.h.

00125 { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }

static int Hop_Base2Log ( unsigned  n  )  [inline, static]

Definition at line 124 of file hop.h.

00124 { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }

static int Hop_BitWordNum ( int  nBits  )  [inline, static]

Definition at line 119 of file hop.h.

00119 { return (nBits>>5) + ((nBits&31) > 0);           }

Hop_Obj_t* Hop_Compose ( Hop_Man_t *  p,
Hop_Obj_t *  pRoot,
Hop_Obj_t *  pFunc,
int  iVar 
)

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

Synopsis [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]

Description []

SideEffects []

SeeAlso []

Definition at line 380 of file hopDfs.c.

00381 {
00382     // quit if the PI variable is not defined
00383     if ( iVar >= Hop_ManPiNum(p) )
00384     {
00385         printf( "Hop_Compose(): The PI variable %d is not defined.\n", iVar );
00386         return NULL;
00387     }
00388     // recursively perform composition
00389     Hop_Compose_rec( p, Hop_Regular(pRoot), pFunc, Hop_ManPi(p, iVar) );
00390     // clear the markings
00391     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
00392     return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
00393 }

void Hop_ConeUnmark_rec ( Hop_Obj_t *  pObj  ) 

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

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 254 of file hopDfs.c.

00255 {
00256     assert( !Hop_IsComplement(pObj) );
00257     if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
00258         return;
00259     Hop_ConeUnmark_rec( Hop_ObjFanin0(pObj) ); 
00260     Hop_ConeUnmark_rec( Hop_ObjFanin1(pObj) );
00261     assert( Hop_ObjIsMarkA(pObj) ); // loop detection
00262     Hop_ObjClearMarkA( pObj );
00263 }

Hop_Obj_t* Hop_CreateAnd ( Hop_Man_t *  p,
int  nVars 
)

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

Synopsis [Creates AND function with nVars inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file hopOper.c.

00318 {
00319     Hop_Obj_t * pFunc;
00320     int i;
00321     pFunc = Hop_ManConst1( p );
00322     for ( i = 0; i < nVars; i++ )
00323         pFunc = Hop_And( p, pFunc, Hop_IthVar(p, i) );
00324     return pFunc;
00325 }

Hop_Obj_t* Hop_CreateExor ( Hop_Man_t *  p,
int  nVars 
)

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

Synopsis [Creates AND function with nVars inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 359 of file hopOper.c.

00360 {
00361     Hop_Obj_t * pFunc;
00362     int i;
00363     pFunc = Hop_ManConst0( p );
00364     for ( i = 0; i < nVars; i++ )
00365         pFunc = Hop_Exor( p, pFunc, Hop_IthVar(p, i) );
00366     return pFunc;
00367 }

Hop_Obj_t* Hop_CreateOr ( Hop_Man_t *  p,
int  nVars 
)

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

Synopsis [Creates AND function with nVars inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 338 of file hopOper.c.

00339 {
00340     Hop_Obj_t * pFunc;
00341     int i;
00342     pFunc = Hop_ManConst0( p );
00343     for ( i = 0; i < nVars; i++ )
00344         pFunc = Hop_Or( p, pFunc, Hop_IthVar(p, i) );
00345     return pFunc;
00346 }

int Hop_DagSize ( Hop_Obj_t *  pObj  ) 

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

Synopsis [Counts the number of AIG nodes rooted at this cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 276 of file hopDfs.c.

00277 {
00278     int Counter;
00279     Counter = Hop_ConeCountAndMark_rec( Hop_Regular(pObj) );
00280     Hop_ConeUnmark_rec( Hop_Regular(pObj) );
00281     return Counter;
00282 }

static Hop_Edge_t Hop_EdgeCreate ( int  Id,
int  fCompl 
) [inline, static]

Definition at line 139 of file hop.h.

00139 { return (Id << 1) | fCompl;             }

static int Hop_EdgeId ( Hop_Edge_t  Edge  )  [inline, static]

Definition at line 140 of file hop.h.

00140 { return Edge >> 1;                      }

static int Hop_EdgeIsComplement ( Hop_Edge_t  Edge  )  [inline, static]

Definition at line 141 of file hop.h.

00141 { return Edge & 1;                       }

static Hop_Edge_t Hop_EdgeNot ( Hop_Edge_t  Edge  )  [inline, static]

Definition at line 143 of file hop.h.

00143 { return Edge ^ 1;                       }

static Hop_Edge_t Hop_EdgeNotCond ( Hop_Edge_t  Edge,
int  fCond 
) [inline, static]

Definition at line 144 of file hop.h.

00144 { return Edge ^ fCond;                   }

static Hop_Edge_t Hop_EdgeRegular ( Hop_Edge_t  Edge  )  [inline, static]

Definition at line 142 of file hop.h.

00142 { return (Edge >> 1) << 1;               }

Hop_Obj_t* Hop_Exor ( Hop_Man_t *  p,
Hop_Obj_t *  p0,
Hop_Obj_t *  p1 
)

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

Synopsis [Performs canonicization step.]

Description [The argument nodes can be complemented.]

SideEffects []

SeeAlso []

Definition at line 135 of file hopOper.c.

00136 {
00137 /*
00138     Hop_Obj_t * pGhost, * pResult;
00139     // check trivial cases
00140     if ( p0 == p1 )
00141         return Hop_Not(p->pConst1);
00142     if ( p0 == Hop_Not(p1) )
00143         return p->pConst1;
00144     if ( Hop_Regular(p0) == p->pConst1 )
00145         return Hop_NotCond( p1, p0 == p->pConst1 );
00146     if ( Hop_Regular(p1) == p->pConst1 )
00147         return Hop_NotCond( p0, p1 == p->pConst1 );
00148     // check the table
00149     pGhost = Hop_ObjCreateGhost( p, p0, p1, AIG_EXOR );
00150     if ( pResult = Hop_TableLookup( p, pGhost ) )
00151         return pResult;
00152     return Hop_ObjCreate( p, pGhost );
00153 */
00154     return Hop_Or( p, Hop_And(p, p0, Hop_Not(p1)), Hop_And(p, Hop_Not(p0), p1) );
00155 }

static int Hop_InfoHasBit ( unsigned *  p,
int  i 
) [inline, static]

Definition at line 121 of file hop.h.

00121 { return (p[(i)>>5] & (1<<((i) & 31))) > 0;       }

static void Hop_InfoSetBit ( unsigned *  p,
int  i 
) [inline, static]

Definition at line 122 of file hop.h.

00122 { p[(i)>>5] |= (1<<((i) & 31));                   }

static void Hop_InfoXorBit ( unsigned *  p,
int  i 
) [inline, static]

Definition at line 123 of file hop.h.

00123 { p[(i)>>5] ^= (1<<((i) & 31));                   }

static int Hop_IsComplement ( Hop_Obj_t *  p  )  [inline, static]

Definition at line 130 of file hop.h.

00130 { return (int )(((unsigned long)p) & 01);              }

Hop_Obj_t* Hop_IthVar ( Hop_Man_t *  p,
int  i 
)

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

Synopsis [Returns i-th elementary variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file hopOper.c.

00061 {
00062     int v;
00063     for ( v = Hop_ManPiNum(p); v <= i; v++ )
00064         Hop_ObjCreatePi( p );
00065     assert( i < Vec_PtrSize(p->vPis) );
00066     return Hop_ManPi( p, i );
00067 }

Hop_Obj_t* Hop_Maj ( Hop_Man_t *  p,
Hop_Obj_t *  pA,
Hop_Obj_t *  pB,
Hop_Obj_t *  pC 
)

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

Synopsis [Implements ITE operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 239 of file hopOper.c.

00240 {
00241     return Hop_Or( p, Hop_Or(p, Hop_And(p, pA, pB), Hop_And(p, pA, pC)), Hop_And(p, pB, pC) );
00242 }

static int Hop_ManAndNum ( Hop_Man_t *  p  )  [inline, static]

Definition at line 148 of file hop.h.

00148 { return p->nObjs[AIG_AND];                   }

Hop_Man_t* Hop_ManBalance ( Hop_Man_t *  p,
int  fUpdateLevel 
)

FUNCTION DECLARATIONS ///

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

Synopsis [Performs algebraic balancing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file hopBalance.c.

00049 {
00050     Hop_Man_t * pNew;
00051     Hop_Obj_t * pObj, * pObjNew;
00052     Vec_Vec_t * vStore;
00053     int i;
00054     // create the new manager 
00055     pNew = Hop_ManStart();
00056     pNew->fRefCount = 0;
00057     // map the PI nodes
00058     Hop_ManCleanData( p );
00059     Hop_ManConst1(p)->pData = Hop_ManConst1(pNew);
00060     Hop_ManForEachPi( p, pObj, i )
00061         pObj->pData = Hop_ObjCreatePi(pNew);
00062     // balance the AIG
00063     vStore = Vec_VecAlloc( 50 );
00064     Hop_ManForEachPo( p, pObj, i )
00065     {
00066         pObjNew = Hop_NodeBalance_rec( pNew, Hop_ObjFanin0(pObj), vStore, 0, fUpdateLevel );
00067         Hop_ObjCreatePo( pNew, Hop_NotCond( pObjNew, Hop_ObjFaninC0(pObj) ) );
00068     }
00069     Vec_VecFree( vStore );
00070     // remove dangling nodes
00071 //    Hop_ManCreateRefs( pNew );
00072 //    if ( i = Hop_ManCleanup( pNew ) )
00073 //        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
00074     // check the resulting AIG
00075     if ( !Hop_ManCheck(pNew) )
00076         printf( "Hop_ManBalance(): The check has failed.\n" );
00077     return pNew;
00078 }

int Hop_ManCheck ( Hop_Man_t *  p  ) 

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

FileName [hopCheck.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Minimalistic And-Inverter Graph package.]

Synopsis [AIG checking procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
hopCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

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

Synopsis [Checks the consistency of the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file hopCheck.c.

00043 {
00044     Hop_Obj_t * pObj, * pObj2;
00045     int i;
00046     // check primary inputs
00047     Hop_ManForEachPi( p, pObj, i )
00048     {
00049         if ( Hop_ObjFanin0(pObj) || Hop_ObjFanin1(pObj) )
00050         {
00051             printf( "Hop_ManCheck: The PI node \"%p\" has fanins.\n", pObj );
00052             return 0;
00053         }
00054     }
00055     // check primary outputs
00056     Hop_ManForEachPo( p, pObj, i )
00057     {
00058         if ( !Hop_ObjFanin0(pObj) )
00059         {
00060             printf( "Hop_ManCheck: The PO node \"%p\" has NULL fanin.\n", pObj );
00061             return 0;
00062         }
00063         if ( Hop_ObjFanin1(pObj) )
00064         {
00065             printf( "Hop_ManCheck: The PO node \"%p\" has second fanin.\n", pObj );
00066             return 0;
00067         }
00068     }
00069     // check internal nodes
00070     Hop_ManForEachNode( p, pObj, i )
00071     {
00072         if ( !Hop_ObjFanin0(pObj) || !Hop_ObjFanin1(pObj) )
00073         {
00074             printf( "Hop_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj );
00075             return 0;
00076         }
00077         if ( Hop_ObjFanin0(pObj)->Id >= Hop_ObjFanin1(pObj)->Id )
00078         {
00079             printf( "Hop_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj );
00080             return 0;
00081         }
00082         pObj2 = Hop_TableLookup( p, pObj );
00083         if ( pObj2 != pObj )
00084         {
00085             printf( "Hop_ManCheck: Node \"%p\" is not in the structural hashing table.\n", pObj );
00086             return 0;
00087         }
00088     }
00089     // count the total number of nodes
00090     if ( Hop_ManObjNum(p) != 1 + Hop_ManPiNum(p) + Hop_ManPoNum(p) + Hop_ManAndNum(p) + Hop_ManExorNum(p) )
00091     {
00092         printf( "Hop_ManCheck: The number of created nodes is wrong.\n" );
00093         return 0;
00094     }
00095     // count the number of nodes in the table
00096     if ( Hop_TableCountEntries(p) != Hop_ManAndNum(p) + Hop_ManExorNum(p) )
00097     {
00098         printf( "Hop_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
00099         return 0;
00100     }
00101 //    if ( !Hop_ManIsAcyclic(p) )
00102 //        return 0;
00103     return 1; 
00104 }

void Hop_ManCleanData ( Hop_Man_t *  p  ) 

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

Synopsis [Cleans the data pointers for the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file hopUtil.c.

00061 {
00062     Hop_Obj_t * pObj;
00063     int i;
00064     p->nTravIds = 1;
00065     Hop_ManConst1(p)->pData = NULL;
00066     Hop_ManForEachPi( p, pObj, i )
00067         pObj->pData = NULL;
00068     Hop_ManForEachPo( p, pObj, i )
00069         pObj->pData = NULL;
00070     Hop_ManForEachNode( p, pObj, i )
00071         pObj->pData = NULL;
00072 }

int Hop_ManCleanup ( Hop_Man_t *  p  ) 

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

Synopsis [Returns the number of dangling nodes removed.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file hopMan.c.

00118 {
00119     Vec_Ptr_t * vObjs;
00120     Hop_Obj_t * pNode;
00121     int i, nNodesOld;
00122     assert( p->fRefCount );
00123     nNodesOld = Hop_ManNodeNum(p);
00124     // collect roots of dangling nodes
00125     vObjs = Vec_PtrAlloc( 100 );
00126     Hop_ManForEachNode( p, pNode, i )
00127         if ( Hop_ObjRefs(pNode) == 0 )
00128             Vec_PtrPush( vObjs, pNode );
00129     // recursively remove dangling nodes
00130     Vec_PtrForEachEntry( vObjs, pNode, i )
00131         Hop_ObjDelete_rec( p, pNode );
00132     Vec_PtrFree( vObjs );
00133     return nNodesOld - Hop_ManNodeNum(p);
00134 }

static Hop_Obj_t* Hop_ManConst0 ( Hop_Man_t *  p  )  [inline, static]

Definition at line 132 of file hop.h.

00132 { return Hop_Not(p->pConst1);                     }

static Hop_Obj_t* Hop_ManConst1 ( Hop_Man_t *  p  )  [inline, static]

Definition at line 133 of file hop.h.

00133 { return p->pConst1;                              }

int Hop_ManCountLevels ( Hop_Man_t *  p  ) 

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

Synopsis [Computes the max number of levels in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file hopDfs.c.

00114 {
00115     Vec_Ptr_t * vNodes;
00116     Hop_Obj_t * pObj;
00117     int i, LevelsMax, Level0, Level1;
00118     // initialize the levels
00119     Hop_ManConst1(p)->pData = NULL;
00120     Hop_ManForEachPi( p, pObj, i )
00121         pObj->pData = NULL;
00122     // compute levels in a DFS order
00123     vNodes = Hop_ManDfs( p );
00124     Vec_PtrForEachEntry( vNodes, pObj, i )
00125     {
00126         Level0 = (int)Hop_ObjFanin0(pObj)->pData;
00127         Level1 = (int)Hop_ObjFanin1(pObj)->pData;
00128         pObj->pData = (void *)(1 + Hop_ObjIsExor(pObj) + AIG_MAX(Level0, Level1));
00129     }
00130     Vec_PtrFree( vNodes );
00131     // get levels of the POs
00132     LevelsMax = 0;
00133     Hop_ManForEachPo( p, pObj, i )
00134         LevelsMax = AIG_MAX( LevelsMax, (int)Hop_ObjFanin0(pObj)->pData );
00135     return LevelsMax;
00136 }

void Hop_ManCreateRefs ( Hop_Man_t *  p  ) 

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

Synopsis [Creates correct reference counters at each node.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file hopDfs.c.

00150 {
00151     Hop_Obj_t * pObj;
00152     int i;
00153     if ( p->fRefCount )
00154         return;
00155     p->fRefCount = 1;
00156     // clear refs
00157     Hop_ObjClearRef( Hop_ManConst1(p) );
00158     Hop_ManForEachPi( p, pObj, i )
00159         Hop_ObjClearRef( pObj );
00160     Hop_ManForEachNode( p, pObj, i )
00161         Hop_ObjClearRef( pObj );
00162     Hop_ManForEachPo( p, pObj, i )
00163         Hop_ObjClearRef( pObj );
00164     // set refs
00165     Hop_ManForEachNode( p, pObj, i )
00166     {
00167         Hop_ObjRef( Hop_ObjFanin0(pObj) );
00168         Hop_ObjRef( Hop_ObjFanin1(pObj) );
00169     }
00170     Hop_ManForEachPo( p, pObj, i )
00171         Hop_ObjRef( Hop_ObjFanin0(pObj) );
00172 }

Vec_Ptr_t* Hop_ManDfs ( Hop_Man_t *  p  ) 

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

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file hopDfs.c.

00066 {
00067     Vec_Ptr_t * vNodes;
00068     Hop_Obj_t * pObj;
00069     int i;
00070     vNodes = Vec_PtrAlloc( Hop_ManNodeNum(p) );
00071     Hop_ManForEachNode( p, pObj, i )
00072         Hop_ManDfs_rec( pObj, vNodes );
00073     Hop_ManForEachNode( p, pObj, i )
00074         Hop_ObjClearMarkA(pObj);
00075     return vNodes;
00076 }

Vec_Ptr_t* Hop_ManDfsNode ( Hop_Man_t *  p,
Hop_Obj_t *  pNode 
)

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

Synopsis [Collects internal nodes in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file hopDfs.c.

00090 {
00091     Vec_Ptr_t * vNodes;
00092     Hop_Obj_t * pObj;
00093     int i;
00094     assert( !Hop_IsComplement(pNode) );
00095     vNodes = Vec_PtrAlloc( 16 );
00096     Hop_ManDfs_rec( pNode, vNodes );
00097     Vec_PtrForEachEntry( vNodes, pObj, i )
00098         Hop_ObjClearMarkA(pObj);
00099     return vNodes;
00100 }

void Hop_ManDumpBlif ( Hop_Man_t *  p,
char *  pFileName 
)

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

Synopsis [Writes the AIG into the BLIF file.]

Description []

SideEffects []

SeeAlso []

Definition at line 505 of file hopUtil.c.

00506 {
00507     FILE * pFile;
00508     Vec_Ptr_t * vNodes;
00509     Hop_Obj_t * pObj, * pConst1 = NULL;
00510     int i, nDigits, Counter = 0;
00511     if ( Hop_ManPoNum(p) == 0 )
00512     {
00513         printf( "Hop_ManDumpBlif(): AIG manager does not have POs.\n" );
00514         return;
00515     }
00516     // collect nodes in the DFS order
00517     vNodes = Hop_ManDfs( p );
00518     // assign IDs to objects
00519     Hop_ManConst1(p)->pData = (void *)Counter++;
00520     Hop_ManForEachPi( p, pObj, i )
00521         pObj->pData = (void *)Counter++;
00522     Hop_ManForEachPo( p, pObj, i )
00523         pObj->pData = (void *)Counter++;
00524     Vec_PtrForEachEntry( vNodes, pObj, i )
00525         pObj->pData = (void *)Counter++;
00526     nDigits = Hop_Base10Log( Counter );
00527     // write the file
00528     pFile = fopen( pFileName, "w" );
00529     fprintf( pFile, "# BLIF file written by procedure Hop_ManDumpBlif() in ABC\n" );
00530     fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
00531     fprintf( pFile, ".model test\n" );
00532     // write PIs
00533     fprintf( pFile, ".inputs" );
00534     Hop_ManForEachPi( p, pObj, i )
00535         fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
00536     fprintf( pFile, "\n" );
00537     // write POs
00538     fprintf( pFile, ".outputs" );
00539     Hop_ManForEachPo( p, pObj, i )
00540         fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
00541     fprintf( pFile, "\n" );
00542     // write nodes
00543     Vec_PtrForEachEntry( vNodes, pObj, i )
00544     {
00545         fprintf( pFile, ".names n%0*d n%0*d n%0*d\n", 
00546             nDigits, (int)Hop_ObjFanin0(pObj)->pData, 
00547             nDigits, (int)Hop_ObjFanin1(pObj)->pData, 
00548             nDigits, (int)pObj->pData );
00549         fprintf( pFile, "%d%d 1\n", !Hop_ObjFaninC0(pObj), !Hop_ObjFaninC1(pObj) );
00550     }
00551     // write POs
00552     Hop_ManForEachPo( p, pObj, i )
00553     {
00554         fprintf( pFile, ".names n%0*d n%0*d\n", 
00555             nDigits, (int)Hop_ObjFanin0(pObj)->pData, 
00556             nDigits, (int)pObj->pData );
00557         fprintf( pFile, "%d 1\n", !Hop_ObjFaninC0(pObj) );
00558         if ( Hop_ObjIsConst1(Hop_ObjFanin0(pObj)) )
00559             pConst1 = Hop_ManConst1(p);
00560     }
00561     if ( pConst1 )
00562         fprintf( pFile, ".names n%0*d\n 1\n", nDigits, (int)pConst1->pData );
00563     fprintf( pFile, ".end\n\n" );
00564     fclose( pFile );
00565     Vec_PtrFree( vNodes );
00566 }

Hop_Man_t* Hop_ManDup ( Hop_Man_t *  p  ) 
static int Hop_ManExorNum ( Hop_Man_t *  p  )  [inline, static]

Definition at line 149 of file hop.h.

00149 { return p->nObjs[AIG_EXOR];                  }

static Hop_Obj_t* Hop_ManFetchMemory ( Hop_Man_t *  p  )  [inline, static]

Definition at line 229 of file hop.h.

00230 { 
00231     extern void Hop_ManAddMemory( Hop_Man_t * p );
00232     Hop_Obj_t * pTemp;
00233     if ( p->pListFree == NULL )
00234         Hop_ManAddMemory( p );
00235     pTemp = p->pListFree;
00236     p->pListFree = *((Hop_Obj_t **)pTemp);
00237     memset( pTemp, 0, sizeof(Hop_Obj_t) ); 
00238     if ( p->vObjs )
00239     {
00240         assert( p->nCreated == Vec_PtrSize(p->vObjs) );
00241         Vec_PtrPush( p->vObjs, pTemp );
00242     }
00243     pTemp->Id = p->nCreated++;
00244     return pTemp;
00245 }

static int Hop_ManGetCost ( Hop_Man_t *  p  )  [inline, static]

Definition at line 151 of file hop.h.

00151 { return p->nObjs[AIG_AND]+3*p->nObjs[AIG_EXOR]; }

static Hop_Obj_t* Hop_ManGhost ( Hop_Man_t *  p  )  [inline, static]

Definition at line 134 of file hop.h.

00134 { return &p->Ghost;                               }

void Hop_ManIncrementTravId ( Hop_Man_t *  p  ) 

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

FileName [hopUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Various procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
hopUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

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

Synopsis [Increments the current traversal ID of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file hopUtil.c.

00043 {
00044     if ( p->nTravIds >= (1<<30)-1 )
00045         Hop_ManCleanData( p );
00046     p->nTravIds++;
00047 }

static int Hop_ManNodeNum ( Hop_Man_t *  p  )  [inline, static]

Definition at line 150 of file hop.h.

00150 { return p->nObjs[AIG_AND]+p->nObjs[AIG_EXOR];}

static Hop_Obj_t* Hop_ManObj ( Hop_Man_t *  p,
int  i 
) [inline, static]

Definition at line 137 of file hop.h.

00137 { return p->vObjs ? (Hop_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL;  }

static int Hop_ManObjNum ( Hop_Man_t *  p  )  [inline, static]

Definition at line 152 of file hop.h.

00152 { return p->nCreated - p->nDeleted;           }

static Hop_Obj_t* Hop_ManPi ( Hop_Man_t *  p,
int  i 
) [inline, static]

Definition at line 135 of file hop.h.

00135 { return (Hop_Obj_t *)Vec_PtrEntry(p->vPis, i);   }

static int Hop_ManPiNum ( Hop_Man_t *  p  )  [inline, static]

Definition at line 146 of file hop.h.

00146 { return p->nObjs[AIG_PI];                    }

static Hop_Obj_t* Hop_ManPo ( Hop_Man_t *  p,
int  i 
) [inline, static]

Definition at line 136 of file hop.h.

00136 { return (Hop_Obj_t *)Vec_PtrEntry(p->vPos, i);   }

static int Hop_ManPoNum ( Hop_Man_t *  p  )  [inline, static]

Definition at line 147 of file hop.h.

00147 { return p->nObjs[AIG_PO];                    }

void Hop_ManPrintStats ( Hop_Man_t *  p  ) 

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

Synopsis [Stops the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file hopMan.c.

00148 {
00149     printf( "PI/PO = %d/%d. ", Hop_ManPiNum(p), Hop_ManPoNum(p) );
00150     printf( "A = %7d. ",       Hop_ManAndNum(p) );
00151     printf( "X = %5d. ",       Hop_ManExorNum(p) );
00152     printf( "Cre = %7d. ",     p->nCreated );
00153     printf( "Del = %7d. ",     p->nDeleted );
00154     printf( "Lev = %3d. ",     Hop_ManCountLevels(p) );
00155     printf( "\n" );
00156 }

void Hop_ManPrintVerbose ( Hop_Man_t *  p,
int  fHaig 
)

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

Synopsis [Prints node in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 479 of file hopUtil.c.

00480 {
00481     Vec_Ptr_t * vNodes;
00482     Hop_Obj_t * pObj;
00483     int i;
00484     printf( "PIs: " );
00485     Hop_ManForEachPi( p, pObj, i )
00486         printf( " %p", pObj );
00487     printf( "\n" );
00488     vNodes = Hop_ManDfs( p );
00489     Vec_PtrForEachEntry( vNodes, pObj, i )
00490         Hop_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
00491     printf( "\n" );
00492 }

static void Hop_ManRecycleMemory ( Hop_Man_t *  p,
Hop_Obj_t *  pEntry 
) [inline, static]

Definition at line 246 of file hop.h.

00247 {
00248     pEntry->Type = AIG_NONE; // distinquishes dead node from live node
00249     *((Hop_Obj_t **)pEntry) = p->pListFree;
00250     p->pListFree = pEntry;
00251 }

Hop_Man_t* Hop_ManStart (  ) 

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

FileName [hopMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Minimalistic And-Inverter Graph package.]

Synopsis [AIG manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
hopMan.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

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

Synopsis [Starts the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file hopMan.c.

00043 {
00044     Hop_Man_t * p;
00045     // start the manager
00046     p = ALLOC( Hop_Man_t, 1 );
00047     memset( p, 0, sizeof(Hop_Man_t) );
00048     // perform initializations
00049     p->nTravIds = 1;
00050     p->fRefCount = 1;
00051     p->fCatchExor = 0;
00052     // allocate arrays for nodes
00053     p->vPis = Vec_PtrAlloc( 100 );
00054     p->vPos = Vec_PtrAlloc( 100 );
00055     // prepare the internal memory manager
00056     Hop_ManStartMemory( p );
00057     // create the constant node
00058     p->pConst1 = Hop_ManFetchMemory( p );
00059     p->pConst1->Type = AIG_CONST1;
00060     p->pConst1->fPhase = 1;
00061     p->nCreated = 1;
00062     // start the table
00063 //    p->nTableSize = 107;
00064     p->nTableSize = 10007;
00065     p->pTable = ALLOC( Hop_Obj_t *, p->nTableSize );
00066     memset( p->pTable, 0, sizeof(Hop_Obj_t *) * p->nTableSize );
00067     return p;
00068 }

void Hop_ManStartMemory ( Hop_Man_t *  p  ) 

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

Synopsis [Starts the internal memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file hopMem.c.

00047 {
00048     p->vChunks = Vec_PtrAlloc( 128 );
00049     p->vPages = Vec_PtrAlloc( 128 );
00050 }

void Hop_ManStop ( Hop_Man_t *  p  ) 

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

Synopsis [Stops the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file hopMan.c.

00082 {
00083     Hop_Obj_t * pObj;
00084     int i;
00085     // make sure the nodes have clean marks
00086     pObj = Hop_ManConst1(p);
00087     assert( !pObj->fMarkA && !pObj->fMarkB );
00088     Hop_ManForEachPi( p, pObj, i )
00089         assert( !pObj->fMarkA && !pObj->fMarkB );
00090     Hop_ManForEachPo( p, pObj, i )
00091         assert( !pObj->fMarkA && !pObj->fMarkB );
00092     Hop_ManForEachNode( p, pObj, i )
00093         assert( !pObj->fMarkA && !pObj->fMarkB );
00094     // print time
00095     if ( p->time1 ) { PRT( "time1", p->time1 ); }
00096     if ( p->time2 ) { PRT( "time2", p->time2 ); }
00097 //    Hop_TableProfile( p );
00098     if ( p->vChunks )  Hop_ManStopMemory( p );
00099     if ( p->vPis )     Vec_PtrFree( p->vPis );
00100     if ( p->vPos )     Vec_PtrFree( p->vPos );
00101     if ( p->vObjs )    Vec_PtrFree( p->vObjs );
00102     free( p->pTable );
00103     free( p );
00104 }

void Hop_ManStopMemory ( Hop_Man_t *  p  ) 

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

Synopsis [Stops the internal memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file hopMem.c.

00064 {
00065     void * pMemory;
00066     int i;
00067     Vec_PtrForEachEntry( p->vChunks, pMemory, i )
00068         free( pMemory );
00069     Vec_PtrFree( p->vChunks );
00070     Vec_PtrFree( p->vPages );
00071     p->pListFree = NULL;
00072 }

Hop_Obj_t* Hop_Miter ( Hop_Man_t *  p,
Vec_Ptr_t *  vPairs 
)

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

Synopsis [Implements the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 294 of file hopOper.c.

00295 {
00296     int i;
00297     assert( vPairs->nSize > 0 );
00298     assert( vPairs->nSize % 2 == 0 );
00299     // go through the cubes of the node's SOP
00300     for ( i = 0; i < vPairs->nSize; i += 2 )
00301         vPairs->pArray[i/2] = Hop_Not( Hop_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) );
00302     vPairs->nSize = vPairs->nSize/2;
00303     return Hop_Not( Hop_Multi_rec( p, (Hop_Obj_t **)vPairs->pArray, vPairs->nSize, AIG_AND ) );
00304 }

Hop_Obj_t* Hop_Mux ( Hop_Man_t *  p,
Hop_Obj_t *  pC,
Hop_Obj_t *  p1,
Hop_Obj_t *  p0 
)

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

Synopsis [Implements ITE operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 184 of file hopOper.c.

00185 {
00186 /*    
00187     Hop_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
00188     int Count0, Count1;
00189     // consider trivial cases
00190     if ( p0 == Hop_Not(p1) )
00191         return Hop_Exor( p, pC, p0 );
00192     // other cases can be added
00193     // implement the first MUX (F = C * x1 + C' * x0)
00194 
00195     // check for constants here!!!
00196 
00197     pTempA1 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, pC,          p1, AIG_AND) );
00198     pTempA2 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pC), p0, AIG_AND) );
00199     if ( pTempA1 && pTempA2 )
00200     {
00201         pTemp = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pTempA1), Hop_Not(pTempA2), AIG_AND) );
00202         if ( pTemp ) return Hop_Not(pTemp);
00203     }
00204     Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
00205     // implement the second MUX (F' = C * x1' + C' * x0')
00206     pTempB1 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, pC,          Hop_Not(p1), AIG_AND) );
00207     pTempB2 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pC), Hop_Not(p0), AIG_AND) );
00208     if ( pTempB1 && pTempB2 )
00209     {
00210         pTemp = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pTempB1), Hop_Not(pTempB2), AIG_AND) );
00211         if ( pTemp ) return pTemp;
00212     }
00213     Count1 = (pTempB1 != NULL) + (pTempB2 != NULL);
00214     // compare and decide which one to implement
00215     if ( Count0 >= Count1 )
00216     {
00217         pTempA1 = pTempA1? pTempA1 : Hop_And(p, pC,          p1);
00218         pTempA2 = pTempA2? pTempA2 : Hop_And(p, Hop_Not(pC), p0);
00219         return Hop_Or( p, pTempA1, pTempA2 );
00220     }
00221     pTempB1 = pTempB1? pTempB1 : Hop_And(p, pC,          Hop_Not(p1));
00222     pTempB2 = pTempB2? pTempB2 : Hop_And(p, Hop_Not(pC), Hop_Not(p0));
00223     return Hop_Not( Hop_Or( p, pTempB1, pTempB2 ) );
00224 */
00225     return Hop_Or( p, Hop_And(p, pC, p1), Hop_And(p, Hop_Not(pC), p0) );
00226 }

Hop_Obj_t* Hop_NodeBalanceBuildSuper ( Hop_Man_t *  p,
Vec_Ptr_t *  vSuper,
Hop_Type_t  Type,
int  fUpdateLevel 
)

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

Synopsis [Builds implication supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file hopBalance.c.

00236 {
00237     Hop_Obj_t * pObj1, * pObj2;
00238     int LeftBound;
00239     assert( vSuper->nSize > 1 );
00240     // sort the new nodes by level in the decreasing order
00241     Vec_PtrSort( vSuper, Hop_NodeCompareLevelsDecrease );
00242     // balance the nodes
00243     while ( vSuper->nSize > 1 )
00244     {
00245         // find the left bound on the node to be paired
00246         LeftBound = (!fUpdateLevel)? 0 : Hop_NodeBalanceFindLeft( vSuper );
00247         // find the node that can be shared (if no such node, randomize choice)
00248         Hop_NodeBalancePermute( p, vSuper, LeftBound, Type == AIG_EXOR );
00249         // pull out the last two nodes
00250         pObj1 = Vec_PtrPop(vSuper);
00251         pObj2 = Vec_PtrPop(vSuper);
00252         Hop_NodeBalancePushUniqueOrderByLevel( vSuper, Hop_Oper(p, pObj1, pObj2, Type) );
00253     }
00254     return Vec_PtrEntry(vSuper, 0);
00255 }

static Hop_Obj_t* Hop_Not ( Hop_Obj_t *  p  )  [inline, static]

Definition at line 128 of file hop.h.

00128 { return (Hop_Obj_t *)((unsigned long)(p) ^  01);      }

static Hop_Obj_t* Hop_NotCond ( Hop_Obj_t *  p,
int  c 
) [inline, static]

Definition at line 129 of file hop.h.

00129 { return (Hop_Obj_t *)((unsigned long)(p) ^ (c));      }

static Hop_Obj_t* Hop_ObjChild0 ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 185 of file hop.h.

00185 { return pObj->pFanin0;                          }

static Hop_Obj_t* Hop_ObjChild0Copy ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 187 of file hop.h.

00187 { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL;  }

static Hop_Obj_t* Hop_ObjChild1 ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 186 of file hop.h.

00186 { return pObj->pFanin1;                          }

static Hop_Obj_t* Hop_ObjChild1Copy ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 188 of file hop.h.

00188 { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL;  }

static void Hop_ObjClean ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 192 of file hop.h.

00192 { memset( pObj, 0, sizeof(Hop_Obj_t) ); }

void Hop_ObjCleanData_rec ( Hop_Obj_t *  pObj  ) 

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

Synopsis [Recursively cleans the data pointers in the cone of the node.]

Description [Applicable to small AIGs only because no caching is performed.]

SideEffects []

SeeAlso []

Definition at line 85 of file hopUtil.c.

00086 {
00087     assert( !Hop_IsComplement(pObj) );
00088     assert( !Hop_ObjIsPo(pObj) );
00089     if ( Hop_ObjIsAnd(pObj) )
00090     {
00091         Hop_ObjCleanData_rec( Hop_ObjFanin0(pObj) );
00092         Hop_ObjCleanData_rec( Hop_ObjFanin1(pObj) );
00093     }
00094     pObj->pData = NULL;
00095 }

static void Hop_ObjClearMarkA ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 167 of file hop.h.

00167 { pObj->fMarkA = 0;     }

static void Hop_ObjClearRef ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 180 of file hop.h.

00180 { pObj->nRefs = 0;                               }

void Hop_ObjCollectMulti ( Hop_Obj_t *  pRoot,
Vec_Ptr_t *  vSuper 
)

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

Synopsis [Detects multi-input gate rooted at this node.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file hopUtil.c.

00131 {
00132     assert( !Hop_IsComplement(pRoot) );
00133     Vec_PtrClear( vSuper );
00134     Hop_ObjCollectMulti_rec( pRoot, pRoot, vSuper );
00135 }

void Hop_ObjConnect ( Hop_Man_t *  p,
Hop_Obj_t *  pObj,
Hop_Obj_t *  pFan0,
Hop_Obj_t *  pFan1 
)

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

Synopsis [Connect the object to the fanin.]

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file hopObj.c.

00122 {
00123     assert( !Hop_IsComplement(pObj) );
00124     assert( Hop_ObjIsNode(pObj) );
00125     // add the first fanin
00126     pObj->pFanin0 = pFan0;
00127     pObj->pFanin1 = pFan1;
00128     // increment references of the fanins and add their fanouts
00129     if ( p->fRefCount )
00130     {
00131         if ( pFan0 != NULL )
00132             Hop_ObjRef( Hop_ObjFanin0(pObj) );
00133         if ( pFan1 != NULL )
00134             Hop_ObjRef( Hop_ObjFanin1(pObj) );
00135     }
00136     else
00137         pObj->nRefs = Hop_ObjLevelNew( pObj );
00138     // set the phase
00139     pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1);
00140     // add the node to the structural hash table
00141     Hop_TableInsert( p, pObj );
00142 }

Hop_Obj_t* Hop_ObjCreate ( Hop_Man_t *  p,
Hop_Obj_t *  pGhost 
)

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

Synopsis [Create the new node assuming it does not exist.]

Description []

SideEffects []

SeeAlso []

Definition at line 93 of file hopObj.c.

00094 {
00095     Hop_Obj_t * pObj;
00096     assert( !Hop_IsComplement(pGhost) );
00097     assert( Hop_ObjIsNode(pGhost) );
00098     assert( pGhost == &p->Ghost );
00099     // get memory for the new object
00100     pObj = Hop_ManFetchMemory( p );
00101     pObj->Type = pGhost->Type;
00102     // add connections
00103     Hop_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 );
00104     // update node counters of the manager
00105     p->nObjs[Hop_ObjType(pObj)]++;
00106     assert( pObj->pData == NULL );
00107     return pObj;
00108 }

void Hop_ObjCreateChoice ( Hop_Obj_t *  pOld,
Hop_Obj_t *  pNew 
)

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

Synopsis [Sets an equivalence relation between the nodes.]

Description [Makes the representative of pNew point to the representaive of pOld.]

SideEffects []

SeeAlso []

Definition at line 256 of file hopObj.c.

00257 {
00258     Hop_Obj_t * pOldRepr;
00259     Hop_Obj_t * pNewRepr;
00260     assert( pOld != NULL && pNew != NULL );
00261     pOldRepr = Hop_ObjRepr(pOld);
00262     pNewRepr = Hop_ObjRepr(pNew);
00263     if ( pNewRepr != pOldRepr )
00264         pNewRepr->pData = pOldRepr;
00265 }

static Hop_Obj_t* Hop_ObjCreateGhost ( Hop_Man_t *  p,
Hop_Obj_t *  p0,
Hop_Obj_t *  p1,
Hop_Type_t  Type 
) [inline, static]

Definition at line 207 of file hop.h.

00208 {
00209     Hop_Obj_t * pGhost;
00210     assert( Type != AIG_AND || !Hop_ObjIsConst1(Hop_Regular(p0)) );
00211     assert( p1 == NULL || !Hop_ObjIsConst1(Hop_Regular(p1)) );
00212     assert( Type == AIG_PI || Hop_Regular(p0) != Hop_Regular(p1) );
00213     pGhost = Hop_ManGhost(p);
00214     pGhost->Type = Type;
00215     if ( Hop_Regular(p0)->Id < Hop_Regular(p1)->Id )
00216     {
00217         pGhost->pFanin0 = p0;
00218         pGhost->pFanin1 = p1;
00219     }
00220     else
00221     {
00222         pGhost->pFanin0 = p1;
00223         pGhost->pFanin1 = p0;
00224     }
00225     return pGhost;
00226 }

Hop_Obj_t* Hop_ObjCreatePi ( Hop_Man_t *  p  ) 

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

FileName [hopObj.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Minimalistic And-Inverter Graph package.]

Synopsis [Adding/removing objects.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
hopObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

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

Synopsis [Creates primary input.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file hopObj.c.

00043 {
00044     Hop_Obj_t * pObj;
00045     pObj = Hop_ManFetchMemory( p );
00046     pObj->Type = AIG_PI;
00047     Vec_PtrPush( p->vPis, pObj );
00048     p->nObjs[AIG_PI]++;
00049     return pObj;
00050 }

Hop_Obj_t* Hop_ObjCreatePo ( Hop_Man_t *  p,
Hop_Obj_t *  pDriver 
)

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

Synopsis [Creates primary output with the given driver.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file hopObj.c.

00064 {
00065     Hop_Obj_t * pObj;
00066     pObj = Hop_ManFetchMemory( p );
00067     pObj->Type = AIG_PO;
00068     Vec_PtrPush( p->vPos, pObj );
00069     // add connections
00070     pObj->pFanin0 = pDriver;
00071     if ( p->fRefCount )
00072         Hop_ObjRef( Hop_Regular(pDriver) );
00073     else
00074         pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) );
00075     // set the phase
00076     pObj->fPhase = Hop_ObjFaninPhase(pDriver);
00077     // update node counters of the manager
00078     p->nObjs[AIG_PO]++;
00079     return pObj;
00080 }

void Hop_ObjDelete ( Hop_Man_t *  p,
Hop_Obj_t *  pObj 
)

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

Synopsis [Deletes the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 182 of file hopObj.c.

00183 {
00184     assert( !Hop_IsComplement(pObj) );
00185     assert( !Hop_ObjIsTerm(pObj) );
00186     assert( Hop_ObjRefs(pObj) == 0 );
00187     // update node counters of the manager
00188     p->nObjs[pObj->Type]--;
00189     p->nDeleted++;
00190     // remove connections
00191     Hop_ObjDisconnect( p, pObj );
00192     // remove PIs/POs from the arrays
00193     if ( Hop_ObjIsPi(pObj) )
00194         Vec_PtrRemove( p->vPis, pObj );
00195     // free the node
00196     Hop_ManRecycleMemory( p, pObj );
00197 }

void Hop_ObjDelete_rec ( Hop_Man_t *  p,
Hop_Obj_t *  pObj 
)

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

Synopsis [Deletes the MFFC of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 210 of file hopObj.c.

00211 {
00212     Hop_Obj_t * pFanin0, * pFanin1;
00213     assert( !Hop_IsComplement(pObj) );
00214     if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) )
00215         return;
00216     assert( Hop_ObjIsNode(pObj) );
00217     pFanin0 = Hop_ObjFanin0(pObj);
00218     pFanin1 = Hop_ObjFanin1(pObj);
00219     Hop_ObjDelete( p, pObj );
00220     if ( pFanin0 && !Hop_ObjIsNone(pFanin0) && Hop_ObjRefs(pFanin0) == 0 )
00221         Hop_ObjDelete_rec( p, pFanin0 );
00222     if ( pFanin1 && !Hop_ObjIsNone(pFanin1) && Hop_ObjRefs(pFanin1) == 0 )
00223         Hop_ObjDelete_rec( p, pFanin1 );
00224 }

static void Hop_ObjDeref ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 179 of file hop.h.

00179 { assert( pObj->nRefs > 0 ); pObj->nRefs--;      }

void Hop_ObjDisconnect ( Hop_Man_t *  p,
Hop_Obj_t *  pObj 
)

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

Synopsis [Connect the object to the fanin.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file hopObj.c.

00156 {
00157     assert( !Hop_IsComplement(pObj) );
00158     assert( Hop_ObjIsNode(pObj) );
00159     // remove connections
00160     if ( pObj->pFanin0 != NULL )
00161         Hop_ObjDeref(Hop_ObjFanin0(pObj));
00162     if ( pObj->pFanin1 != NULL )
00163         Hop_ObjDeref(Hop_ObjFanin1(pObj));
00164     // remove the node from the structural hash table
00165     Hop_TableDelete( p, pObj );
00166     // add the first fanin
00167     pObj->pFanin0 = NULL;
00168     pObj->pFanin1 = NULL;
00169 }

static Hop_Obj_t* Hop_ObjFanin0 ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 183 of file hop.h.

00183 { return Hop_Regular(pObj->pFanin0);             }

static Hop_Obj_t* Hop_ObjFanin1 ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 184 of file hop.h.

00184 { return Hop_Regular(pObj->pFanin1);             }

static int Hop_ObjFaninC0 ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 181 of file hop.h.

00181 { return Hop_IsComplement(pObj->pFanin0);        }

static int Hop_ObjFaninC1 ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 182 of file hop.h.

00182 { return Hop_IsComplement(pObj->pFanin1);        }

static int Hop_ObjFaninPhase ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 191 of file hop.h.

00191 { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }

static int Hop_ObjFanoutC ( Hop_Obj_t *  pObj,
Hop_Obj_t *  pFanout 
) [inline, static]

Definition at line 199 of file hop.h.

00200 { 
00201     if ( Hop_ObjFanin0(pFanout) == pObj ) return Hop_ObjFaninC0(pObj); 
00202     if ( Hop_ObjFanin1(pFanout) == pObj ) return Hop_ObjFaninC1(pObj); 
00203     assert(0); return -1; 
00204 }

static int Hop_ObjIsAnd ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 159 of file hop.h.

00159 { return pObj->Type == AIG_AND;    }

static int Hop_ObjIsConst1 ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 156 of file hop.h.

00156 { assert(!Hop_IsComplement(pObj)); return pObj->Type == AIG_CONST1; }

static int Hop_ObjIsExor ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 160 of file hop.h.

00160 { return pObj->Type == AIG_EXOR;   }

static int Hop_ObjIsHash ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 163 of file hop.h.

00163 { return pObj->Type == AIG_AND || pObj->Type == AIG_EXOR;   }

static int Hop_ObjIsMarkA ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 165 of file hop.h.

00165 { return pObj->fMarkA;  }

int Hop_ObjIsMuxType ( Hop_Obj_t *  pNode  ) 

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

Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file hopUtil.c.

00149 {
00150     Hop_Obj_t * pNode0, * pNode1;
00151     // check that the node is regular
00152     assert( !Hop_IsComplement(pNode) );
00153     // if the node is not AND, this is not MUX
00154     if ( !Hop_ObjIsAnd(pNode) )
00155         return 0;
00156     // if the children are not complemented, this is not MUX
00157     if ( !Hop_ObjFaninC0(pNode) || !Hop_ObjFaninC1(pNode) )
00158         return 0;
00159     // get children
00160     pNode0 = Hop_ObjFanin0(pNode);
00161     pNode1 = Hop_ObjFanin1(pNode);
00162     // if the children are not ANDs, this is not MUX
00163     if ( !Hop_ObjIsAnd(pNode0) || !Hop_ObjIsAnd(pNode1) )
00164         return 0;
00165     // otherwise the node is MUX iff it has a pair of equal grandchildren
00166     return (Hop_ObjFanin0(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC0(pNode1))) || 
00167            (Hop_ObjFanin0(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC1(pNode1))) ||
00168            (Hop_ObjFanin1(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC0(pNode1))) ||
00169            (Hop_ObjFanin1(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC1(pNode1)));
00170 }

static int Hop_ObjIsNode ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 161 of file hop.h.

00161 { return pObj->Type == AIG_AND || pObj->Type == AIG_EXOR;   }

static int Hop_ObjIsNone ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 155 of file hop.h.

00155 { return pObj->Type == AIG_NONE;   }

static int Hop_ObjIsPi ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 157 of file hop.h.

00157 { return pObj->Type == AIG_PI;     }

static int Hop_ObjIsPo ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 158 of file hop.h.

00158 { return pObj->Type == AIG_PO;     }

static int Hop_ObjIsTerm ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 162 of file hop.h.

00162 { return pObj->Type == AIG_PI  || pObj->Type == AIG_PO || pObj->Type == AIG_CONST1; }

static int Hop_ObjIsTravIdCurrent ( Hop_Man_t *  p,
Hop_Obj_t *  pObj 
) [inline, static]

Definition at line 172 of file hop.h.

00172 { return (int )((int)pObj->pData == p->nTravIds);     }

static int Hop_ObjIsTravIdPrevious ( Hop_Man_t *  p,
Hop_Obj_t *  pObj 
) [inline, static]

Definition at line 173 of file hop.h.

00173 { return (int )((int)pObj->pData == p->nTravIds - 1); }

static int Hop_ObjLevel ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 189 of file hop.h.

00189 { return pObj->nRefs;                            }

static int Hop_ObjLevelNew ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 190 of file hop.h.

00190 { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs);       }

static int Hop_ObjPhase ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 176 of file hop.h.

00176 { return pObj->fPhase;                           }

void Hop_ObjPrintEqn ( FILE *  pFile,
Hop_Obj_t *  pObj,
Vec_Vec_t *  vLevels,
int  Level 
)

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

Synopsis [Prints Eqn formula for the AIG rooted at this node.]

Description [The formula is in terms of PIs, which should have their names assigned in pObj->pData fields.]

SideEffects []

SeeAlso []

Definition at line 319 of file hopUtil.c.

00320 {
00321     Vec_Ptr_t * vSuper;
00322     Hop_Obj_t * pFanin;
00323     int fCompl, i;
00324     // store the complemented attribute
00325     fCompl = Hop_IsComplement(pObj);
00326     pObj = Hop_Regular(pObj);
00327     // constant case
00328     if ( Hop_ObjIsConst1(pObj) )
00329     {
00330         fprintf( pFile, "%d", !fCompl );
00331         return;
00332     }
00333     // PI case
00334     if ( Hop_ObjIsPi(pObj) )
00335     {
00336         fprintf( pFile, "%s%s", fCompl? "!" : "", pObj->pData );
00337         return;
00338     }
00339     // AND case
00340     Vec_VecExpand( vLevels, Level );
00341     vSuper = Vec_VecEntry(vLevels, Level);
00342     Hop_ObjCollectMulti( pObj, vSuper );
00343     fprintf( pFile, "%s", (Level==0? "" : "(") );
00344     Vec_PtrForEachEntry( vSuper, pFanin, i )
00345     {
00346         Hop_ObjPrintEqn( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1 );
00347         if ( i < Vec_PtrSize(vSuper) - 1 )
00348             fprintf( pFile, " %s ", fCompl? "+" : "*" );
00349     }
00350     fprintf( pFile, "%s", (Level==0? "" : ")") );
00351     return;
00352 }

void Hop_ObjPrintVerbose ( Hop_Obj_t *  pObj,
int  fHaig 
)

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

Synopsis [Prints node in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 453 of file hopUtil.c.

00454 {
00455     assert( !Hop_IsComplement(pObj) );
00456     printf( "Node %p : ", pObj );
00457     if ( Hop_ObjIsConst1(pObj) )
00458         printf( "constant 1" );
00459     else if ( Hop_ObjIsPi(pObj) )
00460         printf( "PI" );
00461     else
00462         printf( "AND( %p%s, %p%s )", 
00463             Hop_ObjFanin0(pObj), (Hop_ObjFaninC0(pObj)? "\'" : " "), 
00464             Hop_ObjFanin1(pObj), (Hop_ObjFaninC1(pObj)? "\'" : " ") );
00465     printf( " (refs = %3d)", Hop_ObjRefs(pObj) );
00466 }

void Hop_ObjPrintVerilog ( FILE *  pFile,
Hop_Obj_t *  pObj,
Vec_Vec_t *  vLevels,
int  Level 
)

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

Synopsis [Prints Verilog formula for the AIG rooted at this node.]

Description [The formula is in terms of PIs, which should have their names assigned in pObj->pData fields.]

SideEffects []

SeeAlso []

Definition at line 366 of file hopUtil.c.

00367 {
00368     Vec_Ptr_t * vSuper;
00369     Hop_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
00370     int fCompl, i;
00371     // store the complemented attribute
00372     fCompl = Hop_IsComplement(pObj);
00373     pObj = Hop_Regular(pObj);
00374     // constant case
00375     if ( Hop_ObjIsConst1(pObj) )
00376     {
00377         fprintf( pFile, "1\'b%d", !fCompl );
00378         return;
00379     }
00380     // PI case
00381     if ( Hop_ObjIsPi(pObj) )
00382     {
00383         fprintf( pFile, "%s%s", fCompl? "~" : "", pObj->pData );
00384         return;
00385     }
00386     // EXOR case
00387     if ( Hop_ObjIsExor(pObj) )
00388     {
00389         Vec_VecExpand( vLevels, Level );
00390         vSuper = Vec_VecEntry( vLevels, Level );
00391         Hop_ObjCollectMulti( pObj, vSuper );
00392         fprintf( pFile, "%s", (Level==0? "" : "(") );
00393         Vec_PtrForEachEntry( vSuper, pFanin, i )
00394         {
00395             Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
00396             if ( i < Vec_PtrSize(vSuper) - 1 )
00397                 fprintf( pFile, " ^ " );
00398         }
00399         fprintf( pFile, "%s", (Level==0? "" : ")") );
00400         return;
00401     }
00402     // MUX case
00403     if ( Hop_ObjIsMuxType(pObj) )
00404     {
00405         if ( Hop_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
00406         {
00407             fprintf( pFile, "%s", (Level==0? "" : "(") );
00408             Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1 );
00409             fprintf( pFile, " ^ " );
00410             Hop_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
00411             fprintf( pFile, "%s", (Level==0? "" : ")") );
00412         }
00413         else 
00414         {
00415             pFaninC = Hop_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
00416             fprintf( pFile, "%s", (Level==0? "" : "(") );
00417             Hop_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
00418             fprintf( pFile, " ? " );
00419             Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin1, fCompl), vLevels, Level+1 );
00420             fprintf( pFile, " : " );
00421             Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1 );
00422             fprintf( pFile, "%s", (Level==0? "" : ")") );
00423         }
00424         return;
00425     }
00426     // AND case
00427     Vec_VecExpand( vLevels, Level );
00428     vSuper = Vec_VecEntry(vLevels, Level);
00429     Hop_ObjCollectMulti( pObj, vSuper );
00430     fprintf( pFile, "%s", (Level==0? "" : "(") );
00431     Vec_PtrForEachEntry( vSuper, pFanin, i )
00432     {
00433         Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1 );
00434         if ( i < Vec_PtrSize(vSuper) - 1 )
00435             fprintf( pFile, " %s ", fCompl? "|" : "&" );
00436     }
00437     fprintf( pFile, "%s", (Level==0? "" : ")") );
00438     return;
00439 }

int Hop_ObjRecognizeExor ( Hop_Obj_t *  pObj,
Hop_Obj_t **  ppFan0,
Hop_Obj_t **  ppFan1 
)

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

Synopsis [Recognizes what nodes are inputs of the EXOR.]

Description []

SideEffects []

SeeAlso []

Definition at line 184 of file hopUtil.c.

00185 {
00186     Hop_Obj_t * p0, * p1;
00187     assert( !Hop_IsComplement(pObj) );
00188     if ( !Hop_ObjIsNode(pObj) )
00189         return 0;
00190     if ( Hop_ObjIsExor(pObj) )
00191     {
00192         *ppFan0 = Hop_ObjChild0(pObj);
00193         *ppFan1 = Hop_ObjChild1(pObj);
00194         return 1;
00195     }
00196     assert( Hop_ObjIsAnd(pObj) );
00197     p0 = Hop_ObjChild0(pObj);
00198     p1 = Hop_ObjChild1(pObj);
00199     if ( !Hop_IsComplement(p0) || !Hop_IsComplement(p1) )
00200         return 0;
00201     p0 = Hop_Regular(p0);
00202     p1 = Hop_Regular(p1);
00203     if ( !Hop_ObjIsAnd(p0) || !Hop_ObjIsAnd(p1) )
00204         return 0;
00205     if ( Hop_ObjFanin0(p0) != Hop_ObjFanin0(p1) || Hop_ObjFanin1(p0) != Hop_ObjFanin1(p1) )
00206         return 0;
00207     if ( Hop_ObjFaninC0(p0) == Hop_ObjFaninC0(p1) || Hop_ObjFaninC1(p0) == Hop_ObjFaninC1(p1) )
00208         return 0;
00209     *ppFan0 = Hop_ObjChild0(p0);
00210     *ppFan1 = Hop_ObjChild1(p0);
00211     return 1;
00212 }

Hop_Obj_t* Hop_ObjRecognizeMux ( Hop_Obj_t *  pNode,
Hop_Obj_t **  ppNodeT,
Hop_Obj_t **  ppNodeE 
)

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

Synopsis [Recognizes what nodes are control and data inputs of a MUX.]

Description [If the node is a MUX, returns the control variable C. Assigns nodes T and E to be the then and else variables of the MUX. Node C is never complemented. Nodes T and E can be complemented. This function also recognizes EXOR/NEXOR gates as MUXes.]

SideEffects []

SeeAlso []

Definition at line 228 of file hopUtil.c.

00229 {
00230     Hop_Obj_t * pNode0, * pNode1;
00231     assert( !Hop_IsComplement(pNode) );
00232     assert( Hop_ObjIsMuxType(pNode) );
00233     // get children
00234     pNode0 = Hop_ObjFanin0(pNode);
00235     pNode1 = Hop_ObjFanin1(pNode);
00236 
00237     // find the control variable
00238     if ( Hop_ObjFanin1(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC1(pNode1)) )
00239     {
00240 //        if ( Fraig_IsComplement(pNode1->p2) )
00241         if ( Hop_ObjFaninC1(pNode0) )
00242         { // pNode2->p2 is positive phase of C
00243             *ppNodeT = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1);
00244             *ppNodeE = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1);
00245             return Hop_ObjChild1(pNode1);//pNode2->p2;
00246         }
00247         else
00248         { // pNode1->p2 is positive phase of C
00249             *ppNodeT = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1);
00250             *ppNodeE = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1);
00251             return Hop_ObjChild1(pNode0);//pNode1->p2;
00252         }
00253     }
00254     else if ( Hop_ObjFanin0(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC0(pNode1)) )
00255     {
00256 //        if ( Fraig_IsComplement(pNode1->p1) )
00257         if ( Hop_ObjFaninC0(pNode0) )
00258         { // pNode2->p1 is positive phase of C
00259             *ppNodeT = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2);
00260             *ppNodeE = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2);
00261             return Hop_ObjChild0(pNode1);//pNode2->p1;
00262         }
00263         else
00264         { // pNode1->p1 is positive phase of C
00265             *ppNodeT = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2);
00266             *ppNodeE = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2);
00267             return Hop_ObjChild0(pNode0);//pNode1->p1;
00268         }
00269     }
00270     else if ( Hop_ObjFanin0(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC1(pNode1)) )
00271     {
00272 //        if ( Fraig_IsComplement(pNode1->p1) )
00273         if ( Hop_ObjFaninC0(pNode0) )
00274         { // pNode2->p2 is positive phase of C
00275             *ppNodeT = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1);
00276             *ppNodeE = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2);
00277             return Hop_ObjChild1(pNode1);//pNode2->p2;
00278         }
00279         else
00280         { // pNode1->p1 is positive phase of C
00281             *ppNodeT = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2);
00282             *ppNodeE = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1);
00283             return Hop_ObjChild0(pNode0);//pNode1->p1;
00284         }
00285     }
00286     else if ( Hop_ObjFanin1(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC0(pNode1)) )
00287     {
00288 //        if ( Fraig_IsComplement(pNode1->p2) )
00289         if ( Hop_ObjFaninC1(pNode0) )
00290         { // pNode2->p1 is positive phase of C
00291             *ppNodeT = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2);
00292             *ppNodeE = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1);
00293             return Hop_ObjChild0(pNode1);//pNode2->p1;
00294         }
00295         else
00296         { // pNode1->p2 is positive phase of C
00297             *ppNodeT = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1);
00298             *ppNodeE = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2);
00299             return Hop_ObjChild1(pNode0);//pNode1->p2;
00300         }
00301     }
00302     assert( 0 ); // this is not MUX
00303     return NULL;
00304 }

static void Hop_ObjRef ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 178 of file hop.h.

00178 { pObj->nRefs++;                                 }

static int Hop_ObjRefs ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 177 of file hop.h.

00177 { return pObj->nRefs;                            }

Hop_Obj_t* Hop_ObjRepr ( Hop_Obj_t *  pObj  ) 

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

Synopsis [Returns the representative of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file hopObj.c.

00238 {
00239     assert( !Hop_IsComplement(pObj) );
00240     if ( pObj->pData == NULL || pObj->pData == pObj )
00241         return pObj;
00242     return Hop_ObjRepr( pObj->pData );
00243 }

static void Hop_ObjSetMarkA ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 166 of file hop.h.

00166 { pObj->fMarkA = 1;     }

static void Hop_ObjSetTravId ( Hop_Obj_t *  pObj,
int  TravId 
) [inline, static]

Definition at line 169 of file hop.h.

00169 { pObj->pData = (void *)TravId;                       }

static void Hop_ObjSetTravIdCurrent ( Hop_Man_t *  p,
Hop_Obj_t *  pObj 
) [inline, static]

Definition at line 170 of file hop.h.

00170 { pObj->pData = (void *)p->nTravIds;                  }

static void Hop_ObjSetTravIdPrevious ( Hop_Man_t *  p,
Hop_Obj_t *  pObj 
) [inline, static]

Definition at line 171 of file hop.h.

00171 { pObj->pData = (void *)(p->nTravIds - 1);            }

static int Hop_ObjTravId ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 175 of file hop.h.

00175 { return (int)pObj->pData;                       }

static Hop_Type_t Hop_ObjType ( Hop_Obj_t *  pObj  )  [inline, static]

Definition at line 154 of file hop.h.

00154 { return (Hop_Type_t)pObj->Type;               }

static int Hop_ObjWhatFanin ( Hop_Obj_t *  pObj,
Hop_Obj_t *  pFanin 
) [inline, static]

Definition at line 193 of file hop.h.

00194 { 
00195     if ( Hop_ObjFanin0(pObj) == pFanin ) return 0; 
00196     if ( Hop_ObjFanin1(pObj) == pFanin ) return 1; 
00197     assert(0); return -1; 
00198 }

Hop_Obj_t* Hop_Oper ( Hop_Man_t *  p,
Hop_Obj_t *  p0,
Hop_Obj_t *  p1,
Hop_Type_t  Type 
)

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

Synopsis [Perform one operation.]

Description [The argument nodes can be complemented.]

SideEffects []

SeeAlso []

Definition at line 80 of file hopOper.c.

00081 {
00082     if ( Type == AIG_AND )
00083         return Hop_And( p, p0, p1 );
00084     if ( Type == AIG_EXOR )
00085         return Hop_Exor( p, p0, p1 );
00086     assert( 0 );
00087     return NULL;
00088 }

Hop_Obj_t* Hop_Or ( Hop_Man_t *  p,
Hop_Obj_t *  p0,
Hop_Obj_t *  p1 
)

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

Synopsis [Implements Boolean OR.]

Description []

SideEffects []

SeeAlso []

Definition at line 168 of file hopOper.c.

00169 {
00170     return Hop_Not( Hop_And( p, Hop_Not(p0), Hop_Not(p1) ) );
00171 }

static Hop_Obj_t* Hop_Regular ( Hop_Obj_t *  p  )  [inline, static]

Definition at line 127 of file hop.h.

00127 { return (Hop_Obj_t *)((unsigned long)(p) & ~01);      }

int Hop_TableCountEntries ( Hop_Man_t *  p  ) 

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

Synopsis [Count the number of nodes in the table.]

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file hopTable.c.

00144 {
00145     Hop_Obj_t * pEntry;
00146     int i, Counter = 0;
00147     for ( i = 0; i < p->nTableSize; i++ )
00148         for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext )
00149             Counter++;
00150     return Counter;
00151 }

void Hop_TableDelete ( Hop_Man_t *  p,
Hop_Obj_t *  pObj 
)

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

Synopsis [Deletes the node from the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file hopTable.c.

00122 {
00123     Hop_Obj_t ** ppPlace;
00124     assert( !Hop_IsComplement(pObj) );
00125     ppPlace = Hop_TableFind( p, pObj );
00126     assert( *ppPlace == pObj ); // node should be in the table
00127     // remove the node
00128     *ppPlace = pObj->pNext;
00129     pObj->pNext = NULL;
00130 }

void Hop_TableInsert ( Hop_Man_t *  p,
Hop_Obj_t *  pObj 
)

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

Synopsis [Adds the new node to the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file hopTable.c.

00099 {
00100     Hop_Obj_t ** ppPlace;
00101     assert( !Hop_IsComplement(pObj) );
00102     assert( Hop_TableLookup(p, pObj) == NULL );
00103     if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Hop_ManNodeNum(p) )
00104         Hop_TableResize( p );
00105     ppPlace = Hop_TableFind( p, pObj );
00106     assert( *ppPlace == NULL );
00107     *ppPlace = pObj;
00108 }

Hop_Obj_t* Hop_TableLookup ( Hop_Man_t *  p,
Hop_Obj_t *  pGhost 
)

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

Synopsis [Checks if a node with the given attributes is in the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file hopTable.c.

00070 {
00071     Hop_Obj_t * pEntry;
00072     assert( !Hop_IsComplement(pGhost) );
00073     assert( Hop_ObjChild0(pGhost) && Hop_ObjChild1(pGhost) );
00074     assert( Hop_ObjFanin0(pGhost)->Id < Hop_ObjFanin1(pGhost)->Id );
00075     if ( p->fRefCount && (!Hop_ObjRefs(Hop_ObjFanin0(pGhost)) || !Hop_ObjRefs(Hop_ObjFanin1(pGhost))) )
00076         return NULL;
00077     for ( pEntry = p->pTable[Hop_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
00078     {
00079         if ( Hop_ObjChild0(pEntry) == Hop_ObjChild0(pGhost) && 
00080              Hop_ObjChild1(pEntry) == Hop_ObjChild1(pGhost) && 
00081              Hop_ObjType(pEntry) == Hop_ObjType(pGhost) )
00082             return pEntry;
00083     }
00084     return NULL;
00085 }

void Hop_TableProfile ( Hop_Man_t *  p  ) 

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

Synopsis [Profiles the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file hopTable.c.

00210 {
00211     Hop_Obj_t * pEntry;
00212     int i, Counter;
00213     for ( i = 0; i < p->nTableSize; i++ )
00214     {
00215         Counter = 0;
00216         for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext )
00217             Counter++;
00218         if ( Counter ) 
00219             printf( "%d ", Counter );
00220     }
00221 }

Hop_Obj_t* Hop_Transfer ( Hop_Man_t *  pSour,
Hop_Man_t *  pDest,
Hop_Obj_t *  pRoot,
int  nVars 
)

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

Synopsis [Transfers the AIG from one manager into another.]

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file hopDfs.c.

00319 {
00320     Hop_Obj_t * pObj;
00321     int i;
00322     // solve simple cases
00323     if ( pSour == pDest )
00324         return pRoot;
00325     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
00326         return Hop_NotCond( Hop_ManConst1(pDest), Hop_IsComplement(pRoot) );
00327     // set the PI mapping
00328     Hop_ManForEachPi( pSour, pObj, i )
00329     {
00330         if ( i == nVars )
00331            break;
00332         pObj->pData = Hop_IthVar(pDest, i);
00333     }
00334     // transfer and set markings
00335     Hop_Transfer_rec( pDest, Hop_Regular(pRoot) );
00336     // clear the markings
00337     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
00338     return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
00339 }

static int Hop_TruthWordNum ( int  nVars  )  [inline, static]

Definition at line 120 of file hop.h.

00120 { return nVars <= 5 ? 1 : (1 << (nVars - 5));     }

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