#include "fra.h"

Include dependency graph for fraLcr.c:

Classes
struct	Fra_Lcr_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Fra_Lcr_t_	Fra_Lcr_t
	DECLARATIONS ///.

Functions
Fra_Lcr_t *	Lcr_ManAlloc (Aig_Man_t *pAig)
	FUNCTION DEFINITIONS ///.

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

◆ Fra_Lcr_t

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

◆ Fra_ClassNodesMark()

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;
        }
    }
}

Here is the caller graph for this function:

◆ Fra_ClassNodesUnmark()

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;
        }
    }
}

Here is the caller graph for this function:

◆ Fra_FraigLatchCorrespondence()

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);
 
    // perform iterative 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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fra_LcrAigPrepare()

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fra_LcrAigPrepareTwo()

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;
}

Here is the caller graph for this function:

◆ Fra_LcrCreatePart()

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fra_LcrCreatePart_rec()

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) ));
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fra_LcrDeriveAigForPartitioning()

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fra_LcrManDup_rec()

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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Fra_LcrNodeIsConst()

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);
}

Here is the caller graph for this function:

◆ Fra_LcrNodesAreEqual()

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);
}

Here is the caller graph for this function:

◆ Fra_LcrRemapPartitions()

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 );
    }
}

Here is the caller graph for this function:

◆ Lcr_ManAlloc()

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Lcr_ManFree()

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Lcr_ManPrint()

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 );
}

Here is the caller graph for this function:

Classes

Typedefs

Functions

Typedef Documentation

◆ Fra_Lcr_t

Function Documentation

◆ Fra_ClassNodesMark()

◆ Fra_ClassNodesUnmark()

◆ Fra_FraigLatchCorrespondence()

◆ Fra_LcrAigPrepare()

◆ Fra_LcrAigPrepareTwo()

◆ Fra_LcrCreatePart()

◆ Fra_LcrCreatePart_rec()

◆ Fra_LcrDeriveAigForPartitioning()

◆ Fra_LcrManDup_rec()

◆ Fra_LcrNodeIsConst()

◆ Fra_LcrNodesAreEqual()

◆ Fra_LcrRemapPartitions()

◆ Lcr_ManAlloc()

◆ Lcr_ManFree()

◆ Lcr_ManPrint()