/**CFile****************************************************************
FileName [kitCloud.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [Procedures using BDD package CLOUD.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [$Id: kitCloud.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
***********************************************************************/
#include "kit.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// internal representation of the function to be decomposed
typedef struct Kit_Mux_t_ Kit_Mux_t;
struct Kit_Mux_t_
{
unsigned v : 5; // variable
unsigned t : 12; // then edge
unsigned e : 12; // else edge
unsigned c : 1; // complemented attr of else edge
unsigned i : 1; // complemented attr of top node
};
static inline int Kit_Mux2Int( Kit_Mux_t m ) { union { Kit_Mux_t x; int y; } v; v.x = m; return v.y; }
static inline Kit_Mux_t Kit_Int2Mux( int m ) { union { Kit_Mux_t x; int y; } v; v.y = m; return v.x; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Derive BDD from the truth table for 5 variable functions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
CloudNode * Kit_TruthToCloud5_rec( CloudManager * dd, unsigned uTruth, int nVars, int nVarsAll )
{
static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
CloudNode * pCof0, * pCof1;
unsigned uCof0, uCof1;
assert( nVars <= 5 );
if ( uTruth == 0 )
return dd->zero;
if ( uTruth == ~0 )
return dd->one;
if ( nVars == 1 )
{
if ( uTruth == uVars[0] )
return dd->vars[nVarsAll-1];
if ( uTruth == ~uVars[0] )
return Cloud_Not(dd->vars[nVarsAll-1]);
assert( 0 );
}
// Count++;
assert( nVars > 1 );
uCof0 = uTruth & ~uVars[nVars-1];
uCof1 = uTruth & uVars[nVars-1];
uCof0 |= uCof0 << (1<<(nVars-1));
uCof1 |= uCof1 >> (1<<(nVars-1));
if ( uCof0 == uCof1 )
return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
if ( uCof0 == ~uCof1 )
{
pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
pCof1 = Cloud_Not( pCof0 );
}
else
{
pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll );
}
return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
}
/**Function********************************************************************
Synopsis [Compute BDD for the truth table.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
CloudNode * Kit_TruthToCloud_rec( CloudManager * dd, unsigned * pTruth, int nVars, int nVarsAll )
{
CloudNode * pCof0, * pCof1;
unsigned * pTruth0, * pTruth1;
if ( nVars <= 5 )
return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll );
if ( Kit_TruthIsConst0(pTruth, nVars) )
return dd->zero;
if ( Kit_TruthIsConst1(pTruth, nVars) )
return dd->one;
// Count++;
pTruth0 = pTruth;
pTruth1 = pTruth + Kit_TruthWordNum(nVars-1);
if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) )
return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) )
{
pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
pCof1 = Cloud_Not( pCof0 );
}
else
{
pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll );
}
return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
}
/**Function********************************************************************
Synopsis [Compute BDD for the truth table.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars )
{
CloudNode * pRes;
pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
// printf( "%d/%d ", Count, Cloud_DagSize(dd, pRes) );
return pRes;
}
/**Function********************************************************************
Synopsis [Transforms the array of BDDs into the integer array.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes )
{
Kit_Mux_t Mux;
int nNodes, i;
// collect BDD nodes
nNodes = Cloud_DagCollect( dd, pFunc );
if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
return 0;
assert( nNodes == Cloud_DagSize( dd, pFunc ) );
assert( nNodes < dd->nNodesLimit );
Vec_IntClear( vNodes );
Vec_IntPush( vNodes, 0 ); // const1 node
dd->ppNodes[0]->s = 0;
for ( i = 1; i < nNodes; i++ )
{
dd->ppNodes[i]->s = i;
Mux.v = dd->ppNodes[i]->v;
Mux.t = dd->ppNodes[i]->t->s;
Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e);
Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
// put the MUX into the array
Vec_IntPush( vNodes, Kit_Mux2Int(Mux) );
}
assert( Vec_IntSize(vNodes) == nNodes );
// reset signatures
for ( i = 0; i < nNodes; i++ )
dd->ppNodes[i]->s = dd->nSignCur;
return 1;
}
/**Function********************************************************************
Synopsis [Transforms the array of BDDs into the integer array.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes )
{
CloudNode * pFunc;
Cloud_Restart( dd );
pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
Vec_IntClear( vNodes );
return Kit_CreateCloud( dd, pFunc, vNodes );
}
/**Function*************************************************************
Synopsis [Computes composition of truth tables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv )
{
unsigned * pThis, * pFan0, * pFan1;
Kit_Mux_t Mux;
int i, Entry;
assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
Kit_TruthFill( pThis, nVars );
Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
{
Mux = Kit_Int2Mux(Entry);
assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );
pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
pThis = (unsigned *)Vec_PtrEntry( vStore, i );
Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
}
// complement the result
if ( Mux.i )
Kit_TruthNot( pThis, pThis, nVars );
return pThis;
}
/**Function*************************************************************
Synopsis [Computes composition of truth tables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars,
unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes )
{
CloudNode * pFunc;
unsigned * pThis, * pFan0, * pFan1;
Kit_Mux_t Mux;
int i, Entry, RetValue;
// derive BDD from truth table
Cloud_Restart( dd );
pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
// convert it into nodes
RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
if ( RetValue == 0 )
printf( "Kit_TruthCompose(): Internal failure!!!\n" );
// verify the result
// pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
// if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
// printf( "Failed!\n" );
// compute truth table from the BDD
assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
Kit_TruthFill( pThis, nVarsAll );
Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
{
Mux = Kit_Int2Mux(Entry);
pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
pThis = (unsigned *)Vec_PtrEntry( vStore, i );
Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
}
// complement the result
if ( Mux.i )
Kit_TruthNot( pThis, pThis, nVarsAll );
return pThis;
}
/**Function********************************************************************
Synopsis [Compute BDD for the truth table.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps )
{
Kit_Mux_t Mux;
unsigned * puSuppAll;
unsigned * pThis = NULL; // Suppress "might be used uninitialized"
unsigned * pFan0, * pFan1;
int i, v, Var, Entry, nSupps;
nSupps = 2 * nVars;
// extend storage
if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
puSuppAll = (unsigned *)Vec_IntArray( vMemory );
// clear storage for the const node
memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
// compute supports from nodes
Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
{
Mux = Kit_Int2Mux(Entry);
Var = nVars - 1 - Mux.v;
pFan0 = puSuppAll + nSupps * Mux.e;
pFan1 = puSuppAll + nSupps * Mux.t;
pThis = puSuppAll + nSupps * i;
for ( v = 0; v < nSupps; v++ )
pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
}
// copy the result
memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
// compute the inverse
// extend storage
if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
puSuppAll = (unsigned *)Vec_IntArray( vMemory );
// clear storage for the const node
memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
// compute supports from nodes
Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
{
Mux = Kit_Int2Mux(Entry);
// Var = nVars - 1 - Mux.v;
Var = Mux.v;
pFan0 = puSuppAll + nSupps * Mux.e;
pFan1 = puSuppAll + nSupps * Mux.t;
pThis = puSuppAll + nSupps * i;
for ( v = 0; v < nSupps; v++ )
pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
}
// merge supports
for ( Var = 0; Var < nSupps; Var++ )
puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END