/**CFile****************************************************************
FileName [fraClass.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraClass.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
ABC_NAMESPACE_IMPL_START
/*
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.
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
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; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
{
Fra_Cla_t * p;
p = ABC_ALLOC( Fra_Cla_t, 1 );
memset( p, 0, sizeof(Fra_Cla_t) );
p->pAig = pAig;
p->pMemRepr = ABC_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;
}
/**Function*************************************************************
Synopsis [Stop representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClassesStop( Fra_Cla_t * p )
{
ABC_FREE( p->pMemClasses );
ABC_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 );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Starts representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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( Aig_Obj_t *, vFailed, pObj, i )
p->pAig->pReprs[pObj->Id] = NULL;
}
/**Function*************************************************************
Synopsis [Prints simulation classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClassCount( Aig_Obj_t ** pClass )
{
Aig_Obj_t * pTemp;
int i;
for ( i = 0; (pTemp = pClass[i]); i++ );
return i;
}
/**Function*************************************************************
Synopsis [Count the number of literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClassesCountLits( Fra_Cla_t * p )
{
Aig_Obj_t ** pClass;
int i, nNodes, nLits = 0;
nLits = Vec_PtrSize( p->vClasses1 );
Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
{
nNodes = Fra_ClassCount( pClass );
assert( nNodes > 1 );
nLits += nNodes - 1;
}
return nLits;
}
/**Function*************************************************************
Synopsis [Count the number of pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_ClassesCountPairs( Fra_Cla_t * p )
{
Aig_Obj_t ** pClass;
int i, nNodes, nPairs = 0;
Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
{
nNodes = Fra_ClassCount( pClass );
assert( nNodes > 1 );
nPairs += nNodes * (nNodes - 1) / 2;
}
return nPairs;
}
/**Function*************************************************************
Synopsis [Prints simulation classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_PrintClass( Fra_Cla_t * p, 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,%d) ", pTemp->Id, pTemp->Level, Aig_SupportSize(p->pAig,pTemp) );
printf( "}\n" );
}
/**Function*************************************************************
Synopsis [Prints simulation classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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( Aig_Obj_t *, p->vClasses1, pObj, i )
assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
printf( "Constants { " );
Vec_PtrForEachEntry( Aig_Obj_t *, p->vClasses1, pObj, i )
printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
printf( "}\n" );
Vec_PtrForEachEntry( Aig_Obj_t **, p->vClasses, pClass, i )
{
printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
Fra_PrintClass( p, pClass );
}
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis [Creates initial simulation classes.]
Description [Assumes that simulation info is assigned.]
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
{
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 = Abc_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
ppTable = ABC_FALLOC( Aig_Obj_t *, nTableSize );
ppNexts = ABC_FALLOC( 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_ObjIsCi(pObj) )
continue;
}
else
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
continue;
// skip the node with more that the given number of levels
if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
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 = ABC_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_ObjIsCi(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;
}
ABC_FREE( ppTable );
ABC_FREE( ppNexts );
// now it is time to refine the classes
Fra_ClassesRefine( p );
// Fra_ClassesPrint( p, 0 );
}
/**Function*************************************************************
Synopsis [Refines one class using simulation info.]
Description [Returns the new class if refinement happened.]
SideEffects []
SeeAlso []
***********************************************************************/
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( Aig_Obj_t *, p->vClassOld, pObj, i )
printf( "%d,", pObj->Id );
printf( ") + (" );
Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
printf( "%d,", pObj->Id );
printf( ")\n" );
*/
// put the nodes back into the class memory
Vec_PtrForEachEntry( Aig_Obj_t *, 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( Aig_Obj_t *, p->vClassNew, pObj, i )
{
ppClass[i] = pObj;
ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
}
return ppClass;
}
/**Function*************************************************************
Synopsis [Iteratively refines the classes after simulation.]
Description [Returns the number of refinements performed.]
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses )
{
Aig_Obj_t ** pClass, ** pClass2;
int nRefis;
pClass = (Aig_Obj_t **)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;
}
/**Function*************************************************************
Synopsis [Refines the classes after simulation.]
Description [Assumes that simulation info is assigned. Returns the
number of classes refined.]
SideEffects []
SeeAlso []
***********************************************************************/
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( Aig_Obj_t **, 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;
}
/**Function*************************************************************
Synopsis [Refines constant 1 equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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( Aig_Obj_t *, 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( Aig_Obj_t *, p->vClassNew, pObj, i )
printf( " %d", pObj->Id );
printf( " }\n" );
*/
if ( Vec_PtrSize(p->vClassNew) == 1 )
{
Fra_ClassObjSetRepr( (Aig_Obj_t *)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( Aig_Obj_t *, 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;
}
/**Function*************************************************************
Synopsis [Starts representation of equivalence classes with one class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
{
Aig_Obj_t ** pClass;
p->pMemClasses = ABC_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 );
}
/**Function*************************************************************
Synopsis [Creates latch correspondence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 = ABC_ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
}
/**Function*************************************************************
Synopsis [Postprocesses the classes by removing half of the less useful.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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, 0 );
// compute the weight of each node in the classes
pWeights = ABC_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 = Abc_MaxInt( 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( Aig_Obj_t *, 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( Aig_Obj_t **, 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( Aig_Obj_t **, 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) );
ABC_FREE( pWeights );
}
/**Function*************************************************************
Synopsis [Postprocesses the classes by selecting representative lowest in top order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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( Aig_Obj_t **, p->vClasses, pClass, i )
{
// collect support sizes and find the min-support node
cMinSupp = -1;
pNodeMin = NULL;
nSuppSizeMin = ABC_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)); }
/**Function*************************************************************
Synopsis [Add the node and its constraints to the new AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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_ObjCreateCo( pManFraig, pMiter );
}
/**Function*************************************************************
Synopsis [Derives AIG for the partitioned problem.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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_ManCiNum(p->pAig) );
assert( nFramesK > 0 );
// start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
pManFraig->pName = Abc_UtilStrsav( p->pAig->pName );
pManFraig->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
// allocate place for the node mapping
ppEquivs = ABC_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_ObjCreateCi(pManFraig) );
// add timeframes
pLatches = ABC_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_ObjCreateCi(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_ManCoNum(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++] );
}
ABC_FREE( pLatches );
ABC_FREE( ppEquivs );
// mark the asserts
assert( Aig_ManCoNum(pManFraig) % nFramesAll == 0 );
printf( "Assert miters = %6d. Output miters = %6d.\n",
pManFraig->nAsserts, Aig_ManCoNum(pManFraig) - pManFraig->nAsserts );
// remove dangling nodes
Aig_ManCleanup( pManFraig );
return pManFraig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END