abcOdc.c File Reference

#include "base/abc/abc.h"

Go to the source code of this file.

Data Structures
struct	Odc_Obj_t_
struct	Odc_Man_t_

Macros
#define	ABC_DC_MAX_NODES   (1<<15)
	DECLARATIONS ///. More...
#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

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_t *	Odc_ObjNew (Odc_Man_t *p)
static Odc_Lit_t	Odc_Obj2Lit (Odc_Man_t *p, Odc_Obj_t *pObj)
static Odc_Obj_t *	Odc_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_t *	Abc_NtkDontCareAlloc (int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose)
	FUNCTION DEFINITIONS ///. More...
void	Abc_NtkDontCareClear (Odc_Man_t *p)
void	Abc_NtkDontCareFree (Odc_Man_t *p)
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_t *	Odc_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)
int	Abc_NtkDontCareCompute (Odc_Man_t *p, Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves, unsigned *puTruth)

Macro Definition Documentation

#define ABC_DC_MAX_NODES   (1<<15)

DECLARATIONS ///.

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

]

Definition at line 30 of file abcOdc.c.

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

Definition at line 142 of file abcOdc.c.

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

Definition at line 140 of file abcOdc.c.

Typedef Documentation

typedef unsigned short Odc_Lit_t

Definition at line 32 of file abcOdc.c.

typedef struct Odc_Obj_t_ Odc_Obj_t

Definition at line 34 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 162 of file abcOdc.c.

{
    Odc_Man_t * p;
    unsigned * pData;
    int i, k;
    p = ABC_ALLOC( Odc_Man_t, 1 );
    memset( p, 0, sizeof(Odc_Man_t) );
    assert( nVarsMax > 4 && nVarsMax < 16 );
    assert( nLevels > 0 && nLevels < 10 );

    srand( 0xABC );

    // dont'-care parameters
    p->nVarsMax     = nVarsMax;
    p->nLevels      = nLevels;
    p->fVerbose     = fVerbose;
    p->fVeryVerbose = fVeryVerbose;
    p->nPercCutoff  = 10;

    // windowing
    p->vRoots    = Vec_PtrAlloc( 128 );
    p->vBranches = Vec_PtrAlloc( 128 );

    // internal AIG package
    // allocate room for objects
    p->nObjsAlloc = ABC_DC_MAX_NODES; 
    p->pObjs = ABC_ALLOC( Odc_Obj_t, p->nObjsAlloc * sizeof(Odc_Obj_t) );
    p->nPis  = nVarsMax + 32;
    p->nObjs = 1 + p->nPis;
    memset( p->pObjs, 0, p->nObjs * sizeof(Odc_Obj_t) );
    // set the PI masks
    for ( i = 0; i < 32; i++ )
        p->pObjs[1 + p->nVarsMax + i].uMask = (1 << i);
    // allocate hash table
    p->nTableSize = p->nObjsAlloc/3 + 1;
    p->pTable = ABC_ALLOC( Odc_Lit_t, p->nTableSize * sizeof(Odc_Lit_t) );
    memset( p->pTable, 0, p->nTableSize * sizeof(Odc_Lit_t) );
    p->vUsedSpots = Vec_IntAlloc( 1000 );

    // truth tables
    p->nWords = Abc_TruthWordNum( p->nVarsMax );
    p->nBits = p->nWords * 8 * sizeof(unsigned);
    p->vTruths = Vec_PtrAllocSimInfo( p->nObjsAlloc, p->nWords );
    p->vTruthsElem = Vec_PtrAllocSimInfo( p->nVarsMax, p->nWords );

    // set elementary truth tables
    Abc_InfoFill( (unsigned *)Vec_PtrEntry(p->vTruths, 0), p->nWords );
    for ( k = 0; k < p->nVarsMax; k++ )
    {
//        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
        pData = (unsigned *)Vec_PtrEntry( p->vTruthsElem, k );
        Abc_InfoClear( pData, p->nWords );
        for ( i = 0; i < p->nBits; i++ )
            if ( i & (1 << k) )
                pData[i>>5] |= (1 << (i&31));
    }

    // set random truth table for the additional inputs
    for ( k = p->nVarsMax; k < p->nPis; k++ )
    {
        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
        Abc_InfoRandom( pData, p->nWords );
    }

    // set the miter to the unused value
    p->iRoot = 0xffff;
    return p;
}

void Abc_NtkDontCareClear

(

Odc_Man_t *

p

)

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

Synopsis [Clears the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 242 of file abcOdc.c.

{
    abctime clk = Abc_Clock();
    // clean the structural hashing table
    if ( Vec_IntSize(p->vUsedSpots) > p->nTableSize/3 ) // more than one third
        memset( p->pTable, 0, sizeof(Odc_Lit_t) * p->nTableSize );
    else
    {
        int iSpot, i;
        Vec_IntForEachEntry( p->vUsedSpots, iSpot, i )
            p->pTable[iSpot] = 0;
    }
    Vec_IntClear( p->vUsedSpots ); 
    // reset the number of nodes
    p->nObjs = 1 + p->nPis;
    // reset the root node
    p->iRoot = 0xffff;

p->timeClean += Abc_Clock() - clk;
}

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 738 of file abcOdc.c.

{
    Odc_Obj_t * pObj;
    unsigned uData0, uData1;
    Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
    assert( !Odc_IsComplement(Lit) );
    // skip visited objects
    pObj = Odc_Lit2Obj( p, Lit );
    if ( Odc_ObjIsTravIdCurrent(p, pObj) )
        return pObj->uData;
    Odc_ObjSetTravIdCurrent(p, pObj);
    // skip objects out of the cone
    if ( (pObj->uMask & uMask) == 0 )
        return pObj->uData = ((Lit << 16) | Lit);
    // consider the case when the node is the var
    if ( pObj->uMask == uMask && Odc_IsTerm(p, Lit) )
        return pObj->uData = ((Odc_Const1() << 16) | Odc_Const0());
    // compute the cofactors
    uData0 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin0(pObj), uMask );
    uData1 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin1(pObj), uMask );
    // find the 0-cofactor
    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Odc_ObjFaninC0(pObj) );
    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Odc_ObjFaninC1(pObj) );
    uRes0 = Odc_And( p, uLit0, uLit1 );
    // find the 1-cofactor
    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Odc_ObjFaninC0(pObj) );
    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Odc_ObjFaninC1(pObj) );
    uRes1 = Odc_And( p, uLit0, uLit1 );
    // find the result
    return pObj->uData = ((uRes1 << 16) | uRes0);
}

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 1033 of file abcOdc.c.

{
    int nMints, RetValue;
    abctime clk, clkTotal = Abc_Clock();

    p->nWins++;
    
    // set the parameters
    assert( !Abc_ObjIsComplement(pNode) );
    assert( Abc_ObjIsNode(pNode) );
    assert( Vec_PtrSize(vLeaves) <= p->nVarsMax );
    p->vLeaves = vLeaves;
    p->pNode = pNode;

    // compute the window
clk = Abc_Clock();
    RetValue = Abc_NtkDontCareWindow( p );
p->timeWin += Abc_Clock() - clk;
    if ( !RetValue )
    {
p->timeAbort += Abc_Clock() - clkTotal;
        Abc_InfoFill( puTruth, p->nWords );
        p->nWinsEmpty++;        
        return 0;
    }

    if ( p->fVeryVerbose )
    {
        printf( " %5d : ", pNode->Id );
        printf( "Leaf = %2d ", Vec_PtrSize(p->vLeaves) );
        printf( "Root = %2d ", Vec_PtrSize(p->vRoots) );
        printf( "Bran = %2d ", Vec_PtrSize(p->vBranches) );
        printf( " |  " );
    }

    // transfer the window into the AIG package
clk = Abc_Clock();
    Abc_NtkDontCareTransfer( p );
p->timeMiter += Abc_Clock() - clk;

    // simulate to estimate the amount of don't-cares
clk = Abc_Clock();
    nMints = Abc_NtkDontCareSimulateBefore( p, puTruth );
p->timeSim += Abc_Clock() - clk;
    if ( p->fVeryVerbose )
    {
        printf( "AIG = %5d ", Odc_NodeNum(p) );
        printf( "%6.2f %%  ", 100.0 * (p->nBits - nMints) / p->nBits );
    }

    // if there is less then the given percentage of don't-cares, skip
    if ( 100.0 * (p->nBits - nMints) / p->nBits < 1.0 * p->nPercCutoff )
    {
p->timeAbort += Abc_Clock() - clkTotal;
        if ( p->fVeryVerbose )
            printf( "Simulation cutoff.\n" );
        Abc_InfoFill( puTruth, p->nWords );
        p->nSimsEmpty++;
        return 0;
    }

    // quantify external variables
clk = Abc_Clock();
    RetValue = Abc_NtkDontCareQuantify( p );
p->timeQuant += Abc_Clock() - clk;
    if ( !RetValue )
    {
p->timeAbort += Abc_Clock() - clkTotal;
        if ( p->fVeryVerbose )
            printf( "=== Overflow! ===\n" );
        Abc_InfoFill( puTruth, p->nWords );
        p->nQuantsOver++;
        return 0;
    }

    // get the truth table
clk = Abc_Clock();
    Abc_NtkDontCareSimulateSetElem( p );
    nMints = Abc_NtkDontCareSimulate( p, puTruth );
p->timeTruth += Abc_Clock() - clk;
    if ( p->fVeryVerbose )
    {
        printf( "AIG = %5d ", Odc_NodeNum(p) );
        printf( "%6.2f %%  ", 100.0 * (p->nBits - nMints) / p->nBits );
        printf( "\n" );
    }
p->timeTotal += Abc_Clock() - clkTotal;
    p->nWinsFinish++;
    p->nTotalDcs += (int)(100.0 * (p->nBits - nMints) / p->nBits);
    return nMints;
}

int Abc_NtkDontCareCountMintsWord	(	Odc_Man_t *	p,
		unsigned *	puTruth
	)

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

Synopsis [Set random simulation words for PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 892 of file abcOdc.c.

{
    int w, Counter = 0;
    for ( w = 0; w < p->nWords; w++ )
        if ( puTruth[w] )
            Counter++;
    return Counter;
}

void Abc_NtkDontCareFree

(

Odc_Man_t *

p

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file abcOdc.c.

{
    if ( p->fVerbose )
    {
        printf( "Wins = %5d. Empty = %5d. SimsEmpty = %5d. QuantOver = %5d. WinsFinish = %5d.\n", 
            p->nWins, p->nWinsEmpty, p->nSimsEmpty, p->nQuantsOver, p->nWinsFinish );
        printf( "Ave DCs per window = %6.2f %%. Ave DCs per finished window = %6.2f %%.\n", 
            1.0*p->nTotalDcs/p->nWins, 1.0*p->nTotalDcs/p->nWinsFinish );
        printf( "Runtime stats of the ODC manager:\n" );
        ABC_PRT( "Cleaning    ", p->timeClean );
        ABC_PRT( "Windowing   ", p->timeWin   );
        ABC_PRT( "Miter       ", p->timeMiter );
        ABC_PRT( "Simulation  ", p->timeSim   );
        ABC_PRT( "Quantifying ", p->timeQuant );
        ABC_PRT( "Truth table ", p->timeTruth );
        ABC_PRT( "TOTAL       ", p->timeTotal );
        ABC_PRT( "Aborted     ", p->timeAbort );
    }
    Vec_PtrFree( p->vRoots );
    Vec_PtrFree( p->vBranches );
    Vec_PtrFree( p->vTruths );
    Vec_PtrFree( p->vTruthsElem );
    Vec_IntFree( p->vUsedSpots );
    ABC_FREE( p->pObjs );
    ABC_FREE( p->pTable );
    ABC_FREE( p );
}

int Abc_NtkDontCareQuantify

(

Odc_Man_t *

p

)

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

Synopsis [Quantifies the branch variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 781 of file abcOdc.c.

{   
    Odc_Lit_t uRes0, uRes1;
    unsigned uData;
    int i;
    assert( p->iRoot < 0xffff );
    assert( Vec_PtrSize(p->vBranches) <= 32 ); // the mask size
    for ( i = 0; i < Vec_PtrSize(p->vBranches); i++ )
    {
        // compute the cofactors w.r.t. this variable
        Odc_ManIncrementTravId( p );
        uData = Abc_NtkDontCareCofactors_rec( p, Odc_Regular(p->iRoot), (1 << i) );
        uRes0 = Odc_NotCond( (Odc_Lit_t)(uData & 0xffff), Odc_IsComplement(p->iRoot) );
        uRes1 = Odc_NotCond( (Odc_Lit_t)(uData >> 16),    Odc_IsComplement(p->iRoot) );
        // quantify this variable existentially
        p->iRoot = Odc_Or( p, uRes0, uRes1 );
        // check the limit
        if ( Odc_ObjNum(p) > ABC_DC_MAX_NODES/2 )
            return 0;
    }
    assert( p->nObjs <= p->nObjsAlloc );
    return 1;
}

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 982 of file abcOdc.c.

{
    Odc_ManIncrementTravId( p );
    Abc_NtkDontCareSimulate_rec( p, Odc_Regular(p->iRoot) );
    Abc_InfoCopy( puTruth, Odc_ObjTruth(p, Odc_Regular(p->iRoot)), p->nWords );
    if ( Odc_IsComplement(p->iRoot) )
        Abc_InfoNot( puTruth, p->nWords );
    return Extra_TruthCountOnes( puTruth, p->nVarsMax );
}

void Abc_NtkDontCareSimulate_rec	(	Odc_Man_t *	p,
		Odc_Lit_t	Lit
	)

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

Synopsis [Computes the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 952 of file abcOdc.c.

{
    Odc_Obj_t * pObj;
    assert( !Odc_IsComplement(Lit) );
    // skip terminals
    if ( Odc_IsTerm(p, Lit) )
        return;
    // skip visited objects
    pObj = Odc_Lit2Obj( p, Lit );
    if ( Odc_ObjIsTravIdCurrent(p, pObj) )
        return;
    Odc_ObjSetTravIdCurrent(p, pObj);
    // call recursively
    Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin0(pObj) );
    Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin1(pObj) );
    // construct the truth table
    Abc_NtkDontCareTruthOne( p, Lit );
}

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 1003 of file abcOdc.c.

{
    int nIters = 2;
    int nRounds, Counter, r;
    // decide how many rounds to simulate
    nRounds = p->nBits / p->nWords;
    Counter = 0;
    for ( r = 0; r < nIters; r++ )
    {
        Abc_NtkDontCareSimulateSetRand( p );
        Abc_NtkDontCareSimulate( p, puTruth );
        Counter += Abc_NtkDontCareCountMintsWord( p, puTruth );
    }
    // normalize
    Counter = Counter * nRounds / nIters;
    return Counter;
}

void Abc_NtkDontCareSimulateSetElem

(

Odc_Man_t *

p

)

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

Synopsis [Set elementary truth tables for PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 843 of file abcOdc.c.

{
    unsigned * pData, * pData2;
    int k;
    for ( k = 0; k < p->nVarsMax; k++ )
    {
        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
        pData2 = (unsigned *)Vec_PtrEntry( p->vTruthsElem, k );
        Abc_InfoCopy( pData, pData2, p->nWords );
    }
}

void Abc_NtkDontCareSimulateSetElem2

(

Odc_Man_t *

p

)

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

Synopsis [Set elementary truth tables for PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 818 of file abcOdc.c.

{
    unsigned * pData;
    int i, k;
    for ( k = 0; k < p->nVarsMax; k++ )
    {
        pData = Odc_ObjTruth( p, Odc_Var(p, k) );
        Abc_InfoClear( pData, p->nWords );
        for ( i = 0; i < p->nBits; i++ )
            if ( i & (1 << k) )
                pData[i>>5] |= (1 << (i&31));
    }
}

void Abc_NtkDontCareSimulateSetRand

(

Odc_Man_t *

p

)

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

Synopsis [Set random simulation words for PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 866 of file abcOdc.c.

{
    unsigned * pData;
    int w, k, Number;
    for ( w = 0; w < p->nWords; w++ )
    {
        Number = rand();
        for ( k = 0; k < p->nVarsMax; k++ )
        {
            pData = Odc_ObjTruth( p, Odc_Var(p, k) );
            pData[w] = (Number & (1<<k)) ? ~0 : 0;
        }
    }
}

int Abc_NtkDontCareTransfer

(

Odc_Man_t *

p

)

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

Synopsis [Transfers the window into the AIG package.]

Description []

SideEffects []

SeeAlso []

Definition at line 688 of file abcOdc.c.

{
    Abc_Obj_t * pObj;
    Odc_Lit_t uRes0, uRes1;
    Odc_Lit_t uLit;
    unsigned uData;
    int i;
    Abc_NtkIncrementTravId( p->pNode->pNtk );
    // set elementary variables at the leaves 
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
    {
        uLit = Odc_Var( p, i );
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((uLit << 16) | uLit);
        Abc_NodeSetTravIdCurrent(pObj);
    }
    // set elementary variables at the branched 
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vBranches, pObj, i )
    {
        uLit = Odc_Var( p, i+p->nVarsMax );
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((uLit << 16) | uLit);
        Abc_NodeSetTravIdCurrent(pObj);
    }
    // compute the AIG for the window
    p->iRoot = Odc_Const0();
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
    {
        uData = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode );
        // get the cofactors
        uRes0 = uData & 0xffff;
        uRes1 = uData >> 16;
        // compute the miter
//        assert( uRes0 != uRes1 ); // may be false if the node is redundant w.r.t. this root
        uLit = Odc_Xor( p, uRes0, uRes1 );
        p->iRoot = Odc_Or( p, p->iRoot, uLit );
    }
    return 1;
}

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 649 of file abcOdc.c.

{
    unsigned uData0, uData1;
    Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
    assert( !Abc_ObjIsComplement(pNode) );
    // skip visited objects
    if ( Abc_NodeIsTravIdCurrent(pNode) )
        return pNode->pCopy;
    Abc_NodeSetTravIdCurrent(pNode);
    assert( Abc_ObjIsNode(pNode) );
    // consider the case when the node is the pivot
    if ( pNode == pPivot )
        return pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((Odc_Const1() << 16) | Odc_Const0());
    // compute the cofactors
    uData0 = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot );
    uData1 = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot );
    // find the 0-cofactor
    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Abc_ObjFaninC0(pNode) );
    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Abc_ObjFaninC1(pNode) );
    uRes0 = Odc_And( p, uLit0, uLit1 );
    // find the 1-cofactor
    uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Abc_ObjFaninC0(pNode) );
    uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Abc_ObjFaninC1(pNode) );
    uRes1 = Odc_And( p, uLit0, uLit1 );
    // find the result
    return pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((uRes1 << 16) | uRes0);
}

void Abc_NtkDontCareTruthOne	(	Odc_Man_t *	p,
		Odc_Lit_t	Lit
	)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 912 of file abcOdc.c.

{
    Odc_Obj_t * pObj;
    unsigned * pInfo, * pInfo1, * pInfo2;
    int k, fComp1, fComp2;
    assert( !Odc_IsComplement( Lit ) );
    assert( !Odc_IsTerm( p, Lit ) );
    // get the truth tables
    pObj   = Odc_Lit2Obj( p, Lit );
    pInfo  = Odc_ObjTruth( p, Lit );
    pInfo1 = Odc_ObjTruth( p, Odc_ObjFanin0(pObj) );
    pInfo2 = Odc_ObjTruth( p, Odc_ObjFanin1(pObj) );
    fComp1 = Odc_ObjFaninC0( pObj );
    fComp2 = Odc_ObjFaninC1( pObj );
    // simulate
    if ( fComp1 && fComp2 )
        for ( k = 0; k < p->nWords; k++ )
            pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
    else if ( fComp1 && !fComp2 )
        for ( k = 0; k < p->nWords; k++ )
            pInfo[k] = ~pInfo1[k] &  pInfo2[k];
    else if ( !fComp1 && fComp2 )
        for ( k = 0; k < p->nWords; k++ )
            pInfo[k] =  pInfo1[k] & ~pInfo2[k];
    else // if ( fComp1 && fComp2 )
        for ( k = 0; k < p->nWords; k++ )
            pInfo[k] =  pInfo1[k] &  pInfo2[k];
}

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 450 of file abcOdc.c.

{
    Abc_Obj_t * pObj;
    int i;
    // set the leaves
    Abc_NtkIncrementTravId( p->pNode->pNtk );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
        Abc_NodeSetTravIdCurrent( pObj );        
    // explore from the roots
    Vec_PtrClear( p->vBranches );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
        if ( !Abc_NtkDontCareWinAddMissing_rec( p, pObj ) )
            return 0;
    return 1;
}

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 418 of file abcOdc.c.

{
    Abc_Obj_t * pFanin;
    int i;
    // skip the already collected leaves and branches
    if ( Abc_NodeIsTravIdCurrent(pObj) )
        return 1;
    // if this is not an internal node - make it a new branch
    if ( !Abc_NodeIsTravIdPrevious(pObj) || Abc_ObjIsCi(pObj) ) //|| (int)pObj->Level <= p->nLevLeaves )
    {
        Abc_NodeSetTravIdCurrent( pObj );
        Vec_PtrPush( p->vBranches, pObj );
        return Vec_PtrSize(p->vBranches) <= 32;
    }
    // visit the fanins of the node
    Abc_ObjForEachFanin( pObj, pFanin, i )
        if ( !Abc_NtkDontCareWinAddMissing_rec( p, pFanin ) )
            return 0;
    return 1;
}

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 397 of file abcOdc.c.

{
    assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
    // mark the node with the old traversal ID
    Abc_NodeSetTravIdCurrent( p->pNode ); 
    // collect the roots
    Vec_PtrClear( p->vRoots );
    Abc_NtkDontCareWinCollectRoots_rec( p->pNode, p->vRoots );
}

void Abc_NtkDontCareWinCollectRoots_rec	(	Abc_Obj_t *	pObj,
		Vec_Ptr_t *	vRoots
	)

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

Synopsis [Recursively collects the roots.]

Description []

SideEffects []

SeeAlso []

Definition at line 364 of file abcOdc.c.

{
    Abc_Obj_t * pFanout;
    int i;
    assert( Abc_ObjIsNode(pObj) );
    assert( Abc_NodeIsTravIdCurrent(pObj) );
    // check if the node has all fanouts marked
    Abc_ObjForEachFanout( pObj, pFanout, i )
        if ( !Abc_NodeIsTravIdCurrent(pFanout) )
            break;
    // if some of the fanouts are unmarked, add the node to the root
    if ( i < Abc_ObjFanoutNum(pObj) ) 
    {
        Vec_PtrPushUnique( vRoots, pObj );
        return;
    }
    // otherwise, call recursively
    Abc_ObjForEachFanout( pObj, pFanout, i )
        Abc_NtkDontCareWinCollectRoots_rec( pFanout, vRoots );
}

int Abc_NtkDontCareWindow

(

Odc_Man_t *

p

)

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

Synopsis [Computes window for the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 477 of file abcOdc.c.

{
    // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax)
    Abc_NtkDontCareWinSweepLeafTfo( p );
    // find the roots of the window
    Abc_NtkDontCareWinCollectRoots( p );
    if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
    {
//        printf( "Empty window\n" );
        return 0;
    }
    // add the nodes in the TFI of the roots that are not yet in the window
    if ( !Abc_NtkDontCareWinAddMissing( p ) )
    {
//        printf( "Too many branches (%d)\n", Vec_PtrSize(p->vBranches) );
        return 0;
    }
    return 1;
}

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 344 of file abcOdc.c.

{
    Abc_Obj_t * pObj;
    int i;
    Abc_NtkIncrementTravId( p->pNode->pNtk );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
        Abc_NtkDontCareWinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nLevels, p->pNode );
}

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 315 of file abcOdc.c.

{
    Abc_Obj_t * pFanout;
    int i;
    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode )
        return;
    if ( Abc_NodeIsTravIdCurrent(pObj) )
        return;
    Abc_NodeSetTravIdCurrent( pObj );
    ////////////////////////////////////////
    // try to reduce the runtime
    if ( Abc_ObjFanoutNum(pObj) > 100 )
        return;
    ////////////////////////////////////////
    Abc_ObjForEachFanout( pObj, pFanout, i )
        Abc_NtkDontCareWinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode );
}

static Odc_Lit_t Odc_And ( Odc_Man_t *  p, Odc_Lit_t  iFan0, Odc_Lit_t  iFan1  )

inlinestatic

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 565 of file abcOdc.c.

{
    Odc_Obj_t * pObj;
    Odc_Lit_t * pEntry;
    unsigned uMask0, uMask1;
    int Temp;
    // consider trivial cases
    if ( iFan0 == iFan1 )
        return iFan0;
    if ( iFan0 == Odc_Not(iFan1) )
        return Odc_Const0();
    if ( Odc_Regular(iFan0) == Odc_Const1() )
        return iFan0 == Odc_Const1() ? iFan1 : Odc_Const0();
    if ( Odc_Regular(iFan1) == Odc_Const1() )
        return iFan1 == Odc_Const1() ? iFan0 : Odc_Const0();
    // canonicize the fanin order
    if ( iFan0 > iFan1 )
        Temp = iFan0, iFan0 = iFan1, iFan1 = Temp;
    // check if a node with these fanins exists
    pEntry = Odc_HashLookup( p, iFan0, iFan1 );
    if ( *pEntry )
        return *pEntry;
    // create a new node
    pObj = Odc_ObjNew( p );
    pObj->iFan0 = iFan0;
    pObj->iFan1 = iFan1;
    pObj->iNext = 0;
    pObj->TravId = 0;
    // set the mask
    uMask0 = Odc_Lit2Obj(p, Odc_Regular(iFan0))->uMask;
    uMask1 = Odc_Lit2Obj(p, Odc_Regular(iFan1))->uMask;
    pObj->uMask = uMask0 | uMask1;
    // add to the table
    *pEntry = Odc_Obj2Lit( p, pObj );
    return *pEntry;
}

static Odc_Lit_t Odc_Const0 ( )

inlinestatic

Definition at line 112 of file abcOdc.c.

{ return 1;                             }

static Odc_Lit_t Odc_Const1 ( )

inlinestatic

Definition at line 113 of file abcOdc.c.

{ return 0;                             }

static unsigned Odc_HashKey ( Odc_Lit_t  iFan0, Odc_Lit_t  iFan1, int  TableSize  )

inlinestatic

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

Synopsis [Performing hashing of two AIG Literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 512 of file abcOdc.c.

{
    unsigned Key = 0;
    Key ^= Odc_Regular(iFan0) * 7937;
    Key ^= Odc_Regular(iFan1) * 2971;
    Key ^= Odc_IsComplement(iFan0) * 911;
    Key ^= Odc_IsComplement(iFan1) * 353;
    return Key % TableSize;
}

static Odc_Lit_t* Odc_HashLookup ( Odc_Man_t *  p, Odc_Lit_t  iFan0, Odc_Lit_t  iFan1  )

inlinestatic

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 533 of file abcOdc.c.

{
    Odc_Obj_t * pObj;
    Odc_Lit_t * pEntry;
    unsigned uHashKey;
    assert( iFan0 < iFan1 );
    // get the hash key for this node
    uHashKey = Odc_HashKey( iFan0, iFan1, p->nTableSize );
    // remember the spot in the hash table that will be used
    if ( p->pTable[uHashKey] == 0 )
        Vec_IntPush( p->vUsedSpots, uHashKey );
    // find the entry
    for ( pEntry = p->pTable + uHashKey; *pEntry; pEntry = &pObj->iNext )
    {
        pObj = Odc_Lit2Obj( p, *pEntry );
        if ( pObj->iFan0 == iFan0 && pObj->iFan1 == iFan1 )
            return pEntry;
    }
    return pEntry;
}

static int Odc_IsComplement ( Odc_Lit_t  Lit )

inlinestatic

Definition at line 106 of file abcOdc.c.

{ return Lit &  (Odc_Lit_t)1;           }

static int Odc_IsConst ( Odc_Lit_t  Lit )

inlinestatic

Definition at line 115 of file abcOdc.c.

{ return Lit <  (Odc_Lit_t)2;           }

static int Odc_IsTerm ( Odc_Man_t *  p, Odc_Lit_t  Lit  )

inlinestatic

Definition at line 116 of file abcOdc.c.

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

static Odc_Obj_t* Odc_Lit2Obj ( Odc_Man_t *  p, Odc_Lit_t  Lit  )

inlinestatic

Definition at line 121 of file abcOdc.c.

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

static void Odc_ManIncrementTravId ( Odc_Man_t *  p )

inlinestatic

Definition at line 132 of file abcOdc.c.

{ p->nTravIds++;                                    }

static int Odc_NodeNum ( Odc_Man_t *  p )

inlinestatic

Definition at line 102 of file abcOdc.c.

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

static Odc_Lit_t Odc_Not ( Odc_Lit_t  Lit )

inlinestatic

Definition at line 108 of file abcOdc.c.

{ return Lit ^  (Odc_Lit_t)1;           }

static Odc_Lit_t Odc_NotCond ( Odc_Lit_t  Lit, int  c  )

inlinestatic

Definition at line 109 of file abcOdc.c.

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

static Odc_Lit_t Odc_Obj2Lit ( Odc_Man_t *  p, Odc_Obj_t *  pObj  )

inlinestatic

Definition at line 120 of file abcOdc.c.

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

static Odc_Lit_t Odc_ObjChild0 ( Odc_Obj_t *  pObj )

inlinestatic

Definition at line 124 of file abcOdc.c.

{ return pObj->iFan0;                   }

static Odc_Lit_t Odc_ObjChild1 ( Odc_Obj_t *  pObj )

inlinestatic

Definition at line 125 of file abcOdc.c.

{ return pObj->iFan1;                   }

static Odc_Lit_t Odc_ObjFanin0 ( Odc_Obj_t *  pObj )

inlinestatic

Definition at line 126 of file abcOdc.c.

{ return Odc_Regular(pObj->iFan0);      }

static Odc_Lit_t Odc_ObjFanin1 ( Odc_Obj_t *  pObj )

inlinestatic

Definition at line 127 of file abcOdc.c.

{ return Odc_Regular(pObj->iFan1);      }

static int Odc_ObjFaninC0 ( Odc_Obj_t *  pObj )

inlinestatic

Definition at line 128 of file abcOdc.c.

{ return Odc_IsComplement(pObj->iFan0); }

static int Odc_ObjFaninC1 ( Odc_Obj_t *  pObj )

inlinestatic

Definition at line 129 of file abcOdc.c.

{ return Odc_IsComplement(pObj->iFan1); }

static int Odc_ObjIsTravIdCurrent ( Odc_Man_t *  p, Odc_Obj_t *  pObj  )

inlinestatic

Definition at line 134 of file abcOdc.c.

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

static Odc_Obj_t* Odc_ObjNew ( Odc_Man_t *  p )

inlinestatic

Definition at line 119 of file abcOdc.c.

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

static int Odc_ObjNum ( Odc_Man_t *  p )

inlinestatic

Definition at line 103 of file abcOdc.c.

{ return p->nObjs;                      }

static void Odc_ObjSetTravIdCurrent ( Odc_Man_t *  p, Odc_Obj_t *  pObj  )

inlinestatic

Definition at line 133 of file abcOdc.c.

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

static unsigned* Odc_ObjTruth ( Odc_Man_t *  p, Odc_Lit_t  Lit  )

inlinestatic

Definition at line 137 of file abcOdc.c.

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

static Odc_Lit_t Odc_Or ( Odc_Man_t *  p, Odc_Lit_t  iFan0, Odc_Lit_t  iFan1  )

inlinestatic

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

Synopsis [Boolean OR.]

Description []

SideEffects []

SeeAlso []

Definition at line 613 of file abcOdc.c.

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

static int Odc_PiNum ( Odc_Man_t *  p )

inlinestatic

Definition at line 101 of file abcOdc.c.

{ return p->nPis;                       }

static Odc_Lit_t Odc_Regular ( Odc_Lit_t  Lit )

inlinestatic

Definition at line 107 of file abcOdc.c.

{ return Lit & ~(Odc_Lit_t)1;           }

static Odc_Lit_t Odc_Var ( Odc_Man_t *  p, int  i  )

inlinestatic

Definition at line 114 of file abcOdc.c.

{ 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  )

inlinestatic

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

Synopsis [Boolean XOR.]

Description []

SideEffects []

SeeAlso []

Definition at line 629 of file abcOdc.c.

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