blob: ce70e7b42cb03278301dce112b51492efde76bc1 [file] [log] [blame]
/**CFile****************************************************************
FileName [saigWnd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Sequential windowing.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigWnd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns the array of PI/internal nodes.]
Description [Marks all the visited nodes with the current ID.
Does not collect constant node and PO/LI nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManWindowOutline_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Vec_Ptr_t * vNodes, int * pDists )
{
Aig_Obj_t * pMatch, * pFanout;
int fCollected, iFanout = -1, i;
if ( nDist == 0 )
return;
if ( pDists[pObj->Id] >= nDist )
return;
pDists[pObj->Id] = nDist;
fCollected = Aig_ObjIsTravIdCurrent( p, pObj );
Aig_ObjSetTravIdCurrent( p, pObj );
if ( Aig_ObjIsConst1(pObj) )
return;
if ( Saig_ObjIsPo(p, pObj) )
return;
if ( Saig_ObjIsLi(p, pObj) )
{
pMatch = Saig_ObjLiToLo( p, pObj );
if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) )
Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists );
Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists );
return;
}
if ( !fCollected )
Vec_PtrPush( vNodes, pObj );
if ( Saig_ObjIsPi(p, pObj) )
return;
if ( Saig_ObjIsLo(p, pObj) )
{
pMatch = Saig_ObjLoToLi( p, pObj );
if ( !Aig_ObjIsTravIdCurrent( p, pMatch ) )
Saig_ManWindowOutline_rec( p, pMatch, nDist, vNodes, pDists );
Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists );
return;
}
assert( Aig_ObjIsNode(pObj) );
Saig_ManWindowOutline_rec( p, Aig_ObjFanin0(pObj), nDist-1, vNodes, pDists );
Saig_ManWindowOutline_rec( p, Aig_ObjFanin1(pObj), nDist-1, vNodes, pDists );
Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
Saig_ManWindowOutline_rec( p, pFanout, nDist-1, vNodes, pDists );
}
/**Function*************************************************************
Synopsis [Returns the array of PI/internal nodes.]
Description [Marks all the visited nodes with the current ID.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Saig_ManWindowOutline( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObjLi, * pObjLo;
int * pDists, i;
pDists = ABC_CALLOC( int, Aig_ManObjNumMax(p) );
vNodes = Vec_PtrAlloc( 1000 );
Aig_ManIncrementTravId( p );
Saig_ManWindowOutline_rec( p, pObj, nDist, vNodes, pDists );
Vec_PtrSort( vNodes, (int (*)(void))Aig_ObjCompareIdIncrease );
// make sure LI/LO are labeled/unlabeled mutually
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
assert( Aig_ObjIsTravIdCurrent(p, pObjLi) ==
Aig_ObjIsTravIdCurrent(p, pObjLo) );
ABC_FREE( pDists );
return vNodes;
}
/**Function*************************************************************
Synopsis [Returns 1 if the node has unlabeled fanout.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Saig_ObjHasUnlabeledFanout( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pFanout;
int iFanout = -1, i;
Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
if ( Saig_ObjIsPo(p, pFanout) || !Aig_ObjIsTravIdCurrent(p, pFanout) )
return pFanout;
return NULL;
}
/**Function*************************************************************
Synopsis [Collects primary inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Saig_ManWindowCollectPis( Aig_Man_t * p, Vec_Ptr_t * vNodes )
{
Vec_Ptr_t * vNodesPi;
Aig_Obj_t * pObj, * pMatch, * pFanin;
int i;
vNodesPi = Vec_PtrAlloc( 1000 );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
if ( Saig_ObjIsPi(p, pObj) )
{
assert( pObj->pData == NULL );
Vec_PtrPush( vNodesPi, pObj );
}
else if ( Saig_ObjIsLo(p, pObj) )
{
pMatch = Saig_ObjLoToLi( p, pObj );
pFanin = Aig_ObjFanin0(pMatch);
if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
Vec_PtrPush( vNodesPi, pFanin );
}
else
{
assert( Aig_ObjIsNode(pObj) );
pFanin = Aig_ObjFanin0(pObj);
if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
Vec_PtrPush( vNodesPi, pFanin );
pFanin = Aig_ObjFanin1(pObj);
if ( !Aig_ObjIsTravIdCurrent(p, pFanin) && pFanin->pData == NULL )
Vec_PtrPush( vNodesPi, pFanin );
}
}
return vNodesPi;
}
/**Function*************************************************************
Synopsis [Collects primary outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Saig_ManWindowCollectPos( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t ** pvPointers )
{
Vec_Ptr_t * vNodesPo;
Aig_Obj_t * pObj, * pPointer;
int i;
vNodesPo = Vec_PtrAlloc( 1000 );
if ( pvPointers )
*pvPointers = Vec_PtrAlloc( 1000 );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
if ( (pPointer = Saig_ObjHasUnlabeledFanout(p, pObj)) )
{
Vec_PtrPush( vNodesPo, pObj );
if ( pvPointers )
Vec_PtrPush( *pvPointers, pPointer );
}
}
return vNodesPo;
}
/**Function*************************************************************
Synopsis [Extracts the window AIG from the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManWindowExtractNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pMatch;
Vec_Ptr_t * vNodesPi, * vNodesPo;
int i, nRegCount;
Aig_ManCleanData( p );
// create the new manager
pNew = Aig_ManStart( Vec_PtrSize(vNodes) );
pNew->pName = Abc_UtilStrsav( "wnd" );
pNew->pSpec = NULL;
// map constant nodes
pObj = Aig_ManConst1( p );
pObj->pData = Aig_ManConst1( pNew );
// create real PIs
vNodesPi = Saig_ManWindowCollectPis( p, vNodes );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPi, pObj, i )
pObj->pData = Aig_ObjCreateCi(pNew);
Vec_PtrFree( vNodesPi );
// create register outputs
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
if ( Saig_ObjIsLo(p, pObj) )
pObj->pData = Aig_ObjCreateCi(pNew);
}
// create internal nodes
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
// create POs
vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPo, pObj, i )
Aig_ObjCreateCo( pNew, (Aig_Obj_t *)pObj->pData );
Vec_PtrFree( vNodesPo );
// create register inputs
nRegCount = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
{
if ( Saig_ObjIsLo(p, pObj) )
{
pMatch = Saig_ObjLoToLi( p, pObj );
Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) );
nRegCount++;
}
}
Aig_ManSetRegNum( pNew, nRegCount );
Aig_ManCleanup( pNew );
return pNew;
}
static void Saig_ManWindowInsertSmall_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjSmall,
Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode );
/**Function*************************************************************
Synopsis [Adds nodes for the big manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManWindowInsertBig_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjBig,
Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode )
{
Aig_Obj_t * pMatch;
if ( pObjBig->pData )
return;
if ( (pMatch = (Aig_Obj_t *)Vec_PtrEntry( vBigNode2SmallPo, pObjBig->Id )) )
{
Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pMatch), vBigNode2SmallPo, vSmallPi2BigNode );
pObjBig->pData = Aig_ObjChild0Copy(pMatch);
return;
}
assert( Aig_ObjIsNode(pObjBig) );
Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode );
Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin1(pObjBig), vBigNode2SmallPo, vSmallPi2BigNode );
pObjBig->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjBig), Aig_ObjChild1Copy(pObjBig) );
}
/**Function*************************************************************
Synopsis [Adds nodes for the small manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManWindowInsertSmall_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjSmall,
Vec_Ptr_t * vBigNode2SmallPo, Vec_Ptr_t * vSmallPi2BigNode )
{
Aig_Obj_t * pMatch;
if ( pObjSmall->pData )
return;
if ( (pMatch = (Aig_Obj_t *)Vec_PtrEntry( vSmallPi2BigNode, pObjSmall->Id )) )
{
Saig_ManWindowInsertBig_rec( pNew, pMatch, vBigNode2SmallPo, vSmallPi2BigNode );
pObjSmall->pData = pMatch->pData;
return;
}
assert( Aig_ObjIsNode(pObjSmall) );
Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode );
Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin1(pObjSmall), vBigNode2SmallPo, vSmallPi2BigNode );
pObjSmall->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObjSmall), Aig_ObjChild1Copy(pObjSmall) );
}
/**Function*************************************************************
Synopsis [Extracts the network from the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManWindowInsertNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes, Aig_Man_t * pWnd )
{
Aig_Man_t * pNew;
Vec_Ptr_t * vBigNode2SmallPo, * vSmallPi2BigNode;
Vec_Ptr_t * vNodesPi, * vNodesPo;
Aig_Obj_t * pObj;
int i;
// set mapping of small PIs into big nodes
vSmallPi2BigNode = Vec_PtrStart( Aig_ManObjNumMax(pWnd) );
vNodesPi = Saig_ManWindowCollectPis( p, vNodes );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPi, pObj, i )
Vec_PtrWriteEntry( vSmallPi2BigNode, Aig_ManCi(pWnd, i)->Id, pObj );
assert( i == Saig_ManPiNum(pWnd) );
Vec_PtrFree( vNodesPi );
// set mapping of big nodes into small POs
vBigNode2SmallPo = Vec_PtrStart( Aig_ManObjNumMax(p) );
vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL );
Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPo, pObj, i )
Vec_PtrWriteEntry( vBigNode2SmallPo, pObj->Id, Aig_ManCo(pWnd, i) );
assert( i == Saig_ManPoNum(pWnd) );
Vec_PtrFree( vNodesPo );
// create the new manager
Aig_ManCleanData( p );
Aig_ManCleanData( pWnd );
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
// map constant nodes
pObj = Aig_ManConst1( p );
pObj->pData = Aig_ManConst1( pNew );
pObj = Aig_ManConst1( pWnd );
pObj->pData = Aig_ManConst1( pNew );
// create real PIs
Aig_ManForEachCi( p, pObj, i )
if ( Saig_ObjIsPi(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) )
pObj->pData = Aig_ObjCreateCi(pNew);
// create additional latch outputs
Saig_ManForEachLo( pWnd, pObj, i )
pObj->pData = Aig_ObjCreateCi(pNew);
// create internal nodes starting from the big
Aig_ManForEachCo( p, pObj, i )
if ( Saig_ObjIsPo(p, pObj) || !Aig_ObjIsTravIdCurrent(p, pObj) )
{
Saig_ManWindowInsertBig_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode );
pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
}
// create internal nodes starting from the small
Saig_ManForEachLi( pWnd, pObj, i )
{
Saig_ManWindowInsertSmall_rec( pNew, Aig_ObjFanin0(pObj), vBigNode2SmallPo, vSmallPi2BigNode );
pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
}
Vec_PtrFree( vBigNode2SmallPo );
Vec_PtrFree( vSmallPi2BigNode );
// set the new number of registers
assert( Aig_ManCiNum(pNew) - Aig_ManCiNum(p) == Aig_ManCoNum(pNew) - Aig_ManCoNum(p) );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) + (Aig_ManCiNum(pNew) - Aig_ManCiNum(p)) );
Aig_ManCleanup( pNew );
return pNew;
}
/**Function*************************************************************
Synopsis [Find a good object.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Saig_ManFindPivot( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i, Counter;
if ( Aig_ManRegNum(p) > 0 )
{
if ( Aig_ManRegNum(p) == 1 )
return Saig_ManLo( p, 0 );
Saig_ManForEachLo( p, pObj, i )
{
if ( i == Aig_ManRegNum(p)/2 )
return pObj;
}
}
else
{
Counter = 0;
assert( Aig_ManNodeNum(p) > 1 );
Aig_ManForEachNode( p, pObj, i )
{
if ( Counter++ == Aig_ManNodeNum(p)/2 )
return pObj;
}
}
return NULL;
}
/**Function*************************************************************
Synopsis [Computes sequential window of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManWindowExtract( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist )
{
Aig_Man_t * pWnd;
Vec_Ptr_t * vNodes;
Aig_ManFanoutStart( p );
vNodes = Saig_ManWindowOutline( p, pObj, nDist );
pWnd = Saig_ManWindowExtractNodes( p, vNodes );
Vec_PtrFree( vNodes );
Aig_ManFanoutStop( p );
return pWnd;
}
/**Function*************************************************************
Synopsis [Computes sequential window of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManWindowInsert( Aig_Man_t * p, Aig_Obj_t * pObj, int nDist, Aig_Man_t * pWnd )
{
Aig_Man_t * pNew, * pWndTest;
Vec_Ptr_t * vNodes;
Aig_ManFanoutStart( p );
vNodes = Saig_ManWindowOutline( p, pObj, nDist );
pWndTest = Saig_ManWindowExtractNodes( p, vNodes );
if ( Saig_ManPiNum(pWndTest) != Saig_ManPiNum(pWnd) ||
Saig_ManPoNum(pWndTest) != Saig_ManPoNum(pWnd) )
{
printf( "The window cannot be reinserted because PI/PO counts do not match.\n" );
Aig_ManStop( pWndTest );
Vec_PtrFree( vNodes );
Aig_ManFanoutStop( p );
return NULL;
}
Aig_ManStop( pWndTest );
Vec_PtrFree( vNodes );
// insert the nodes
Aig_ManCleanData( p );
vNodes = Saig_ManWindowOutline( p, pObj, nDist );
pNew = Saig_ManWindowInsertNodes( p, vNodes, pWnd );
Vec_PtrFree( vNodes );
Aig_ManFanoutStop( p );
return pNew;
}
/**Function*************************************************************
Synopsis [Tests the above computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManWindowTest( Aig_Man_t * p )
{
int nDist = 3;
Aig_Man_t * pWnd, * pNew;
Aig_Obj_t * pPivot;
pPivot = Saig_ManFindPivot( p );
assert( pPivot != NULL );
pWnd = Saig_ManWindowExtract( p, pPivot, nDist );
pNew = Saig_ManWindowInsert( p, pPivot, nDist, pWnd );
Aig_ManStop( pWnd );
return pNew;
}
/**Function*************************************************************
Synopsis [Collects the nodes that are not linked to each other.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Saig_ManCollectedDiffNodes( Aig_Man_t * p0, Aig_Man_t * p1 )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj0, * pObj1;
int i;
// collect nodes that are not linked
Aig_ManIncrementTravId( p0 );
vNodes = Vec_PtrAlloc( 1000 );
Aig_ManForEachObj( p0, pObj0, i )
{
pObj1 = Aig_ObjRepr( p0, pObj0 );
if ( pObj1 != NULL )
{
assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
continue;
}
// mark and collect unmatched objects
Aig_ObjSetTravIdCurrent( p0, pObj0 );
if ( Aig_ObjIsNode(pObj0) || Aig_ObjIsCi(pObj0) )
Vec_PtrPush( vNodes, pObj0 );
}
// make sure LI/LO are labeled/unlabeled mutually
Saig_ManForEachLiLo( p0, pObj0, pObj1, i )
assert( Aig_ObjIsTravIdCurrent(p0, pObj0) ==
Aig_ObjIsTravIdCurrent(p0, pObj1) );
return vNodes;
}
/**Function*************************************************************
Synopsis [Creates PIs of the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManWindowCreatePis( Aig_Man_t * pNew, Aig_Man_t * p0, Aig_Man_t * p1, Vec_Ptr_t * vNodes0 )
{
Aig_Obj_t * pObj, * pMatch, * pFanin;
int i, Counter = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj, i )
{
if ( Saig_ObjIsLo(p0, pObj) )
{
pMatch = Saig_ObjLoToLi( p0, pObj );
pFanin = Aig_ObjFanin0(pMatch);
if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
{
pFanin->pData = Aig_ObjCreateCi(pNew);
pMatch = Aig_ObjRepr( p0, pFanin );
assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
assert( pMatch != NULL );
pMatch->pData = pFanin->pData;
Counter++;
}
}
else
{
assert( Aig_ObjIsNode(pObj) );
pFanin = Aig_ObjFanin0(pObj);
if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
{
pFanin->pData = Aig_ObjCreateCi(pNew);
pMatch = Aig_ObjRepr( p0, pFanin );
assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
assert( pMatch != NULL );
pMatch->pData = pFanin->pData;
Counter++;
}
pFanin = Aig_ObjFanin1(pObj);
if ( !Aig_ObjIsTravIdCurrent(p0, pFanin) && pFanin->pData == NULL )
{
pFanin->pData = Aig_ObjCreateCi(pNew);
pMatch = Aig_ObjRepr( p0, pFanin );
assert( pFanin == Aig_ObjRepr( p1, pMatch ) );
assert( pMatch != NULL );
pMatch->pData = pFanin->pData;
Counter++;
}
}
}
// printf( "Added %d primary inputs.\n", Counter );
}
/**Function*************************************************************
Synopsis [Creates POs of the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManWindowCreatePos( Aig_Man_t * pNew, Aig_Man_t * p0, Aig_Man_t * p1 )
{
Aig_Obj_t * pObj0, * pObj1, * pMiter;
Aig_Obj_t * pFanin0, * pFanin1;
int i;
Aig_ManForEachObj( p0, pObj0, i )
{
if ( Aig_ObjIsTravIdCurrent(p0, pObj0) )
continue;
if ( Aig_ObjIsConst1(pObj0) )
continue;
if ( Aig_ObjIsCi(pObj0) )
continue;
pObj1 = Aig_ObjRepr( p0, pObj0 );
assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) );
if ( Aig_ObjIsCo(pObj0) )
{
pFanin0 = Aig_ObjFanin0(pObj0);
pFanin1 = Aig_ObjFanin0(pObj1);
assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
Aig_ObjIsTravIdCurrent(p1, pFanin1) );
if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
{
pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData );
Aig_ObjCreateCo( pNew, pMiter );
}
}
else
{
assert( Aig_ObjIsNode(pObj0) );
pFanin0 = Aig_ObjFanin0(pObj0);
pFanin1 = Aig_ObjFanin0(pObj1);
assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
Aig_ObjIsTravIdCurrent(p1, pFanin1) );
if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
{
pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData );
Aig_ObjCreateCo( pNew, pMiter );
}
pFanin0 = Aig_ObjFanin1(pObj0);
pFanin1 = Aig_ObjFanin1(pObj1);
assert( Aig_ObjIsTravIdCurrent(p0, pFanin0) ==
Aig_ObjIsTravIdCurrent(p1, pFanin1) );
if ( Aig_ObjIsTravIdCurrent(p0, pFanin0) )
{
pMiter = Aig_Exor( pNew, (Aig_Obj_t *)pFanin0->pData, (Aig_Obj_t *)pFanin1->pData );
Aig_ObjCreateCo( pNew, pMiter );
}
}
}
}
/**Function*************************************************************
Synopsis [Extracts the window AIG from the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj0, * pObj1, * pMatch0, * pMatch1;
Vec_Ptr_t * vNodes0, * vNodes1;
int i, nRegCount;
// add matching of POs and LIs
Saig_ManForEachPo( p0, pObj0, i )
{
pObj1 = Aig_ManCo( p1, i );
Aig_ObjSetRepr( p0, pObj0, pObj1 );
Aig_ObjSetRepr( p1, pObj1, pObj0 );
}
Saig_ManForEachLi( p0, pObj0, i )
{
pMatch0 = Saig_ObjLiToLo( p0, pObj0 );
pMatch1 = Aig_ObjRepr( p0, pMatch0 );
if ( pMatch1 == NULL )
continue;
assert( pMatch0 == Aig_ObjRepr( p1, pMatch1 ) );
pObj1 = Saig_ObjLoToLi( p1, pMatch1 );
Aig_ObjSetRepr( p0, pObj0, pObj1 );
Aig_ObjSetRepr( p1, pObj1, pObj0 );
}
// clean the markings
Aig_ManCleanData( p0 );
Aig_ManCleanData( p1 );
// collect nodes that are not linked
vNodes0 = Saig_ManCollectedDiffNodes( p0, p1 );
vNodes1 = Saig_ManCollectedDiffNodes( p1, p0 );
// create the new manager
pNew = Aig_ManStart( Vec_PtrSize(vNodes0) + Vec_PtrSize(vNodes1) );
pNew->pName = Abc_UtilStrsav( "wnd" );
pNew->pSpec = NULL;
// map constant nodes
pObj0 = Aig_ManConst1( p0 );
pObj0->pData = Aig_ManConst1( pNew );
pObj1 = Aig_ManConst1( p1 );
pObj1->pData = Aig_ManConst1( pNew );
// create real PIs
Saig_ManWindowCreatePis( pNew, p0, p1, vNodes0 );
Saig_ManWindowCreatePis( pNew, p1, p0, vNodes1 );
// create register outputs
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i )
{
if ( Saig_ObjIsLo(p0, pObj0) )
pObj0->pData = Aig_ObjCreateCi(pNew);
}
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i )
{
if ( Saig_ObjIsLo(p1, pObj1) )
pObj1->pData = Aig_ObjCreateCi(pNew);
}
// create internal nodes
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i )
{
if ( Aig_ObjIsNode(pObj0) )
pObj0->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
}
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i )
{
if ( Aig_ObjIsNode(pObj1) )
pObj1->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj1), Aig_ObjChild1Copy(pObj1) );
}
// create POs
Saig_ManWindowCreatePos( pNew, p0, p1 );
// Saig_ManWindowCreatePos( pNew, p1, p0 );
// create register inputs
nRegCount = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pObj0, i )
{
if ( Saig_ObjIsLo(p0, pObj0) )
{
pMatch0 = Saig_ObjLoToLi( p0, pObj0 );
Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch0) );
nRegCount++;
}
}
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pObj1, i )
{
if ( Saig_ObjIsLo(p1, pObj1) )
{
pMatch1 = Saig_ObjLoToLi( p1, pObj1 );
Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch1) );
nRegCount++;
}
}
Aig_ManSetRegNum( pNew, nRegCount );
Aig_ManCleanup( pNew );
Vec_PtrFree( vNodes0 );
Vec_PtrFree( vNodes1 );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END