diff options
Diffstat (limited to 'src/bool/kit/kitCloud.c')
| -rw-r--r-- | src/bool/kit/kitCloud.c | 378 |
1 files changed, 378 insertions, 0 deletions
diff --git a/src/bool/kit/kitCloud.c b/src/bool/kit/kitCloud.c new file mode 100644 index 00000000..dea56749 --- /dev/null +++ b/src/bool/kit/kitCloud.c @@ -0,0 +1,378 @@ +/**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 + |