/**CFile****************************************************************
FileName [abcCascade.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Collapsing the network into two-levels.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcCollapse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "base/abc/abc.h"
#include "bdd/reo/reo.h"
#include "misc/extra/extraBdd.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define BDD_FUNC_MAX 256
//extern void Abc_NodeShowBddOne( DdManager * dd, DdNode * bFunc );
extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Derive BDD of the characteristic function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_ResBuildBdd( Abc_Ntk_t * pNtk, DdManager * dd )
{
Vec_Ptr_t * vNodes, * vBdds, * vLocals;
Abc_Obj_t * pObj, * pFanin;
DdNode * bFunc, * bPart, * bTemp, * bVar;
int i, k;
assert( Abc_NtkIsSopLogic(pNtk) );
assert( Abc_NtkCoNum(pNtk) <= 3 );
vBdds = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachCi( pNtk, pObj, i )
Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), Cudd_bddIthVar(dd, i) );
// create internal node BDDs
vNodes = Abc_NtkDfs( pNtk, 0 );
vLocals = Vec_PtrAlloc( 6 );
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
{
if ( Abc_ObjFaninNum(pObj) == 0 )
{
bFunc = Cudd_NotCond( Cudd_ReadOne(dd), Abc_SopIsConst0((char *)pObj->pData) ); Cudd_Ref( bFunc );
Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), bFunc );
continue;
}
Vec_PtrClear( vLocals );
Abc_ObjForEachFanin( pObj, pFanin, k )
Vec_PtrPush( vLocals, Vec_PtrEntry(vBdds, Abc_ObjId(pFanin)) );
bFunc = Abc_ConvertSopToBdd( dd, (char *)pObj->pData, (DdNode **)Vec_PtrArray(vLocals) ); Cudd_Ref( bFunc );
Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), bFunc );
}
Vec_PtrFree( vLocals );
// create char function
bFunc = Cudd_ReadOne( dd ); Cudd_Ref( bFunc );
Abc_NtkForEachCo( pNtk, pObj, i )
{
bVar = Cudd_bddIthVar( dd, i + Abc_NtkCiNum(pNtk) );
bTemp = (DdNode *)Vec_PtrEntry( vBdds, Abc_ObjFaninId0(pObj) );
bPart = Cudd_bddXnor( dd, bTemp, bVar ); Cudd_Ref( bPart );
bFunc = Cudd_bddAnd( dd, bTemp = bFunc, bPart ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bPart );
}
// dereference
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
Cudd_RecursiveDeref( dd, (DdNode *)Vec_PtrEntry(vBdds, Abc_ObjId(pObj)) );
Vec_PtrFree( vBdds );
Vec_PtrFree( vNodes );
// reorder
Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
Cudd_Deref( bFunc );
return bFunc;
}
/**Function*************************************************************
Synopsis [Initializes variable partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ResStartPart( int nInputs, unsigned uParts[], int nParts )
{
int i, Group, Left, Shift = 0, Count = 0;
Group = nInputs / nParts;
Left = nInputs % nParts;
for ( i = 0; i < Left; i++ )
{
uParts[i] = (~((~0) << (Group+1))) << Shift;
Shift += Group+1;
}
for ( ; i < nParts; i++ )
{
uParts[i] = (~((~0) << Group)) << Shift;
Shift += Group;
}
for ( i = 0; i < nParts; i++ )
Count += Extra_WordCountOnes( uParts[i] );
assert( Count == nInputs );
}
/**Function*************************************************************
Synopsis [Initializes variable partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ResStartPart2( int nInputs, unsigned uParts[], int nParts )
{
int i, Count = 0;
for ( i = 0; i < nParts; i++ )
uParts[i] = 0;
for ( i = 0; i < nInputs; i++ )
uParts[i % nParts] |= (1 << i);
for ( i = 0; i < nParts; i++ )
Count += Extra_WordCountOnes( uParts[i] );
assert( Count == nInputs );
}
/**Function*************************************************************
Synopsis [Returns one if unique pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ResCheckUnique( char Pats[], int nPats, int pat )
{
int i;
for ( i = 0; i < nPats; i++ )
if ( Pats[i] == pat )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Check if pattern is decomposable with non-strict.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ResCheckNonStrict( char Pattern[], int nVars, int nBits )
{
static char Pat0[256], Pat1[256];
int v, m, nPats0, nPats1, nNumber = (1 << (nBits - 1));
int Result = 0;
for ( v = 0; v < nVars; v++ )
{
nPats0 = nPats1 = 0;
for ( m = 0; m < (1<<nVars); m++ )
{
if ( (m & (1 << v)) == 0 )
{
if ( Abc_ResCheckUnique( Pat0, nPats0, Pattern[m] ) )
{
Pat0[ nPats0++ ] = Pattern[m];
if ( nPats0 > nNumber )
break;
}
}
else
{
if ( Abc_ResCheckUnique( Pat1, nPats1, Pattern[m] ) )
{
Pat1[ nPats1++ ] = Pattern[m];
if ( nPats1 > nNumber )
break;
}
}
}
if ( m == (1<<nVars) )
Result++;
}
return Result;
}
/**Function*************************************************************
Synopsis [Compute the number of distinct cofactors in the BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ResCofCount( DdManager * dd, DdNode * bFunc, unsigned uMask, int * pCheck )
{
static char Pattern[256];
DdNode * pbVars[32];
Vec_Ptr_t * vCofs;
DdNode * bCof, * bCube, * bTemp;
int i, k, Result, nVars = 0;
// collect variables
for ( i = 0; i < 32; i++ )
if ( uMask & (1 << i) )
pbVars[nVars++] = dd->vars[i];
assert( nVars <= 8 );
// compute cofactors
vCofs = Vec_PtrAlloc( 100 );
for ( i = 0; i < (1 << nVars); i++ )
{
bCube = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 ); Cudd_Ref( bCube );
bCof = Cudd_Cofactor( dd, bFunc, bCube ); Cudd_Ref( bCof );
Cudd_RecursiveDeref( dd, bCube );
Vec_PtrForEachEntry( DdNode *, vCofs, bTemp, k )
if ( bTemp == bCof )
break;
if ( k < Vec_PtrSize(vCofs) )
Cudd_RecursiveDeref( dd, bCof );
else
Vec_PtrPush( vCofs, bCof );
Pattern[i] = k;
}
Result = Vec_PtrSize( vCofs );
Vec_PtrForEachEntry( DdNode *, vCofs, bCof, i )
Cudd_RecursiveDeref( dd, bCof );
Vec_PtrFree( vCofs );
if ( pCheck )
{
*pCheck = Abc_ResCheckNonStrict( Pattern, nVars, Abc_Base2Log(Result) );
/*
if ( *pCheck == 1 && nVars == 4 && Result == 8 )
{
for ( i = 0; i < (1 << nVars); i++ )
printf( "%d ", Pattern[i] );
i = 0;
}
*/
}
return Result;
}
/**Function*************************************************************
Synopsis [Computes cost of the partition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ResCost( DdManager * dd, DdNode * bFunc, unsigned uMask, int * pnCofs, int * pCheck )
{
int nCofs = Abc_ResCofCount( dd, bFunc, uMask, pCheck );
int n2Log = Abc_Base2Log( nCofs );
if ( pnCofs ) *pnCofs = nCofs;
return 10000 * n2Log + (nCofs - (1 << (n2Log-1))) * (nCofs - (1 << (n2Log-1)));
}
/**Function*************************************************************
Synopsis [Migrates variables between the two groups.]
Description [Returns 1 if there is change.]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ResMigrate( DdManager * dd, DdNode * bFunc, int nInputs, unsigned uParts[], int iPart1, int iPart2 )
{
unsigned uParts2[2] = { uParts[iPart1], uParts[iPart2] };
int i, k, CostCur, CostBest, fChange = 0;
assert( (uParts[iPart1] & uParts[iPart2]) == 0 );
CostBest = Abc_ResCost( dd, bFunc, uParts[iPart1], NULL, NULL )
+ Abc_ResCost( dd, bFunc, uParts[iPart2], NULL, NULL );
for ( i = 0; i < nInputs; i++ )
if ( uParts[iPart1] & (1 << i) )
{
for ( k = 0; k < nInputs; k++ )
if ( uParts[iPart2] & (1 << k) )
{
if ( i == k )
continue;
uParts[iPart1] ^= (1 << i) | (1 << k);
uParts[iPart2] ^= (1 << i) | (1 << k);
CostCur = Abc_ResCost( dd, bFunc, uParts[iPart1], NULL, NULL ) + Abc_ResCost( dd, bFunc, uParts[iPart2], NULL, NULL );
if ( CostCur < CostBest )
{
CostCur = CostBest;
uParts2[0] = uParts[iPart1];
uParts2[1] = uParts[iPart2];
fChange = 1;
}
uParts[iPart1] ^= (1 << i) | (1 << k);
uParts[iPart2] ^= (1 << i) | (1 << k);
}
}
uParts[iPart1] = uParts2[0];
uParts[iPart2] = uParts2[1];
return fChange;
}
/**Function*************************************************************
Synopsis [Migrates variables between the two groups.]
Description [Returns 1 if there is change.]
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ResPrint( DdManager * dd, DdNode * bFunc, int nInputs, unsigned uParts[], int nParts )
{
int i, k, nCofs, Cost, CostAll = 0, fCheck;
for ( i = 0; i < nParts; i++ )
{
Cost = Abc_ResCost( dd, bFunc, uParts[i], &nCofs, &fCheck );
CostAll += Cost;
for ( k = 0; k < nInputs; k++ )
printf( "%c", (uParts[i] & (1 << k))? 'a' + k : '-' );
printf( " %2d %d-%d %6d ", nCofs, Abc_Base2Log(nCofs), fCheck, Cost );
}
printf( "%4d\n", CostAll );
}
/**Function*************************************************************
Synopsis [PrintCompute the number of distinct cofactors in the BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ResPrintAllCofs( DdManager * dd, DdNode * bFunc, int nInputs, int nCofMax )
{
int i, k, nBits, nCofs, Cost, fCheck;
for ( i = 0; i < (1<<nInputs); i++ )
{
nBits = Extra_WordCountOnes( i );
if ( nBits < 3 || nBits > 6 )
continue;
Cost = Abc_ResCost( dd, bFunc, i, &nCofs, &fCheck );
if ( nCofs > nCofMax )
continue;
for ( k = 0; k < nInputs; k++ )
printf( "%c", (i & (1 << k))? 'a' + k : '-' );
printf( " n=%2d c=%2d l=%d-%d %6d\n",
Extra_WordCountOnes(i), nCofs, Abc_Base2Log(nCofs), fCheck, Cost );
}
}
/**Function*************************************************************
Synopsis [Compute the number of distinct cofactors in the BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ResSwapRandom( DdManager * dd, DdNode * bFunc, int nInputs, unsigned uParts[], int nParts, int nTimes )
{
int i, k, n, iPart1, iPart2;
for ( n = 0; n < nTimes; )
{
// get the vars
i = k = 0;
while ( i == k )
{
i = rand() % nInputs;
k = rand() % nInputs;
}
// find the groups
for ( iPart1 = 0; iPart1 < nParts; iPart1++ )
if ( uParts[iPart1] & (1 << i) )
break;
for ( iPart2 = 0; iPart2 < nParts; iPart2++ )
if ( uParts[iPart2] & (1 << k) )
break;
if ( iPart1 == iPart2 )
continue;
// swap the vars
uParts[iPart1] ^= (1 << i) | (1 << k);
uParts[iPart2] ^= (1 << i) | (1 << k);
n++;
//printf( " " );
//Abc_ResPrint( dd, bFunc, nInputs, uParts, nParts );
}
}
/**Function*************************************************************
Synopsis [Compute the number of distinct cofactors in the BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ResPartition( DdManager * dd, DdNode * bFunc, int nInputs )
{
int nIters = 5;
unsigned uParts[10];
int i, fChange = 1;
int nSuppSize = Cudd_SupportSize( dd, bFunc );
printf( "Ins =%3d. Outs =%2d. Nodes =%3d. Supp =%2d.\n",
nInputs, dd->size-nInputs, Cudd_DagSize(bFunc), nSuppSize );
//Abc_ResPrintAllCofs( dd, bFunc, nInputs, 4 );
if ( nSuppSize <= 6 )
{
printf( "Support is less or equal than 6\n" );
return;
}
if ( nInputs <= 12 )
{
Abc_ResStartPart( nInputs, uParts, 2 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 2 );
for ( i = 0; i < nIters; i++ )
{
if ( i )
{
printf( "Randomizing... \n" );
Abc_ResSwapRandom( dd, bFunc, nInputs, uParts, 2, 20 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 2 );
}
fChange = 1;
while ( fChange )
{
fChange = Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 1 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 2 );
}
}
}
else if ( nInputs > 12 && nInputs <= 18 )
{
Abc_ResStartPart( nInputs, uParts, 3 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
for ( i = 0; i < nIters; i++ )
{
if ( i )
{
printf( "Randomizing... \n" );
Abc_ResSwapRandom( dd, bFunc, nInputs, uParts, 3, 20 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
}
fChange = 1;
while ( fChange )
{
fChange = Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 1 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 2 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 1, 2 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
}
}
}
else if ( nInputs > 18 && nInputs <= 24 )
{
Abc_ResStartPart( nInputs, uParts, 4 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
for ( i = 0; i < nIters; i++ )
{
if ( i )
{
printf( "Randomizing... \n" );
Abc_ResSwapRandom( dd, bFunc, nInputs, uParts, 4, 20 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
}
fChange = 1;
while ( fChange )
{
fChange = Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 1 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 2 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 3 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 1, 2 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 1, 3 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 2, 3 );
Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
}
}
}
// else assert( 0 );
}
/**Function*************************************************************
Synopsis [Compute the number of distinct cofactors in the BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ResPartitionTest( Abc_Ntk_t * pNtk )
{
DdManager * dd;
DdNode * bFunc;
dd = Cudd_Init( Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
bFunc = Abc_ResBuildBdd( pNtk, dd ); Cudd_Ref( bFunc );
Abc_ResPartition( dd, bFunc, Abc_NtkCiNum(pNtk) );
Cudd_RecursiveDeref( dd, bFunc );
Extra_StopManager( dd );
}
/**Function*************************************************************
Synopsis [Compute the number of distinct cofactors in the BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkBddCofCount( DdManager * dd, DdNode * bFunc, DdNode ** pbVars, int nVars )
{
Vec_Ptr_t * vCofs;
DdNode * bCof, * bCube;
int i, Result;
vCofs = Vec_PtrAlloc( 100 );
for ( i = 0; i < (1 << nVars); i++ )
{
bCube = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 ); Cudd_Ref( bCube );
bCof = Cudd_Cofactor( dd, bFunc, bCube ); Cudd_Ref( bCof );
Cudd_RecursiveDeref( dd, bCube );
if ( Vec_PtrPushUnique( vCofs, bCof ) )
Cudd_RecursiveDeref( dd, bCof );
}
Result = Vec_PtrSize( vCofs );
Vec_PtrForEachEntry( DdNode *, vCofs, bCof, i )
Cudd_RecursiveDeref( dd, bCof );
Vec_PtrFree( vCofs );
return Result;
}
/**Function*************************************************************
Synopsis [Compute the number of distinct cofactors in the BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkExploreCofs2( DdManager * dd, DdNode * bFunc, DdNode ** pbVars, int nIns, int nLutSize )
{
int i;
printf( "Inputs = %2d. Nodes = %2d. LutSize = %2d.\n", nIns, Cudd_DagSize(bFunc), nLutSize );
for ( i = 0; i <= nIns - nLutSize; i++ )
printf( "[%2d %2d] : %3d\n", i, i+nLutSize-1, Abc_NtkBddCofCount(dd, bFunc, dd->vars+i, nLutSize) );
}
/**Function*************************************************************
Synopsis [Compute the number of distinct cofactors in the BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkExploreCofs( DdManager * dd, DdNode * bFunc, DdNode ** pbVars, int nIns, int nLutSize )
{
DdManager * ddNew;
DdNode * bFuncNew;
DdNode * pbVarsNew[32];
int i, k, c, nCofs, nBits;
ddNew = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
Cudd_ShuffleHeap( ddNew, dd->invperm );
bFuncNew = Cudd_bddTransfer( dd, ddNew, bFunc ); Cudd_Ref( bFuncNew );
for ( i = 0; i < (1 << nIns); i++ )
{
nBits = Extra_WordCountOnes(i);
if ( nBits != nLutSize && nBits != nLutSize -1 && nBits != nLutSize -2 )
continue;
for ( c = k = 0; k < nIns; k++ )
{
if ( (i & (1 << k)) == 0 )
continue;
// pbVarsNew[c++] = pbVars[k];
pbVarsNew[c++] = ddNew->vars[k];
}
nCofs = Abc_NtkBddCofCount(ddNew, bFuncNew, pbVarsNew, c);
if ( nCofs > 8 )
continue;
for ( c = k = 0; k < nIns; k++ )
{
if ( (i & (1 << k)) == 0 )
{
printf( "-" );
continue;
}
printf( "%c", k + 'a' );
}
printf( " : %2d\n", nCofs );
}
Cudd_RecursiveDeref( ddNew, bFuncNew );
Extra_StopManager( ddNew );
}
/**Function*************************************************************
Synopsis [Find the constant node corresponding to the encoded output value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkBddFindAddConst( DdManager * dd, DdNode * bFunc, int nOuts )
{
int i, TermMask = 0;
DdNode * bFunc0, * bFunc1, * bConst0, * bConst1;
bConst0 = Cudd_ReadLogicZero( dd );
bConst1 = Cudd_ReadOne( dd );
for ( i = 0; i < nOuts; i++ )
{
if ( Cudd_IsComplement(bFunc) )
{
bFunc0 = Cudd_Not(Cudd_E(bFunc));
bFunc1 = Cudd_Not(Cudd_T(bFunc));
}
else
{
bFunc0 = Cudd_E(bFunc);
bFunc1 = Cudd_T(bFunc);
}
assert( bFunc0 == bConst0 || bFunc1 == bConst0 );
if ( bFunc0 == bConst0 )
{
TermMask ^= (1 << i);
bFunc = bFunc1;
}
else
bFunc = bFunc0;
}
assert( bFunc == bConst1 );
return Cudd_addConst( dd, TermMask );
}
/**Function*************************************************************
Synopsis [Recursively construct ADD for BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkBddToAdd_rec( DdManager * dd, DdNode * bFunc, int nOuts, stmm_table * tTable, int fCompl )
{
DdNode * aFunc0, * aFunc1, * aFunc;
DdNode ** ppSlot;
assert( !Cudd_IsComplement(bFunc) );
if ( stmm_find_or_add( tTable, (char *)bFunc, (char ***)&ppSlot ) )
return *ppSlot;
if ( (int)bFunc->index >= Cudd_ReadSize(dd) - nOuts )
{
assert( Cudd_ReadPerm(dd, bFunc->index) >= Cudd_ReadSize(dd) - nOuts );
aFunc = Abc_NtkBddFindAddConst( dd, Cudd_NotCond(bFunc, fCompl), nOuts ); Cudd_Ref( aFunc );
}
else
{
aFunc0 = Abc_NtkBddToAdd_rec( dd, Cudd_Regular(cuddE(bFunc)), nOuts, tTable, fCompl ^ Cudd_IsComplement(cuddE(bFunc)) );
aFunc1 = Abc_NtkBddToAdd_rec( dd, cuddT(bFunc), nOuts, tTable, fCompl );
aFunc = Cudd_addIte( dd, Cudd_addIthVar(dd, bFunc->index), aFunc1, aFunc0 ); Cudd_Ref( aFunc );
}
return (*ppSlot = aFunc);
}
/**Function*************************************************************
Synopsis [R]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkBddToAdd( DdManager * dd, DdNode * bFunc, int nOuts )
{
DdNode * aFunc, * aTemp, * bTemp;
stmm_table * tTable;
stmm_generator * gen;
tTable = stmm_init_table( st__ptrcmp, st__ptrhash );
aFunc = Abc_NtkBddToAdd_rec( dd, Cudd_Regular(bFunc), nOuts, tTable, Cudd_IsComplement(bFunc) );
stmm_foreach_item( tTable, gen, (char **)&bTemp, (char **)&aTemp )
Cudd_RecursiveDeref( dd, aTemp );
stmm_free_table( tTable );
Cudd_Deref( aFunc );
return aFunc;
}
/**Function*************************************************************
Synopsis [Recursively construct ADD for BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkAddToBdd_rec( DdManager * dd, DdNode * aFunc, int nIns, int nOuts, stmm_table * tTable )
{
DdNode * bFunc0, * bFunc1, * bFunc;
DdNode ** ppSlot;
assert( !Cudd_IsComplement(aFunc) );
if ( stmm_find_or_add( tTable, (char *)aFunc, (char ***)&ppSlot ) )
return *ppSlot;
if ( Cudd_IsConstant(aFunc) )
{
assert( Cudd_ReadSize(dd) >= nIns + nOuts );
bFunc = Extra_bddBitsToCube( dd, (int)Cudd_V(aFunc), nOuts, dd->vars + nIns, 1 ); Cudd_Ref( bFunc );
}
else
{
assert( aFunc->index < nIns );
bFunc0 = Abc_NtkAddToBdd_rec( dd, cuddE(aFunc), nIns, nOuts, tTable );
bFunc1 = Abc_NtkAddToBdd_rec( dd, cuddT(aFunc), nIns, nOuts, tTable );
bFunc = Cudd_bddIte( dd, Cudd_bddIthVar(dd, aFunc->index), bFunc1, bFunc0 ); Cudd_Ref( bFunc );
}
return (*ppSlot = bFunc);
}
/**Function*************************************************************
Synopsis [R]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkAddToBdd( DdManager * dd, DdNode * aFunc, int nIns, int nOuts )
{
DdNode * bFunc, * bTemp, * aTemp;
stmm_table * tTable;
stmm_generator * gen;
tTable = stmm_init_table( st__ptrcmp, st__ptrhash );
bFunc = Abc_NtkAddToBdd_rec( dd, aFunc, nIns, nOuts, tTable );
stmm_foreach_item( tTable, gen, (char **)&aTemp, (char **)&bTemp )
Cudd_RecursiveDeref( dd, bTemp );
stmm_free_table( tTable );
Cudd_Deref( bFunc );
return bFunc;
}
/**Function*************************************************************
Synopsis [Computes the characteristic function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkBddDecCharFunc( DdManager * dd, DdNode ** pFuncs, int nOuts, int Mask, int nBits )
{
DdNode * bFunc, * bTemp, * bExor, * bVar;
int i, Count = 0;
bFunc = Cudd_ReadOne( dd ); Cudd_Ref( bFunc );
for ( i = 0; i < nOuts; i++ )
{
if ( (Mask & (1 << i)) == 0 )
continue;
Count++;
bVar = Cudd_bddIthVar( dd, dd->size - nOuts + i );
bExor = Cudd_bddXor( dd, pFuncs[i], bVar ); Cudd_Ref( bExor );
bFunc = Cudd_bddAnd( dd, bTemp = bFunc, Cudd_Not(bExor) ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bExor );
}
Cudd_Deref( bFunc );
assert( Count == nBits );
return bFunc;
}
/**Function*************************************************************
Synopsis [Evaluate Sasao's decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkBddDecTry( reo_man * pReo, DdManager * dd, DdNode ** pFuncs, int nIns, int nOuts, int Mask, int nBits )
{
// int fReorder = 0;
DdNode * bFunc;//, * aFunc, * aFuncNew;
// derive the characteristic function
bFunc = Abc_NtkBddDecCharFunc( dd, pFuncs, nOuts, Mask, nBits ); Cudd_Ref( bFunc );
/*
// transfer to ADD
aFunc = Abc_NtkBddToAdd( dd, bFunc, nOuts ); Cudd_Ref( aFunc );
Cudd_RecursiveDeref( dd, bFunc );
//Abc_NodeShowBddOne( dd, aFunc );
// perform reordering for BDD width
if ( fReorder )
{
aFuncNew = Extra_Reorder( pReo, dd, aFunc, NULL ); Cudd_Ref( aFuncNew );
printf( "Before = %d. After = %d.\n", Cudd_DagSize(aFunc), Cudd_DagSize(aFuncNew) );
Cudd_RecursiveDeref( dd, aFunc );
}
else
aFuncNew = aFunc;
// get back to BDD
bFunc = Abc_NtkAddToBdd( dd, aFuncNew, nIns, nOuts ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, aFuncNew );
//Abc_NodeShowBddOne( dd, bFunc );
// print the result
// reoProfileWidthPrint( pReo );
*/
Cudd_Deref( bFunc );
return bFunc;
}
/**Function*************************************************************
Synopsis [Evaluate Sasao's decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Abc_NtkBddDecInt( reo_man * pReo, DdManager * dd, DdNode ** pFuncs, int nIns, int nOuts )
{
/*
int i, k;
for ( i = 1; i <= nOuts; i++ )
{
for ( k = 0; k < (1<<nOuts); k++ )
if ( Extra_WordCountOnes(k) == i )
{
Extra_PrintBinary( stdout, (unsigned *)&k, nOuts );
Abc_NtkBddDecTry( pReo, dd, pFuncs, nOuts, k, i );
printf( "\n" );
}
}
*/
return Abc_NtkBddDecTry( pReo, dd, pFuncs, nIns, nOuts, ~(1<<(32-nOuts)), nOuts );
}
/**Function*************************************************************
Synopsis [Evaluate Sasao's decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkCreateFromCharFunc( Abc_Ntk_t * pNtk, DdManager * dd, DdNode * bFunc )
{
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pNodeNew, * pNodePo;
int i;
// start the network
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
// create inputs for CIs
pNodeNew = Abc_NtkCreateNode( pNtkNew );
Abc_NtkForEachCi( pNtk, pNode, i )
{
pNode->pCopy = Abc_NtkCreatePi( pNtkNew );
Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
Abc_ObjAssignName( pNode->pCopy, Abc_ObjName(pNode), NULL );
}
// create inputs for COs
Abc_NtkForEachCo( pNtk, pNode, i )
{
pNode->pCopy = Abc_NtkCreatePi( pNtkNew );
Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
Abc_ObjAssignName( pNode->pCopy, Abc_ObjName(pNode), NULL );
}
// transfer BDD
pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData );
// transfer BDD into to be the local function
pNodePo = Abc_NtkCreatePo( pNtkNew );
Abc_ObjAddFanin( pNodePo, pNodeNew );
Abc_ObjAssignName( pNodePo, "out", NULL );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkCreateFromCharFunc(): Network check has failed.\n" );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Evaluate Sasao's decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose )
{
int nBddSizeMax = 1000000;
int fDropInternal = 0;
int fReorder = 1;
Abc_Ntk_t * pNtkNew;
reo_man * pReo;
DdManager * dd;
DdNode * pFuncs[BDD_FUNC_MAX];
DdNode * bFunc;
Abc_Obj_t * pNode;
int i;
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkCoNum(pNtk) <= BDD_FUNC_MAX );
dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddSizeMax, fDropInternal, fReorder, fVerbose );
if ( dd == NULL )
{
Abc_Print( -1, "Construction of global BDDs has failed.\n" );
return NULL;
}
// collect global BDDs
Abc_NtkForEachCo( pNtk, pNode, i )
pFuncs[i] = (DdNode *)Abc_ObjGlobalBdd(pNode);
// create new variables at the bottom
assert( dd->size == Abc_NtkCiNum(pNtk) );
for ( i = 0; i < Abc_NtkCoNum(pNtk); i++ )
Cudd_addNewVarAtLevel( dd, dd->size );
// prepare reordering engine
pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
Extra_ReorderSetMinimizationType( pReo, REO_MINIMIZE_WIDTH );
Extra_ReorderSetVerification( pReo, 1 );
Extra_ReorderSetVerbosity( pReo, 1 );
// derive characteristic function
bFunc = Abc_NtkBddDecInt( pReo, dd, pFuncs, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk) ); Cudd_Ref( bFunc );
Extra_ReorderQuit( pReo );
Abc_NtkExploreCofs( dd, bFunc, dd->vars, Abc_NtkCiNum(pNtk), 6 );
// create new network
// pNtkNew = Abc_NtkCreateFromCharFunc( pNtk, dd, bFunc );
pNtkNew = Abc_NtkDup( pNtk );
// cleanup
Cudd_RecursiveDeref( dd, bFunc );
Abc_NtkFreeGlobalBdds( pNtk, 1 );
return pNtkNew;
}
ABC_NAMESPACE_IMPL_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////