summaryrefslogtreecommitdiffstats
path: root/src/aig/kit/kitCloud.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/kit/kitCloud.c')
-rw-r--r--src/aig/kit/kitCloud.c378
1 files changed, 0 insertions, 378 deletions
diff --git a/src/aig/kit/kitCloud.c b/src/aig/kit/kitCloud.c
deleted file mode 100644
index dea56749..00000000
--- a/src/aig/kit/kitCloud.c
+++ /dev/null
@@ -1,378 +0,0 @@
-/**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
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 18:20:37 +0000