aigUtil.c File Reference

#include "aig.h"
#include "proof/fra/fra.h"
#include "aig/saig/saig.h"

Go to the source code of this file.

Macros
#define	NUMBER1   3716960521u
#define	NUMBER2   2174103536u

Functions
ABC_NAMESPACE_IMPL_START void	Aig_ManIncrementTravId (Aig_Man_t *p)
	DECLARATIONS ///. More...
char *	Aig_TimeStamp ()
int	Aig_ManHasNoGaps (Aig_Man_t *p)
int	Aig_ManLevels (Aig_Man_t *p)
void	Aig_ManResetRefs (Aig_Man_t *p)
void	Aig_ManCleanMarkA (Aig_Man_t *p)
void	Aig_ManCleanMarkB (Aig_Man_t *p)
void	Aig_ManCleanMarkAB (Aig_Man_t *p)
void	Aig_ManCleanData (Aig_Man_t *p)
void	Aig_ManCleanNext (Aig_Man_t *p)
void	Aig_ObjCleanData_rec (Aig_Obj_t *pObj)
void	Aig_ObjCollectMulti_rec (Aig_Obj_t *pRoot, Aig_Obj_t *pObj, Vec_Ptr_t *vSuper)
void	Aig_ObjCollectMulti (Aig_Obj_t *pRoot, Vec_Ptr_t *vSuper)
int	Aig_ObjIsMuxType (Aig_Obj_t *pNode)
int	Aig_ObjRecognizeExor (Aig_Obj_t *pObj, Aig_Obj_t **ppFan0, Aig_Obj_t **ppFan1)
Aig_Obj_t *	Aig_ObjRecognizeMux (Aig_Obj_t *pNode, Aig_Obj_t **ppNodeT, Aig_Obj_t **ppNodeE)
Aig_Obj_t *	Aig_ObjReal_rec (Aig_Obj_t *pObj)
int	Aig_ObjCompareIdIncrease (Aig_Obj_t **pp1, Aig_Obj_t **pp2)
void	Aig_ObjPrintEqn (FILE *pFile, Aig_Obj_t *pObj, Vec_Vec_t *vLevels, int Level)
void	Aig_ObjPrintVerilog (FILE *pFile, Aig_Obj_t *pObj, Vec_Vec_t *vLevels, int Level)
void	Aig_ObjPrintVerbose (Aig_Obj_t *pObj, int fHaig)
void	Aig_ManPrintVerbose (Aig_Man_t *p, int fHaig)
void	Aig_ManDump (Aig_Man_t *p)
void	Aig_ManDumpBlif (Aig_Man_t *p, char *pFileName, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vPoNames)
void	Aig_ManDumpVerilog (Aig_Man_t *p, char *pFileName)
void	Aig_ManSetCioIds (Aig_Man_t *p)
void	Aig_ManCleanCioIds (Aig_Man_t *p)
int	Aig_ManChoiceNum (Aig_Man_t *p)
void	Aig_ManPrintControlFanouts (Aig_Man_t *p)
char *	Aig_FileNameGenericAppend (char *pBase, char *pSuffix)
void	Aig_ManRandomTest2 ()
void	Aig_ManRandomTest1 ()
unsigned	Aig_ManRandom (int fReset)
	GLOBAL VARIABLES ///. More...
word	Aig_ManRandom64 (int fReset)
void	Aig_ManRandomInfo (Vec_Ptr_t *vInfo, int iInputStart, int iWordStart, int iWordStop)
void	Aig_NodeUnionLists (Vec_Ptr_t *vArr1, Vec_Ptr_t *vArr2, Vec_Ptr_t *vArr)
void	Aig_NodeIntersectLists (Vec_Ptr_t *vArr1, Vec_Ptr_t *vArr2, Vec_Ptr_t *vArr)
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void	Aig_ManCounterExampleValueStart (Aig_Man_t *pAig, Abc_Cex_t *pCex)
void	Aig_ManCounterExampleValueStop (Aig_Man_t *pAig)
int	Aig_ManCounterExampleValueLookup (Aig_Man_t *pAig, int Id, int iFrame)
void	Aig_ManCounterExampleValueTest (Aig_Man_t *pAig, Abc_Cex_t *pCex)
void	Aig_ManSetPhase (Aig_Man_t *pAig)
Vec_Ptr_t *	Aig_ManMuxesCollect (Aig_Man_t *pAig)
void	Aig_ManMuxesDeref (Aig_Man_t *pAig, Vec_Ptr_t *vMuxes)
void	Aig_ManMuxesRef (Aig_Man_t *pAig, Vec_Ptr_t *vMuxes)
void	Aig_ManInvertConstraints (Aig_Man_t *pAig)

Macro Definition Documentation

#define NUMBER1   3716960521u

Definition at line 1143 of file aigUtil.c.

#define NUMBER2   2174103536u

Definition at line 1144 of file aigUtil.c.

Function Documentation

char* Aig_FileNameGenericAppend	(	char *	pBase,
		char *	pSuffix
	)

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

Synopsis [Returns the composite name of the file.]

Description []

SideEffects []

SeeAlso []

Definition at line 1070 of file aigUtil.c.

{
    static char Buffer[1000];
    char * pDot;
    strcpy( Buffer, pBase );
    if ( (pDot = strrchr( Buffer, '.' )) )
        *pDot = 0;
    strcat( Buffer, pSuffix );
    if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) )
        return pDot+1;
    return Buffer;
}

int Aig_ManChoiceNum

(

Aig_Man_t *

p

)

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

Synopsis [Sets the PI/PO numbers.]

Description []

SideEffects []

SeeAlso []

Definition at line 1007 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Aig_ManForEachNode( p, pObj, i )
        Counter += Aig_ObjIsChoice( p, pObj );
    return Counter;
}

void Aig_ManCleanCioIds

(

Aig_Man_t *

p

)

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

Synopsis [Sets the PI/PO numbers.]

Description []

SideEffects []

SeeAlso []

Definition at line 986 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachCi( p, pObj, i )
        pObj->pNext = NULL;
    Aig_ManForEachCo( p, pObj, i )
        pObj->pNext = NULL;
}

void Aig_ManCleanData

(

Aig_Man_t *

p

)

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

Synopsis [Cleans the data pointers for the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachObj( p, pObj, i )
        pObj->pData = NULL;
}

void Aig_ManCleanMarkA

(

Aig_Man_t *

p

)

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

Synopsis [Cleans fMarkA.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachObj( p, pObj, i )
        pObj->fMarkA = 0;
}

void Aig_ManCleanMarkAB

(

Aig_Man_t *

p

)

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

Synopsis [Cleans fMarkB.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachObj( p, pObj, i )
        pObj->fMarkA = pObj->fMarkB = 0;
}

void Aig_ManCleanMarkB

(

Aig_Man_t *

p

)

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

Synopsis [Cleans fMarkB.]

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachObj( p, pObj, i )
        pObj->fMarkB = 0;
}

void Aig_ManCleanNext

(

Aig_Man_t *

p

)

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

Synopsis [Cleans the data pointers for the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 224 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachObj( p, pObj, i )
        pObj->pNext = NULL;
}

int Aig_ManCounterExampleValueLookup	(	Aig_Man_t *	pAig,
		int	Id,
		int	iFrame
	)

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

Synopsis [Returns the value of the given object in the given timeframe.]

Description [Should be called to probe the value of an object with the given ID (iFrame is a 0-based number of a time frame - should not exceed the number of timeframes in the original counter-example).]

SideEffects []

SeeAlso []

Definition at line 1392 of file aigUtil.c.

{
    assert( Id >= 0 && Id < Aig_ManObjNumMax(pAig) );
    return Abc_InfoHasBit( (unsigned *)pAig->pData2, Aig_ManObjNumMax(pAig) * iFrame + Id );
}

void Aig_ManCounterExampleValueStart	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	pCex
	)

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

Synopsis [Starts the process of retuning values for internal nodes.]

Description [Should be called when pCex is available, before probing any object for its value using Aig_ManCounterExampleValueLookup().]

SideEffects []

SeeAlso []

Definition at line 1313 of file aigUtil.c.

{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int Val0, Val1, nObjs, i, k, iBit = 0;
    assert( Aig_ManRegNum(pAig) > 0 ); // makes sense only for sequential AIGs
    assert( pAig->pData2 == NULL );    // if this fail, there may be a memory leak
    // allocate memory to store simulation bits for internal nodes
    pAig->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNumMax(pAig) ) );
    // the register values in the counter-example should be zero
    Saig_ManForEachLo( pAig, pObj, k )
        assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
    // iterate through the timeframes
    nObjs = Aig_ManObjNumMax(pAig);
    for ( i = 0; i <= pCex->iFrame; i++ )
    {
        // set constant 1 node
        Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 );
        // set primary inputs according to the counter-example
        Saig_ManForEachPi( pAig, pObj, k )
            if ( Abc_InfoHasBit(pCex->pData, iBit++) )
                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
        // compute values for each node
        Aig_ManForEachNode( pAig, pObj, k )
        {
            Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
            Val1 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
            if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) )
                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
        }
        // derive values for combinational outputs
        Aig_ManForEachCo( pAig, pObj, k )
        {
            Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
            if ( Val0 ^ Aig_ObjFaninC0(pObj) )
                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
        }
        if ( i == pCex->iFrame )
            continue;
        // transfer values to the register output of the next frame
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            if ( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
    }
    assert( iBit == pCex->nBits );
    // check that the counter-example is correct, that is, the corresponding output is asserted
    assert( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManCo(pAig, pCex->iPo)) ) );
}

void Aig_ManCounterExampleValueStop

(

Aig_Man_t *

pAig

)

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

Synopsis [Stops the process of retuning values for internal nodes.]

Description [Should be called when probing is no longer needed]

SideEffects []

SeeAlso []

Definition at line 1372 of file aigUtil.c.

{
    assert( pAig->pData2 != NULL );    // if this fail, we try to call this procedure more than once
    free( pAig->pData2 );
    pAig->pData2 = NULL;
}

void Aig_ManCounterExampleValueTest	(	Aig_Man_t *	pAig,
		Abc_Cex_t *	pCex
	)

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

Synopsis [Procedure to test the above code.]

Description []

SideEffects []

SeeAlso []

Definition at line 1409 of file aigUtil.c.

{
    Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNumMax(pAig)/2 );
    int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 );
    printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
    Aig_ManCounterExampleValueStart( pAig, pCex );
    printf( "Value of object %d in frame %d is %d.\n", Aig_ObjId(pObj), iFrame,
        Aig_ManCounterExampleValueLookup(pAig, Aig_ObjId(pObj), iFrame) );
    Aig_ManCounterExampleValueStop( pAig );
}

void Aig_ManDump

(

Aig_Man_t *

p

)

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

Synopsis [Write speculative miter for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 712 of file aigUtil.c.

{ 
    static int Counter = 0;
    char FileName[20];
    // dump the logic into a file
    sprintf( FileName, "aigbug\\%03d.blif", ++Counter );
    Aig_ManDumpBlif( p, FileName, NULL, NULL );
    printf( "Intermediate AIG with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(p), FileName );
}

void Aig_ManDumpBlif	(	Aig_Man_t *	p,
		char *	pFileName,
		Vec_Ptr_t *	vPiNames,
		Vec_Ptr_t *	vPoNames
	)

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

Synopsis [Writes the AIG into a BLIF file.]

Description []

SideEffects []

SeeAlso []

Definition at line 733 of file aigUtil.c.

{
    FILE * pFile;
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
    int i, nDigits, Counter = 0;
    if ( Aig_ManCoNum(p) == 0 )
    {
        printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
        return;
    }
    // check if constant is used
    Aig_ManForEachCo( p, pObj, i )
        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
            pConst1 = Aig_ManConst1(p);
    // collect nodes in the DFS order
    vNodes = Aig_ManDfs( p, 1 );
    // assign IDs to objects
    Aig_ManConst1(p)->iData = Counter++;
    Aig_ManForEachCi( p, pObj, i )
        pObj->iData = Counter++;
    Aig_ManForEachCo( p, pObj, i )
        pObj->iData = Counter++;
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        pObj->iData = Counter++;
    nDigits = Abc_Base10Log( Counter );
    // write the file 
    pFile = fopen( pFileName, "w" );
    fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
//    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
    fprintf( pFile, ".model %s\n", p->pName );
    // write PIs
    fprintf( pFile, ".inputs" );
    Aig_ManForEachPiSeq( p, pObj, i )
        if ( vPiNames )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, i) );
        else
            fprintf( pFile, " n%0*d", nDigits, pObj->iData );
    fprintf( pFile, "\n" );
    // write POs
    fprintf( pFile, ".outputs" );
    Aig_ManForEachPoSeq( p, pObj, i )
        if ( vPoNames )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, i) );
        else
            fprintf( pFile, " n%0*d", nDigits, pObj->iData );
    fprintf( pFile, "\n" );
    // write latches
    if ( Aig_ManRegNum(p) )
    {
        fprintf( pFile, "\n" );
        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
        {
            fprintf( pFile, ".latch" );
            if ( vPoNames )
                fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, Aig_ManCoNum(p)-Aig_ManRegNum(p)+i) );
            else
                fprintf( pFile, " n%0*d", nDigits, pObjLi->iData );
            if ( vPiNames )
                fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ManCiNum(p)-Aig_ManRegNum(p)+i) );
            else
                fprintf( pFile, " n%0*d", nDigits, pObjLo->iData );
            fprintf( pFile, " 0\n" );
        }
        fprintf( pFile, "\n" );
    } 
    // write nodes
    if ( pConst1 )
        fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
    Aig_ManSetCioIds( p );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        fprintf( pFile, ".names" );
        if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
        else
            fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
        if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin1(pObj)) )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin1(pObj))) );
        else
            fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData );
        fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
        fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
    }
    // write POs
    Aig_ManForEachCo( p, pObj, i )
    {
        fprintf( pFile, ".names" );
        if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) )
            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) );
        else
            fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData );
        if ( vPoNames )
            fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjCioId(pObj)) );
        else
            fprintf( pFile, " n%0*d\n", nDigits, pObj->iData );
        fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
    }
    Aig_ManCleanCioIds( p );
    fprintf( pFile, ".end\n\n" );
    fclose( pFile );
    Vec_PtrFree( vNodes );
}

void Aig_ManDumpVerilog	(	Aig_Man_t *	p,
		char *	pFileName
	)

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

Synopsis [Writes the AIG into a Verilog file.]

Description []

SideEffects []

SeeAlso []

Definition at line 848 of file aigUtil.c.

{
    FILE * pFile;
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
    int i, nDigits, Counter = 0;
    if ( Aig_ManCoNum(p) == 0 )
    {
        printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
        return;
    }
    // check if constant is used
    Aig_ManForEachCo( p, pObj, i )
        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
            pConst1 = Aig_ManConst1(p);
    // collect nodes in the DFS order
    vNodes = Aig_ManDfs( p, 1 );
    // assign IDs to objects
    Aig_ManConst1(p)->iData = Counter++;
    Aig_ManForEachCi( p, pObj, i )
        pObj->iData = Counter++;
    Aig_ManForEachCo( p, pObj, i )
        pObj->iData = Counter++;
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        pObj->iData = Counter++;
    nDigits = Abc_Base10Log( Counter );
    // write the file
    pFile = fopen( pFileName, "w" );
    fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog()\n" );
//    fprintf( pFile, "// http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
    if ( Aig_ManRegNum(p) )
        fprintf( pFile, "module %s ( clock", p->pName? p->pName: "test" );
    else
        fprintf( pFile, "module %s (", p->pName? p->pName: "test" );
    Aig_ManForEachPiSeq( p, pObj, i )
        fprintf( pFile, "%s n%0*d", ((Aig_ManRegNum(p) || i)? ",":""), nDigits, pObj->iData );
    Aig_ManForEachPoSeq( p, pObj, i )
        fprintf( pFile, ", n%0*d", nDigits, pObj->iData );
    fprintf( pFile, " );\n" );

    // write PIs
    if ( Aig_ManRegNum(p) )
        fprintf( pFile, "input clock;\n" );
    Aig_ManForEachPiSeq( p, pObj, i )
        fprintf( pFile, "input n%0*d;\n", nDigits, pObj->iData );
    // write POs
    Aig_ManForEachPoSeq( p, pObj, i )
        fprintf( pFile, "output n%0*d;\n", nDigits, pObj->iData );
    // write latches
    if ( Aig_ManRegNum(p) )
    {
    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
        fprintf( pFile, "reg n%0*d;\n", nDigits, pObjLo->iData );
    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
        fprintf( pFile, "wire n%0*d;\n", nDigits, pObjLi->iData );
    }
    // write nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        fprintf( pFile, "wire n%0*d;\n", nDigits, pObj->iData );
    if ( pConst1 )
        fprintf( pFile, "wire n%0*d;\n", nDigits, pConst1->iData );
    // write nodes
    if ( pConst1 )
        fprintf( pFile, "assign n%0*d = 1\'b1;\n", nDigits, pConst1->iData );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        fprintf( pFile, "assign n%0*d = %sn%0*d & %sn%0*d;\n", 
            nDigits, pObj->iData,
            !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData, 
            !Aig_ObjFaninC1(pObj) ? " " : "~", nDigits, Aig_ObjFanin1(pObj)->iData
            );
    }
    // write POs
    Aig_ManForEachPoSeq( p, pObj, i )
    {
        fprintf( pFile, "assign n%0*d = %sn%0*d;\n", 
            nDigits, pObj->iData,
            !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData );
    }
    if ( Aig_ManRegNum(p) )
    {
        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
        {
            fprintf( pFile, "assign n%0*d = %sn%0*d;\n", 
                nDigits, pObjLi->iData,
                !Aig_ObjFaninC0(pObjLi) ? " " : "~", nDigits, Aig_ObjFanin0(pObjLi)->iData );
        }
    }

    // write initial state
    if ( Aig_ManRegNum(p) )
    {
        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
            fprintf( pFile, "always @ (posedge clock) begin n%0*d <= n%0*d; end\n", 
                 nDigits, pObjLo->iData,
                 nDigits, pObjLi->iData );
        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
            fprintf( pFile, "initial begin n%0*d <= 1\'b0; end\n", 
                 nDigits, pObjLo->iData );
    }

    fprintf( pFile, "endmodule\n\n" );
    fclose( pFile );
    Vec_PtrFree( vNodes );
}

int Aig_ManHasNoGaps

(

Aig_Man_t *

p

)

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

Synopsis [Make sure AIG has not gaps in the numeric order.]

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file aigUtil.c.

{
    return (int)(Aig_ManObjNum(p) == Aig_ManCiNum(p) + Aig_ManCoNum(p) + Aig_ManNodeNum(p) + 1);
}

ABC_NAMESPACE_IMPL_START void Aig_ManIncrementTravId

(

Aig_Man_t *

p

)

DECLARATIONS ///.

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

FileName [aigUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [Various procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:

aigUtil.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file aigUtil.c.

{
    if ( p->nTravIds >= (1<<30)-1 )
        Aig_ManCleanData( p );
    p->nTravIds++;
}

void Aig_ManInvertConstraints

(

Aig_Man_t *

pAig

)

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

Synopsis [Complements the constraint outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1543 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    if ( Aig_ManConstrNum(pAig) == 0 )
        return;
    Saig_ManForEachPo( pAig, pObj, i )
    {
        if ( i >= Saig_ManPoNum(pAig) - Aig_ManConstrNum(pAig) )
            Aig_ObjChild0Flip( pObj );
    }
}

int Aig_ManLevels

(

Aig_Man_t *

p

)

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

Synopsis [Collect the latches.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i, LevelMax = 0;
    Aig_ManForEachCo( p, pObj, i )
        LevelMax = Abc_MaxInt( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
    return LevelMax;
}

Vec_Ptr_t* Aig_ManMuxesCollect

(

Aig_Man_t *

pAig

)

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

Synopsis [Collects muxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1460 of file aigUtil.c.

{
    Vec_Ptr_t * vMuxes;
    Aig_Obj_t * pObj;
    int i;
    vMuxes = Vec_PtrAlloc( 100 );
    Aig_ManForEachNode( pAig, pObj, i )
        if ( Aig_ObjIsMuxType(pObj) )
            Vec_PtrPush( vMuxes, pObj );
    return vMuxes;
}

void Aig_ManMuxesDeref	(	Aig_Man_t *	pAig,
		Vec_Ptr_t *	vMuxes
	)

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

Synopsis [Dereferences muxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1483 of file aigUtil.c.

{
    Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC;
    int i;
    Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i )
    {
        if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) )
        {
            pNodeT->nRefs--;
            pNodeE->nRefs--;
        }
        else
        {
            pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE );
            pNodeC->nRefs--;
        }
    }
}

void Aig_ManMuxesRef	(	Aig_Man_t *	pAig,
		Vec_Ptr_t *	vMuxes
	)

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

Synopsis [References muxes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1513 of file aigUtil.c.

{
    Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC;
    int i;
    Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i )
    {
        if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) )
        {
            pNodeT->nRefs++;
            pNodeE->nRefs++;
        }
        else
        {
            pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE );
            pNodeC->nRefs++;
        }
    }
}

void Aig_ManPrintControlFanouts

(

Aig_Man_t *

p

)

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

Synopsis [Prints the fanouts of the control register.]

Description [Useful only for Intel MC benchmarks.]

SideEffects []

SeeAlso []

Definition at line 1027 of file aigUtil.c.

{
    Aig_Obj_t * pObj, * pFanin0, * pFanin1, * pCtrl;
    int i;

    pCtrl = Aig_ManCi( p, Aig_ManCiNum(p) - 1 );

    printf( "Control signal:\n" );
    Aig_ObjPrint( p, pCtrl ); printf( "\n\n" );

    Aig_ManForEachObj( p, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) )
            continue;
        assert( pObj != pCtrl );
        pFanin0 = Aig_ObjFanin0(pObj);
        pFanin1 = Aig_ObjFanin1(pObj);
        if ( pFanin0 == pCtrl && Aig_ObjIsCi(pFanin1) )
        {
            Aig_ObjPrint( p, pObj ); printf( "\n" );
            Aig_ObjPrint( p, pFanin1 ); printf( "\n" );
            printf( "\n" );
        }
        if ( pFanin1 == pCtrl && Aig_ObjIsCi(pFanin0) )
        {
            Aig_ObjPrint( p, pObj ); printf( "\n" );
            Aig_ObjPrint( p, pFanin0 ); printf( "\n" );
            printf( "\n" );
        }
    }
}

void Aig_ManPrintVerbose	(	Aig_Man_t *	p,
		int	fHaig
	)

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

Synopsis [Prints node in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 685 of file aigUtil.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj;
    int i;
    printf( "PIs: " );
    Aig_ManForEachCi( p, pObj, i )
        printf( " %p", pObj );
    printf( "\n" );
    vNodes = Aig_ManDfs( p, 0 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
    printf( "\n" );
    Vec_PtrFree( vNodes );
}

unsigned Aig_ManRandom

(

int

fReset

)

GLOBAL VARIABLES ///.

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

Synopsis [Creates a sequence of random numbers.]

Description []

SideEffects []

SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]

Definition at line 1157 of file aigUtil.c.

{
    static unsigned int m_z = NUMBER1;
    static unsigned int m_w = NUMBER2;
    if ( fReset )
    {
        m_z = NUMBER1;
        m_w = NUMBER2;
    }
    m_z = 36969 * (m_z & 65535) + (m_z >> 16);
    m_w = 18000 * (m_w & 65535) + (m_w >> 16);
    return (m_z << 16) + m_w;
}

word Aig_ManRandom64

(

int

fReset

)

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

Synopsis [Creates a sequence of random numbers.]

Description []

SideEffects []

SeeAlso []

Definition at line 1182 of file aigUtil.c.

{
    word Res = (word)Aig_ManRandom(fReset);
    return Res | ((word)Aig_ManRandom(0) << 32);
}

void Aig_ManRandomInfo	(	Vec_Ptr_t *	vInfo,
		int	iInputStart,
		int	iWordStart,
		int	iWordStop
	)

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

Synopsis [Creates random info for the primary inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1200 of file aigUtil.c.

{
    unsigned * pInfo;
    int i, w;
    Vec_PtrForEachEntryStart( unsigned *, vInfo, pInfo, i, iInputStart )
        for ( w = iWordStart; w < iWordStop; w++ )
            pInfo[w] = Aig_ManRandom(0);
}

void Aig_ManRandomTest1

(

)

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

Synopsis [Creates a sequence of random numbers.]

Description []

SideEffects []

SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]

Definition at line 1124 of file aigUtil.c.

{
    FILE * pFile;
    unsigned int lfsr;
    unsigned int period = 0; 
    pFile = fopen( "rand.txt", "w" );
    do {
        lfsr = Aig_ManRandom( 0 );
        ++period;
        fprintf( pFile, "%10d : %10d ", period, lfsr );
//        Extra_PrintBinary( pFile, &lfsr, 32 );
        fprintf( pFile, "\n" );
        if ( period == 20000 )
            break;
    } while(lfsr != 1u);
    fclose( pFile );
}

void Aig_ManRandomTest2

(

)

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

Synopsis [Creates a sequence of random numbers.]

Description []

SideEffects []

SeeAlso [http://en.wikipedia.org/wiki/LFSR]

Definition at line 1094 of file aigUtil.c.

{
    FILE * pFile;
    unsigned int lfsr = 1;
    unsigned int period = 0; 
    pFile = fopen( "rand.txt", "w" );
    do {
//        lfsr = (lfsr >> 1) ^ (-(lfsr & 1u) & 0xd0000001u); // taps 32 31 29 1 
        lfsr = 1; // to prevent the warning
        ++period;
        fprintf( pFile, "%10d : %10d ", period, lfsr );
//        Extra_PrintBinary( pFile, &lfsr, 32 );
        fprintf( pFile, "\n" );
        if ( period == 20000 )
            break;
    } while(lfsr != 1u);
    fclose( pFile );
}

void Aig_ManResetRefs

(

Aig_Man_t *

p

)

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

Synopsis [Reset reference counters.]

Description []

SideEffects []

SeeAlso []

Definition at line 122 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachObj( p, pObj, i )
        pObj->nRefs = 0;
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( Aig_ObjFanin0(pObj) )
            Aig_ObjFanin0(pObj)->nRefs++;
        if ( Aig_ObjFanin1(pObj) )
            Aig_ObjFanin1(pObj)->nRefs++;
    }
}

void Aig_ManSetCioIds

(

Aig_Man_t *

p

)

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

Synopsis [Sets the PI/PO numbers.]

Description []

SideEffects []

SeeAlso []

Definition at line 965 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachCi( p, pObj, i )
        pObj->CioId = i;
    Aig_ManForEachCo( p, pObj, i )
        pObj->CioId = i;
}

void Aig_ManSetPhase

(

Aig_Man_t *

pAig

)

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

Synopsis [Handle the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 1431 of file aigUtil.c.

{
    Aig_Obj_t * pObj;
    int i;
    // set the PI simulation information
    Aig_ManConst1( pAig )->fPhase = 1;
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->fPhase = 0;
    // simulate internal nodes
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
                     & ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) );
    // simulate PO nodes
    Aig_ManForEachCo( pAig, pObj, i )
        pObj->fPhase = Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj);
}

void Aig_NodeIntersectLists	(	Vec_Ptr_t *	vArr1,
		Vec_Ptr_t *	vArr2,
		Vec_Ptr_t *	vArr
	)

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

Synopsis [Returns the result of intersecting the two vectors.]

Description [Assumes that the vectors are sorted in the increasing order.]

SideEffects []

SeeAlso []

Definition at line 1259 of file aigUtil.c.

{
    Aig_Obj_t ** pBeg  = (Aig_Obj_t **)vArr->pArray;
    Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
    Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
    Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
    Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
    Vec_PtrGrow( vArr, Abc_MaxInt( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
    pBeg  = (Aig_Obj_t **)vArr->pArray;
    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
    {
        if ( (*pBeg1)->Id == (*pBeg2)->Id )
            *pBeg++ = *pBeg1++, pBeg2++;
        else if ( (*pBeg1)->Id < (*pBeg2)->Id )
//            *pBeg++ = *pBeg1++;
            pBeg1++;
        else 
//            *pBeg++ = *pBeg2++;
            pBeg2++;
    }
//    while ( pBeg1 < pEnd1 )
//        *pBeg++ = *pBeg1++;
//    while ( pBeg2 < pEnd2 )
//        *pBeg++ = *pBeg2++;
    vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
    assert( vArr->nSize <= vArr->nCap );
    assert( vArr->nSize <= vArr1->nSize );
    assert( vArr->nSize <= vArr2->nSize );
}

void Aig_NodeUnionLists	(	Vec_Ptr_t *	vArr1,
		Vec_Ptr_t *	vArr2,
		Vec_Ptr_t *	vArr
	)

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

Synopsis [Returns the result of merging the two vectors.]

Description [Assumes that the vectors are sorted in the increasing order.]

SideEffects []

SeeAlso []

Definition at line 1220 of file aigUtil.c.

{
    Aig_Obj_t ** pBeg  = (Aig_Obj_t **)vArr->pArray;
    Aig_Obj_t ** pBeg1 = (Aig_Obj_t **)vArr1->pArray;
    Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
    Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
    Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
    Vec_PtrGrow( vArr, Vec_PtrSize(vArr1) + Vec_PtrSize(vArr2) );
    pBeg  = (Aig_Obj_t **)vArr->pArray;
    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
    {
        if ( (*pBeg1)->Id == (*pBeg2)->Id )
            *pBeg++ = *pBeg1++, pBeg2++;
        else if ( (*pBeg1)->Id < (*pBeg2)->Id )
            *pBeg++ = *pBeg1++;
        else 
            *pBeg++ = *pBeg2++;
    }
    while ( pBeg1 < pEnd1 )
        *pBeg++ = *pBeg1++;
    while ( pBeg2 < pEnd2 )
        *pBeg++ = *pBeg2++;
    vArr->nSize = pBeg - (Aig_Obj_t **)vArr->pArray;
    assert( vArr->nSize <= vArr->nCap );
    assert( vArr->nSize >= vArr1->nSize );
    assert( vArr->nSize >= vArr2->nSize );
}

void Aig_ObjCleanData_rec

(

Aig_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 243 of file aigUtil.c.

{
    assert( !Aig_IsComplement(pObj) );
    assert( !Aig_ObjIsCo(pObj) );
    if ( Aig_ObjIsAnd(pObj) )
    {
        Aig_ObjCleanData_rec( Aig_ObjFanin0(pObj) );
        Aig_ObjCleanData_rec( Aig_ObjFanin1(pObj) );
    }
    pObj->pData = NULL;
}

void Aig_ObjCollectMulti	(	Aig_Obj_t *	pRoot,
		Vec_Ptr_t *	vSuper
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 289 of file aigUtil.c.

{
    assert( !Aig_IsComplement(pRoot) );
    Vec_PtrClear( vSuper );
    Aig_ObjCollectMulti_rec( pRoot, pRoot, vSuper );
}

void Aig_ObjCollectMulti_rec	(	Aig_Obj_t *	pRoot,
		Aig_Obj_t *	pObj,
		Vec_Ptr_t *	vSuper
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 267 of file aigUtil.c.

{
    if ( pRoot != pObj && (Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || Aig_ObjType(pRoot) != Aig_ObjType(pObj)) )
    {
        Vec_PtrPushUnique(vSuper, pObj);
        return;
    }
    Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
    Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
}

int Aig_ObjCompareIdIncrease	(	Aig_Obj_t **	pp1,
		Aig_Obj_t **	pp2
	)

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

Synopsis [Procedure used for sorting the nodes in increasing order of IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 496 of file aigUtil.c.

{
    int Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2);
    if ( Diff < 0 )
        return -1;
    if ( Diff > 0 ) 
        return 1;
    return 0; 
}

int Aig_ObjIsMuxType

(

Aig_Obj_t *

pNode

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file aigUtil.c.

{
    Aig_Obj_t * pNode0, * pNode1;
    // check that the node is regular
    assert( !Aig_IsComplement(pNode) );
    // if the node is not AND, this is not MUX
    if ( !Aig_ObjIsAnd(pNode) )
        return 0;
    // if the children are not complemented, this is not MUX
    if ( !Aig_ObjFaninC0(pNode) || !Aig_ObjFaninC1(pNode) )
        return 0;
    // get children
    pNode0 = Aig_ObjFanin0(pNode);
    pNode1 = Aig_ObjFanin1(pNode);
    // if the children are not ANDs, this is not MUX
    if ( !Aig_ObjIsAnd(pNode0) || !Aig_ObjIsAnd(pNode1) )
        return 0;
    // otherwise the node is MUX iff it has a pair of equal grandchildren
    return (Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1))) || 
           (Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1))) ||
           (Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1))) ||
           (Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)));
}

void Aig_ObjPrintEqn	(	FILE *	pFile,
		Aig_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 519 of file aigUtil.c.

{
    Vec_Ptr_t * vSuper;
    Aig_Obj_t * pFanin;
    int fCompl, i;
    // store the complemented attribute
    fCompl = Aig_IsComplement(pObj);
    pObj = Aig_Regular(pObj);
    // constant case
    if ( Aig_ObjIsConst1(pObj) )
    {
        fprintf( pFile, "%d", !fCompl );
        return;
    }
    // PI case
    if ( Aig_ObjIsCi(pObj) )
    {
        fprintf( pFile, "%s%s", fCompl? "!" : "", (char*)pObj->pData );
        return;
    }
    // AND case
    Vec_VecExpand( vLevels, Level );
    vSuper = Vec_VecEntry(vLevels, Level);
    Aig_ObjCollectMulti( pObj, vSuper );
    fprintf( pFile, "%s", (Level==0? "" : "(") );
    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
    {
        Aig_ObjPrintEqn( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
        if ( i < Vec_PtrSize(vSuper) - 1 )
            fprintf( pFile, " %s ", fCompl? "+" : "*" );
    }
    fprintf( pFile, "%s", (Level==0? "" : ")") );
    return;
}

void Aig_ObjPrintVerbose	(	Aig_Obj_t *	pObj,
		int	fHaig
	)

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

Synopsis [Prints node in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 653 of file aigUtil.c.

{
    assert( !Aig_IsComplement(pObj) );
    printf( "Node %p : ", pObj );
    if ( Aig_ObjIsConst1(pObj) )
        printf( "constant 1" );
    else if ( Aig_ObjIsCi(pObj) )
        printf( "PI" );
    else if ( Aig_ObjIsCo(pObj) )
    {
        printf( "PO" );
        printf( "%p%s", 
            Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " ") );
    }
    else
        printf( "AND( %p%s, %p%s )", 
            Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " "), 
            Aig_ObjFanin1(pObj), (Aig_ObjFaninC1(pObj)? "\'" : " ") );
    printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
}

void Aig_ObjPrintVerilog	(	FILE *	pFile,
		Aig_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 566 of file aigUtil.c.

{
    Vec_Ptr_t * vSuper;
    Aig_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
    int fCompl, i;
    // store the complemented attribute
    fCompl = Aig_IsComplement(pObj);
    pObj = Aig_Regular(pObj);
    // constant case
    if ( Aig_ObjIsConst1(pObj) )
    {
        fprintf( pFile, "1\'b%d", !fCompl );
        return;
    }
    // PI case
    if ( Aig_ObjIsCi(pObj) )
    {
        fprintf( pFile, "%s%s", fCompl? "~" : "", (char*)pObj->pData );
        return;
    }
    // EXOR case
    if ( Aig_ObjIsExor(pObj) )
    {
        Vec_VecExpand( vLevels, Level );
        vSuper = Vec_VecEntry( vLevels, Level );
        Aig_ObjCollectMulti( pObj, vSuper );
        fprintf( pFile, "%s", (Level==0? "" : "(") );
        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
        {
            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
            if ( i < Vec_PtrSize(vSuper) - 1 )
                fprintf( pFile, " ^ " );
        }
        fprintf( pFile, "%s", (Level==0? "" : ")") );
        return;
    }
    // MUX case
    if ( Aig_ObjIsMuxType(pObj) )
    {
        if ( Aig_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
        {
            fprintf( pFile, "%s", (Level==0? "" : "(") );
            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
            fprintf( pFile, " ^ " );
            Aig_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
            fprintf( pFile, "%s", (Level==0? "" : ")") );
        }
        else 
        {
            pFaninC = Aig_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
            fprintf( pFile, "%s", (Level==0? "" : "(") );
            Aig_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
            fprintf( pFile, " ? " );
            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin1, fCompl), vLevels, Level+1 );
            fprintf( pFile, " : " );
            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
            fprintf( pFile, "%s", (Level==0? "" : ")") );
        }
        return;
    }
    // AND case
    Vec_VecExpand( vLevels, Level );
    vSuper = Vec_VecEntry(vLevels, Level);
    Aig_ObjCollectMulti( pObj, vSuper );
    fprintf( pFile, "%s", (Level==0? "" : "(") );
    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
    {
        Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
        if ( i < Vec_PtrSize(vSuper) - 1 )
            fprintf( pFile, " %s ", fCompl? "|" : "&" );
    }
    fprintf( pFile, "%s", (Level==0? "" : ")") );
    return;
}

Aig_Obj_t* Aig_ObjReal_rec

(

Aig_Obj_t *

pObj

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 476 of file aigUtil.c.

{
    Aig_Obj_t * pObjNew, * pObjR = Aig_Regular(pObj);
    if ( !Aig_ObjIsBuf(pObjR) )
        return pObj;
    pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObjR) );
    return Aig_NotCond( pObjNew, Aig_IsComplement(pObj) );
}

int Aig_ObjRecognizeExor	(	Aig_Obj_t *	pObj,
		Aig_Obj_t **	ppFan0,
		Aig_Obj_t **	ppFan1
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 343 of file aigUtil.c.

{
    Aig_Obj_t * p0, * p1;
    assert( !Aig_IsComplement(pObj) );
    if ( !Aig_ObjIsNode(pObj) )
        return 0;
    if ( Aig_ObjIsExor(pObj) )
    {
        *ppFan0 = Aig_ObjChild0(pObj);
        *ppFan1 = Aig_ObjChild1(pObj);
        return 1;
    }
    assert( Aig_ObjIsAnd(pObj) );
    p0 = Aig_ObjChild0(pObj);
    p1 = Aig_ObjChild1(pObj);
    if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
        return 0;
    p0 = Aig_Regular(p0);
    p1 = Aig_Regular(p1);
    if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
        return 0;
    if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
        return 0;
    if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
        return 0;
    *ppFan0 = Aig_ObjChild0(p0);
    *ppFan1 = Aig_ObjChild1(p0);
    return 1;
}

Aig_Obj_t* Aig_ObjRecognizeMux	(	Aig_Obj_t *	pNode,
		Aig_Obj_t **	ppNodeT,
		Aig_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 387 of file aigUtil.c.

{
    Aig_Obj_t * pNode0, * pNode1;
    assert( !Aig_IsComplement(pNode) );
    assert( Aig_ObjIsMuxType(pNode) );
    // get children
    pNode0 = Aig_ObjFanin0(pNode);
    pNode1 = Aig_ObjFanin1(pNode);

    // find the control variable
    if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
    {
//        if ( Fraig_IsComplement(pNode1->p2) )
        if ( Aig_ObjFaninC1(pNode0) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
            *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
            return Aig_ObjChild1(pNode1);//pNode2->p2;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
            *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
            return Aig_ObjChild1(pNode0);//pNode1->p2;
        }
    }
    else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
    {
//        if ( Fraig_IsComplement(pNode1->p1) )
        if ( Aig_ObjFaninC0(pNode0) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
            *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
            return Aig_ObjChild0(pNode1);//pNode2->p1;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
            *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
            return Aig_ObjChild0(pNode0);//pNode1->p1;
        }
    }
    else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
    {
//        if ( Fraig_IsComplement(pNode1->p1) )
        if ( Aig_ObjFaninC0(pNode0) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
            *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
            return Aig_ObjChild1(pNode1);//pNode2->p2;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
            *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
            return Aig_ObjChild0(pNode0);//pNode1->p1;
        }
    }
    else if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
    {
//        if ( Fraig_IsComplement(pNode1->p2) )
        if ( Aig_ObjFaninC1(pNode0) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
            *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
            return Aig_ObjChild0(pNode1);//pNode2->p1;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
            *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
            return Aig_ObjChild1(pNode0);//pNode1->p2;
        }
    }
    assert( 0 ); // this is not MUX
    return NULL;
}

char* Aig_TimeStamp

(

)

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

Synopsis [Returns the time stamp.]

Description [The file should be closed.]

SideEffects []

SeeAlso []

Definition at line 62 of file aigUtil.c.

{
    static char Buffer[100];
    char * TimeStamp;
    time_t ltime;
    // get the current time
    time( &ltime );
    TimeStamp = asctime( localtime( &ltime ) );
    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
    strcpy( Buffer, TimeStamp );
    return Buffer;
}