src/aig/kit/kitCloud.c File Reference

#include "kit.h"
Include dependency graph for kitCloud.c:

Go to the source code of this file.

Data Structures

struct  Kit_Mux_t_

Typedefs

typedef struct Kit_Mux_t_ Kit_Mux_t

Functions

CloudNode * Kit_TruthToCloud5_rec (CloudManager *dd, unsigned uTruth, int nVars, int nVarsAll)
CloudNode * Kit_TruthToCloud_rec (CloudManager *dd, unsigned *pTruth, int nVars, int nVarsAll)
CloudNode * Kit_TruthToCloud (CloudManager *dd, unsigned *pTruth, int nVars)
int Kit_CreateCloud (CloudManager *dd, CloudNode *pFunc, Vec_Int_t *vNodes)
int Kit_CreateCloudFromTruth (CloudManager *dd, unsigned *pTruth, int nVars, Vec_Int_t *vNodes)
unsigned * Kit_CloudToTruth (Vec_Int_t *vNodes, int nVars, Vec_Ptr_t *vStore, int fInv)
unsigned * Kit_TruthCompose (CloudManager *dd, unsigned *pTruth, int nVars, unsigned **pInputs, int nVarsAll, Vec_Ptr_t *vStore, Vec_Int_t *vNodes)
void Kit_TruthCofSupports (Vec_Int_t *vBddDir, Vec_Int_t *vBddInv, int nVars, Vec_Int_t *vMemory, unsigned *puSupps)

Typedef Documentation

typedef struct Kit_Mux_t_ Kit_Mux_t

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

] DECLARATIONS ///

Definition at line 28 of file kitCloud.c.

Function Documentation

unsigned* Kit_CloudToTruth ( Vec_Int_t *  vNodes,
int  nVars,
Vec_Ptr_t *  vStore,
int  fInv 
)

Function*************************************************************

Synopsis [Computes composition of truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file kitCloud.c.

00224 {
00225     unsigned * pThis, * pFan0, * pFan1;
00226     Kit_Mux_t Mux;
00227     int i, Entry;
00228     assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
00229     pThis = Vec_PtrEntry( vStore, 0 );
00230     Kit_TruthFill( pThis, nVars );
00231     Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
00232     {
00233         Mux = *((Kit_Mux_t *)&Entry);
00234         assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );          
00235         pFan0 = Vec_PtrEntry( vStore, Mux.e );
00236         pFan1 = Vec_PtrEntry( vStore, Mux.t );
00237         pThis = Vec_PtrEntry( vStore, i );
00238         Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
00239     } 
00240     // complement the result
00241     if ( Mux.i )
00242         Kit_TruthNot( pThis, pThis, nVars );
00243     return pThis;
00244 }

int Kit_CreateCloud ( CloudManager *  dd,
CloudNode *  pFunc,
Vec_Int_t *  vNodes 
)

Function********************************************************************

Synopsis [Transforms the array of BDDs into the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 161 of file kitCloud.c.

00162 {
00163     Kit_Mux_t Mux;
00164     int nNodes, i;
00165     // collect BDD nodes
00166     nNodes = Cloud_DagCollect( dd, pFunc );
00167     if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
00168         return 0;
00169     assert( nNodes == Cloud_DagSize( dd, pFunc ) );
00170     assert( nNodes < dd->nNodesLimit );
00171     Vec_IntClear( vNodes );
00172     Vec_IntPush( vNodes, 0 ); // const1 node
00173     dd->ppNodes[0]->s = 0;
00174     for ( i = 1; i < nNodes; i++ )
00175     {
00176         dd->ppNodes[i]->s = i;
00177         Mux.v = dd->ppNodes[i]->v;
00178         Mux.t = dd->ppNodes[i]->t->s;
00179         Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
00180         Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e); 
00181         Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
00182         // put the MUX into the array
00183         Vec_IntPush( vNodes, *((int *)&Mux) );
00184     }
00185     assert( Vec_IntSize(vNodes) == nNodes );
00186     // reset signatures
00187     for ( i = 0; i < nNodes; i++ )
00188         dd->ppNodes[i]->s = dd->nSignCur;
00189     return 1;
00190 }

int Kit_CreateCloudFromTruth ( CloudManager *  dd,
unsigned *  pTruth,
int  nVars,
Vec_Int_t *  vNodes 
)

Function********************************************************************

Synopsis [Transforms the array of BDDs into the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file kitCloud.c.

00204 {
00205     CloudNode * pFunc;
00206     Cloud_Restart( dd );
00207     pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
00208     Vec_IntClear( vNodes );
00209     return Kit_CreateCloud( dd, pFunc, vNodes );
00210 }

void Kit_TruthCofSupports ( Vec_Int_t *  vBddDir,
Vec_Int_t *  vBddInv,
int  nVars,
Vec_Int_t *  vMemory,
unsigned *  puSupps 
)

Function********************************************************************

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 304 of file kitCloud.c.

00305 {
00306     Kit_Mux_t Mux;
00307     unsigned * puSuppAll, * pThis, * pFan0, * pFan1;
00308     int i, v, Var, Entry, nSupps;
00309     nSupps = 2 * nVars;
00310 
00311     // extend storage
00312     if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
00313         Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
00314     puSuppAll = Vec_IntArray( vMemory );
00315     // clear storage for the const node
00316     memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
00317     // compute supports from nodes
00318     Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
00319     {
00320         Mux = *((Kit_Mux_t *)&Entry);
00321         Var = nVars - 1 - Mux.v;
00322         pFan0 = puSuppAll + nSupps * Mux.e;
00323         pFan1 = puSuppAll + nSupps * Mux.t;
00324         pThis = puSuppAll + nSupps * i;
00325         for ( v = 0; v < nSupps; v++ )
00326             pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
00327         assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
00328         assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
00329         pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
00330         pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
00331     }
00332     // copy the result
00333     memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
00334     // compute the inverse
00335 
00336     // extend storage
00337     if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
00338         Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
00339     puSuppAll = Vec_IntArray( vMemory );
00340     // clear storage for the const node
00341     memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
00342     // compute supports from nodes
00343     Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
00344     {
00345         Mux = *((Kit_Mux_t *)&Entry);
00346 //        Var = nVars - 1 - Mux.v;
00347         Var = Mux.v;
00348         pFan0 = puSuppAll + nSupps * Mux.e;
00349         pFan1 = puSuppAll + nSupps * Mux.t;
00350         pThis = puSuppAll + nSupps * i;
00351         for ( v = 0; v < nSupps; v++ )
00352             pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
00353         assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
00354         assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
00355         pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
00356         pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
00357     }
00358 
00359     // merge supports
00360     for ( Var = 0; Var < nSupps; Var++ )
00361         puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
00362 }

unsigned* Kit_TruthCompose ( CloudManager *  dd,
unsigned *  pTruth,
int  nVars,
unsigned **  pInputs,
int  nVarsAll,
Vec_Ptr_t *  vStore,
Vec_Int_t *  vNodes 
)

Function*************************************************************

Synopsis [Computes composition of truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 257 of file kitCloud.c.

00259 {
00260     CloudNode * pFunc;
00261     unsigned * pThis, * pFan0, * pFan1;
00262     Kit_Mux_t Mux;
00263     int i, Entry, RetValue;
00264     // derive BDD from truth table
00265     Cloud_Restart( dd );
00266     pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
00267     // convert it into nodes
00268     RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
00269     if ( RetValue == 0 )
00270         printf( "Kit_TruthCompose(): Internal failure!!!\n" );
00271     // verify the result
00272 //    pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
00273 //    if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
00274 //        printf( "Failed!\n" );
00275     // compute truth table from the BDD
00276     assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
00277     pThis = Vec_PtrEntry( vStore, 0 );
00278     Kit_TruthFill( pThis, nVarsAll );
00279     Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
00280     {
00281         Mux = *((Kit_Mux_t *)&Entry);
00282         pFan0 = Vec_PtrEntry( vStore, Mux.e );
00283         pFan1 = Vec_PtrEntry( vStore, Mux.t );
00284         pThis = Vec_PtrEntry( vStore, i );
00285         Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
00286     }
00287     // complement the result
00288     if ( Mux.i )
00289         Kit_TruthNot( pThis, pThis, nVarsAll );
00290     return pThis;
00291 }

CloudNode* Kit_TruthToCloud ( CloudManager *  dd,
unsigned *  pTruth,
int  nVars 
)

Function********************************************************************

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file kitCloud.c.

00143 {
00144     CloudNode * pRes;
00145     pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
00146 //    printf( "%d/%d  ", Count, Cloud_DagSize(dd, pRes) );
00147     return pRes;
00148 }

CloudNode* Kit_TruthToCloud5_rec ( CloudManager *  dd,
unsigned  uTruth,
int  nVars,
int  nVarsAll 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Derive BDD from the truth table for 5 variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file kitCloud.c.

00054 {
00055     static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
00056     CloudNode * pCof0, * pCof1;
00057     unsigned uCof0, uCof1;
00058     assert( nVars <= 5 );
00059     if ( uTruth == 0 )
00060         return dd->zero;
00061     if ( uTruth == ~0 )
00062         return dd->one;
00063     if ( nVars == 1 )
00064     {
00065         if ( uTruth == uVars[0] )
00066             return dd->vars[nVarsAll-1];
00067         if ( uTruth == ~uVars[0] )
00068             return Cloud_Not(dd->vars[nVarsAll-1]);
00069         assert( 0 );
00070     }
00071 //    Count++;
00072     assert( nVars > 1 );
00073     uCof0 = uTruth & ~uVars[nVars-1];
00074     uCof1 = uTruth &  uVars[nVars-1];
00075     uCof0 |= uCof0 << (1<<(nVars-1));
00076     uCof1 |= uCof1 >> (1<<(nVars-1));
00077     if ( uCof0 == uCof1 )
00078         return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
00079     if ( uCof0 == ~uCof1 )
00080     {
00081         pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
00082         pCof1 = Cloud_Not( pCof0 );
00083     }
00084     else
00085     {
00086         pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
00087         pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll );
00088     }
00089     return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
00090 }

CloudNode* Kit_TruthToCloud_rec ( CloudManager *  dd,
unsigned *  pTruth,
int  nVars,
int  nVarsAll 
)

Function********************************************************************

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 103 of file kitCloud.c.

00104 {
00105     CloudNode * pCof0, * pCof1;
00106     unsigned * pTruth0, * pTruth1;
00107     if ( nVars <= 5 )
00108         return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll );
00109     if ( Kit_TruthIsConst0(pTruth, nVars) )
00110         return dd->zero;
00111     if ( Kit_TruthIsConst1(pTruth, nVars) )
00112         return dd->one;
00113 //    Count++;
00114     pTruth0 = pTruth;
00115     pTruth1 = pTruth + Kit_TruthWordNum(nVars-1);
00116     if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) )
00117         return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
00118     if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) )
00119     {
00120         pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
00121         pCof1 = Cloud_Not( pCof0 );
00122     }
00123     else
00124     {
00125         pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
00126         pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll );
00127     }
00128     return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
00129 }

Generated on Tue Jan 5 12:18:27 2010 for abc70930 by  doxygen 1.6.1