src/base/abci/abcRr.c File Reference

#include "abc.h"
#include "fraig.h"
#include "sim.h"
Include dependency graph for abcRr.c:

Go to the source code of this file.

Data Structures

struct  Abc_RRMan_t_

Typedefs

typedef struct Abc_RRMan_t_ Abc_RRMan_t

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)
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 struct Abc_RRMan_t_ Abc_RRMan_t

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

] DECLARATIONS ///

Definition at line 29 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 95 of file abcRr.c.

00096 {
00097     ProgressBar * pProgress;
00098     Abc_RRMan_t * p;
00099     Abc_Obj_t * pNode, * pFanin, * pFanout;
00100     int i, k, m, nNodes, RetValue, clk, clkTotal = clock();
00101     // start the manager
00102     p = Abc_RRManStart( nFaninLevels, nFanoutLevels );
00103     p->pNtk          = pNtk;
00104     p->nFaninLevels  = nFaninLevels;
00105     p->nFanoutLevels = nFanoutLevels;
00106     p->nNodesOld     = Abc_NtkNodeNum(pNtk);
00107     p->nLevelsOld    = Abc_AigLevel(pNtk);
00108     // remember latch values
00109 //    Abc_NtkForEachLatch( pNtk, pNode, i )
00110 //        pNode->pNext = pNode->pData;
00111     // go through the nodes
00112     Abc_NtkCleanCopy(pNtk);
00113     nNodes = Abc_NtkObjNumMax(pNtk);
00114     Abc_NtkRRSimulateStart(pNtk);
00115     pProgress = Extra_ProgressBarStart( stdout, nNodes );
00116     Abc_NtkForEachNode( pNtk, pNode, i )
00117     {
00118         Extra_ProgressBarUpdate( pProgress, i, NULL );
00119         // stop if all nodes have been tried once
00120         if ( i >= nNodes )
00121             break;
00122         // skip the constant node
00123 //        if ( Abc_NodeIsConst(pNode) )
00124 //            continue;
00125         // skip persistant nodes
00126         if ( Abc_NodeIsPersistant(pNode) )
00127             continue;
00128         // skip the nodes with many fanouts
00129         if ( Abc_ObjFanoutNum(pNode) > 1000 )
00130             continue;
00131         // construct the window
00132         if ( !fUseFanouts )
00133         {
00134             Abc_ObjForEachFanin( pNode, pFanin, k )
00135             {
00136                 // skip the nodes with only one fanout (tree nodes)
00137                 if ( Abc_ObjFanoutNum(pFanin) == 1 )
00138                     continue;
00139 /*
00140                 if ( pFanin->Id == 228 && pNode->Id == 2649 )
00141                 {
00142                     int k = 0;
00143                 }
00144 */
00145                 p->nEdgesTried++;
00146                 Abc_RRManClean( p );
00147                 p->pNode   = pNode;
00148                 p->pFanin  = pFanin;
00149                 p->pFanout = NULL;
00150 
00151                 clk = clock();
00152                 RetValue = Abc_NtkRRWindow( p );
00153                 p->timeWindow += clock() - clk;
00154                 if ( !RetValue )
00155                     continue;
00156 /*
00157                 if ( pFanin->Id == 228 && pNode->Id == 2649 )
00158                 {
00159                     Abc_NtkShowAig( p->pWnd, 0 );
00160                 }
00161 */
00162                 clk = clock();
00163                 RetValue = Abc_NtkRRProve( p );
00164                 p->timeMiter += clock() - clk;
00165                 if ( !RetValue )
00166                     continue;
00167 //printf( "%d -> %d (%d)\n", pFanin->Id, pNode->Id, k );
00168 
00169                 clk = clock();
00170                 Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
00171                 p->timeUpdate += clock() - clk;
00172 
00173                 p->nEdgesRemoved++;
00174                 break;
00175             }
00176             continue;
00177         }
00178         // use the fanouts
00179         Abc_ObjForEachFanin( pNode, pFanin, k )
00180         Abc_ObjForEachFanout( pNode, pFanout, m )
00181         {
00182             // skip the nodes with only one fanout (tree nodes)
00183 //            if ( Abc_ObjFanoutNum(pFanin) == 1 && Abc_ObjFanoutNum(pNode) == 1 )
00184 //                continue;
00185 
00186             p->nEdgesTried++;
00187             Abc_RRManClean( p );
00188             p->pNode   = pNode;
00189             p->pFanin  = pFanin;
00190             p->pFanout = pFanout;
00191 
00192             clk = clock();
00193             RetValue = Abc_NtkRRWindow( p );
00194             p->timeWindow += clock() - clk;
00195             if ( !RetValue )
00196                 continue;
00197 
00198             clk = clock();
00199             RetValue = Abc_NtkRRProve( p );
00200             p->timeMiter += clock() - clk;
00201             if ( !RetValue )
00202                 continue;
00203 
00204             clk = clock();
00205             Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
00206             p->timeUpdate += clock() - clk;
00207 
00208             p->nEdgesRemoved++;
00209             break;
00210         }
00211     }
00212     Abc_NtkRRSimulateStop(pNtk);
00213     Extra_ProgressBarStop( pProgress );
00214     p->timeTotal = clock() - clkTotal;
00215     if ( fVerbose )
00216         Abc_RRManPrintStats( p );
00217     Abc_RRManStop( p );
00218     // restore latch values
00219 //    Abc_NtkForEachLatch( pNtk, pNode, i )
00220 //        pNode->pData = pNode->pNext, pNode->pNext = NULL;
00221     // put the nodes into the DFS order and reassign their IDs
00222     Abc_NtkReassignIds( pNtk );
00223     Abc_NtkLevel( pNtk );
00224     // check
00225     if ( !Abc_NtkCheck( pNtk ) )
00226     {
00227         printf( "Abc_NtkRR: The network check has failed.\n" );
00228         return 0;
00229     }
00230     return 1;
00231 }

int Abc_NtkRRProve ( Abc_RRMan_t *  p  )  [static]

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 348 of file abcRr.c.

00349 {
00350     Abc_Ntk_t * pWndCopy;
00351     int RetValue, clk;
00352 //    Abc_NtkShowAig( p->pWnd, 0 );
00353     pWndCopy = Abc_NtkDup( p->pWnd );
00354     Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
00355     if ( !Abc_NtkIsDfsOrdered(pWndCopy) )
00356         Abc_NtkReassignIds(pWndCopy);
00357     p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0 );
00358     Abc_NtkDelete( pWndCopy );
00359 clk = clock();
00360     RetValue  = Abc_NtkMiterProve( &p->pMiter, p->pParams );
00361 p->timeProve += clock() - clk;
00362     if ( RetValue == 1 )
00363         return 1;
00364     return 0;
00365 }

Vec_Str_t* Abc_NtkRRSimulate ( Abc_Ntk_t *  pNtk  ) 

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

Synopsis [Simulation to detect non-redundant edges.]

Description []

SideEffects []

SeeAlso []

Definition at line 785 of file abcRr.c.

00786 {
00787     Vec_Ptr_t * vNodes, * vField;
00788     Vec_Str_t * vTargets;
00789     Abc_Obj_t * pObj;
00790     unsigned uData, uData0, uData1;
00791     int PrevCi, Phase, i, k;
00792 
00793     // start the candidates
00794     vTargets = Vec_StrStart( Abc_NtkObjNumMax(pNtk) + 1 );
00795     Abc_NtkForEachNode( pNtk, pObj, i )
00796     {
00797         Phase = ((Abc_ObjFanoutNum(Abc_ObjFanin1(pObj)) > 1) << 1);
00798         Phase |= (Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) > 1);
00799         Vec_StrWriteEntry( vTargets, pObj->Id, (char)Phase );
00800     }
00801 
00802     // simulate patters and store them in copy
00803     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)~((unsigned)0);
00804     Abc_NtkForEachCi( pNtk, pObj, i )
00805         pObj->pCopy = (Abc_Obj_t *)SIM_RANDOM_UNSIGNED;
00806     Abc_NtkForEachNode( pNtk, pObj, i )
00807     {
00808         if ( i == 0 ) continue;
00809         uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
00810         uData1 = (unsigned)Abc_ObjFanin1(pObj)->pData;
00811         uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
00812         uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
00813         pObj->pCopy = (Abc_Obj_t *)uData;
00814     }
00815     // store the result in data
00816     Abc_NtkForEachCo( pNtk, pObj, i )
00817     {
00818         uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
00819         if ( Abc_ObjFaninC0(pObj) )
00820             pObj->pData = (void *)~uData0;
00821         else
00822             pObj->pData = (void *)uData0;
00823     }
00824 
00825     // refine the candidates
00826     for ( PrevCi = 0; PrevCi < Abc_NtkCiNum(pNtk); PrevCi = i )
00827     {
00828         vNodes = Vec_PtrAlloc( 10 );
00829         Abc_NtkIncrementTravId( pNtk );
00830         for ( i = PrevCi; i < Abc_NtkCiNum(pNtk); i++ )
00831         {
00832             Sim_TraverseNodes_rec( Abc_NtkCi(pNtk, i), vTargets, vNodes );
00833             if ( Vec_PtrSize(vNodes) > 128 )
00834                 break;
00835         }
00836         // collect the marked nodes in the topological order
00837         vField = Vec_PtrAlloc( 10 );
00838         Abc_NtkIncrementTravId( pNtk );
00839         Abc_NtkForEachCo( pNtk, pObj, k )
00840             Sim_CollectNodes_rec( pObj, vField );
00841 
00842         // simulate these nodes
00843         Sim_SimulateCollected( vTargets, vNodes, vField );
00844         // prepare for the next loop
00845         Vec_PtrFree( vNodes );
00846     }
00847 
00848     // clean
00849     Abc_NtkForEachObj( pNtk, pObj, i )
00850         pObj->pData = NULL;
00851     return vTargets;
00852 }

void Abc_NtkRRSimulateStart ( Abc_Ntk_t *  pNtk  )  [static]

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 725 of file abcRr.c.

00726 {
00727     Abc_Obj_t * pObj;
00728     unsigned uData, uData0, uData1;
00729     int i;
00730     Abc_AigConst1(pNtk)->pData = (void *)~((unsigned)0);
00731     Abc_NtkForEachCi( pNtk, pObj, i )
00732         pObj->pData = (void *)SIM_RANDOM_UNSIGNED;
00733     Abc_NtkForEachNode( pNtk, pObj, i )
00734     {
00735         if ( i == 0 ) continue;
00736         uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
00737         uData1 = (unsigned)Abc_ObjFanin1(pObj)->pData;
00738         uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
00739         uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
00740         assert( pObj->pData == NULL );
00741         pObj->pData = (void *)uData;
00742     }
00743 }

void Abc_NtkRRSimulateStop ( Abc_Ntk_t *  pNtk  )  [static]

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 756 of file abcRr.c.

00757 {
00758     Abc_Obj_t * pObj;
00759     int i;
00760     Abc_NtkForEachObj( pNtk, pObj, i )
00761         pObj->pData = NULL;
00762 }

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 487 of file abcRr.c.

00488 {
00489     Abc_Obj_t * pObj, * pNext;
00490     int i, k, LevelMax, nSize;
00491     assert( LevelLimit >= 0 );
00492     // find the maximum level of leaves
00493     LevelMax = 0;
00494     Vec_PtrForEachEntry( vLeaves, pObj, i )
00495         if ( LevelMax < (int)pObj->Level )
00496             LevelMax = pObj->Level;
00497     // if the nodes are all PIs, LevelMax == 0
00498     if ( LevelMax <= LevelLimit )
00499         return 0;
00500     // expand the nodes with the minimum level
00501     nSize = Vec_PtrSize(vLeaves);
00502     Vec_PtrForEachEntryStop( vLeaves, pObj, i, nSize )
00503     {
00504         if ( LevelMax != (int)pObj->Level )
00505             continue;
00506         Abc_ObjForEachFanin( pObj, pNext, k )
00507         {
00508             if ( Abc_NodeIsTravIdCurrent(pNext) )
00509                 continue;
00510             Abc_NodeSetTravIdCurrent( pNext );
00511             Vec_PtrPush( vLeaves, pNext );
00512         }
00513     }
00514     // remove old nodes (cannot remove a PI)
00515     k = 0;
00516     Vec_PtrForEachEntry( vLeaves, pObj, i )
00517     {
00518         if ( LevelMax == (int)pObj->Level )
00519             continue;
00520         Vec_PtrWriteEntry( vLeaves, k++, pObj );
00521     }
00522     Vec_PtrShrink( vLeaves, k );
00523     if ( Vec_PtrSize(vLeaves) > 2000 )
00524         return 0;
00525     return 1;
00526 }

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 637 of file abcRr.c.

00638 {
00639     Abc_Obj_t * pFanin;
00640     int i;
00641     // skip visited nodes
00642     if ( Abc_NodeIsTravIdCurrent(pNode) )
00643         return;
00644     // add node to leaves if it is not in TFI cone of the leaves (marked before) or below the limit
00645     if ( !Abc_NodeIsTravIdPrevious(pNode) || (int)pNode->Level <= LevelLimit )
00646     {
00647         Abc_NodeSetTravIdCurrent( pNode );
00648         Vec_PtrPush( vLeaves, pNode );
00649         return;
00650     }
00651     // mark the node as visited
00652     Abc_NodeSetTravIdCurrent( pNode );
00653     // call for the node's fanins
00654     Abc_ObjForEachFanin( pNode, pFanin, i )
00655         Abc_NtkRRTfi_rec( pFanin, vLeaves, vCone, LevelLimit );
00656     // add the node to the cone in topological order
00657     Vec_PtrPush( vCone, pNode );
00658 }

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 539 of file abcRr.c.

00540 {
00541     Abc_Obj_t * pObj, * pNext;
00542     int i, k, LevelMin, nSize, fObjIsRoot;
00543     // find the minimum level of leaves
00544     LevelMin = ABC_INFINITY;
00545     Vec_PtrForEachEntry( vLeaves, pObj, i )
00546         if ( LevelMin > (int)pObj->Level )
00547             LevelMin = pObj->Level;
00548     // if the minimum level exceed the limit, we are done
00549     if ( LevelMin > LevelLimit )
00550         return 0;
00551     // expand the nodes with the minimum level
00552     nSize = Vec_PtrSize(vLeaves);
00553     Vec_PtrForEachEntryStop( vLeaves, pObj, i, nSize )
00554     {
00555         if ( LevelMin != (int)pObj->Level )
00556             continue;
00557         fObjIsRoot = 0;
00558         Abc_ObjForEachFanout( pObj, pNext, k )
00559         {
00560             // check if the fanout is outside of the cone
00561             if ( Abc_ObjIsCo(pNext) || pNext->Level > (unsigned)LevelLimit )
00562             {
00563                 fObjIsRoot = 1;
00564                 continue;
00565             }
00566             // skip the edge under check
00567             if ( pObj == pEdgeFanin && pNext == pEdgeFanout )
00568                 continue;
00569             // skip the visited fanouts
00570             if ( Abc_NodeIsTravIdCurrent(pNext) )
00571                 continue;
00572             Abc_NodeSetTravIdCurrent( pNext );
00573             Vec_PtrPush( vLeaves, pNext );
00574         }
00575         if ( fObjIsRoot )
00576             Vec_PtrPush( vRoots, pObj );
00577     }
00578     // remove old nodes
00579     k = 0;
00580     Vec_PtrForEachEntry( vLeaves, pObj, i )
00581     {
00582         if ( LevelMin == (int)pObj->Level )
00583             continue;
00584         Vec_PtrWriteEntry( vLeaves, k++, pObj );
00585     }
00586     Vec_PtrShrink( vLeaves, k );
00587     if ( Vec_PtrSize(vLeaves) > 2000 )
00588         return 0;
00589     return 1;
00590 }

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 604 of file abcRr.c.

00605 {
00606     Abc_Obj_t * pFanout;
00607     int i;
00608     // if we encountered a node outside of the TFO cone of the fanins, quit
00609     if ( Abc_ObjIsCo(pNode) || pNode->Level > (unsigned)LevelLimit )
00610         return 0;
00611     // if we encountered a node on the boundary, add it to the roots
00612     if ( pNode->fMarkA )
00613     {
00614         Vec_PtrPushUnique( vRoots, pNode );
00615         return 1;
00616     }
00617     // mark the node with the current TravId (needed to have all internal nodes marked)
00618     Abc_NodeSetTravIdCurrent( pNode );
00619     // traverse the fanouts
00620     Abc_ObjForEachFanout( pNode, pFanout, i )
00621         if ( !Abc_NtkRRTfo_rec( pFanout, vRoots, LevelLimit ) )
00622             return 0;
00623     return 1;
00624 }

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 380 of file abcRr.c.

00381 {
00382     Abc_Obj_t * pNodeNew, * pFanoutNew;
00383     assert( pFanout == NULL );
00384     assert( !Abc_ObjIsComplement(pNode) );
00385     assert( !Abc_ObjIsComplement(pFanin) );
00386     assert( !Abc_ObjIsComplement(pFanout) );
00387     // find the node after redundancy removal
00388     if ( pFanin == Abc_ObjFanin0(pNode) )
00389         pNodeNew = Abc_ObjChild1(pNode);
00390     else if ( pFanin == Abc_ObjFanin1(pNode) )
00391         pNodeNew = Abc_ObjChild0(pNode);
00392     else assert( 0 );
00393     // replace
00394     if ( pFanout == NULL )
00395     {
00396         Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew, 1 );
00397         return 1;
00398     }
00399     // find the fanout after redundancy removal
00400     if ( pNode == Abc_ObjFanin0(pFanout) )
00401         pFanoutNew = Abc_AigAnd( pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC0(pFanout)), Abc_ObjChild1(pFanout) );
00402     else if ( pNode == Abc_ObjFanin1(pFanout) )
00403         pFanoutNew = Abc_AigAnd( pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC1(pFanout)), Abc_ObjChild0(pFanout) );
00404     else assert( 0 );
00405     // replace
00406     Abc_AigReplace( pNtk->pManFunc, pFanout, pFanoutNew, 1 );
00407     return 1;
00408 }

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 424 of file abcRr.c.

00425 {
00426     Abc_Obj_t * pObj, * pEdgeFanin, * pEdgeFanout;
00427     int i, LevelMin, LevelMax, RetValue;
00428 
00429     // get the edge
00430     pEdgeFanout = p->pFanout? p->pFanout : p->pNode;
00431     pEdgeFanin  = p->pFanout? p->pNode : p->pFanin;
00432     // get the minimum and maximum levels of the window
00433     LevelMin = ABC_MAX( 0, ((int)p->pFanin->Level) - p->nFaninLevels );
00434     LevelMax = (int)pEdgeFanout->Level + p->nFanoutLevels;
00435 
00436     // start the TFI leaves with the fanin
00437     Abc_NtkIncrementTravId( p->pNtk );
00438     Abc_NodeSetTravIdCurrent( p->pFanin );
00439     Vec_PtrPush( p->vFaninLeaves, p->pFanin );
00440     // mark the TFI cone and collect the leaves down to the given level
00441     while ( Abc_NtkRRTfi_int(p->vFaninLeaves, LevelMin) );
00442 
00443     // mark the leaves with the new TravId
00444     Abc_NtkIncrementTravId( p->pNtk );
00445     Vec_PtrForEachEntry( p->vFaninLeaves, pObj, i )
00446         Abc_NodeSetTravIdCurrent( pObj );
00447     // traverse the TFO cone of the leaves (while skipping the edge)
00448     // (a) mark the nodes in the cone using the current TravId
00449     // (b) collect the nodes that have external fanouts into p->vFanoutRoots
00450     while ( Abc_NtkRRTfo_int(p->vFaninLeaves, p->vFanoutRoots, LevelMax, pEdgeFanin, pEdgeFanout) );
00451 
00452     // mark the fanout roots
00453     Vec_PtrForEachEntry( p->vFanoutRoots, pObj, i )
00454         pObj->fMarkA = 1;
00455     // collect roots reachable from the fanout (p->vRoots)
00456     RetValue = Abc_NtkRRTfo_rec( pEdgeFanout, p->vRoots, LevelMax + 1 );
00457     // unmark the fanout roots
00458     Vec_PtrForEachEntry( p->vFanoutRoots, pObj, i )
00459         pObj->fMarkA = 0;
00460 
00461     // return if the window is infeasible
00462     if ( RetValue == 0 )
00463         return 0;
00464 
00465     // collect the DFS-ordered new cone (p->vCone) and new leaves (p->vLeaves)
00466     // using the previous marks coming from the TFO cone
00467     Abc_NtkIncrementTravId( p->pNtk );
00468     Vec_PtrForEachEntry( p->vRoots, pObj, i )
00469         Abc_NtkRRTfi_rec( pObj, p->vLeaves, p->vCone, LevelMin );
00470 
00471     // create a new network
00472     p->pWnd = Abc_NtkWindow( p->pNtk, p->vLeaves, p->vCone, p->vRoots );
00473     return 1;
00474 }

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 671 of file abcRr.c.

00672 {
00673     Abc_Ntk_t * pNtkNew; 
00674     Abc_Obj_t * pObj;
00675     int fCheck = 1;
00676     int i;
00677     assert( Abc_NtkIsStrash(pNtk) );
00678     // start the network
00679     pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
00680     // duplicate the name and the spec
00681     pNtkNew->pName = Extra_UtilStrsav( "temp" );
00682     // map the constant nodes
00683     Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
00684     // create and map the PIs
00685     Vec_PtrForEachEntry( vLeaves, pObj, i )
00686         pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
00687     // copy the AND gates
00688     Vec_PtrForEachEntry( vCone, pObj, i )
00689         pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
00690     // compare the number of nodes before and after
00691     if ( Vec_PtrSize(vCone) != Abc_NtkNodeNum(pNtkNew) )
00692         printf( "Warning: Structural hashing during windowing reduced %d nodes (this is a bug).\n",
00693             Vec_PtrSize(vCone) - Abc_NtkNodeNum(pNtkNew) );
00694     // create the POs
00695     Vec_PtrForEachEntry( vRoots, pObj, i )
00696     {
00697         assert( !Abc_ObjIsComplement(pObj->pCopy) );
00698         Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pObj->pCopy );
00699     }
00700     // add the PI/PO names
00701     Abc_NtkAddDummyPiNames( pNtkNew );
00702     Abc_NtkAddDummyPoNames( pNtkNew );
00703     Abc_NtkAddDummyAssertNames( pNtkNew );
00704     // check
00705     if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
00706     {
00707         printf( "Abc_NtkWindow: The network check has failed.\n" );
00708         return NULL;
00709     }
00710     return pNtkNew;
00711 }

void Abc_RRManClean ( Abc_RRMan_t *  p  )  [static]

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

Synopsis [Clean the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file abcRr.c.

00322 {
00323     p->pNode   = NULL; 
00324     p->pFanin  = NULL; 
00325     p->pFanout = NULL; 
00326     Vec_PtrClear( p->vFaninLeaves  );  
00327     Vec_PtrClear( p->vFanoutRoots  );  
00328     Vec_PtrClear( p->vLeaves );  
00329     Vec_PtrClear( p->vCone );  
00330     Vec_PtrClear( p->vRoots );  
00331     if ( p->pWnd )   Abc_NtkDelete( p->pWnd );
00332     if ( p->pMiter ) Abc_NtkDelete( p->pMiter );
00333     p->pWnd   = NULL;
00334     p->pMiter = NULL;
00335 }

void Abc_RRManPrintStats ( Abc_RRMan_t *  p  )  [static]

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

Synopsis [Stop the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 294 of file abcRr.c.

00295 {
00296     double Ratio = 100.0*(p->nNodesOld  - Abc_NtkNodeNum(p->pNtk))/p->nNodesOld;
00297     printf( "Redundancy removal statistics:\n" );
00298     printf( "Edges tried     = %6d.\n", p->nEdgesTried );
00299     printf( "Edges removed   = %6d. (%5.2f %%)\n", p->nEdgesRemoved, 100.0*p->nEdgesRemoved/p->nEdgesTried );
00300     printf( "Node gain       = %6d. (%5.2f %%)\n", p->nNodesOld  - Abc_NtkNodeNum(p->pNtk), Ratio );
00301     printf( "Level gain      = %6d.\n", p->nLevelsOld - Abc_AigLevel(p->pNtk) );
00302     PRT( "Windowing      ", p->timeWindow );
00303     PRT( "Miter          ", p->timeMiter );
00304     PRT( "    Construct  ", p->timeMiter - p->timeProve );
00305     PRT( "    Prove      ", p->timeProve );
00306     PRT( "Update         ", p->timeUpdate );
00307     PRT( "TOTAL          ", p->timeTotal );
00308 }

Abc_RRMan_t * Abc_RRManStart (  )  [static]

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

Synopsis [Start the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 244 of file abcRr.c.

00245 {
00246     Abc_RRMan_t * p;
00247     p = ALLOC( Abc_RRMan_t, 1 );
00248     memset( p, 0, sizeof(Abc_RRMan_t) );
00249     p->vFaninLeaves  = Vec_PtrAlloc( 100 );  // the leaves of the fanin cone
00250     p->vFanoutRoots  = Vec_PtrAlloc( 100 );  // the roots of the fanout cone
00251     p->vLeaves       = Vec_PtrAlloc( 100 );  // the leaves of the window
00252     p->vCone         = Vec_PtrAlloc( 100 );  // the internal nodes of the window
00253     p->vRoots        = Vec_PtrAlloc( 100 );  // the roots of the window
00254     p->pParams       = ALLOC( Prove_Params_t, 1 );
00255     memset( p->pParams, 0, sizeof(Prove_Params_t) );
00256     Prove_ParamsSetDefault( p->pParams );
00257     return p;
00258 }

void Abc_RRManStop ( Abc_RRMan_t *  p  )  [static]

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

Synopsis [Stop the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 271 of file abcRr.c.

00272 {
00273     Abc_RRManClean( p );
00274     Vec_PtrFree( p->vFaninLeaves  );  
00275     Vec_PtrFree( p->vFanoutRoots  );  
00276     Vec_PtrFree( p->vLeaves );  
00277     Vec_PtrFree( p->vCone );  
00278     Vec_PtrFree( p->vRoots );  
00279     free( p->pParams );
00280     free( p );
00281 }

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 895 of file abcRr.c.

00896 {
00897     Abc_Obj_t * pFanin;
00898     int i;
00899     if ( Abc_NodeIsTravIdCurrent(pRoot) )
00900         return;
00901     if ( !Abc_NodeIsTravIdPrevious(pRoot) )
00902         return;
00903     Abc_NodeSetTravIdCurrent( pRoot );
00904     Abc_ObjForEachFanin( pRoot, pFanin, i )
00905         Sim_CollectNodes_rec( pFanin, vField );
00906     if ( !Abc_ObjIsCo(pRoot) )
00907         pRoot->pData = (void *)Vec_PtrSize(vField);
00908     Vec_PtrPush( vField, pRoot );
00909 }

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 922 of file abcRr.c.

00923 {
00924     Abc_Obj_t * pObj, * pFanin0, * pFanin1, * pDisproved;
00925     Vec_Ptr_t * vSims;
00926     unsigned * pUnsigned, * pUnsignedF;
00927     int i, k, Phase, fCompl;
00928     // get simulation info
00929     vSims = Sim_UtilInfoAlloc( Vec_PtrSize(vField), Vec_PtrSize(vNodes), 0 );
00930     // simulate the nodes
00931     Vec_PtrForEachEntry( vField, pObj, i )
00932     {
00933         if ( Abc_ObjIsCi(pObj) )
00934         {
00935             pUnsigned = Vec_PtrEntry( vSims, i );
00936             for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
00937                 pUnsigned[k] = (unsigned)pObj->pCopy;
00938             continue;
00939         }
00940         if ( Abc_ObjIsCo(pObj) )
00941         {
00942             pUnsigned  = Vec_PtrEntry( vSims, i );
00943             pUnsignedF = Vec_PtrEntry( vSims, (int)Abc_ObjFanin0(pObj)->pData );
00944             if ( Abc_ObjFaninC0(pObj) )
00945                 for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
00946                     pUnsigned[k] = ~pUnsignedF[k];
00947             else
00948                 for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
00949                     pUnsigned[k] = pUnsignedF[k];
00950             // update targets
00951             for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
00952             {
00953                 if ( pUnsigned[k] == (unsigned)pObj->pData )
00954                     continue;
00955                 pDisproved = Vec_PtrEntry( vNodes, k );
00956                 fCompl = Abc_ObjIsComplement(pDisproved);
00957                 pDisproved = Abc_ObjRegular(pDisproved);
00958                 Phase = Vec_StrEntry( vTargets, pDisproved->Id );
00959                 if ( fCompl )
00960                     Phase = (Phase & 2);
00961                 else
00962                     Phase = (Phase & 1);
00963                 Vec_StrWriteEntry( vTargets, pDisproved->Id, (char)Phase );
00964             }
00965             continue;
00966         }
00967         // simulate the node
00968         pFanin0 = Abc_ObjFanin0(pObj);
00969         pFanin1 = Abc_ObjFanin1(pObj);
00970     }
00971 }

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 865 of file abcRr.c.

00866 {
00867     Abc_Obj_t * pFanout;
00868     char Entry;
00869     int k;
00870     if ( Abc_NodeIsTravIdCurrent(pRoot) )
00871         return;
00872     Abc_NodeSetTravIdCurrent( pRoot );
00873     // save the reached targets
00874     Entry = Vec_StrEntry(vTargets, pRoot->Id);
00875     if ( Entry & 1 )
00876         Vec_PtrPush( vNodes, Abc_ObjNot(pRoot) );
00877     if ( Entry & 2 )
00878         Vec_PtrPush( vNodes, pRoot );
00879     // explore the fanouts
00880     Abc_ObjForEachFanout( pRoot, pFanout, k )
00881         Sim_TraverseNodes_rec( pFanout, vTargets, vNodes );
00882 }

Generated on Tue Jan 5 12:18:41 2010 for abc70930 by  doxygen 1.6.1