#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "opt/sim/sim.h"

Data Structures
struct	Abc_RRMan_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Abc_RRMan_t_	Abc_RRMan_t
	DECLARATIONS ///. More...

Functions
static Abc_RRMan_t *	Abc_RRManStart ()

static void	Abc_RRManStop (Abc_RRMan_t *p)

static void	Abc_RRManPrintStats (Abc_RRMan_t *p)

static void	Abc_RRManClean (Abc_RRMan_t *p)

static int	Abc_NtkRRProve (Abc_RRMan_t *p)

static int	Abc_NtkRRUpdate (Abc_Ntk_t pNtk, Abc_Obj_t pNode, Abc_Obj_t pFanin, Abc_Obj_t pFanout)

static int	Abc_NtkRRWindow (Abc_RRMan_t *p)

static int	Abc_NtkRRTfi_int (Vec_Ptr_t *vLeaves, int LevelLimit)

static int	Abc_NtkRRTfo_int (Vec_Ptr_t vLeaves, Vec_Ptr_t vRoots, int LevelLimit, Abc_Obj_t pEdgeFanin, Abc_Obj_t pEdgeFanout)

static int	Abc_NtkRRTfo_rec (Abc_Obj_t pNode, Vec_Ptr_t vRoots, int LevelLimit)

static void	Abc_NtkRRTfi_rec (Abc_Obj_t pNode, Vec_Ptr_t vLeaves, Vec_Ptr_t *vCone, int LevelLimit)

static Abc_Ntk_t *	Abc_NtkWindow (Abc_Ntk_t pNtk, Vec_Ptr_t vLeaves, Vec_Ptr_t vCone, Vec_Ptr_t vRoots)

static void	Abc_NtkRRSimulateStart (Abc_Ntk_t *pNtk)

static void	Abc_NtkRRSimulateStop (Abc_Ntk_t *pNtk)

int	Abc_NtkRR (Abc_Ntk_t *pNtk, int nFaninLevels, int nFanoutLevels, int fUseFanouts, int fVerbose)
	FUNCTION DEFINITIONS ///. More...

static void	Sim_TraverseNodes_rec (Abc_Obj_t pRoot, Vec_Str_t vTargets, Vec_Ptr_t *vNodes)

static void	Sim_CollectNodes_rec (Abc_Obj_t pRoot, Vec_Ptr_t vField)

static void	Sim_SimulateCollected (Vec_Str_t vTargets, Vec_Ptr_t vNodes, Vec_Ptr_t *vField)

Vec_Str_t *	Abc_NtkRRSimulate (Abc_Ntk_t *pNtk)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Abc_RRMan_t_ Abc_RRMan_t

DECLARATIONS ///.

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

FileName [abcRr.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Redundancy removal.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 32 of file abcRr.c.

Function Documentation

int Abc_NtkRR	(	Abc_Ntk_t *	pNtk,
		int	nFaninLevels,
		int	nFanoutLevels,
		int	fUseFanouts,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Removes stuck-at redundancies.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file abcRr.c.

 {
     ProgressBar * pProgress;
     Abc_RRMan_t * p;
     Abc_Obj_t * pNode, * pFanin, * pFanout;
     int i, k, m, nNodes, RetValue;
     abctime clk, clkTotal = Abc_Clock();
     // start the manager
     p = Abc_RRManStart();
     p->pNtk          = pNtk;
     p->nFaninLevels  = nFaninLevels;
     p->nFanoutLevels = nFanoutLevels;
     p->nNodesOld     = Abc_NtkNodeNum(pNtk);
     p->nLevelsOld    = Abc_AigLevel(pNtk);
     // remember latch values
 //    Abc_NtkForEachLatch( pNtk, pNode, i )
 //        pNode->pNext = pNode->pData;
     // go through the nodes
     Abc_NtkCleanCopy(pNtk);
     nNodes = Abc_NtkObjNumMax(pNtk);
     Abc_NtkRRSimulateStart(pNtk);
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         // stop if all nodes have been tried once
         if ( i >= nNodes )
             break;
         // skip the constant node
 //        if ( Abc_NodeIsConst(pNode) )
 //            continue;
         // skip persistant nodes
         if ( Abc_NodeIsPersistant(pNode) )
             continue;
         // skip the nodes with many fanouts
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;
         // construct the window
         if ( !fUseFanouts )
         {
             Abc_ObjForEachFanin( pNode, pFanin, k )
             {
                 // skip the nodes with only one fanout (tree nodes)
                 if ( Abc_ObjFanoutNum(pFanin) == 1 )
                     continue;
 /*
                 if ( pFanin->Id == 228 && pNode->Id == 2649 )
                 {
                     int k = 0;
                 }
 */
                 p->nEdgesTried++;
                 Abc_RRManClean( p );
                 p->pNode   = pNode;
                 p->pFanin  = pFanin;
                 p->pFanout = NULL;
 
                 clk = Abc_Clock();
                 RetValue = Abc_NtkRRWindow( p );
                 p->timeWindow += Abc_Clock() - clk;
                 if ( !RetValue )
                     continue;
 /*
                 if ( pFanin->Id == 228 && pNode->Id == 2649 )
                 {
                     Abc_NtkShowAig( p->pWnd, 0 );
                 }
 */
                 clk = Abc_Clock();
                 RetValue = Abc_NtkRRProve( p );
                 p->timeMiter += Abc_Clock() - clk;
                 if ( !RetValue )
                     continue;
 //printf( "%d -> %d (%d)\n", pFanin->Id, pNode->Id, k );
 
                 clk = Abc_Clock();
                 Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
                 p->timeUpdate += Abc_Clock() - clk;
 
                 p->nEdgesRemoved++;
                 break;
             }
             continue;
         }
         // use the fanouts
         Abc_ObjForEachFanin( pNode, pFanin, k )
         Abc_ObjForEachFanout( pNode, pFanout, m )
         {
             // skip the nodes with only one fanout (tree nodes)
 //            if ( Abc_ObjFanoutNum(pFanin) == 1 && Abc_ObjFanoutNum(pNode) == 1 )
 //                continue;
 
             p->nEdgesTried++;
             Abc_RRManClean( p );
             p->pNode   = pNode;
             p->pFanin  = pFanin;
             p->pFanout = pFanout;
 
             clk = Abc_Clock();
             RetValue = Abc_NtkRRWindow( p );
             p->timeWindow += Abc_Clock() - clk;
             if ( !RetValue )
                 continue;
 
             clk = Abc_Clock();
             RetValue = Abc_NtkRRProve( p );
             p->timeMiter += Abc_Clock() - clk;
             if ( !RetValue )
                 continue;
 
             clk = Abc_Clock();
             Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
             p->timeUpdate += Abc_Clock() - clk;
 
             p->nEdgesRemoved++;
             break;
         }
     }
     Abc_NtkRRSimulateStop(pNtk);
     Extra_ProgressBarStop( pProgress );
     p->timeTotal = Abc_Clock() - clkTotal;
     if ( fVerbose )
         Abc_RRManPrintStats( p );
     Abc_RRManStop( p );
     // restore latch values
 //    Abc_NtkForEachLatch( pNtk, pNode, i )
 //        pNode->pData = pNode->pNext, pNode->pNext = NULL;
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
     Abc_NtkLevel( pNtk );
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
         printf( "Abc_NtkRR: The network check has failed.\n" );
         return 0;
     }
     return 1;
 }

int Abc_NtkRRProve ( Abc_RRMan_t * p )

static

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

Synopsis [Returns 1 if the miter is constant 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 352 of file abcRr.c.

 {
     Abc_Ntk_t * pWndCopy;
     int RetValue;
     abctime clk;
 //    Abc_NtkShowAig( p->pWnd, 0 );
     pWndCopy = Abc_NtkDup( p->pWnd );
     Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
     if ( !Abc_NtkIsDfsOrdered(pWndCopy) )
         Abc_NtkReassignIds(pWndCopy);
     p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0, 0, 0 );
     Abc_NtkDelete( pWndCopy );
 clk = Abc_Clock();
     RetValue  = Abc_NtkMiterProve( &p->pMiter, p->pParams );
 p->timeProve += Abc_Clock() - clk;
     if ( RetValue == 1 )
         return 1;
     return 0;
 }

Vec_Str_t* Abc_NtkRRSimulate ( Abc_Ntk_t * pNtk )

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

Synopsis [Simulation to detect non-redundant edges.]

Description []

SideEffects []

SeeAlso []

Definition at line 789 of file abcRr.c.

 {
     Vec_Ptr_t * vNodes, * vField;
     Vec_Str_t * vTargets;
     Abc_Obj_t * pObj;
     unsigned uData, uData0, uData1;
     int PrevCi, Phase, i, k;
 
     // start the candidates
     vTargets = Vec_StrStart( Abc_NtkObjNumMax(pNtk) + 1 );
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         Phase = ((Abc_ObjFanoutNum(Abc_ObjFanin1(pObj)) > 1) << 1);
         Phase |= (Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) > 1);
         Vec_StrWriteEntry( vTargets, pObj->Id, (char)Phase );
     }
 
     // simulate patters and store them in copy
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)~((unsigned)0);
     Abc_NtkForEachCi( pNtk, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)SIM_RANDOM_UNSIGNED;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( i == 0 ) continue;
         uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
         uData1 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
         uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
         uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
         pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)uData;
     }
     // store the result in data
     Abc_NtkForEachCo( pNtk, pObj, i )
     {
         uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
         if ( Abc_ObjFaninC0(pObj) )
             pObj->pData = (void *)(ABC_PTRUINT_T)~uData0;
         else
             pObj->pData = (void *)(ABC_PTRUINT_T)uData0;
     }
 
     // refine the candidates
     for ( PrevCi = 0; PrevCi < Abc_NtkCiNum(pNtk); PrevCi = i )
     {
         vNodes = Vec_PtrAlloc( 10 );
         Abc_NtkIncrementTravId( pNtk );
         for ( i = PrevCi; i < Abc_NtkCiNum(pNtk); i++ )
         {
             Sim_TraverseNodes_rec( Abc_NtkCi(pNtk, i), vTargets, vNodes );
             if ( Vec_PtrSize(vNodes) > 128 )
                 break;
         }
         // collect the marked nodes in the topological order
         vField = Vec_PtrAlloc( 10 );
         Abc_NtkIncrementTravId( pNtk );
         Abc_NtkForEachCo( pNtk, pObj, k )
             Sim_CollectNodes_rec( pObj, vField );
 
         // simulate these nodes
         Sim_SimulateCollected( vTargets, vNodes, vField );
         // prepare for the next loop
         Vec_PtrFree( vNodes );
     }
 
     // clean
     Abc_NtkForEachObj( pNtk, pObj, i )
         pObj->pData = NULL;
     return vTargets;
 }

void Abc_NtkRRSimulateStart ( Abc_Ntk_t * pNtk )

static

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

Synopsis [Starts simulation to detect non-redundant edges.]

Description []

SideEffects []

SeeAlso []

Definition at line 729 of file abcRr.c.

 {
     Abc_Obj_t * pObj;
     unsigned uData, uData0, uData1;
     int i;
     Abc_AigConst1(pNtk)->pData = (void *)~((unsigned)0);
     Abc_NtkForEachCi( pNtk, pObj, i )
         pObj->pData = (void *)(ABC_PTRUINT_T)SIM_RANDOM_UNSIGNED;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( i == 0 ) continue;
         uData0 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
         uData1 = (unsigned)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
         uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
         uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
         assert( pObj->pData == NULL );
         pObj->pData = (void *)(ABC_PTRUINT_T)uData;
     }
 }

void Abc_NtkRRSimulateStop ( Abc_Ntk_t * pNtk )

static

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

Synopsis [Stops simulation to detect non-redundant edges.]

Description []

SideEffects []

SeeAlso []

Definition at line 760 of file abcRr.c.

 {
     Abc_Obj_t * pObj;
     int i;
     Abc_NtkForEachObj( pNtk, pObj, i )
         pObj->pData = NULL;
 }

int Abc_NtkRRTfi_int	(	Vec_Ptr_t *	vLeaves,
		int	LevelLimit
	)

static

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

Synopsis [Marks the nodes in the TFI and collects their leaves.]

Description []

SideEffects []

SeeAlso []

Definition at line 492 of file abcRr.c.

 {
     Abc_Obj_t * pObj, * pNext;
     int i, k, LevelMax, nSize;
     assert( LevelLimit >= 0 );
     // find the maximum level of leaves
     LevelMax = 0;
     Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
         if ( LevelMax < (int)pObj->Level )
             LevelMax = pObj->Level;
     // if the nodes are all PIs, LevelMax == 0
     if ( LevelMax <= LevelLimit )
         return 0;
     // expand the nodes with the minimum level
     nSize = Vec_PtrSize(vLeaves);
     Vec_PtrForEachEntryStop( Abc_Obj_t *, vLeaves, pObj, i, nSize )
     {
         if ( LevelMax != (int)pObj->Level )
             continue;
         Abc_ObjForEachFanin( pObj, pNext, k )
         {
             if ( Abc_NodeIsTravIdCurrent(pNext) )
                 continue;
             Abc_NodeSetTravIdCurrent( pNext );
             Vec_PtrPush( vLeaves, pNext );
         }
     }
     // remove old nodes (cannot remove a PI)
     k = 0;
     Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
     {
         if ( LevelMax == (int)pObj->Level )
             continue;
         Vec_PtrWriteEntry( vLeaves, k++, pObj );
     }
     Vec_PtrShrink( vLeaves, k );
     if ( Vec_PtrSize(vLeaves) > 2000 )
         return 0;
     return 1;
 }

void Abc_NtkRRTfi_rec	(	Abc_Obj_t *	pNode,
		Vec_Ptr_t *	vLeaves,
		Vec_Ptr_t *	vCone,
		int	LevelLimit
	)

static

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

Synopsis [Collects the leaves and cone of the roots.]

Description []

SideEffects []

SeeAlso []

Definition at line 642 of file abcRr.c.

 {
     Abc_Obj_t * pFanin;
     int i;
     // skip visited nodes
     if ( Abc_NodeIsTravIdCurrent(pNode) )
         return;
     // add node to leaves if it is not in TFI cone of the leaves (marked before) or below the limit
     if ( !Abc_NodeIsTravIdPrevious(pNode) || (int)pNode->Level <= LevelLimit )
     {
         Abc_NodeSetTravIdCurrent( pNode );
         Vec_PtrPush( vLeaves, pNode );
         return;
     }
     // mark the node as visited
     Abc_NodeSetTravIdCurrent( pNode );
     // call for the node's fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
         Abc_NtkRRTfi_rec( pFanin, vLeaves, vCone, LevelLimit );
     // add the node to the cone in topological order
     Vec_PtrPush( vCone, pNode );
 }

int Abc_NtkRRTfo_int	(	Vec_Ptr_t *	vLeaves,
		Vec_Ptr_t *	vRoots,
		int	LevelLimit,
		Abc_Obj_t *	pEdgeFanin,
		Abc_Obj_t *	pEdgeFanout
	)

static

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

Synopsis [Marks the nodes in the TFO and collects their roots.]

Description []

SideEffects []

SeeAlso []

Definition at line 544 of file abcRr.c.

 {
     Abc_Obj_t * pObj, * pNext;
     int i, k, LevelMin, nSize, fObjIsRoot;
     // find the minimum level of leaves
     LevelMin = ABC_INFINITY;
     Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
         if ( LevelMin > (int)pObj->Level )
             LevelMin = pObj->Level;
     // if the minimum level exceed the limit, we are done
     if ( LevelMin > LevelLimit )
         return 0;
     // expand the nodes with the minimum level
     nSize = Vec_PtrSize(vLeaves);
     Vec_PtrForEachEntryStop( Abc_Obj_t *, vLeaves, pObj, i, nSize )
     {
         if ( LevelMin != (int)pObj->Level )
             continue;
         fObjIsRoot = 0;
         Abc_ObjForEachFanout( pObj, pNext, k )
         {
             // check if the fanout is outside of the cone
             if ( Abc_ObjIsCo(pNext) || pNext->Level > (unsigned)LevelLimit )
             {
                 fObjIsRoot = 1;
                 continue;
             }
             // skip the edge under check
             if ( pObj == pEdgeFanin && pNext == pEdgeFanout )
                 continue;
             // skip the visited fanouts
             if ( Abc_NodeIsTravIdCurrent(pNext) )
                 continue;
             Abc_NodeSetTravIdCurrent( pNext );
             Vec_PtrPush( vLeaves, pNext );
         }
         if ( fObjIsRoot )
             Vec_PtrPush( vRoots, pObj );
     }
     // remove old nodes
     k = 0;
     Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
     {
         if ( LevelMin == (int)pObj->Level )
             continue;
         Vec_PtrWriteEntry( vLeaves, k++, pObj );
     }
     Vec_PtrShrink( vLeaves, k );
     if ( Vec_PtrSize(vLeaves) > 2000 )
         return 0;
     return 1;
 }

int Abc_NtkRRTfo_rec	(	Abc_Obj_t *	pNode,
		Vec_Ptr_t *	vRoots,
		int	LevelLimit
	)

static

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

Synopsis [Collects the roots in the TFO of the node.]

Description [Note that this procedure can be improved by marking and skipping the visited nodes.]

SideEffects []

SeeAlso []

Definition at line 609 of file abcRr.c.

 {
     Abc_Obj_t * pFanout;
     int i;
     // if we encountered a node outside of the TFO cone of the fanins, quit
     if ( Abc_ObjIsCo(pNode) || pNode->Level > (unsigned)LevelLimit )
         return 0;
     // if we encountered a node on the boundary, add it to the roots
     if ( pNode->fMarkA )
     {
         Vec_PtrPushUnique( vRoots, pNode );
         return 1;
     }
     // mark the node with the current TravId (needed to have all internal nodes marked)
     Abc_NodeSetTravIdCurrent( pNode );
     // traverse the fanouts
     Abc_ObjForEachFanout( pNode, pFanout, i )
         if ( !Abc_NtkRRTfo_rec( pFanout, vRoots, LevelLimit ) )
             return 0;
     return 1;
 }

int Abc_NtkRRUpdate	(	Abc_Ntk_t *	pNtk,
		Abc_Obj_t *	pNode,
		Abc_Obj_t *	pFanin,
		Abc_Obj_t *	pFanout
	)

static

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

Synopsis [Updates the network after redundancy removal.]

Description [This procedure assumes that non-control value of the fanin was proved redundant. It is okay to concentrate on non-control values because the control values can be seen as redundancy of the fanout edge.]

SideEffects []

SeeAlso []

Definition at line 385 of file abcRr.c.

 {
     Abc_Obj_t * pNodeNew, * pFanoutNew;
     assert( pFanout == NULL );
     assert( !Abc_ObjIsComplement(pNode) );
     assert( !Abc_ObjIsComplement(pFanin) );
     assert( !Abc_ObjIsComplement(pFanout) );
     // find the node after redundancy removal
     if ( pFanin == Abc_ObjFanin0(pNode) )
         pNodeNew = Abc_ObjChild1(pNode);
     else if ( pFanin == Abc_ObjFanin1(pNode) )
         pNodeNew = Abc_ObjChild0(pNode);
     else assert( 0 );
     // replace
     if ( pFanout == NULL )
     {
         Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pNode, pNodeNew, 1 );
         return 1;
     }
     // find the fanout after redundancy removal
     if ( pNode == Abc_ObjFanin0(pFanout) )
         pFanoutNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC0(pFanout)), Abc_ObjChild1(pFanout) );
     else if ( pNode == Abc_ObjFanin1(pFanout) )
         pFanoutNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC1(pFanout)), Abc_ObjChild0(pFanout) );
     else assert( 0 );
     // replace
     Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pFanout, pFanoutNew, 1 );
     return 1;
 }

int Abc_NtkRRWindow ( Abc_RRMan_t * p )

static

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

Synopsis [Constructs window for checking RR.]

Description [If the window (p->pWnd) with the given scope (p->nFaninLevels, p->nFanoutLevels) cannot be constructed, returns 0. Otherwise, returns 1. The levels are measured from the fanin node (pFanin) and the fanout node (pEdgeFanout), respectively.]

SideEffects []

SeeAlso []

Definition at line 429 of file abcRr.c.

 {
     Abc_Obj_t * pObj, * pEdgeFanin, * pEdgeFanout;
     int i, LevelMin, LevelMax, RetValue;
 
     // get the edge
     pEdgeFanout = p->pFanout? p->pFanout : p->pNode;
     pEdgeFanin  = p->pFanout? p->pNode : p->pFanin;
     // get the minimum and maximum levels of the window
     LevelMin = Abc_MaxInt( 0, ((int)p->pFanin->Level) - p->nFaninLevels );
     LevelMax = (int)pEdgeFanout->Level + p->nFanoutLevels;
 
     // start the TFI leaves with the fanin
     Abc_NtkIncrementTravId( p->pNtk );
     Abc_NodeSetTravIdCurrent( p->pFanin );
     Vec_PtrPush( p->vFaninLeaves, p->pFanin );
     // mark the TFI cone and collect the leaves down to the given level
     while ( Abc_NtkRRTfi_int(p->vFaninLeaves, LevelMin) );
 
     // mark the leaves with the new TravId
     Abc_NtkIncrementTravId( p->pNtk );
     Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninLeaves, pObj, i )
         Abc_NodeSetTravIdCurrent( pObj );
     // traverse the TFO cone of the leaves (while skipping the edge)
     // (a) mark the nodes in the cone using the current TravId
     // (b) collect the nodes that have external fanouts into p->vFanoutRoots
     while ( Abc_NtkRRTfo_int(p->vFaninLeaves, p->vFanoutRoots, LevelMax, pEdgeFanin, pEdgeFanout) );
 
     // mark the fanout roots
     Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanoutRoots, pObj, i )
         pObj->fMarkA = 1;
     // collect roots reachable from the fanout (p->vRoots)
     RetValue = Abc_NtkRRTfo_rec( pEdgeFanout, p->vRoots, LevelMax + 1 );
     // unmark the fanout roots
     Vec_PtrForEachEntry( Abc_Obj_t *, p->vFanoutRoots, pObj, i )
         pObj->fMarkA = 0;
 
     // return if the window is infeasible
     if ( RetValue == 0 )
         return 0;
 
     // collect the DFS-ordered new cone (p->vCone) and new leaves (p->vLeaves)
     // using the previous marks coming from the TFO cone
     Abc_NtkIncrementTravId( p->pNtk );
     Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
         Abc_NtkRRTfi_rec( pObj, p->vLeaves, p->vCone, LevelMin );
 
     // create a new network
     p->pWnd = Abc_NtkWindow( p->pNtk, p->vLeaves, p->vCone, p->vRoots );
     return 1;
 }

Abc_Ntk_t * Abc_NtkWindow	(	Abc_Ntk_t *	pNtk,
		Vec_Ptr_t *	vLeaves,
		Vec_Ptr_t *	vCone,
		Vec_Ptr_t *	vRoots
	)

static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 676 of file abcRr.c.

 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj;
     int fCheck = 1;
     int i;
     assert( Abc_NtkIsStrash(pNtk) );
     // start the network
     pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav( "temp" );
     // map the constant nodes
     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
     // create and map the PIs
     Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pObj, i )
         pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
     // copy the AND gates
     Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, i )
         pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
     // compare the number of nodes before and after
     if ( Vec_PtrSize(vCone) != Abc_NtkNodeNum(pNtkNew) )
         printf( "Warning: Structural hashing during windowing reduced %d nodes (this is a bug).\n",
             Vec_PtrSize(vCone) - Abc_NtkNodeNum(pNtkNew) );
     // create the POs
     Vec_PtrForEachEntry( Abc_Obj_t *, vRoots, pObj, i )
     {
         assert( !Abc_ObjIsComplement(pObj->pCopy) );
         Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pObj->pCopy );
     }
     // add the PI/PO names
     Abc_NtkAddDummyPiNames( pNtkNew );
     Abc_NtkAddDummyPoNames( pNtkNew );
     // check
     if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkWindow: The network check has failed.\n" );
         return NULL;
     }
     return pNtkNew;
 }

void Abc_RRManClean ( Abc_RRMan_t * p )

static

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

Synopsis [Clean the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 325 of file abcRr.c.

 {
     p->pNode   = NULL; 
     p->pFanin  = NULL; 
     p->pFanout = NULL; 
     Vec_PtrClear( p->vFaninLeaves  );  
     Vec_PtrClear( p->vFanoutRoots  );  
     Vec_PtrClear( p->vLeaves );  
     Vec_PtrClear( p->vCone );  
     Vec_PtrClear( p->vRoots );  
     if ( p->pWnd )   Abc_NtkDelete( p->pWnd );
     if ( p->pMiter ) Abc_NtkDelete( p->pMiter );
     p->pWnd   = NULL;
     p->pMiter = NULL;
 }

void Abc_RRManPrintStats ( Abc_RRMan_t * p )

static

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

Synopsis [Stop the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 298 of file abcRr.c.

 {
     double Ratio = 100.0*(p->nNodesOld  - Abc_NtkNodeNum(p->pNtk))/p->nNodesOld;
     printf( "Redundancy removal statistics:\n" );
     printf( "Edges tried     = %6d.\n", p->nEdgesTried );
     printf( "Edges removed   = %6d. (%5.2f %%)\n", p->nEdgesRemoved, 100.0*p->nEdgesRemoved/p->nEdgesTried );
     printf( "Node gain       = %6d. (%5.2f %%)\n", p->nNodesOld  - Abc_NtkNodeNum(p->pNtk), Ratio );
     printf( "Level gain      = %6d.\n", p->nLevelsOld - Abc_AigLevel(p->pNtk) );
     ABC_PRT( "Windowing      ", p->timeWindow );
     ABC_PRT( "Miter          ", p->timeMiter );
     ABC_PRT( "    Construct  ", p->timeMiter - p->timeProve );
     ABC_PRT( "    Prove      ", p->timeProve );
     ABC_PRT( "Update         ", p->timeUpdate );
     ABC_PRT( "TOTAL          ", p->timeTotal );
 }

Abc_RRMan_t * Abc_RRManStart ( )

static

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

Synopsis [Start the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 248 of file abcRr.c.

 {
     Abc_RRMan_t * p;
     p = ABC_ALLOC( Abc_RRMan_t, 1 );
     memset( p, 0, sizeof(Abc_RRMan_t) );
     p->vFaninLeaves  = Vec_PtrAlloc( 100 );  // the leaves of the fanin cone
     p->vFanoutRoots  = Vec_PtrAlloc( 100 );  // the roots of the fanout cone
     p->vLeaves       = Vec_PtrAlloc( 100 );  // the leaves of the window
     p->vCone         = Vec_PtrAlloc( 100 );  // the internal nodes of the window
     p->vRoots        = Vec_PtrAlloc( 100 );  // the roots of the window
     p->pParams       = ABC_ALLOC( Prove_Params_t, 1 );
     memset( p->pParams, 0, sizeof(Prove_Params_t) );
     Prove_ParamsSetDefault( p->pParams );
     return p;
 }

void Abc_RRManStop ( Abc_RRMan_t * p )

static

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

Synopsis [Stop the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file abcRr.c.

 {
     Abc_RRManClean( p );
     Vec_PtrFree( p->vFaninLeaves  );  
     Vec_PtrFree( p->vFanoutRoots  );  
     Vec_PtrFree( p->vLeaves );  
     Vec_PtrFree( p->vCone );  
     Vec_PtrFree( p->vRoots );  
     ABC_FREE( p->pParams );
     ABC_FREE( p );
 }

void Sim_CollectNodes_rec	(	Abc_Obj_t *	pRoot,
		Vec_Ptr_t *	vField
	)

static

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

Synopsis [Collects nodes starting from the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 899 of file abcRr.c.

 {
     Abc_Obj_t * pFanin;
     int i;
     if ( Abc_NodeIsTravIdCurrent(pRoot) )
         return;
     if ( !Abc_NodeIsTravIdPrevious(pRoot) )
         return;
     Abc_NodeSetTravIdCurrent( pRoot );
     Abc_ObjForEachFanin( pRoot, pFanin, i )
         Sim_CollectNodes_rec( pFanin, vField );
     if ( !Abc_ObjIsCo(pRoot) )
         pRoot->pData = (void *)(ABC_PTRUINT_T)Vec_PtrSize(vField);
     Vec_PtrPush( vField, pRoot );
 }

void Sim_SimulateCollected	(	Vec_Str_t *	vTargets,
		Vec_Ptr_t *	vNodes,
		Vec_Ptr_t *	vField
	)

static

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

Synopsis [Simulate the given nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 926 of file abcRr.c.

 {
     Abc_Obj_t * pObj, * pFanin0, * pFanin1, * pDisproved;
     Vec_Ptr_t * vSims;
     unsigned * pUnsigned, * pUnsignedF;
     int i, k, Phase, fCompl;
     // get simulation info
     vSims = Sim_UtilInfoAlloc( Vec_PtrSize(vField), Vec_PtrSize(vNodes), 0 );
     // simulate the nodes
     Vec_PtrForEachEntry( Abc_Obj_t *, vField, pObj, i )
     {
         if ( Abc_ObjIsCi(pObj) )
         {
             pUnsigned = (unsigned *)Vec_PtrEntry( vSims, i );
             for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
                 pUnsigned[k] = (unsigned)(ABC_PTRUINT_T)pObj->pCopy;
             continue;
         }
         if ( Abc_ObjIsCo(pObj) )
         {
             pUnsigned  = (unsigned *)Vec_PtrEntry( vSims, i );
             pUnsignedF = (unsigned *)Vec_PtrEntry( vSims, (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pData );
             if ( Abc_ObjFaninC0(pObj) )
                 for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
                     pUnsigned[k] = ~pUnsignedF[k];
             else
                 for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
                     pUnsigned[k] = pUnsignedF[k];
             // update targets
             for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
             {
                 if ( pUnsigned[k] == (unsigned)(ABC_PTRUINT_T)pObj->pData )
                     continue;
                 pDisproved = (Abc_Obj_t *)Vec_PtrEntry( vNodes, k );
                 fCompl = Abc_ObjIsComplement(pDisproved);
                 pDisproved = Abc_ObjRegular(pDisproved);
                 Phase = Vec_StrEntry( vTargets, pDisproved->Id );
                 if ( fCompl )
                     Phase = (Phase & 2);
                 else
                     Phase = (Phase & 1);
                 Vec_StrWriteEntry( vTargets, pDisproved->Id, (char)Phase );
             }
             continue;
         }
         // simulate the node
         pFanin0 = Abc_ObjFanin0(pObj);
         pFanin1 = Abc_ObjFanin1(pObj);
     }
 }

void Sim_TraverseNodes_rec	(	Abc_Obj_t *	pRoot,
		Vec_Str_t *	vTargets,
		Vec_Ptr_t *	vNodes
	)

static

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

Synopsis [Collects nodes starting from the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 869 of file abcRr.c.

 {
     Abc_Obj_t * pFanout;
     char Entry;
     int k;
     if ( Abc_NodeIsTravIdCurrent(pRoot) )
         return;
     Abc_NodeSetTravIdCurrent( pRoot );
     // save the reached targets
     Entry = Vec_StrEntry(vTargets, pRoot->Id);
     if ( Entry & 1 )
         Vec_PtrPush( vNodes, Abc_ObjNot(pRoot) );
     if ( Entry & 2 )
         Vec_PtrPush( vNodes, pRoot );
     // explore the fanouts
     Abc_ObjForEachFanout( pRoot, pFanout, k )
         Sim_TraverseNodes_rec( pFanout, vTargets, vNodes );
 }

Data Structures

Typedefs

Functions

Typedef Documentation

Function Documentation