fraLcr.c File Reference

#include "fra.h"

Go to the source code of this file.

Data Structures
struct	Fra_Lcr_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Fra_Lcr_t_	Fra_Lcr_t
	DECLARATIONS ///. More...

Functions
Fra_Lcr_t *	Lcr_ManAlloc (Aig_Man_t *pAig)
	FUNCTION DEFINITIONS ///. More...
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_Obj_t *	Fra_LcrManDup_rec (Aig_Man_t *pNew, Aig_Man_t *p, 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, float TimeLimit)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Fra_Lcr_t_ Fra_Lcr_t

DECLARATIONS ///.

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

]

Definition at line 30 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 465 of file fraLcr.c.

{
    Aig_Obj_t * pObj, ** ppClass;
    int i, c, Offset;
    // compute the LO/LI offset
    Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig);
    // mark the nodes remaining in the classes
    Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
    {
        pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext );
        pObj->fMarkA = 1;
    }
    Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
    {
        for ( c = 0; ppClass[c]; c++ )
        {
            pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
            pObj->fMarkA = 1;
        }
    }
}

void Fra_ClassNodesUnmark

(

Fra_Lcr_t *

p

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 498 of file fraLcr.c.

{
    Aig_Obj_t * pObj, ** ppClass;
    int i, c, Offset;
    // compute the LO/LI offset
    Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig);
    // mark the nodes remaining in the classes
    Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
    {
        pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext );
        pObj->fMarkA = 0;
    }
    Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
    {
        for ( c = 0; ppClass[c]; c++ )
        {
            pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
            pObj->fMarkA = 0;
        }
    }
}

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

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

Synopsis [Performs choicing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 531 of file fraLcr.c.

{
    int nPartSize    = 200;
    int fReprSelect  = 0;
    Fra_Lcr_t * p;
    Fra_Sml_t * pSml;
    Fra_Man_t * pTemp;
    Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
    Vec_Int_t * vPart;
    int i, nIter;
    abctime timeSim, clk2, clk3, clk = Abc_Clock();
    abctime TimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
    if ( Aig_ManNodeNum(pAig) == 0 )
    {
        if ( pnIter ) *pnIter = 0;
        // Ntl_ManFinalize() requires the following to satisfy an assertion.
        Aig_ManReprStart(pAig,Aig_ManObjNumMax(pAig));
        return Aig_ManDupOrdered(pAig);
    }
    assert( Aig_ManRegNum(pAig) > 0 ); 

    // simulate the AIG 
clk2 = Abc_Clock();
if ( fVerbose )
printf( "Simulating AIG with %d nodes for %d cycles ...  ", Aig_ManNodeNum(pAig), nFramesP + 32 );
    pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1, 1  ); 
if ( fVerbose ) 
{
ABC_PRT( "Time", Abc_Clock() - clk2 );
}
timeSim = Abc_Clock() - clk2;

    // check if simulation discovered non-constant-0 POs
    if ( fProve && pSml->fNonConstOut )
    {
        pAig->pSeqModel = Fra_SmlGetCounterExample( pSml );
        Fra_SmlStop( pSml );
        return NULL;
    }

    // start the manager
    p = Lcr_ManAlloc( pAig );
    p->nFramesP = nFramesP;
    p->fVerbose = fVerbose;
    p->timeSim += timeSim;

    pTemp = Fra_LcrAigPrepare( pAig );
    pTemp->pBmc = (Fra_Bmc_t *)p;
    pTemp->pSml = pSml;

    // get preliminary info about equivalence classes
    pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
    Fra_ClassesPrepare( p->pCla, 1, 0 );
    p->pCla->pFuncNodeIsConst   = Fra_LcrNodeIsConst;
    p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
    Fra_SmlStop( pTemp->pSml );

    // partition the AIG for latch correspondence computation
clk2 = Abc_Clock();
if ( fVerbose )
printf( "Partitioning AIG ...  " );
    pAigPart = Fra_LcrDeriveAigForPartitioning( p );
    p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
    Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
    Aig_ManStop( pAigPart );
if ( fVerbose ) 
{
ABC_PRT( "Time", Abc_Clock() - clk2 );
p->timePart += Abc_Clock() - clk2;
}

    // get the initial stats
    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
    p->nNodesBeg = Aig_ManNodeNum(p->pAig);
    p->nRegsBeg  = Aig_ManRegNum(p->pAig);

    // perforn interative reduction of the partitions
    p->fRefining = 1;
    for ( nIter = 0; p->fRefining; nIter++ )
    {
        p->fRefining = 0;
        clk3 = Abc_Clock();
        // derive AIGs for each partition
        Fra_ClassNodesMark( p );
        Vec_PtrClear( p->vFraigs );
        Vec_PtrForEachEntry( Vec_Int_t *, p->vParts, vPart, i )
        {
            if ( TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
            {
                Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
                    Aig_ManStop( pAigPart );
                Aig_ManCleanMarkA( pAig );
                Aig_ManCleanMarkB( pAig );
                printf( "Fra_FraigLatchCorrespondence(): Runtime limit exceeded.\n" );
                goto finish;
            }
clk2 = Abc_Clock();
            pAigPart = Fra_LcrCreatePart( p, vPart );
p->timeTrav += Abc_Clock() - clk2;
clk2 = Abc_Clock();
            pAigTemp  = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
p->timeFraig += Abc_Clock() - clk2;
            Vec_PtrPush( p->vFraigs, pAigTemp );
/*
            {
                char Name[1000];
                sprintf( Name, "part%04d.blif", i );
                Aig_ManDumpBlif( pAigPart, Name, NULL, NULL );
            }
printf( "Finished part %4d (out of %4d).  ", i, Vec_PtrSize(p->vParts) );
ABC_PRT( "Time", Abc_Clock() - clk3 );
*/

            Aig_ManStop( pAigPart );
        }
        Fra_ClassNodesUnmark( p );
        // report the intermediate results
        if ( fVerbose )
        {
            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. Part = %3d.  ", 
                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
            ABC_PRT( "T", Abc_Clock() - clk3 );
        }
        // refine the classes
        Fra_LcrAigPrepareTwo( p->pAig, pTemp );
        if ( Fra_ClassesRefine( p->pCla ) )
            p->fRefining = 1;
        if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
            p->fRefining = 1;
        // clean the fraigs
        Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
            Aig_ManStop( pAigPart );

        // repartition if needed
        if ( 1 )
        {
clk2 = Abc_Clock();
            Vec_VecFree( (Vec_Vec_t *)p->vParts );
            pAigPart = Fra_LcrDeriveAigForPartitioning( p );
            p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
            Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
            Aig_ManStop( pAigPart );
p->timePart += Abc_Clock() - clk2;
        }
    }
    p->nIters = nIter;

    // move the classes into representatives and reduce AIG
clk2 = Abc_Clock();
//    Fra_ClassesPrint( p->pCla, 1 );
    if ( fReprSelect )
        Fra_ClassesSelectRepr( p->pCla );
    Fra_ClassesCopyReprs( p->pCla, NULL );
    pAigNew = Aig_ManDupRepr( p->pAig, 0 );
    Aig_ManSeqCleanup( pAigNew );
//    Aig_ManCountMergeRegs( pAigNew );
p->timeUpdate += Abc_Clock() - clk2;
p->timeTotal = Abc_Clock() - clk;
    // get the final stats
    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
    p->nNodesEnd = Aig_ManNodeNum(pAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pAigNew);
finish:
    ABC_FREE( pTemp );
    Lcr_ManFree( p );
    if ( pnIter ) *pnIter = nIter;
    return pAigNew;
}

Fra_Man_t* Fra_LcrAigPrepare

(

Aig_Man_t *

pAig

)

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

Synopsis [Prepare the AIG for class computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file fraLcr.c.

{
    Fra_Man_t * p;
    Aig_Obj_t * pObj;
    int i;
    p = ABC_ALLOC( Fra_Man_t, 1 );
    memset( p, 0, sizeof(Fra_Man_t) );
//    Aig_ManForEachCi( pAig, pObj, i )
    Aig_ManForEachObj( pAig, pObj, i )
        pObj->pData = p;
    return p;
}

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 182 of file fraLcr.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = p;
}

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 429 of file fraLcr.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pObjNew;
    int Out, i;
    // create new AIG for this partition
    pNew = Aig_ManStartFrom( p->pAig );
    Aig_ManIncrementTravId( p->pAig );
    Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
    Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
    Vec_IntForEachEntry( vPart, Out, i )
    {
        pObj = Aig_ManCo( p->pAig, Out );
        if ( pObj->fMarkA )
        {
            pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) );
            pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
        }
        else
            pObjNew = Aig_ManConst1( pNew );
        Aig_ObjCreateCo( pNew, pObjNew ); 
    }
    return pNew;
}

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 394 of file fraLcr.c.

{
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return (Aig_Obj_t *)pObj->pData;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
//        Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
        Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
        if ( pRepr == NULL )
            pObj->pData = Aig_ObjCreateCi( pNew );
        else
        {
            pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr );
            pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, pRepr->fPhase ^ pObj->fPhase );
        }
        return (Aig_Obj_t *)pObj->pData;
    }
    Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) );
    Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) );
    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
}

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 296 of file fraLcr.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter;
    int i, c, Offset;
    // remember the numbers of the inputs of the original AIG
    Aig_ManForEachCi( pLcr->pAig, pObj, i )
    {
        pObj->pData = pLcr;
        pObj->pNext = (Aig_Obj_t *)(long)i;
    }
    // compute the LO/LI offset
    Offset = Aig_ManCoNum(pLcr->pAig) - Aig_ManCiNum(pLcr->pAig);
    // create the PIs
    Aig_ManCleanData( pLcr->pAig );
    pNew = Aig_ManStartFrom( pLcr->pAig );
    // go over the equivalence classes
    Vec_PtrForEachEntry( Aig_Obj_t **, pLcr->pCla->vClasses, ppClass, i )
    {
        pMiter = Aig_ManConst0(pNew);
        for ( c = 0; ppClass[c]; c++ )
        {
            assert( Aig_ObjIsCi(ppClass[c]) );
            pObjPo  = Aig_ManCo( pLcr->pAig, Offset+(long)ppClass[c]->pNext );
            pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
            pMiter  = Aig_Exor( pNew, pMiter, pObjNew );
        }
        Aig_ObjCreateCo( pNew, pMiter );
    }
    // go over the constant candidates
    Vec_PtrForEachEntry( Aig_Obj_t *, pLcr->pCla->vClasses1, pObj, i )
    {
        assert( Aig_ObjIsCi(pObj) );
        pObjPo = Aig_ManCo( pLcr->pAig, Offset+(long)pObj->pNext );
        pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
        Aig_ObjCreateCo( pNew, pMiter );
    }
    return pNew;
}

Aig_Obj_t* Fra_LcrManDup_rec	(	Aig_Man_t *	pNew,
		Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Duplicates the AIG manager recursively.]

Description []

SideEffects []

SeeAlso []

Definition at line 266 of file fraLcr.c.

{
    Aig_Obj_t * pObjNew;
    if ( pObj->pData )
        return (Aig_Obj_t *)pObj->pData;
    Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
    if ( Aig_ObjIsBuf(pObj) )
        return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
    Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
    pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
    return (Aig_Obj_t *)(pObj->pData = pObjNew);
}

int Fra_LcrNodeIsConst

(

Aig_Obj_t *

pObj

)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 239 of file fraLcr.c.

{
    Fra_Man_t * pTemp = (Fra_Man_t *)pObj->pData;
    Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
    Aig_Man_t * pFraig;
    Aig_Obj_t * pOut;
    int nPart;
    assert( Aig_ObjIsCi(pObj) );
    // find the partition to which these nodes belong
    nPart = pLcr->pInToOutPart[(long)pObj->pNext];
    pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart );
    // get the fraig outputs
    pOut = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] );
    return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
}

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 201 of file fraLcr.c.

{
    Fra_Man_t * pTemp = (Fra_Man_t *)pObj0->pData;
    Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
    Aig_Man_t * pFraig;
    Aig_Obj_t * pOut0, * pOut1;
    int nPart0, nPart1;
    assert( Aig_ObjIsCi(pObj0) );
    assert( Aig_ObjIsCi(pObj1) );
    // find the partition to which these nodes belong
    nPart0 = pLcr->pInToOutPart[(long)pObj0->pNext];
    nPart1 = pLcr->pInToOutPart[(long)pObj1->pNext];
    // if this is the result of refinement of the class created const-1 nodes
    // the nodes may end up in different partions - we assume them equivalent
    if ( nPart0 != nPart1 )
    {
        assert( 0 );
        return 1;
    }
    assert( nPart0 == nPart1 );
    pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart0 );
    // get the fraig outputs
    pOut0 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] );
    pOut1 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] );
    return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1);
}

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 347 of file fraLcr.c.

{
    Vec_Int_t * vOne, * vOneNew;
    Aig_Obj_t ** ppClass, * pObjPi;
    int Out, Offset, i, k, c;
    // compute the LO/LI offset
    Offset = Aig_ManCoNum(pCla->pAig) - Aig_ManCiNum(pCla->pAig);
    Vec_PtrForEachEntry( Vec_Int_t *, vParts, vOne, i )
    {
        vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
        Vec_IntForEachEntry( vOne, Out, k )
        {
            if ( Out < Vec_PtrSize(pCla->vClasses) )
            {
                ppClass = (Aig_Obj_t **)Vec_PtrEntry( pCla->vClasses, Out );
                for ( c = 0; ppClass[c]; c++ )
                {
                    pInToOutPart[(long)ppClass[c]->pNext] = i;
                    pInToOutNum[(long)ppClass[c]->pNext] = Vec_IntSize(vOneNew);
                    Vec_IntPush( vOneNew, Offset+(long)ppClass[c]->pNext );
                }
            }
            else
            {
                pObjPi = (Aig_Obj_t *)Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) );
                pInToOutPart[(long)pObjPi->pNext] = i;
                pInToOutNum[(long)pObjPi->pNext] = Vec_IntSize(vOneNew);
                Vec_IntPush( vOneNew, Offset+(long)pObjPi->pNext );
            }
        }
        // replace the class
        Vec_PtrWriteEntry( vParts, i, vOneNew );
        Vec_IntFree( vOne );
    }
}

Fra_Lcr_t* Lcr_ManAlloc

(

Aig_Man_t *

pAig

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocates the retiming manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file fraLcr.c.

{
    Fra_Lcr_t * p;
    p = ABC_ALLOC( Fra_Lcr_t, 1 );
    memset( p, 0, sizeof(Fra_Lcr_t) );
    p->pAig = pAig;
    p->pInToOutPart = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
    memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManCiNum(pAig) );
    p->pInToOutNum = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
    memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManCiNum(pAig) );
    p->vFraigs = Vec_PtrAlloc( 1000 );
    return p;
}

void Lcr_ManFree

(

Fra_Lcr_t *

p

)

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

Synopsis [Deallocates the retiming manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file fraLcr.c.

{
    Aig_Obj_t * pObj;
    int i;
    if ( p->fVerbose )
        Lcr_ManPrint( p );
    Aig_ManForEachCi( p->pAig, pObj, i )
        pObj->pNext = NULL;
    Vec_PtrFree( p->vFraigs );
    if ( p->pCla  )     Fra_ClassesStop( p->pCla );
    if ( p->vParts  )   Vec_VecFree( (Vec_Vec_t *)p->vParts );
    ABC_FREE( p->pInToOutPart );
    ABC_FREE( p->pInToOutNum );
    ABC_FREE( p );
}

void Lcr_ManPrint

(

Fra_Lcr_t *

p

)

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

Synopsis [Prints stats for the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file fraLcr.c.

{
    printf( "Iterations = %d.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
        p->nIters, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
    printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
    ABC_PRT( "AIG simulation  ", p->timeSim  );
    ABC_PRT( "AIG partitioning", p->timePart );
    ABC_PRT( "AIG rebuiding   ", p->timeTrav );
    ABC_PRT( "FRAIGing        ", p->timeFraig );
    ABC_PRT( "AIG updating    ", p->timeUpdate );
    ABC_PRT( "TOTAL RUNTIME   ", p->timeTotal );
}