src/base/abci/abcOdc.c File Reference

#include "abc.h"
Include dependency graph for abcOdc.c:

Go to the source code of this file.

Data Structures

struct  Odc_Obj_t_
struct  Odc_Man_t_

Defines

#define ABC_DC_MAX_NODES   (1<<15)
#define Odc_ForEachPi(p, Lit, i)   for ( i = 0; (i < Odc_PiNum(p)) && (((Lit) = Odc_Var(p, i)), 1); i++ )
#define Odc_ForEachAnd(p, pObj, i)   for ( i = 1 + Odc_CiNum(p); (i < Odc_ObjNum(p)) && ((pObj) = (p)->pObjs + i); i++ )

Typedefs

typedef unsigned short Odc_Lit_t
typedef struct Odc_Obj_t_ Odc_Obj_t
typedef struct Odc_Man_t_ Odc_Man_t

Functions

static int Odc_PiNum (Odc_Man_t *p)
static int Odc_NodeNum (Odc_Man_t *p)
static int Odc_ObjNum (Odc_Man_t *p)
static int Odc_IsComplement (Odc_Lit_t Lit)
static Odc_Lit_t Odc_Regular (Odc_Lit_t Lit)
static Odc_Lit_t Odc_Not (Odc_Lit_t Lit)
static Odc_Lit_t Odc_NotCond (Odc_Lit_t Lit, int c)
static Odc_Lit_t Odc_Const0 ()
static Odc_Lit_t Odc_Const1 ()
static Odc_Lit_t Odc_Var (Odc_Man_t *p, int i)
static int Odc_IsConst (Odc_Lit_t Lit)
static int Odc_IsTerm (Odc_Man_t *p, Odc_Lit_t Lit)
static Odc_Obj_tOdc_ObjNew (Odc_Man_t *p)
static Odc_Lit_t Odc_Obj2Lit (Odc_Man_t *p, Odc_Obj_t *pObj)
static Odc_Obj_tOdc_Lit2Obj (Odc_Man_t *p, Odc_Lit_t Lit)
static Odc_Lit_t Odc_ObjChild0 (Odc_Obj_t *pObj)
static Odc_Lit_t Odc_ObjChild1 (Odc_Obj_t *pObj)
static Odc_Lit_t Odc_ObjFanin0 (Odc_Obj_t *pObj)
static Odc_Lit_t Odc_ObjFanin1 (Odc_Obj_t *pObj)
static int Odc_ObjFaninC0 (Odc_Obj_t *pObj)
static int Odc_ObjFaninC1 (Odc_Obj_t *pObj)
static void Odc_ManIncrementTravId (Odc_Man_t *p)
static void Odc_ObjSetTravIdCurrent (Odc_Man_t *p, Odc_Obj_t *pObj)
static int Odc_ObjIsTravIdCurrent (Odc_Man_t *p, Odc_Obj_t *pObj)
static unsigned * Odc_ObjTruth (Odc_Man_t *p, Odc_Lit_t Lit)
Odc_Man_tAbc_NtkDontCareAlloc (int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose)
void Abc_NtkDontCareClear (Odc_Man_t *p)
void Abc_NtkDontCareFree (Odc_Man_t *p)
int Abc_NtkDontCareCompute (Odc_Man_t *p, Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves, unsigned *puTruth)
void Abc_NtkDontCareWinSweepLeafTfo_rec (Abc_Obj_t *pObj, int nLevelLimit, Abc_Obj_t *pNode)
void Abc_NtkDontCareWinSweepLeafTfo (Odc_Man_t *p)
void Abc_NtkDontCareWinCollectRoots_rec (Abc_Obj_t *pObj, Vec_Ptr_t *vRoots)
void Abc_NtkDontCareWinCollectRoots (Odc_Man_t *p)
int Abc_NtkDontCareWinAddMissing_rec (Odc_Man_t *p, Abc_Obj_t *pObj)
int Abc_NtkDontCareWinAddMissing (Odc_Man_t *p)
int Abc_NtkDontCareWindow (Odc_Man_t *p)
static unsigned Odc_HashKey (Odc_Lit_t iFan0, Odc_Lit_t iFan1, int TableSize)
static Odc_Lit_tOdc_HashLookup (Odc_Man_t *p, Odc_Lit_t iFan0, Odc_Lit_t iFan1)
static Odc_Lit_t Odc_And (Odc_Man_t *p, Odc_Lit_t iFan0, Odc_Lit_t iFan1)
static Odc_Lit_t Odc_Or (Odc_Man_t *p, Odc_Lit_t iFan0, Odc_Lit_t iFan1)
static Odc_Lit_t Odc_Xor (Odc_Man_t *p, Odc_Lit_t iFan0, Odc_Lit_t iFan1)
void * Abc_NtkDontCareTransfer_rec (Odc_Man_t *p, Abc_Obj_t *pNode, Abc_Obj_t *pPivot)
int Abc_NtkDontCareTransfer (Odc_Man_t *p)
unsigned Abc_NtkDontCareCofactors_rec (Odc_Man_t *p, Odc_Lit_t Lit, unsigned uMask)
int Abc_NtkDontCareQuantify (Odc_Man_t *p)
void Abc_NtkDontCareSimulateSetElem2 (Odc_Man_t *p)
void Abc_NtkDontCareSimulateSetElem (Odc_Man_t *p)
void Abc_NtkDontCareSimulateSetRand (Odc_Man_t *p)
int Abc_NtkDontCareCountMintsWord (Odc_Man_t *p, unsigned *puTruth)
void Abc_NtkDontCareTruthOne (Odc_Man_t *p, Odc_Lit_t Lit)
void Abc_NtkDontCareSimulate_rec (Odc_Man_t *p, Odc_Lit_t Lit)
int Abc_NtkDontCareSimulate (Odc_Man_t *p, unsigned *puTruth)
int Abc_NtkDontCareSimulateBefore (Odc_Man_t *p, unsigned *puTruth)

Define Documentation

#define ABC_DC_MAX_NODES   (1<<15)

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

FileName [abcOdc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Scalable computation of observability don't-cares.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
abcOdc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 27 of file abcOdc.c.

#define Odc_ForEachAnd ( p,
pObj,
 )     for ( i = 1 + Odc_CiNum(p); (i < Odc_ObjNum(p)) && ((pObj) = (p)->pObjs + i); i++ )

Definition at line 140 of file abcOdc.c.

#define Odc_ForEachPi ( p,
Lit,
 )     for ( i = 0; (i < Odc_PiNum(p)) && (((Lit) = Odc_Var(p, i)), 1); i++ )

Definition at line 138 of file abcOdc.c.


Typedef Documentation

typedef unsigned short Odc_Lit_t

Definition at line 29 of file abcOdc.c.

typedef struct Odc_Man_t_ Odc_Man_t

Definition at line 42 of file abcOdc.c.

typedef struct Odc_Obj_t_ Odc_Obj_t

Definition at line 31 of file abcOdc.c.


Function Documentation

Odc_Man_t * Abc_NtkDontCareAlloc ( int  nVarsMax,
int  nLevels,
int  fVerbose,
int  fVeryVerbose 
)

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

Synopsis [Allocates the don't-care manager.]

Description [The parameters are the max number of cut variables, the number of fanout levels used for the ODC computation, and verbosiness.]

SideEffects []

SeeAlso []

Definition at line 166 of file abcOdc.c.

00167 {
00168     Odc_Man_t * p;
00169     unsigned * pData;
00170     int i, k;
00171     p = ALLOC( Odc_Man_t, 1 );
00172     memset( p, 0, sizeof(Odc_Man_t) );
00173     assert( nVarsMax > 4 && nVarsMax < 16 );
00174     assert( nLevels > 0 && nLevels < 10 );
00175 
00176     srand( 0xABC );
00177 
00178     // dont'-care parameters
00179     p->nVarsMax     = nVarsMax;
00180     p->nLevels      = nLevels;
00181     p->fVerbose     = fVerbose;
00182     p->fVeryVerbose = fVeryVerbose;
00183     p->nPercCutoff  = 10;
00184 
00185     // windowing
00186     p->vRoots    = Vec_PtrAlloc( 128 );
00187     p->vBranches = Vec_PtrAlloc( 128 );
00188 
00189     // internal AIG package
00190     // allocate room for objects
00191     p->nObjsAlloc = ABC_DC_MAX_NODES; 
00192     p->pObjs = ALLOC( Odc_Obj_t, p->nObjsAlloc * sizeof(Odc_Obj_t) );
00193     p->nPis  = nVarsMax + 32;
00194     p->nObjs = 1 + p->nPis;
00195     memset( p->pObjs, 0, p->nObjs * sizeof(Odc_Obj_t) );
00196     // set the PI masks
00197     for ( i = 0; i < 32; i++ )
00198         p->pObjs[1 + p->nVarsMax + i].uMask = (1 << i);
00199     // allocate hash table
00200     p->nTableSize = p->nObjsAlloc/3 + 1;
00201     p->pTable = ALLOC( Odc_Lit_t, p->nTableSize * sizeof(Odc_Lit_t) );
00202     memset( p->pTable, 0, p->nTableSize * sizeof(Odc_Lit_t) );
00203     p->vUsedSpots = Vec_IntAlloc( 1000 );
00204 
00205     // truth tables
00206     p->nWords = Abc_TruthWordNum( p->nVarsMax );
00207     p->nBits = p->nWords * 8 * sizeof(unsigned);
00208     p->vTruths = Vec_PtrAllocSimInfo( p->nObjsAlloc, p->nWords );
00209     p->vTruthsElem = Vec_PtrAllocSimInfo( p->nVarsMax, p->nWords );
00210 
00211     // set elementary truth tables
00212     Abc_InfoFill( Vec_PtrEntry(p->vTruths, 0), p->nWords );
00213     for ( k = 0; k < p->nVarsMax; k++ )
00214     {
00215 //        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
00216         pData = Vec_PtrEntry( p->vTruthsElem, k );
00217         Abc_InfoClear( pData, p->nWords );
00218         for ( i = 0; i < p->nBits; i++ )
00219             if ( i & (1 << k) )
00220                 pData[i>>5] |= (1 << (i&31));
00221     }
00222 
00223     // set random truth table for the additional inputs
00224     for ( k = p->nVarsMax; k < p->nPis; k++ )
00225     {
00226         pData = Odc_ObjTruth( p, Odc_Var(p, k) );
00227         Abc_InfoRandom( pData, p->nWords );
00228     }
00229 
00230     // set the miter to the unused value
00231     p->iRoot = 0xffff;
00232     return p;
00233 }

void Abc_NtkDontCareClear ( Odc_Man_t p  ) 

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

Synopsis [Clears the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file abcOdc.c.

00247 {
00248     int clk = clock();
00249     // clean the structural hashing table
00250     if ( Vec_IntSize(p->vUsedSpots) > p->nTableSize/3 ) // more than one third
00251         memset( p->pTable, 0, sizeof(Odc_Lit_t) * p->nTableSize );
00252     else
00253     {
00254         int iSpot, i;
00255         Vec_IntForEachEntry( p->vUsedSpots, iSpot, i )
00256             p->pTable[iSpot] = 0;
00257     }
00258     Vec_IntClear( p->vUsedSpots ); 
00259     // reset the number of nodes
00260     p->nObjs = 1 + p->nPis;
00261     // reset the root node
00262     p->iRoot = 0xffff;
00263 
00264 p->timeClean += clock() - clk;
00265 }

unsigned Abc_NtkDontCareCofactors_rec ( Odc_Man_t p,
Odc_Lit_t  Lit,
unsigned  uMask 
)

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

Synopsis [Recursively computes the pair of cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 742 of file abcOdc.c.

00743 {
00744     Odc_Obj_t * pObj;
00745     unsigned uData0, uData1;
00746     Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
00747     assert( !Odc_IsComplement(Lit) );
00748     // skip visited objects
00749     pObj = Odc_Lit2Obj( p, Lit );
00750     if ( Odc_ObjIsTravIdCurrent(p, pObj) )
00751         return pObj->uData;
00752     Odc_ObjSetTravIdCurrent(p, pObj);
00753     // skip objects out of the cone
00754     if ( (pObj->uMask & uMask) == 0 )
00755         return pObj->uData = ((Lit << 16) | Lit);
00756     // consider the case when the node is the var
00757     if ( pObj->uMask == uMask && Odc_IsTerm(p, Lit) )
00758         return pObj->uData = ((Odc_Const1() << 16) | Odc_Const0());
00759     // compute the cofactors
00760     uData0 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin0(pObj), uMask );
00761     uData1 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin1(pObj), uMask );
00762     // find the 0-cofactor
00763     uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Odc_ObjFaninC0(pObj) );
00764     uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Odc_ObjFaninC1(pObj) );
00765     uRes0 = Odc_And( p, uLit0, uLit1 );
00766     // find the 1-cofactor
00767     uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Odc_ObjFaninC0(pObj) );
00768     uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Odc_ObjFaninC1(pObj) );
00769     uRes1 = Odc_And( p, uLit0, uLit1 );
00770     // find the result
00771     return pObj->uData = ((uRes1 << 16) | uRes0);
00772 }

int Abc_NtkDontCareCompute ( Odc_Man_t p,
Abc_Obj_t pNode,
Vec_Ptr_t vLeaves,
unsigned *  puTruth 
)

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

Synopsis [Computes ODCs for the node in terms of the cut variables.]

Description [Returns the number of don't care minterms in the truth table. In particular, this procedure returns 0 if there is no don't-cares.]

SideEffects []

SeeAlso []

Definition at line 1037 of file abcOdc.c.

01038 {
01039     int nMints, RetValue;
01040     int clk, clkTotal = clock();
01041 
01042     p->nWins++;
01043     
01044     // set the parameters
01045     assert( !Abc_ObjIsComplement(pNode) );
01046     assert( Abc_ObjIsNode(pNode) );
01047     assert( Vec_PtrSize(vLeaves) <= p->nVarsMax );
01048     p->vLeaves = vLeaves;
01049     p->pNode = pNode;
01050 
01051     // compute the window
01052 clk = clock();
01053     RetValue = Abc_NtkDontCareWindow( p );
01054 p->timeWin += clock() - clk;
01055     if ( !RetValue )
01056     {
01057 p->timeAbort += clock() - clkTotal;
01058         Abc_InfoFill( puTruth, p->nWords );
01059         p->nWinsEmpty++;        
01060         return 0;
01061     }
01062 
01063     if ( p->fVeryVerbose )
01064     {
01065         printf( " %5d : ", pNode->Id );
01066         printf( "Leaf = %2d ", Vec_PtrSize(p->vLeaves) );
01067         printf( "Root = %2d ", Vec_PtrSize(p->vRoots) );
01068         printf( "Bran = %2d ", Vec_PtrSize(p->vBranches) );
01069         printf( " |  " );
01070     }
01071 
01072     // transfer the window into the AIG package
01073 clk = clock();
01074     Abc_NtkDontCareTransfer( p );
01075 p->timeMiter += clock() - clk;
01076 
01077     // simulate to estimate the amount of don't-cares
01078 clk = clock();
01079     nMints = Abc_NtkDontCareSimulateBefore( p, puTruth );
01080 p->timeSim += clock() - clk;
01081     if ( p->fVeryVerbose )
01082     {
01083         printf( "AIG = %5d ", Odc_NodeNum(p) );
01084         printf( "%6.2f %%  ", 100.0 * (p->nBits - nMints) / p->nBits );
01085     }
01086 
01087     // if there is less then the given percentage of don't-cares, skip
01088     if ( 100.0 * (p->nBits - nMints) / p->nBits < 1.0 * p->nPercCutoff )
01089     {
01090 p->timeAbort += clock() - clkTotal;
01091         if ( p->fVeryVerbose )
01092             printf( "Simulation cutoff.\n" );
01093         Abc_InfoFill( puTruth, p->nWords );
01094         p->nSimsEmpty++;
01095         return 0;
01096     }
01097 
01098     // quantify external variables
01099 clk = clock();
01100     RetValue = Abc_NtkDontCareQuantify( p );
01101 p->timeQuant += clock() - clk;
01102     if ( !RetValue )
01103     {
01104 p->timeAbort += clock() - clkTotal;
01105         if ( p->fVeryVerbose )
01106             printf( "=== Overflow! ===\n" );
01107         Abc_InfoFill( puTruth, p->nWords );
01108         p->nQuantsOver++;
01109         return 0;
01110     }
01111 
01112     // get the truth table
01113 clk = clock();
01114     Abc_NtkDontCareSimulateSetElem( p );
01115     nMints = Abc_NtkDontCareSimulate( p, puTruth );
01116 p->timeTruth += clock() - clk;
01117     if ( p->fVeryVerbose )
01118     {
01119         printf( "AIG = %5d ", Odc_NodeNum(p) );
01120         printf( "%6.2f %%  ", 100.0 * (p->nBits - nMints) / p->nBits );
01121         printf( "\n" );
01122     }
01123 p->timeTotal += clock() - clkTotal;
01124     p->nWinsFinish++;
01125     p->nTotalDcs += (int)(100.0 * (p->nBits - nMints) / p->nBits);
01126     return nMints;
01127 }

int Abc_NtkDontCareCountMintsWord ( Odc_Man_t p,
unsigned *  puTruth 
)

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

Synopsis [Set random simulation words for PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 896 of file abcOdc.c.

00897 {
00898     int w, Counter = 0;
00899     for ( w = 0; w < p->nWords; w++ )
00900         if ( puTruth[w] )
00901             Counter++;
00902     return Counter;
00903 }

void Abc_NtkDontCareFree ( Odc_Man_t p  ) 

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

Synopsis [Frees the don't-care manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file abcOdc.c.

00279 {
00280     if ( p->fVerbose )
00281     {
00282         printf( "Wins = %5d. Empty = %5d. SimsEmpty = %5d. QuantOver = %5d. WinsFinish = %5d.\n", 
00283             p->nWins, p->nWinsEmpty, p->nSimsEmpty, p->nQuantsOver, p->nWinsFinish );
00284         printf( "Ave DCs per window = %6.2f %%. Ave DCs per finished window = %6.2f %%.\n", 
00285             1.0*p->nTotalDcs/p->nWins, 1.0*p->nTotalDcs/p->nWinsFinish );
00286         printf( "Runtime stats of the ODC manager:\n" );
00287         PRT( "Cleaning    ", p->timeClean );
00288         PRT( "Windowing   ", p->timeWin   );
00289         PRT( "Miter       ", p->timeMiter );
00290         PRT( "Simulation  ", p->timeSim   );
00291         PRT( "Quantifying ", p->timeQuant );
00292         PRT( "Truth table ", p->timeTruth );
00293         PRT( "TOTAL       ", p->timeTotal );
00294         PRT( "Aborted     ", p->timeAbort );
00295     }
00296     Vec_PtrFree( p->vRoots );
00297     Vec_PtrFree( p->vBranches );
00298     Vec_PtrFree( p->vTruths );
00299     Vec_PtrFree( p->vTruthsElem );
00300     Vec_IntFree( p->vUsedSpots );
00301     free( p->pObjs );
00302     free( p->pTable );
00303     free( p );
00304 }

int Abc_NtkDontCareQuantify ( Odc_Man_t p  ) 

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

Synopsis [Quantifies the branch variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 785 of file abcOdc.c.

00786 {   
00787     Odc_Lit_t uRes0, uRes1;
00788     unsigned uData;
00789     int i;
00790     assert( p->iRoot < 0xffff );
00791     assert( Vec_PtrSize(p->vBranches) <= 32 ); // the mask size
00792     for ( i = 0; i < Vec_PtrSize(p->vBranches); i++ )
00793     {
00794         // compute the cofactors w.r.t. this variable
00795         Odc_ManIncrementTravId( p );
00796         uData = Abc_NtkDontCareCofactors_rec( p, Odc_Regular(p->iRoot), (1 << i) );
00797         uRes0 = Odc_NotCond( (Odc_Lit_t)(uData & 0xffff), Odc_IsComplement(p->iRoot) );
00798         uRes1 = Odc_NotCond( (Odc_Lit_t)(uData >> 16),    Odc_IsComplement(p->iRoot) );
00799         // quantify this variable existentially
00800         p->iRoot = Odc_Or( p, uRes0, uRes1 );
00801         // check the limit
00802         if ( Odc_ObjNum(p) > ABC_DC_MAX_NODES/2 )
00803             return 0;
00804     }
00805     assert( p->nObjs <= p->nObjsAlloc );
00806     return 1;
00807 }

int Abc_NtkDontCareSimulate ( Odc_Man_t p,
unsigned *  puTruth 
)

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

Synopsis [Computes the truth table of the care set.]

Description [Returns the number of ones in the simulation info.]

SideEffects []

SeeAlso []

Definition at line 986 of file abcOdc.c.

00987 {
00988     Odc_ManIncrementTravId( p );
00989     Abc_NtkDontCareSimulate_rec( p, Odc_Regular(p->iRoot) );
00990     Abc_InfoCopy( puTruth, Odc_ObjTruth(p, Odc_Regular(p->iRoot)), p->nWords );
00991     if ( Odc_IsComplement(p->iRoot) )
00992         Abc_InfoNot( puTruth, p->nWords );
00993     return Extra_TruthCountOnes( puTruth, p->nVarsMax );
00994 }

void Abc_NtkDontCareSimulate_rec ( Odc_Man_t p,
Odc_Lit_t  Lit 
)

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

Synopsis [Computes the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 956 of file abcOdc.c.

00957 {
00958     Odc_Obj_t * pObj;
00959     assert( !Odc_IsComplement(Lit) );
00960     // skip terminals
00961     if ( Odc_IsTerm(p, Lit) )
00962         return;
00963     // skip visited objects
00964     pObj = Odc_Lit2Obj( p, Lit );
00965     if ( Odc_ObjIsTravIdCurrent(p, pObj) )
00966         return;
00967     Odc_ObjSetTravIdCurrent(p, pObj);
00968     // call recursively
00969     Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin0(pObj) );
00970     Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin1(pObj) );
00971     // construct the truth table
00972     Abc_NtkDontCareTruthOne( p, Lit );
00973 }

int Abc_NtkDontCareSimulateBefore ( Odc_Man_t p,
unsigned *  puTruth 
)

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

Synopsis [Computes the truth table of the care set.]

Description [Returns the number of ones in the simulation info.]

SideEffects []

SeeAlso []

Definition at line 1007 of file abcOdc.c.

01008 {
01009     int nIters = 2;
01010     int nRounds, Counter, r;
01011     // decide how many rounds to simulate
01012     nRounds = p->nBits / p->nWords;
01013     Counter = 0;
01014     for ( r = 0; r < nIters; r++ )
01015     {
01016         Abc_NtkDontCareSimulateSetRand( p );
01017         Abc_NtkDontCareSimulate( p, puTruth );
01018         Counter += Abc_NtkDontCareCountMintsWord( p, puTruth );
01019     }
01020     // normalize
01021     Counter = Counter * nRounds / nIters;
01022     return Counter;
01023 }

void Abc_NtkDontCareSimulateSetElem ( Odc_Man_t p  ) 

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

Synopsis [Set elementary truth tables for PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 847 of file abcOdc.c.

00848 {
00849     unsigned * pData, * pData2;
00850     int k;
00851     for ( k = 0; k < p->nVarsMax; k++ )
00852     {
00853         pData = Odc_ObjTruth( p, Odc_Var(p, k) );
00854         pData2 = Vec_PtrEntry( p->vTruthsElem, k );
00855         Abc_InfoCopy( pData, pData2, p->nWords );
00856     }
00857 }

void Abc_NtkDontCareSimulateSetElem2 ( Odc_Man_t p  ) 

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

Synopsis [Set elementary truth tables for PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 822 of file abcOdc.c.

00823 {
00824     unsigned * pData;
00825     int i, k;
00826     for ( k = 0; k < p->nVarsMax; k++ )
00827     {
00828         pData = Odc_ObjTruth( p, Odc_Var(p, k) );
00829         Abc_InfoClear( pData, p->nWords );
00830         for ( i = 0; i < p->nBits; i++ )
00831             if ( i & (1 << k) )
00832                 pData[i>>5] |= (1 << (i&31));
00833     }
00834 }

void Abc_NtkDontCareSimulateSetRand ( Odc_Man_t p  ) 

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

Synopsis [Set random simulation words for PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 870 of file abcOdc.c.

00871 {
00872     unsigned * pData;
00873     int w, k, Number;
00874     for ( w = 0; w < p->nWords; w++ )
00875     {
00876         Number = rand();
00877         for ( k = 0; k < p->nVarsMax; k++ )
00878         {
00879             pData = Odc_ObjTruth( p, Odc_Var(p, k) );
00880             pData[w] = (Number & (1<<k)) ? ~0 : 0;
00881         }
00882     }
00883 }

int Abc_NtkDontCareTransfer ( Odc_Man_t p  ) 

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

Synopsis [Transfers the window into the AIG package.]

Description []

SideEffects []

SeeAlso []

Definition at line 692 of file abcOdc.c.

00693 {
00694     Abc_Obj_t * pObj;
00695     Odc_Lit_t uRes0, uRes1;
00696     Odc_Lit_t uLit;
00697     unsigned uData;
00698     int i;
00699     Abc_NtkIncrementTravId( p->pNode->pNtk );
00700     // set elementary variables at the leaves 
00701     Vec_PtrForEachEntry( p->vLeaves, pObj, i )
00702     {
00703         uLit = Odc_Var( p, i );
00704         pObj->pCopy = (void *)((uLit << 16) | uLit);
00705         Abc_NodeSetTravIdCurrent(pObj);
00706     }
00707     // set elementary variables at the branched 
00708     Vec_PtrForEachEntry( p->vBranches, pObj, i )
00709     {
00710         uLit = Odc_Var( p, i+p->nVarsMax );
00711         pObj->pCopy = (void *)((uLit << 16) | uLit);
00712         Abc_NodeSetTravIdCurrent(pObj);
00713     }
00714     // compute the AIG for the window
00715     p->iRoot = Odc_Const0();
00716     Vec_PtrForEachEntry( p->vRoots, pObj, i )
00717     {
00718         uData = (unsigned)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode );
00719         // get the cofactors
00720         uRes0 = uData & 0xffff;
00721         uRes1 = uData >> 16;
00722         // compute the miter
00723 //        assert( uRes0 != uRes1 ); // may be false if the node is redundant w.r.t. this root
00724         uLit = Odc_Xor( p, uRes0, uRes1 );
00725         p->iRoot = Odc_Or( p, p->iRoot, uLit );
00726     }
00727     return 1;
00728 }

void* Abc_NtkDontCareTransfer_rec ( Odc_Man_t p,
Abc_Obj_t pNode,
Abc_Obj_t pPivot 
)

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

Synopsis [Transfers the window into the AIG package.]

Description []

SideEffects []

SeeAlso []

Definition at line 653 of file abcOdc.c.

00654 {
00655     unsigned uData0, uData1;
00656     Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
00657     assert( !Abc_ObjIsComplement(pNode) );
00658     // skip visited objects
00659     if ( Abc_NodeIsTravIdCurrent(pNode) )
00660         return pNode->pCopy;
00661     Abc_NodeSetTravIdCurrent(pNode);
00662     assert( Abc_ObjIsNode(pNode) );
00663     // consider the case when the node is the pivot
00664     if ( pNode == pPivot )
00665         return pNode->pCopy = (void *)((Odc_Const1() << 16) | Odc_Const0());
00666     // compute the cofactors
00667     uData0 = (unsigned)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot );
00668     uData1 = (unsigned)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot );
00669     // find the 0-cofactor
00670     uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Abc_ObjFaninC0(pNode) );
00671     uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Abc_ObjFaninC1(pNode) );
00672     uRes0 = Odc_And( p, uLit0, uLit1 );
00673     // find the 1-cofactor
00674     uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Abc_ObjFaninC0(pNode) );
00675     uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Abc_ObjFaninC1(pNode) );
00676     uRes1 = Odc_And( p, uLit0, uLit1 );
00677     // find the result
00678     return pNode->pCopy = (void *)((uRes1 << 16) | uRes0);
00679 }

void Abc_NtkDontCareTruthOne ( Odc_Man_t p,
Odc_Lit_t  Lit 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 916 of file abcOdc.c.

00917 {
00918     Odc_Obj_t * pObj;
00919     unsigned * pInfo, * pInfo1, * pInfo2;
00920     int k, fComp1, fComp2;
00921     assert( !Odc_IsComplement( Lit ) );
00922     assert( !Odc_IsTerm( p, Lit ) );
00923     // get the truth tables
00924     pObj   = Odc_Lit2Obj( p, Lit );
00925     pInfo  = Odc_ObjTruth( p, Lit );
00926     pInfo1 = Odc_ObjTruth( p, Odc_ObjFanin0(pObj) );
00927     pInfo2 = Odc_ObjTruth( p, Odc_ObjFanin1(pObj) );
00928     fComp1 = Odc_ObjFaninC0( pObj );
00929     fComp2 = Odc_ObjFaninC1( pObj );
00930     // simulate
00931     if ( fComp1 && fComp2 )
00932         for ( k = 0; k < p->nWords; k++ )
00933             pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
00934     else if ( fComp1 && !fComp2 )
00935         for ( k = 0; k < p->nWords; k++ )
00936             pInfo[k] = ~pInfo1[k] &  pInfo2[k];
00937     else if ( !fComp1 && fComp2 )
00938         for ( k = 0; k < p->nWords; k++ )
00939             pInfo[k] =  pInfo1[k] & ~pInfo2[k];
00940     else // if ( fComp1 && fComp2 )
00941         for ( k = 0; k < p->nWords; k++ )
00942             pInfo[k] =  pInfo1[k] &  pInfo2[k];
00943 }

int Abc_NtkDontCareWinAddMissing ( Odc_Man_t p  ) 

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

Synopsis [Adds to the window nodes and leaves in the TFI of the roots.]

Description []

SideEffects []

SeeAlso []

Definition at line 454 of file abcOdc.c.

00455 {
00456     Abc_Obj_t * pObj;
00457     int i;
00458     // set the leaves
00459     Abc_NtkIncrementTravId( p->pNode->pNtk );
00460     Vec_PtrForEachEntry( p->vLeaves, pObj, i )
00461         Abc_NodeSetTravIdCurrent( pObj );        
00462     // explore from the roots
00463     Vec_PtrClear( p->vBranches );
00464     Vec_PtrForEachEntry( p->vRoots, pObj, i )
00465         if ( !Abc_NtkDontCareWinAddMissing_rec( p, pObj ) )
00466             return 0;
00467     return 1;
00468 }

int Abc_NtkDontCareWinAddMissing_rec ( Odc_Man_t p,
Abc_Obj_t pObj 
)

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

Synopsis [Recursively adds missing nodes and leaves.]

Description []

SideEffects []

SeeAlso []

Definition at line 422 of file abcOdc.c.

00423 {
00424     Abc_Obj_t * pFanin;
00425     int i;
00426     // skip the already collected leaves and branches
00427     if ( Abc_NodeIsTravIdCurrent(pObj) )
00428         return 1;
00429     // if this is not an internal node - make it a new branch
00430     if ( !Abc_NodeIsTravIdPrevious(pObj) || Abc_ObjIsCi(pObj) ) //|| (int)pObj->Level <= p->nLevLeaves )
00431     {
00432         Abc_NodeSetTravIdCurrent( pObj );
00433         Vec_PtrPush( p->vBranches, pObj );
00434         return Vec_PtrSize(p->vBranches) <= 32;
00435     }
00436     // visit the fanins of the node
00437     Abc_ObjForEachFanin( pObj, pFanin, i )
00438         if ( !Abc_NtkDontCareWinAddMissing_rec( p, pFanin ) )
00439             return 0;
00440     return 1;
00441 }

void Abc_NtkDontCareWinCollectRoots ( Odc_Man_t p  ) 

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

Synopsis [Collects the roots of the window.]

Description [Roots of the window are the nodes that have at least one fanout that it not in the TFO of the leaves.]

SideEffects []

SeeAlso []

Definition at line 401 of file abcOdc.c.

00402 {
00403     assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
00404     // mark the node with the old traversal ID
00405     Abc_NodeSetTravIdCurrent( p->pNode ); 
00406     // collect the roots
00407     Vec_PtrClear( p->vRoots );
00408     Abc_NtkDontCareWinCollectRoots_rec( p->pNode, p->vRoots );
00409 }

void Abc_NtkDontCareWinCollectRoots_rec ( Abc_Obj_t pObj,
Vec_Ptr_t vRoots 
)

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

Synopsis [Recursively collects the roots.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file abcOdc.c.

00369 {
00370     Abc_Obj_t * pFanout;
00371     int i;
00372     assert( Abc_ObjIsNode(pObj) );
00373     assert( Abc_NodeIsTravIdCurrent(pObj) );
00374     // check if the node has all fanouts marked
00375     Abc_ObjForEachFanout( pObj, pFanout, i )
00376         if ( !Abc_NodeIsTravIdCurrent(pFanout) )
00377             break;
00378     // if some of the fanouts are unmarked, add the node to the root
00379     if ( i < Abc_ObjFanoutNum(pObj) ) 
00380     {
00381         Vec_PtrPushUnique( vRoots, pObj );
00382         return;
00383     }
00384     // otherwise, call recursively
00385     Abc_ObjForEachFanout( pObj, pFanout, i )
00386         Abc_NtkDontCareWinCollectRoots_rec( pFanout, vRoots );
00387 }

int Abc_NtkDontCareWindow ( Odc_Man_t p  ) 

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

Synopsis [Computes window for the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 481 of file abcOdc.c.

00482 {
00483     // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax)
00484     Abc_NtkDontCareWinSweepLeafTfo( p );
00485     // find the roots of the window
00486     Abc_NtkDontCareWinCollectRoots( p );
00487     if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
00488     {
00489 //        printf( "Empty window\n" );
00490         return 0;
00491     }
00492     // add the nodes in the TFI of the roots that are not yet in the window
00493     if ( !Abc_NtkDontCareWinAddMissing( p ) )
00494     {
00495 //        printf( "Too many branches (%d)\n", Vec_PtrSize(p->vBranches) );
00496         return 0;
00497     }
00498     return 1;
00499 }

void Abc_NtkDontCareWinSweepLeafTfo ( Odc_Man_t p  ) 

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

Synopsis [Marks the TFO of the collected nodes up to the given level.]

Description []

SideEffects []

SeeAlso []

Definition at line 348 of file abcOdc.c.

00349 {
00350     Abc_Obj_t * pObj;
00351     int i;
00352     Abc_NtkIncrementTravId( p->pNode->pNtk );
00353     Vec_PtrForEachEntry( p->vLeaves, pObj, i )
00354         Abc_NtkDontCareWinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nLevels, p->pNode );
00355 }

void Abc_NtkDontCareWinSweepLeafTfo_rec ( Abc_Obj_t pObj,
int  nLevelLimit,
Abc_Obj_t pNode 
)

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

Synopsis [Marks the TFO of the collected nodes up to the given level.]

Description []

SideEffects []

SeeAlso []

Definition at line 319 of file abcOdc.c.

00320 {
00321     Abc_Obj_t * pFanout;
00322     int i;
00323     if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode )
00324         return;
00325     if ( Abc_NodeIsTravIdCurrent(pObj) )
00326         return;
00327     Abc_NodeSetTravIdCurrent( pObj );
00329     // try to reduce the runtime
00330     if ( Abc_ObjFanoutNum(pObj) > 100 )
00331         return;
00333     Abc_ObjForEachFanout( pObj, pFanout, i )
00334         Abc_NtkDontCareWinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode );
00335 }

static Odc_Lit_t Odc_And ( Odc_Man_t p,
Odc_Lit_t  iFan0,
Odc_Lit_t  iFan1 
) [inline, static]

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

Synopsis [Finds node by structural hashing or creates a new node.]

Description []

SideEffects []

SeeAlso []

Definition at line 569 of file abcOdc.c.

00570 {
00571     Odc_Obj_t * pObj;
00572     Odc_Lit_t * pEntry;
00573     unsigned uMask0, uMask1;
00574     int Temp;
00575     // consider trivial cases
00576     if ( iFan0 == iFan1 )
00577         return iFan0;
00578     if ( iFan0 == Odc_Not(iFan1) )
00579         return Odc_Const0();
00580     if ( Odc_Regular(iFan0) == Odc_Const1() )
00581         return iFan0 == Odc_Const1() ? iFan1 : Odc_Const0();
00582     if ( Odc_Regular(iFan1) == Odc_Const1() )
00583         return iFan1 == Odc_Const1() ? iFan0 : Odc_Const0();
00584     // canonicize the fanin order
00585     if ( iFan0 > iFan1 )
00586         Temp = iFan0, iFan0 = iFan1, iFan1 = Temp;
00587     // check if a node with these fanins exists
00588     pEntry = Odc_HashLookup( p, iFan0, iFan1 );
00589     if ( *pEntry )
00590         return *pEntry;
00591     // create a new node
00592     pObj = Odc_ObjNew( p );
00593     pObj->iFan0 = iFan0;
00594     pObj->iFan1 = iFan1;
00595     pObj->iNext = 0;
00596     pObj->TravId = 0;
00597     // set the mask
00598     uMask0 = Odc_Lit2Obj(p, Odc_Regular(iFan0))->uMask;
00599     uMask1 = Odc_Lit2Obj(p, Odc_Regular(iFan1))->uMask;
00600     pObj->uMask = uMask0 | uMask1;
00601     // add to the table
00602     *pEntry = Odc_Obj2Lit( p, pObj );
00603     return *pEntry;
00604 }

static Odc_Lit_t Odc_Const0 (  )  [inline, static]

Definition at line 110 of file abcOdc.c.

00110 { return 1;                             }

static Odc_Lit_t Odc_Const1 (  )  [inline, static]

Definition at line 111 of file abcOdc.c.

00111 { return 0;                             }

static unsigned Odc_HashKey ( Odc_Lit_t  iFan0,
Odc_Lit_t  iFan1,
int  TableSize 
) [inline, static]

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

Synopsis [Performing hashing of two AIG Literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 516 of file abcOdc.c.

00517 {
00518     unsigned Key = 0;
00519     Key ^= Odc_Regular(iFan0) * 7937;
00520     Key ^= Odc_Regular(iFan1) * 2971;
00521     Key ^= Odc_IsComplement(iFan0) * 911;
00522     Key ^= Odc_IsComplement(iFan1) * 353;
00523     return Key % TableSize;
00524 }

static Odc_Lit_t* Odc_HashLookup ( Odc_Man_t p,
Odc_Lit_t  iFan0,
Odc_Lit_t  iFan1 
) [inline, static]

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

Synopsis [Checks if the given name node already exists in the table.]

Description []

SideEffects []

SeeAlso []

Definition at line 537 of file abcOdc.c.

00538 {
00539     Odc_Obj_t * pObj;
00540     Odc_Lit_t * pEntry;
00541     unsigned uHashKey;
00542     assert( iFan0 < iFan1 );
00543     // get the hash key for this node
00544     uHashKey = Odc_HashKey( iFan0, iFan1, p->nTableSize );
00545     // remember the spot in the hash table that will be used
00546     if ( p->pTable[uHashKey] == 0 )
00547         Vec_IntPush( p->vUsedSpots, uHashKey );
00548     // find the entry
00549     for ( pEntry = p->pTable + uHashKey; *pEntry; pEntry = &pObj->iNext )
00550     {
00551         pObj = Odc_Lit2Obj( p, *pEntry );
00552         if ( pObj->iFan0 == iFan0 && pObj->iFan1 == iFan1 )
00553             return pEntry;
00554     }
00555     return pEntry;
00556 }

static int Odc_IsComplement ( Odc_Lit_t  Lit  )  [inline, static]

Definition at line 104 of file abcOdc.c.

00104 { return Lit &  (Odc_Lit_t)1;           }

static int Odc_IsConst ( Odc_Lit_t  Lit  )  [inline, static]

Definition at line 113 of file abcOdc.c.

00113 { return Lit <  (Odc_Lit_t)2;           }

static int Odc_IsTerm ( Odc_Man_t p,
Odc_Lit_t  Lit 
) [inline, static]

Definition at line 114 of file abcOdc.c.

00114 { return (int)(Lit>>1) <= p->nPis;      }

static Odc_Obj_t* Odc_Lit2Obj ( Odc_Man_t p,
Odc_Lit_t  Lit 
) [inline, static]

Definition at line 119 of file abcOdc.c.

00119 { assert( !(Lit & 1) && (int)(Lit>>1) < p->nObjs ); return p->pObjs + (Lit>>1); }

static void Odc_ManIncrementTravId ( Odc_Man_t p  )  [inline, static]

Definition at line 130 of file abcOdc.c.

00130 { p->nTravIds++;                                    }

static int Odc_NodeNum ( Odc_Man_t p  )  [inline, static]

Definition at line 100 of file abcOdc.c.

00100 { return p->nObjs - p->nPis - 1;        }

static Odc_Lit_t Odc_Not ( Odc_Lit_t  Lit  )  [inline, static]

Definition at line 106 of file abcOdc.c.

00106 { return Lit ^  (Odc_Lit_t)1;           }

static Odc_Lit_t Odc_NotCond ( Odc_Lit_t  Lit,
int  c 
) [inline, static]

Definition at line 107 of file abcOdc.c.

00107 { return Lit ^  (Odc_Lit_t)(c!=0);      }

static Odc_Lit_t Odc_Obj2Lit ( Odc_Man_t p,
Odc_Obj_t pObj 
) [inline, static]

Definition at line 118 of file abcOdc.c.

00118 { assert( pObj ); return (pObj - p->pObjs) << 1;                           }

static Odc_Lit_t Odc_ObjChild0 ( Odc_Obj_t pObj  )  [inline, static]

Definition at line 122 of file abcOdc.c.

00122 { return pObj->iFan0;                   }

static Odc_Lit_t Odc_ObjChild1 ( Odc_Obj_t pObj  )  [inline, static]

Definition at line 123 of file abcOdc.c.

00123 { return pObj->iFan1;                   }

static Odc_Lit_t Odc_ObjFanin0 ( Odc_Obj_t pObj  )  [inline, static]

Definition at line 124 of file abcOdc.c.

00124 { return Odc_Regular(pObj->iFan0);      }

static Odc_Lit_t Odc_ObjFanin1 ( Odc_Obj_t pObj  )  [inline, static]

Definition at line 125 of file abcOdc.c.

00125 { return Odc_Regular(pObj->iFan1);      }

static int Odc_ObjFaninC0 ( Odc_Obj_t pObj  )  [inline, static]

Definition at line 126 of file abcOdc.c.

00126 { return Odc_IsComplement(pObj->iFan0); }

static int Odc_ObjFaninC1 ( Odc_Obj_t pObj  )  [inline, static]

Definition at line 127 of file abcOdc.c.

00127 { return Odc_IsComplement(pObj->iFan1); }

static int Odc_ObjIsTravIdCurrent ( Odc_Man_t p,
Odc_Obj_t pObj 
) [inline, static]

Definition at line 132 of file abcOdc.c.

00132 { return (int )((int)pObj->TravId == p->nTravIds);  }

static Odc_Obj_t* Odc_ObjNew ( Odc_Man_t p  )  [inline, static]

Definition at line 117 of file abcOdc.c.

00117 { assert( p->nObjs < p->nObjsAlloc ); return p->pObjs + p->nObjs++;        }

static int Odc_ObjNum ( Odc_Man_t p  )  [inline, static]

Definition at line 101 of file abcOdc.c.

00101 { return p->nObjs;                      }

static void Odc_ObjSetTravIdCurrent ( Odc_Man_t p,
Odc_Obj_t pObj 
) [inline, static]

Definition at line 131 of file abcOdc.c.

00131 { pObj->TravId = p->nTravIds;                       }

static unsigned* Odc_ObjTruth ( Odc_Man_t p,
Odc_Lit_t  Lit 
) [inline, static]

Definition at line 135 of file abcOdc.c.

00135 { assert( !(Lit & 1) ); return Vec_PtrEntry(p->vTruths, Lit >> 1);  }

static Odc_Lit_t Odc_Or ( Odc_Man_t p,
Odc_Lit_t  iFan0,
Odc_Lit_t  iFan1 
) [inline, static]

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

Synopsis [Boolean OR.]

Description []

SideEffects []

SeeAlso []

Definition at line 617 of file abcOdc.c.

00618 {
00619     return Odc_Not( Odc_And(p, Odc_Not(iFan0), Odc_Not(iFan1)) );
00620 }

static int Odc_PiNum ( Odc_Man_t p  )  [inline, static]

Definition at line 99 of file abcOdc.c.

00099 { return p->nPis;                       }

static Odc_Lit_t Odc_Regular ( Odc_Lit_t  Lit  )  [inline, static]

Definition at line 105 of file abcOdc.c.

00105 { return Lit & ~(Odc_Lit_t)1;           }

static Odc_Lit_t Odc_Var ( Odc_Man_t p,
int  i 
) [inline, static]

Definition at line 112 of file abcOdc.c.

00112 { assert( i >= 0 && i < p->nPis ); return (i+1) << 1;  }

static Odc_Lit_t Odc_Xor ( Odc_Man_t p,
Odc_Lit_t  iFan0,
Odc_Lit_t  iFan1 
) [inline, static]

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

Synopsis [Boolean XOR.]

Description []

SideEffects []

SeeAlso []

Definition at line 633 of file abcOdc.c.

00634 {
00635     return Odc_Or( p, Odc_And(p, iFan0, Odc_Not(iFan1)), Odc_And(p, Odc_Not(iFan0), iFan1) );
00636 }


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