src/aig/fra/fraClass.c

Go to the documentation of this file.

#include "fra.h"

/*
    The candidate equivalence classes are stored as a vector of pointers 
    to the array of pointers to the nodes in each class.
    The first node of the class is its representative node.
    The representative has the smallest topological order among the class nodes.
    The nodes inside each class are ordered according to their topological order.
    The classes are ordered according to the topological order of their representatives.
    The array of pointers to the class nodes is terminated with a NULL pointer.
    To enable dynamic addition of new classes (during class refinement),
    each array has at least as many NULLs in the end, as there are nodes in the class.
*/


static inline Aig_Obj_t *  Fra_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
static inline void         Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }


Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
{
    Fra_Cla_t * p;
    p = ALLOC( Fra_Cla_t, 1 );
    memset( p, 0, sizeof(Fra_Cla_t) );
    p->pAig = pAig;
    p->pMemRepr  = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
    p->vClasses     = Vec_PtrAlloc( 100 );
    p->vClasses1    = Vec_PtrAlloc( 100 );
    p->vClassesTemp = Vec_PtrAlloc( 100 );
    p->vClassOld    = Vec_PtrAlloc( 100 );
    p->vClassNew    = Vec_PtrAlloc( 100 );
    p->pFuncNodeHash      = Fra_SmlNodeHash;
    p->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
    p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
    return p;
}

void Fra_ClassesStop( Fra_Cla_t * p )
{
    FREE( p->pMemClasses );
    FREE( p->pMemRepr );
    if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
    if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
    if ( p->vClasses )     Vec_PtrFree( p->vClasses );
    if ( p->vImps )        Vec_IntFree( p->vImps );
    free( p );
}

void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
    memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
    if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
    {
        Aig_ManForEachObj( p->pAig, pObj, i )
        {
            if ( p->pAig->pReprs[i] != NULL )
                printf( "Classes are not cleared!\n" );
            assert( p->pAig->pReprs[i] == NULL );
        }
    }
    if ( vFailed )
        Vec_PtrForEachEntry( vFailed, pObj, i )
            p->pAig->pReprs[pObj->Id] = NULL;
}

int Fra_ClassCount( Aig_Obj_t ** pClass )
{
    Aig_Obj_t * pTemp;
    int i;
    for ( i = 0; pTemp = pClass[i]; i++ );
    return i;
}

int Fra_ClassesCountLits( Fra_Cla_t * p )
{
    Aig_Obj_t ** pClass;
    int i, nNodes, nLits = 0;
    nLits = Vec_PtrSize( p->vClasses1 );
    Vec_PtrForEachEntry( p->vClasses, pClass, i )
    {
        nNodes = Fra_ClassCount( pClass );
        assert( nNodes > 1 );
        nLits += nNodes - 1;
    }
    return nLits;
}

int Fra_ClassesCountPairs( Fra_Cla_t * p )
{
    Aig_Obj_t ** pClass;
    int i, nNodes, nPairs = 0;
    Vec_PtrForEachEntry( p->vClasses, pClass, i )
    {
        nNodes = Fra_ClassCount( pClass );
        assert( nNodes > 1 );
        nPairs += nNodes * (nNodes - 1) / 2;
    }
    return nPairs;
}

void Fra_PrintClass( Aig_Obj_t ** pClass )
{
    Aig_Obj_t * pTemp;
    int i;
    for ( i = 1; pTemp = pClass[i]; i++ )
        assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
    printf( "{ " );
    for ( i = 0; pTemp = pClass[i]; i++ )
        printf( "%d(%d) ", pTemp->Id, pTemp->Level );
    printf( "}\n" );
}

void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
{
    Aig_Obj_t ** pClass;
    Aig_Obj_t * pObj;
    int i;

    printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
        Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
    if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
        printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
    printf( "\n" );

    if ( fVeryVerbose )
    {
        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
            assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
        printf( "Constants { " );
        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
            printf( "%d ", pObj->Id );
        printf( "}\n" );
        Vec_PtrForEachEntry( p->vClasses, pClass, i )
        {
            printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
            Fra_PrintClass( pClass );
        }
        printf( "\n" );
    }
}

void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
{
    Aig_Obj_t ** ppTable, ** ppNexts;
    Aig_Obj_t * pObj, * pTemp;
    int i, k, nTableSize, nEntries, nNodes, iEntry;

    // allocate the hash table hashing simulation info into nodes
    nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
    ppTable = ALLOC( Aig_Obj_t *, nTableSize ); 
    ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); 
    memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );

    // add all the nodes to the hash table
    Vec_PtrClear( p->vClasses1 );
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Aig_ObjIsPi(pObj) )
                continue;
        }
        else
        {
            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
                continue;
            // skip the node with more that the given number of levels
//            if ( pObj->Level > 3 )
//                continue;
        }
        // hash the node by its simulation info
        iEntry = p->pFuncNodeHash( pObj, nTableSize );
        // check if the node belongs to the class of constant 1
        if ( p->pFuncNodeIsConst( pObj ) )
        {
            Vec_PtrPush( p->vClasses1, pObj );
            Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
            continue;
        }
        // add the node to the class
        if ( ppTable[iEntry] == NULL )
        {
            ppTable[iEntry] = pObj;
            Fra_ObjSetNext( ppNexts, pObj, pObj );
        }
        else
        {
            Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) );
            Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
        }
    }

    // count the total number of nodes in the non-trivial classes
    // mark the representative nodes of each equivalence class
    nEntries = 0;
    for ( i = 0; i < nTableSize; i++ )
        if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) )
        {
            for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; 
                  pTemp != ppTable[i]; 
                  pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
            assert( k > 1 );
            nEntries += k;
            // mark the node
            assert( ppTable[i]->fMarkA == 0 );
            ppTable[i]->fMarkA = 1;
        }

    // allocate room for classes
    p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
    p->pMemClassesFree = p->pMemClasses + 2*nEntries;
 
    // copy the entries into storage in the topological order
    Vec_PtrClear( p->vClasses );
    nEntries = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
            continue;
        // skip the nodes that are not representatives of non-trivial classes
        if ( pObj->fMarkA == 0 )
            continue;
        pObj->fMarkA = 0;
        // add the class of nodes
        Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries );
        // count the number of entries in this class
        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
              pTemp != pObj; 
              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
        nNodes = k;
        assert( nNodes > 1 );
        // add the nodes to the class in the topological order
        p->pMemClasses[2*nEntries] = pObj;
        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
              pTemp != pObj; 
              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
        {
            p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
            Fra_ClassObjSetRepr( pTemp, pObj );
        }
        // add as many empty entries
        p->pMemClasses[2*nEntries + nNodes] = NULL;
        // increment the number of entries
        nEntries += k;
    }
    free( ppTable );
    free( ppNexts );
    // now it is time to refine the classes
    Fra_ClassesRefine( p );
}

Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
{
    Aig_Obj_t * pObj, ** ppThis;
    int i;
    assert( ppClass[0] != NULL && ppClass[1] != NULL );

    // check if the class is going to be refined
    for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
        if ( !p->pFuncNodesAreEqual(ppClass[0], pObj) )
            break;
    if ( pObj == NULL )
        return NULL;
    // split the class
    Vec_PtrClear( p->vClassOld );
    Vec_PtrClear( p->vClassNew );
    Vec_PtrPush( p->vClassOld, ppClass[0] );
    for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
        if ( p->pFuncNodesAreEqual(ppClass[0], pObj) )
            Vec_PtrPush( p->vClassOld, pObj );
        else
            Vec_PtrPush( p->vClassNew, pObj );
/*
    printf( "Refining class (" );
    Vec_PtrForEachEntry( p->vClassOld, pObj, i )
        printf( "%d,", pObj->Id );
    printf( ") + (" );
    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
        printf( "%d,", pObj->Id );
    printf( ")\n" );
*/
    // put the nodes back into the class memory
    Vec_PtrForEachEntry( p->vClassOld, pObj, i )
    {
        ppClass[i] = pObj;
        ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
    }
    ppClass += 2*Vec_PtrSize(p->vClassOld);
    // put the new nodes into the class memory
    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
    {
        ppClass[i] = pObj;
        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
    }
    return ppClass;
}

int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses )
{
    Aig_Obj_t ** pClass, ** pClass2;
    int nRefis;
    pClass = Vec_PtrEntryLast( vClasses );
    for ( nRefis = 0; pClass2 = Fra_RefineClassOne( p, pClass ); nRefis++ )
    {
        // if the original class is trivial, remove it
        if ( pClass[1] == NULL )
            Vec_PtrPop( vClasses );
        // if the new class is trivial, stop
        if ( pClass2[1] == NULL )
        {
            nRefis++;
            break;
        }
        // othewise, add the class and continue
        assert( pClass2[0] != NULL );
        Vec_PtrPush( vClasses, pClass2 );
        pClass = pClass2;
    }
    return nRefis;
}

int Fra_ClassesRefine( Fra_Cla_t * p )
{
    Vec_Ptr_t * vTemp;
    Aig_Obj_t ** pClass;
    int i, nRefis;
    // refine the classes
    nRefis = 0;
    Vec_PtrClear( p->vClassesTemp );
    Vec_PtrForEachEntry( p->vClasses, pClass, i )
    {
        // add the class to the new array
        assert( pClass[0] != NULL );
        Vec_PtrPush( p->vClassesTemp, pClass );
        // refine the class iteratively
        nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
    }
    // exchange the class representation
    vTemp = p->vClassesTemp;
    p->vClassesTemp = p->vClasses;
    p->vClasses = vTemp;
    return nRefis;
}

int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
{
    Aig_Obj_t * pObj, ** ppClass;
    int i, k, nRefis = 1;
    // check if there is anything to refine
    if ( Vec_PtrSize(p->vClasses1) == 0 )
        return 0;
    // make sure constant 1 class contains only non-constant nodes
    assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) );
    // collect all the nodes to be refined
    k = 0;
    Vec_PtrClear( p->vClassNew );
    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
    {
        if ( p->pFuncNodeIsConst( pObj ) )
            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
        else 
            Vec_PtrPush( p->vClassNew, pObj );
    }
    Vec_PtrShrink( p->vClasses1, k );
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
/*
    printf( "Refined const-1 class: {" );
    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
        printf( " %d", pObj->Id );
    printf( " }\n" );
*/
    if ( Vec_PtrSize(p->vClassNew) == 1 )
    {
        Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
        return 1;
    }
    // create a new class composed of these nodes
    ppClass = p->pMemClassesFree;
    p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
    {
        ppClass[i] = pObj;
        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
    }
    assert( ppClass[0] != NULL );
    Vec_PtrPush( p->vClasses, ppClass );
    // iteratively refine this class
    if ( fRefineNewClass )
        nRefis += Fra_RefineClassLastIter( p, p->vClasses );
    else if ( pSkipped )
        (*pSkipped)++;
    return nRefis;
}

void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
{
    Aig_Obj_t ** pClass;
    p->pMemClasses = ALLOC( Aig_Obj_t *, 4 );
    pClass = p->pMemClasses;
    assert( Id1 < Id2 );
    pClass[0] = Aig_ManObj( p->pAig, Id1 );
    pClass[1] = Aig_ManObj( p->pAig, Id2 );
    pClass[2] = NULL;
    pClass[3] = NULL;
    Fra_ClassObjSetRepr( pClass[1], pClass[0] );
    Vec_PtrPush( p->vClasses, pClass );
}

void Fra_ClassesLatchCorr( Fra_Man_t * p )
{
    Aig_Obj_t * pObj;
    int i, nEntries = 0;
    Vec_PtrClear( p->pCla->vClasses1 );
    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
    {
        Vec_PtrPush( p->pCla->vClasses1, pObj );
        Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
    }
    // allocate room for classes
    p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
    p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
}

void Fra_ClassesPostprocess( Fra_Cla_t * p )
{
    int Ratio = 2;
    Fra_Sml_t * pComb;
    Aig_Obj_t * pObj, * pRepr, ** ppClass;
    int * pWeights, WeightMax = 0, i, k, c;
    // perform combinational simulation
    pComb = Fra_SmlSimulateComb( p->pAig, 32 );
    // compute the weight of each node in the classes
    pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
    memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
    Aig_ManForEachObj( p->pAig, pObj, i )
    { 
        pRepr = Fra_ClassObjRepr( pObj );
        if ( pRepr == NULL )
            continue;
        pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
        WeightMax = AIG_MAX( WeightMax, pWeights[i] );
    }
    Fra_SmlStop( pComb );
    printf( "Before: Const = %6d. Class = %6d.  ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
    // remove nodes from classes whose weight is less than WeightMax/Ratio
    k = 0;
    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
    {
        if ( pWeights[pObj->Id] >= WeightMax/Ratio )
            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
        else
            Fra_ClassObjSetRepr( pObj, NULL );
    }
    Vec_PtrShrink( p->vClasses1, k );
    // in each class, compact the nodes
    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
    {
        k = 1;
        for ( c = 1; ppClass[c]; c++ )
        {
            if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio )
                ppClass[k++] = ppClass[c];
            else
                Fra_ClassObjSetRepr( ppClass[c], NULL );
        }
        ppClass[k] = NULL;
    }
    // remove classes with only repr
    k = 0;
    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
        if ( ppClass[1] != NULL )
            Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
    Vec_PtrShrink( p->vClasses, k );
    printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
    free( pWeights );
}

void Fra_ClassesSelectRepr( Fra_Cla_t * p )
{
    Aig_Obj_t ** pClass, * pNodeMin;
    int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
    // reassign representatives in each class
    Vec_PtrForEachEntry( p->vClasses, pClass, i )
    {
        // collect support sizes and find the min-support node
        pNodeMin = NULL;
        nSuppSizeMin = AIG_INFINITY;
        for ( c = 0; pClass[c]; c++ )
        {
            nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
//            nSuppSizeCur = 1;
            if ( nSuppSizeMin > nSuppSizeCur || 
                (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
            {
                nSuppSizeMin = nSuppSizeCur;
                pNodeMin = pClass[c];
                cMinSupp = c; 
            }
        }
        // skip the case when the repr did not change
        if ( cMinSupp == 0 )
            continue;
        // make the new node the representative of the class
        pClass[cMinSupp] = pClass[0];
        pClass[0] = pNodeMin;
        // set the representative
        for ( c = 0; pClass[c]; c++ )
            Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
    }
}



static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj )                       { return ppEquivs[pObj->Id];  }
static inline void        Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; }

static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj));  }
static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj));  }

static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs )
{
    Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2;
    // skip nodes without representative
    if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
        return;
    assert( pObjRepr->Id < pObj->Id );
    // get the new node 
    pObjNew = Fra_ObjEqu( ppEquivs, pObj );
    // get the new node of the representative
    pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr );
    // if this is the same node, no need to add constraints
    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
        return;
    // these are different nodes - perform speculative reduction
//    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
    // set the new node
//    Fra_ObjSetEqu( ppEquivs, pObj, pObjNew2 );
    // add the constraint
    pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
    pMiter = Aig_Not( pMiter );
    Aig_ObjCreatePo( pManFraig, pMiter );
}

Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
{
    Aig_Man_t * pManFraig;
    Aig_Obj_t * pObj, * pObjNew;
    Aig_Obj_t ** pLatches, ** ppEquivs;
    int i, k, f, nFramesAll = nFramesK + 1;
    assert( Aig_ManRegNum(p->pAig) > 0 );
    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
    assert( nFramesK > 0 );
    // start the fraig package
    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
    pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
    // allocate place for the node mapping
    ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
    Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
    // create latches for the first frame
    Aig_ManForEachLoSeq( p->pAig, pObj, i )
        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
    // add timeframes
    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
    for ( f = 0; f < nFramesAll; f++ )
    {
        // create PIs for this frame
        Aig_ManForEachPiSeq( p->pAig, pObj, i )
            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
        // set the constraints on the latch outputs
        Aig_ManForEachLoSeq( p->pAig, pObj, i )
            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
        // add internal nodes of this frame
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
            Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
        }
        if ( f == nFramesAll - 1 )
            break;
        if ( f == nFramesAll - 2 )
            pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
        // save the latch input values
        k = 0;
        Aig_ManForEachLiSeq( p->pAig, pObj, i )
            pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
        // insert them to the latch output values
        k = 0;
        Aig_ManForEachLoSeq( p->pAig, pObj, i )
            Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
    }
    free( pLatches );
    free( ppEquivs );
    // mark the asserts
    assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
printf( "Assert miters = %6d. Output miters = %6d.\n", 
       pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
    // remove dangling nodes
    Aig_ManCleanup( pManFraig );
    return pManFraig;
}

---