/**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<