dchChoice.c File Reference

#include "dchInt.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START int	Dch_ObjCountSupp_rec (Aig_Man_t *p, Aig_Obj_t *pObj)
	DECLARATIONS ///. More...
int	Dch_ObjCountSupp (Aig_Man_t *p, Aig_Obj_t *pObj)
int	Dch_DeriveChoiceCountReprs (Aig_Man_t *pAig)
	FUNCTION DECLARATIONS ///. More...
int	Dch_DeriveChoiceCountEquivs (Aig_Man_t *pAig)
int	Dch_ObjMarkTfi_rec (Aig_Man_t *p, Aig_Obj_t *pObj)
int	Dch_ObjCheckSuppRed (Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
void	Aig_ManCheckReprs (Aig_Man_t *p)
void	Dch_CheckChoices (Aig_Man_t *p, int fSkipRedSupps)
int	Aig_ManCheckAcyclic_rec (Aig_Man_t *p, Aig_Obj_t *pNode, int fVerbose)
int	Aig_ManCheckAcyclic (Aig_Man_t *p, int fVerbose)
int	Dch_ObjCheckTfi_rec (Aig_Man_t *p, Aig_Obj_t *pObj)
int	Dch_ObjCheckTfi (Aig_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
static Aig_Obj_t *	Aig_ObjGetRepr (Aig_Man_t *p, Aig_Obj_t *pObj)
static Aig_Obj_t *	Aig_ObjChild0CopyRepr (Aig_Man_t *p, Aig_Obj_t *pObj)
static Aig_Obj_t *	Aig_ObjChild1CopyRepr (Aig_Man_t *p, Aig_Obj_t *pObj)
void	Dch_DeriveChoiceAigNode (Aig_Man_t *pAigNew, Aig_Man_t *pAigOld, Aig_Obj_t *pObj, int fSkipRedSupps)
Aig_Man_t *	Dch_DeriveChoiceAigInt (Aig_Man_t *pAig, int fSkipRedSupps)
Aig_Man_t *	Dch_DeriveChoiceAig (Aig_Man_t *pAig, int fSkipRedSupps)

Function Documentation

int Aig_ManCheckAcyclic	(	Aig_Man_t *	p,
		int	fVerbose
	)

Definition at line 331 of file dchChoice.c.

{
    Aig_Obj_t * pNode;
    int fAcyclic;
    int i;
    // set the traversal ID for this DFS ordering
    Aig_ManIncrementTravId( p );   
    Aig_ManIncrementTravId( p );   
    // pNode->TravId == pNet->nTravIds      means "pNode is on the path"
    // pNode->TravId == pNet->nTravIds - 1  means "pNode is visited but is not on the path"
    // pNode->TravId <  pNet->nTravIds - 1  means "pNode is not visited"
    // traverse the network to detect cycles
    fAcyclic = 1;
    Aig_ManForEachCo( p, pNode, i )
    {
        pNode = Aig_ObjFanin0(pNode);
        if ( Aig_ObjIsTravIdPrevious(p, pNode) )
            continue;
        // traverse the output logic cone
        if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pNode, fVerbose)) )
            continue;
        // stop as soon as the first loop is detected
        if ( fVerbose )
        Abc_Print( 1, " CO %d\n", i );
        break;
    }
    return fAcyclic;
}

int Aig_ManCheckAcyclic_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pNode,
		int	fVerbose
	)

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

Synopsis [Checks for combinational loops in the AIG.]

Description [Returns 1 if combinational loop is detected.]

SideEffects []

SeeAlso []

Definition at line 257 of file dchChoice.c.

{
    Aig_Obj_t * pFanin;
    int fAcyclic;
    if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) )
        return 1;
    assert( Aig_ObjIsNode(pNode) );
    // make sure the node is not visited
    assert( !Aig_ObjIsTravIdPrevious(p, pNode) );
    // check if the node is part of the combinational loop
    if ( Aig_ObjIsTravIdCurrent(p, pNode) )
    {
        if ( fVerbose )
            Abc_Print( 1, "Network \"%s\" contains combinational loop!\n", p->pSpec? p->pSpec : NULL );
        if ( fVerbose )
        Abc_Print( 1, "Node \"%d\" is encountered twice on the following path to the COs:\n", Aig_ObjId(pNode) );
        return 0;
    }
    // mark this node as a node on the current path
    Aig_ObjSetTravIdCurrent( p, pNode );

    // visit the transitive fanin
    pFanin = Aig_ObjFanin0(pNode);
    // check if the fanin is visited
    if ( !Aig_ObjIsTravIdPrevious(p, pFanin) ) 
    {
        // traverse the fanin's cone searching for the loop
        if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
        {
            // return as soon as the loop is detected
            if ( fVerbose )
            Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) );
            return 0;
        }
    }

    // visit the transitive fanin
    pFanin = Aig_ObjFanin1(pNode);
    // check if the fanin is visited
    if ( !Aig_ObjIsTravIdPrevious(p, pFanin) ) 
    {
        // traverse the fanin's cone searching for the loop
        if ( !(fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
        {
            // return as soon as the loop is detected
            if ( fVerbose )
            Abc_Print( 1, " %d ->", Aig_ObjId(pFanin) );
            return 0;
        }
    }

    // visit choices
    if ( Aig_ObjRepr(p, pNode) == NULL && Aig_ObjEquiv(p, pNode) != NULL )
    {
        for ( pFanin = Aig_ObjEquiv(p, pNode); pFanin; pFanin = Aig_ObjEquiv(p, pFanin) )
        {
            // check if the fanin is visited
            if ( Aig_ObjIsTravIdPrevious(p, pFanin) ) 
                continue;
            // traverse the fanin's cone searching for the loop
            if ( (fAcyclic = Aig_ManCheckAcyclic_rec(p, pFanin, fVerbose)) )
                continue;
            // return as soon as the loop is detected
            if ( fVerbose )
            Abc_Print( 1, " %d", Aig_ObjId(pFanin) );
            if ( fVerbose )
            Abc_Print( 1, " (choice of %d) -> ", Aig_ObjId(pNode) );
            return 0;
        }
    }
    // mark this node as a visited node
    Aig_ObjSetTravIdPrevious( p, pNode );
    return 1;
}

void Aig_ManCheckReprs

(

Aig_Man_t *

p

)

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

Synopsis [Make sure reprsentative nodes do not have representatives.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file dchChoice.c.

{
    int fPrintConst = 0;
    Aig_Obj_t * pObj;
    int i, fProb = 0;
    int Class0 = 0, ClassCi = 0;
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( Aig_ObjRepr(p, pObj) == NULL )
            continue;
        if ( !Aig_ObjIsNode(pObj) )
            printf( "Obj %d is not an AND but it has a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)) ), fProb = 1;
        else if ( Aig_ObjRepr(p, Aig_ObjRepr(p, pObj)) )
            printf( "Obj %d has repr %d with a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)), Aig_ObjId(Aig_ObjRepr(p, Aig_ObjRepr(p, pObj))) ), fProb = 1;
    }
    if ( !fProb )
        printf( "Representive verification successful.\n" );
    else
        printf( "Representive verification FAILED.\n" );
    if ( !fPrintConst )
        return;
    // count how many representatives are const0 or a CI
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( Aig_ObjRepr(p, pObj) == Aig_ManConst1(p) )
            Class0++;
        if ( Aig_ObjRepr(p, pObj) && Aig_ObjIsCi(Aig_ObjRepr(p, pObj)) )
            ClassCi++;
    }
    printf( "Const0 nodes = %d.  ConstCI nodes = %d.\n", Class0, ClassCi );
}

static Aig_Obj_t* Aig_ObjChild0CopyRepr ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 429 of file dchChoice.c.

{ return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }

static Aig_Obj_t* Aig_ObjChild1CopyRepr ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 430 of file dchChoice.c.

{ return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }

static Aig_Obj_t* Aig_ObjGetRepr ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

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

Synopsis [Returns representatives of fanin in approapriate polarity.]

Description []

SideEffects []

SeeAlso []

Definition at line 422 of file dchChoice.c.

{
    Aig_Obj_t * pRepr;
    if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) )
        return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) );
    return pObj;
}

void Dch_CheckChoices	(	Aig_Man_t *	p,
		int	fSkipRedSupps
	)

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

Synopsis [Verify correctness of choices.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file dchChoice.c.

{
    Aig_Obj_t * pObj;
    int i, fProb = 0;
    Aig_ManCleanMarkA( p );
    Aig_ManForEachNode( p, pObj, i )
    {
        if ( p->pEquivs[i] != NULL )
        {
            if ( pObj->fMarkA == 1 )
                printf( "node %d participates in more than one choice class\n", i ), fProb = 1;
            pObj->fMarkA = 1;
            // check redundancy
            if ( fSkipRedSupps && Dch_ObjCheckSuppRed( p, pObj, p->pEquivs[i]) )
                printf( "node %d and repr %d have diff supports\n", pObj->Id, p->pEquivs[i]->Id );
            // consider the next one
            pObj = p->pEquivs[i];
            if ( p->pEquivs[Aig_ObjId(pObj)] == NULL )
            {
                if ( pObj->fMarkA == 1 )
                    printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1;
                pObj->fMarkA = 1;
            }
            // consider the non-head ones
            if ( pObj->nRefs > 0 )
                printf( "node %d belonging to choice has fanout %d\n", pObj->Id, pObj->nRefs );
        }
        if ( p->pReprs && p->pReprs[i] != NULL )
        {
            if ( pObj->nRefs > 0 )
                printf( "node %d has representative %d and fanout count %d\n", pObj->Id, p->pReprs[i]->Id, pObj->nRefs ), fProb = 1;
        }
    }
    Aig_ManCleanMarkA( p );
    if ( !fProb )
        printf( "Verification of choice AIG succeeded.\n" );
    else
        printf( "Verification of choice AIG FAILED.\n" );
}

Aig_Man_t* Dch_DeriveChoiceAig	(	Aig_Man_t *	pAig,
		int	fSkipRedSupps
	)

Definition at line 517 of file dchChoice.c.

{
    int fCheck = 0;
    Aig_Man_t * pChoices, * pTemp;
    // verify
    if ( fCheck )
        Aig_ManCheckReprs( pAig ); 
    // compute choices
    pChoices = Dch_DeriveChoiceAigInt( pAig, fSkipRedSupps );
    ABC_FREE( pChoices->pReprs );
    // verify
    if ( fCheck )
        Dch_CheckChoices( pChoices, fSkipRedSupps ); 
    // find correct topo order with choices
    pChoices = Aig_ManDupDfs( pTemp = pChoices );
    Aig_ManStop( pTemp );
    // verify
    if ( fCheck )
        Dch_CheckChoices( pChoices, fSkipRedSupps ); 
    return pChoices;
}

Aig_Man_t* Dch_DeriveChoiceAigInt	(	Aig_Man_t *	pAig,
		int	fSkipRedSupps
	)

Definition at line 494 of file dchChoice.c.

{
    Aig_Man_t * pChoices;
    Aig_Obj_t * pObj;
    int i;
    // start recording equivalences
    pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
    pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    pChoices->pReprs  = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    // map constants and PIs
    Aig_ManCleanData( pAig );
    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pChoices );
    // construct choices for the internal nodes
    assert( pAig->pReprs != NULL );
    Aig_ManForEachNode( pAig, pObj, i ) 
        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, fSkipRedSupps );
    Aig_ManForEachCo( pAig, pObj, i )
        Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
    Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) );
    return pChoices;
}

void Dch_DeriveChoiceAigNode	(	Aig_Man_t *	pAigNew,
		Aig_Man_t *	pAigOld,
		Aig_Obj_t *	pObj,
		int	fSkipRedSupps
	)

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

Synopsis [Derives the AIG with choices from representatives.]

Description []

SideEffects []

SeeAlso []

Definition at line 443 of file dchChoice.c.

{
    Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
    assert( !Aig_IsComplement(pObj) );
    // get the representative
    pRepr = Aig_ObjRepr( pAigOld, pObj );
    if ( pRepr != NULL && (Aig_ObjIsConst1(pRepr) || Aig_ObjIsCi(pRepr)) )
    {
        assert( pRepr->pData != NULL );
        pObj->pData = Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
        return;
    }
    // get the new node
    pObjNew = Aig_And( pAigNew, 
        Aig_ObjChild0CopyRepr(pAigNew, pObj), 
        Aig_ObjChild1CopyRepr(pAigNew, pObj) );
    pObjNew = Aig_ObjGetRepr( pAigNew, pObjNew );
//    assert( Aig_ObjRepr( pAigNew, pObjNew ) == NULL );
    // assign the copy
    assert( pObj->pData == NULL );
    pObj->pData = pObjNew;
    // skip those without reprs
    if ( pRepr == NULL )
        return;
    assert( pRepr->Id < pObj->Id );
    assert( Aig_ObjIsNode(pRepr) );
    // get the corresponding new nodes
    pObjNew  = Aig_Regular((Aig_Obj_t *)pObj->pData);
    pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
    // skip earlier nodes
    if ( pReprNew->Id >= pObjNew->Id )
        return;
    assert( pReprNew->Id < pObjNew->Id );
    // set the representatives
    Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
    // skip used nodes
    if ( pObjNew->nRefs > 0 )
        return;
    assert( pObjNew->nRefs == 0 );
    // skip choices that can lead to combo loops
    if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
        return;
    // don't add choice if structural support of pObjNew and pReprNew differ
    if ( fSkipRedSupps && Dch_ObjCheckSuppRed(pAigNew, pObjNew, pReprNew) )
        return;
    // add choice to the end of the list
    while ( pAigNew->pEquivs[pReprNew->Id] != NULL )
        pReprNew = pAigNew->pEquivs[pReprNew->Id];
    assert( pAigNew->pEquivs[pReprNew->Id] == NULL );
    pAigNew->pEquivs[pReprNew->Id] = pObjNew;
}

int Dch_DeriveChoiceCountEquivs

(

Aig_Man_t *

pAig

)

Definition at line 89 of file dchChoice.c.

{
    Aig_Obj_t * pObj, * pEquiv;
    int i, nEquivs = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        pEquiv = Aig_ObjEquiv( pAig, pObj );
        if ( pEquiv == NULL )
            continue;
        assert( pEquiv->Id < pObj->Id );
        nEquivs++;
    }
    return nEquivs;
}

int Dch_DeriveChoiceCountReprs

(

Aig_Man_t *

pAig

)

FUNCTION DECLARATIONS ///.

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

Synopsis [Counts the number of representatives.]

Description []

SideEffects []

SeeAlso []

Definition at line 75 of file dchChoice.c.

{
    Aig_Obj_t * pObj, * pRepr;
    int i, nReprs = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        pRepr = Aig_ObjRepr( pAig, pObj );
        if ( pRepr == NULL )
            continue;
        assert( pRepr->Id < pObj->Id );
        nReprs++;
    }
    return nReprs;
}

int Dch_ObjCheckSuppRed	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Aig_Obj_t *	pRepr
	)

Definition at line 135 of file dchChoice.c.

{
    // mark support of the representative node (pRepr)
    Aig_ManIncrementTravId( p );
    Dch_ObjMarkTfi_rec( p, pRepr );
    // detect if the new node (pObj) depends on additional variables
    Aig_ManIncrementTravId( p );
    if ( Dch_ObjMarkTfi_rec( p, pObj ) )
        return 1;//, printf( "1" );
    // detect if the representative node (pRepr) depends on additional variables
    Aig_ManIncrementTravId( p );
    if ( Dch_ObjMarkTfi_rec( p, pRepr ) )
        return 1;//, printf( "2" );
    // skip the choice if this is what is happening
    return 0;
}

int Dch_ObjCheckTfi	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		Aig_Obj_t *	pRepr
	)

Definition at line 393 of file dchChoice.c.

{
    Aig_Obj_t * pTemp;
    int RetValue;
    assert( !Aig_IsComplement(pObj) );
    assert( !Aig_IsComplement(pRepr) );
    // mark nodes of the choice node
    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
        pTemp->fMarkA = 1;
    // traverse the new node
    Aig_ManIncrementTravId( p );
    RetValue = Dch_ObjCheckTfi_rec( p, pObj );
    // unmark nodes of the choice node
    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
        pTemp->fMarkA = 0;
    return RetValue;
}

int Dch_ObjCheckTfi_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Returns 1 if the choice node of pRepr is in the TFI of pObj.]

Description []

SideEffects []

SeeAlso []

Definition at line 372 of file dchChoice.c.

{
    // check the trivial cases
    if ( pObj == NULL )
        return 0;
    if ( Aig_ObjIsCi(pObj) )
        return 0;
    if ( pObj->fMarkA )
        return 1;
    // skip the visited node
    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
        return 0;
    Aig_ObjSetTravIdCurrent( p, pObj );
    // check the children
    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) )
        return 1;
    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) )
        return 1;
    // check equivalent nodes
    return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) );
}

int Dch_ObjCountSupp	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

Definition at line 58 of file dchChoice.c.

{
    Aig_ManIncrementTravId( p );
    return Dch_ObjCountSupp_rec( p, pObj );
}

ABC_NAMESPACE_IMPL_START int Dch_ObjCountSupp_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

DECLARATIONS ///.

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

FileName [dchChoice.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [Contrustion of choices.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:

dchChoice.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

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

Synopsis [Counts support nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file dchChoice.c.

{
    int Count;
    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
        return 0;
    Aig_ObjSetTravIdCurrent( p, pObj );
    if ( Aig_ObjIsCi(pObj) )
        return 1;
    assert( Aig_ObjIsNode(pObj) );
    Count  = Dch_ObjCountSupp_rec( p, Aig_ObjFanin0(pObj) );
    Count += Dch_ObjCountSupp_rec( p, Aig_ObjFanin1(pObj) );
    return Count;
}

int Dch_ObjMarkTfi_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Marks the TFI of the node.]

Description [Returns 1 if there is a CI not marked with previous ID.]

SideEffects []

SeeAlso []

Definition at line 115 of file dchChoice.c.

{
    int RetValue;
    if ( pObj == NULL )
        return 0;
    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
        return 0;
    if ( Aig_ObjIsCi(pObj) )
    {
        RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
        Aig_ObjSetTravIdCurrent( p, pObj );
        return RetValue;
    }
    assert( Aig_ObjIsNode(pObj) );
    Aig_ObjSetTravIdCurrent( p, pObj );
    RetValue  = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
//    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
    return (RetValue > 0);
}