src/aig/fra/fraLcr.c File Reference

#include "fra.h"
Include dependency graph for fraLcr.c:

Go to the source code of this file.

Data Structures

struct  Fra_Lcr_t_

Typedefs

typedef struct Fra_Lcr_t_ Fra_Lcr_t

Functions

Fra_Lcr_t * Lcr_ManAlloc (Aig_Man_t *pAig)
void Lcr_ManPrint (Fra_Lcr_t *p)
void Lcr_ManFree (Fra_Lcr_t *p)
Fra_Man_t * Fra_LcrAigPrepare (Aig_Man_t *pAig)
void Fra_LcrAigPrepareTwo (Aig_Man_t *pAig, Fra_Man_t *p)
int Fra_LcrNodesAreEqual (Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
int Fra_LcrNodeIsConst (Aig_Obj_t *pObj)
Aig_Man_t * Fra_LcrDeriveAigForPartitioning (Fra_Lcr_t *pLcr)
void Fra_LcrRemapPartitions (Vec_Ptr_t *vParts, Fra_Cla_t *pCla, int *pInToOutPart, int *pInToOutNum)
Aig_Obj_t * Fra_LcrCreatePart_rec (Fra_Cla_t *pCla, Aig_Man_t *pNew, Aig_Man_t *p, Aig_Obj_t *pObj)
Aig_Man_t * Fra_LcrCreatePart (Fra_Lcr_t *p, Vec_Int_t *vPart)
void Fra_ClassNodesMark (Fra_Lcr_t *p)
void Fra_ClassNodesUnmark (Fra_Lcr_t *p)
Aig_Man_t * Fra_FraigLatchCorrespondence (Aig_Man_t *pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int *pnIter)

Typedef Documentation

typedef struct Fra_Lcr_t_ Fra_Lcr_t

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

FileName [fraLcorr.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Latch correspondence computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id
fraLcorr.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 27 of file fraLcr.c.

Function Documentation

void Fra_ClassNodesMark ( Fra_Lcr_t *  p  ) 

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

Synopsis [Marks the nodes belonging to the equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 437 of file fraLcr.c.

00438 {
00439     Aig_Obj_t * pObj, ** ppClass;
00440     int i, c, Offset;
00441     // compute the LO/LI offset
00442     Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
00443     // mark the nodes remaining in the classes
00444     Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
00445     {
00446         pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
00447         pObj->fMarkA = 1;
00448     }
00449     Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
00450     {
00451         for ( c = 0; ppClass[c]; c++ )
00452         {
00453             pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
00454             pObj->fMarkA = 1;
00455         }
00456     }
00457 }

void Fra_ClassNodesUnmark ( Fra_Lcr_t *  p  ) 

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

Synopsis [Unmarks the nodes belonging to the equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file fraLcr.c.

00471 {
00472     Aig_Obj_t * pObj, ** ppClass;
00473     int i, c, Offset;
00474     // compute the LO/LI offset
00475     Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
00476     // mark the nodes remaining in the classes
00477     Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
00478     {
00479         pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
00480         pObj->fMarkA = 0;
00481     }
00482     Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
00483     {
00484         for ( c = 0; ppClass[c]; c++ )
00485         {
00486             pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
00487             pObj->fMarkA = 0;
00488         }
00489     }
00490 }

Aig_Man_t* Fra_FraigLatchCorrespondence ( Aig_Man_t *  pAig,
int  nFramesP,
int  nConfMax,
int  fProve,
int  fVerbose,
int *  pnIter 
)

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

Synopsis [Performs choicing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 503 of file fraLcr.c.

00504 {
00505     int nPartSize    = 200;
00506     int fReprSelect  = 0;
00507 
00508     Fra_Lcr_t * p;
00509     Fra_Sml_t * pSml;
00510     Fra_Man_t * pTemp;
00511     Aig_Man_t * pAigPart, * pAigNew = NULL;
00512     Vec_Int_t * vPart;
00513 //    Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
00514     int i, nIter, timeSim, clk = clock(), clk2, clk3;
00515     if ( Aig_ManNodeNum(pAig) == 0 )
00516     {
00517         if ( pnIter ) *pnIter = 0;
00518         return Aig_ManDup(pAig, 1);
00519     }
00520     assert( Aig_ManLatchNum(pAig) == 0 );
00521     assert( Aig_ManRegNum(pAig) > 0 );
00522 
00523     // simulate the AIG 
00524 clk2 = clock();
00525 if ( fVerbose )
00526 printf( "Simulating AIG with %d nodes for %d cycles ...  ", Aig_ManNodeNum(pAig), nFramesP + 32 );
00527     pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1 ); 
00528 if ( fVerbose ) 
00529 {
00530 PRT( "Time", clock() - clk2 );
00531 timeSim = clock() - clk2;
00532 }
00533     // check if simulation discovered non-constant-0 POs
00534     if ( fProve && pSml->fNonConstOut )
00535     {
00536         Fra_SmlStop( pSml );
00537         return NULL;
00538     }
00539 
00540     // start the manager
00541     p = Lcr_ManAlloc( pAig );
00542     p->nFramesP = nFramesP;
00543     p->fVerbose = fVerbose;
00544     p->timeSim += timeSim;
00545 
00546     pTemp = Fra_LcrAigPrepare( pAig );
00547     pTemp->pBmc = (Fra_Bmc_t *)p;
00548     pTemp->pSml = pSml;
00549 
00550     // get preliminary info about equivalence classes
00551     pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
00552     Fra_ClassesPrepare( p->pCla, 1 );
00553     p->pCla->pFuncNodeIsConst   = Fra_LcrNodeIsConst;
00554     p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
00555     Fra_SmlStop( pTemp->pSml );
00556 
00557     // partition the AIG for latch correspondence computation
00558 clk2 = clock();
00559 if ( fVerbose )
00560 printf( "Partitioning AIG ...  " );
00561     pAigPart = Fra_LcrDeriveAigForPartitioning( p );
00562     p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
00563     Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
00564     Aig_ManStop( pAigPart );
00565 if ( fVerbose ) 
00566 {
00567 PRT( "Time", clock() - clk2 );
00568 p->timePart += clock() - clk2;
00569 }
00570 
00571     // get the initial stats
00572     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
00573     p->nNodesBeg = Aig_ManNodeNum(p->pAig);
00574     p->nRegsBeg  = Aig_ManRegNum(p->pAig);
00575 
00576     // perforn interative reduction of the partitions
00577     p->fRefining = 1;
00578     for ( nIter = 0; p->fRefining; nIter++ )
00579     {
00580         p->fRefining = 0;
00581         clk3 = clock();
00582         // derive AIGs for each partition
00583         Fra_ClassNodesMark( p );
00584         Vec_PtrClear( p->vFraigs );
00585         Vec_PtrForEachEntry( p->vParts, vPart, i )
00586         {
00587 clk2 = clock();
00588             pAigPart = Fra_LcrCreatePart( p, vPart );
00589 p->timeTrav += clock() - clk2;
00590 clk2 = clock();
00591             pAigNew  = Fra_FraigEquivence( pAigPart, nConfMax );
00592 p->timeFraig += clock() - clk2;
00593             Vec_PtrPush( p->vFraigs, pAigNew );
00594             Aig_ManStop( pAigPart );
00595         }
00596         Fra_ClassNodesUnmark( p );
00597         // report the intermediate results
00598         if ( fVerbose )
00599         {
00600             printf( "%3d : Const = %6d. Class = %6d.  L = %6d. Part = %3d.  ", 
00601                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
00602                 Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
00603             PRT( "T", clock() - clk3 );
00604         }
00605         // refine the classes
00606         Fra_LcrAigPrepareTwo( p->pAig, pTemp );
00607         if ( Fra_ClassesRefine( p->pCla ) )
00608             p->fRefining = 1;
00609         if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
00610             p->fRefining = 1;
00611         // clean the fraigs
00612         Vec_PtrForEachEntry( p->vFraigs, pAigPart, i )
00613             Aig_ManStop( pAigPart );
00614 
00615         // repartition if needed
00616         if ( 1 )
00617         {
00618 clk2 = clock();
00619             Vec_VecFree( (Vec_Vec_t *)p->vParts );
00620             pAigPart = Fra_LcrDeriveAigForPartitioning( p );
00621             p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
00622             Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
00623             Aig_ManStop( pAigPart );
00624 p->timePart += clock() - clk2;
00625         }
00626     }
00627     free( pTemp );
00628     p->nIters = nIter;
00629 
00630     // move the classes into representatives and reduce AIG
00631 clk2 = clock();
00632 //    Fra_ClassesPrint( p->pCla, 1 );
00633     if ( fReprSelect )
00634         Fra_ClassesSelectRepr( p->pCla );
00635     Fra_ClassesCopyReprs( p->pCla, NULL );
00636     pAigNew = Aig_ManDupRepr( p->pAig, 0 );
00637     Aig_ManSeqCleanup( pAigNew );
00638 //    Aig_ManCountMergeRegs( pAigNew );
00639 p->timeUpdate += clock() - clk2;
00640 p->timeTotal = clock() - clk;
00641     // get the final stats
00642     p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
00643     p->nNodesEnd = Aig_ManNodeNum(pAigNew);
00644     p->nRegsEnd  = Aig_ManRegNum(pAigNew);
00645     Lcr_ManFree( p );
00646     if ( pnIter ) *pnIter = nIter;
00647     return pAigNew;
00648 }

Fra_Man_t* Fra_LcrAigPrepare ( Aig_Man_t *  pAig  ) 

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

Synopsis [Prepare the AIG for class computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file fraLcr.c.

00156 {
00157     Fra_Man_t * p;
00158     Aig_Obj_t * pObj;
00159     int i;
00160     p = ALLOC( Fra_Man_t, 1 );
00161     memset( p, 0, sizeof(Fra_Man_t) );
00162     Aig_ManForEachPi( pAig, pObj, i )
00163         pObj->pData = p;
00164     return p;
00165 }

void Fra_LcrAigPrepareTwo ( Aig_Man_t *  pAig,
Fra_Man_t *  p 
)

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

Synopsis [Prepare the AIG for class computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file fraLcr.c.

00179 {
00180     Aig_Obj_t * pObj;
00181     int i;
00182     Aig_ManForEachPi( pAig, pObj, i )
00183         pObj->pData = p;
00184 }

Aig_Man_t* Fra_LcrCreatePart ( Fra_Lcr_t *  p,
Vec_Int_t *  vPart 
)

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

Synopsis [Creates AIG of one partition with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 401 of file fraLcr.c.

00402 {
00403     Aig_Man_t * pNew;
00404     Aig_Obj_t * pObj, * pObjNew;
00405     int Out, i;
00406     // create new AIG for this partition
00407     pNew = Aig_ManStartFrom( p->pAig );
00408     Aig_ManIncrementTravId( p->pAig );
00409     Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
00410     Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
00411     Vec_IntForEachEntry( vPart, Out, i )
00412     {
00413         pObj = Aig_ManPo( p->pAig, Out );
00414         if ( pObj->fMarkA )
00415         {
00416             pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) );
00417             pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
00418         }
00419         else
00420             pObjNew = Aig_ManConst1( pNew );
00421         Aig_ObjCreatePo( pNew, pObjNew ); 
00422     }
00423     return pNew;
00424 }

Aig_Obj_t* Fra_LcrCreatePart_rec ( Fra_Cla_t *  pCla,
Aig_Man_t *  pNew,
Aig_Man_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Creates AIG of one partition with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 366 of file fraLcr.c.

00367 {
00368     assert( !Aig_IsComplement(pObj) );
00369     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
00370         return pObj->pData;
00371     Aig_ObjSetTravIdCurrent(p, pObj);
00372     if ( Aig_ObjIsPi(pObj) )
00373     {
00374 //        Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
00375         Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
00376         if ( pRepr == NULL )
00377             pObj->pData = Aig_ObjCreatePi( pNew );
00378         else
00379         {
00380             pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr );
00381             pObj->pData = Aig_NotCond( pObj->pData, pRepr->fPhase ^ pObj->fPhase );
00382         }
00383         return pObj->pData;
00384     }
00385     Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) );
00386     Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) );
00387     return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
00388 }

Aig_Man_t* Fra_LcrDeriveAigForPartitioning ( Fra_Lcr_t *  pLcr  ) 

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

Synopsis [Give the AIG and classes, reduces AIG for partitioning.]

Description [Ignores registers that are not in the classes. Places candidate equivalent classes of registers into single outputs (for ease of partitioning). The resulting combinational AIG contains outputs in the same order as equivalence classes of registers, followed by constant-1 registers. Preserves the set of all inputs. Complemented attributes of the outputs do not matter because we need then only for collecting the structural info.]

SideEffects []

SeeAlso []

Definition at line 268 of file fraLcr.c.

00269 {
00270     Aig_Man_t * pNew;
00271     Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter;
00272     int i, c, Offset;
00273     // remember the numbers of the inputs of the original AIG
00274     Aig_ManForEachPi( pLcr->pAig, pObj, i )
00275     {
00276         pObj->pData = pLcr;
00277         pObj->pNext = (Aig_Obj_t *)i;
00278     }
00279     // compute the LO/LI offset
00280     Offset = Aig_ManPoNum(pLcr->pAig) - Aig_ManPiNum(pLcr->pAig);
00281     // create the PIs
00282     Aig_ManCleanData( pLcr->pAig );
00283     pNew = Aig_ManStartFrom( pLcr->pAig );
00284     // go over the equivalence classes
00285     Vec_PtrForEachEntry( pLcr->pCla->vClasses, ppClass, i )
00286     {
00287         pMiter = Aig_ManConst0(pNew);
00288         for ( c = 0; ppClass[c]; c++ )
00289         {
00290             assert( Aig_ObjIsPi(ppClass[c]) );
00291             pObjPo  = Aig_ManPo( pLcr->pAig, Offset+(int)ppClass[c]->pNext );
00292             pObjNew = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
00293             pMiter  = Aig_Exor( pNew, pMiter, pObjNew );
00294         }
00295         Aig_ObjCreatePo( pNew, pMiter );
00296     }
00297     // go over the constant candidates
00298     Vec_PtrForEachEntry( pLcr->pCla->vClasses1, pObj, i )
00299     {
00300         assert( Aig_ObjIsPi(pObj) );
00301         pObjPo = Aig_ManPo( pLcr->pAig, Offset+(int)pObj->pNext );
00302         pMiter = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
00303         Aig_ObjCreatePo( pNew, pMiter );
00304     }
00305     return pNew;
00306 }

int Fra_LcrNodeIsConst ( Aig_Obj_t *  pObj  ) 

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

Synopsis [Compares the node with a constant after partioned fraiging.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file fraLcr.c.

00236 {
00237     Fra_Man_t * pTemp = pObj->pData;
00238     Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
00239     Aig_Man_t * pFraig;
00240     Aig_Obj_t * pOut;
00241     int nPart;
00242     assert( Aig_ObjIsPi(pObj) );
00243     // find the partition to which these nodes belong
00244     nPart = pLcr->pInToOutPart[(int)pObj->pNext];
00245     pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart );
00246     // get the fraig outputs
00247     pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj->pNext] );
00248     return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
00249 }

int Fra_LcrNodesAreEqual ( Aig_Obj_t *  pObj0,
Aig_Obj_t *  pObj1 
)

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

Synopsis [Compares two nodes for equivalence after partitioned fraiging.]

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file fraLcr.c.

00198 {
00199     Fra_Man_t * pTemp = pObj0->pData;
00200     Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
00201     Aig_Man_t * pFraig;
00202     Aig_Obj_t * pOut0, * pOut1;
00203     int nPart0, nPart1;
00204     assert( Aig_ObjIsPi(pObj0) );
00205     assert( Aig_ObjIsPi(pObj1) );
00206     // find the partition to which these nodes belong
00207     nPart0 = pLcr->pInToOutPart[(int)pObj0->pNext];
00208     nPart1 = pLcr->pInToOutPart[(int)pObj1->pNext];
00209     // if this is the result of refinement of the class created const-1 nodes
00210     // the nodes may end up in different partions - we assume them equivalent
00211     if ( nPart0 != nPart1 )
00212     {
00213         assert( 0 );
00214         return 1;
00215     }
00216     assert( nPart0 == nPart1 );
00217     pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart0 );
00218     // get the fraig outputs
00219     pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj0->pNext] );
00220     pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj1->pNext] );
00221     return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1);
00222 }

void Fra_LcrRemapPartitions ( Vec_Ptr_t *  vParts,
Fra_Cla_t *  pCla,
int *  pInToOutPart,
int *  pInToOutNum 
)

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

Synopsis [Remaps partitions into the inputs of original AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 319 of file fraLcr.c.

00320 {
00321     Vec_Int_t * vOne, * vOneNew;
00322     Aig_Obj_t ** ppClass, * pObjPi;
00323     int Out, Offset, i, k, c;
00324     // compute the LO/LI offset
00325     Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig);
00326     Vec_PtrForEachEntry( vParts, vOne, i )
00327     {
00328         vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
00329         Vec_IntForEachEntry( vOne, Out, k )
00330         {
00331             if ( Out < Vec_PtrSize(pCla->vClasses) )
00332             {
00333                 ppClass = Vec_PtrEntry( pCla->vClasses, Out );
00334                 for ( c = 0; ppClass[c]; c++ )
00335                 {
00336                     pInToOutPart[(int)ppClass[c]->pNext] = i;
00337                     pInToOutNum[(int)ppClass[c]->pNext] = Vec_IntSize(vOneNew);
00338                     Vec_IntPush( vOneNew, Offset+(int)ppClass[c]->pNext );
00339                 }
00340             }
00341             else
00342             {
00343                 pObjPi = Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) );
00344                 pInToOutPart[(int)pObjPi->pNext] = i;
00345                 pInToOutNum[(int)pObjPi->pNext] = Vec_IntSize(vOneNew);
00346                 Vec_IntPush( vOneNew, Offset+(int)pObjPi->pNext );
00347             }
00348         }
00349         // replace the class
00350         Vec_PtrWriteEntry( vParts, i, vOneNew );
00351         Vec_IntFree( vOne );
00352     }
00353 }

Fra_Lcr_t* Lcr_ManAlloc ( Aig_Man_t *  pAig  ) 

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

Synopsis [Allocates the retiming manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file fraLcr.c.

00078 {
00079     Fra_Lcr_t * p;
00080     p = ALLOC( Fra_Lcr_t, 1 );
00081     memset( p, 0, sizeof(Fra_Lcr_t) );
00082     p->pAig = pAig;
00083     p->pInToOutPart = ALLOC( int, Aig_ManPiNum(pAig) );
00084     memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) );
00085     p->pInToOutNum = ALLOC( int, Aig_ManPiNum(pAig) );
00086     memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) );
00087     p->vFraigs = Vec_PtrAlloc( 1000 );
00088     return p;
00089 }

void Lcr_ManFree ( Fra_Lcr_t *  p  ) 

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

Synopsis [Deallocates the retiming manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file fraLcr.c.

00129 {
00130     Aig_Obj_t * pObj;
00131     int i;
00132     if ( p->fVerbose )
00133         Lcr_ManPrint( p );
00134     Aig_ManForEachPi( p->pAig, pObj, i )
00135         pObj->pNext = NULL;
00136     Vec_PtrFree( p->vFraigs );
00137     if ( p->pCla  )     Fra_ClassesStop( p->pCla );
00138     if ( p->vParts  )   Vec_VecFree( (Vec_Vec_t *)p->vParts );
00139     free( p->pInToOutPart );
00140     free( p->pInToOutNum );
00141     free( p );
00142 }

void Lcr_ManPrint ( Fra_Lcr_t *  p  ) 

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

Synopsis [Prints stats for the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file fraLcr.c.

00103 {
00104     printf( "Iterations = %d.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
00105         p->nIters, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
00106     printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
00107         p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
00108         p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
00109     PRT( "AIG simulation  ", p->timeSim  );
00110     PRT( "AIG partitioning", p->timePart );
00111     PRT( "AIG rebuiding   ", p->timeTrav );
00112     PRT( "FRAIGing        ", p->timeFraig );
00113     PRT( "AIG updating    ", p->timeUpdate );
00114     PRT( "TOTAL RUNTIME   ", p->timeTotal );
00115 }

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