ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
kitCloud.c File Reference
#include "kit.h"
Include dependency graph for kitCloud.c:

Go to the source code of this file.

Classes

struct  Kit_Mux_t_
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t
 DECLARATIONS ///.
 

Functions

CloudNode * Kit_TruthToCloud5_rec (CloudManager *dd, unsigned uTruth, int nVars, int nVarsAll)
 FUNCTION DEFINITIONS ///.
 
CloudNode * Kit_TruthToCloud_rec (CloudManager *dd, unsigned *pTruth, int nVars, int nVarsAll)
 
CloudNode * Kit_TruthToCloud (CloudManager *dd, unsigned *pTruth, int nVars)
 FUNCTION DECLARATIONS ///.
 
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

◆ Kit_Mux_t

typedef typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t

DECLARATIONS ///.

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

]

Definition at line 31 of file kitCloud.c.

Function Documentation

◆ Kit_CloudToTruth()

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 229 of file kitCloud.c.

230{
231 unsigned * pThis, * pFan0, * pFan1;
232 Kit_Mux_t Mux;
233 int i, Entry;
234 assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
235 pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
236 Kit_TruthFill( pThis, nVars );
237 Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
238 {
239 Mux = Kit_Int2Mux(Entry);
240 assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );
241 pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
242 pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
243 pThis = (unsigned *)Vec_PtrEntry( vStore, i );
244 Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
245 }
246 // complement the result
247 if ( Mux.i )
248 Kit_TruthNot( pThis, pThis, nVars );
249 return pThis;
250}
Kit_Mux_t
typedefABC_NAMESPACE_IMPL_START struct Kit_Mux_t_ Kit_Mux_t
DECLARATIONS ///.
Definition kitCloud.c:31
Kit_TruthMuxVarPhase
void Kit_TruthMuxVarPhase(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar, int fCompl0)
Definition kitTruth.c:1125
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the call graph for this function:

◆ Kit_CreateCloud()

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 167 of file kitCloud.c.

168{
169 Kit_Mux_t Mux;
170 int nNodes, i;
171 // collect BDD nodes
172 nNodes = Cloud_DagCollect( dd, pFunc );
173 if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
174 return 0;
175 assert( nNodes == Cloud_DagSize( dd, pFunc ) );
176 assert( nNodes < dd->nNodesLimit );
177 Vec_IntClear( vNodes );
178 Vec_IntPush( vNodes, 0 ); // const1 node
179 dd->ppNodes[0]->s = 0;
180 for ( i = 1; i < nNodes; i++ )
181 {
182 dd->ppNodes[i]->s = i;
183 Mux.v = dd->ppNodes[i]->v;
184 Mux.t = dd->ppNodes[i]->t->s;
185 Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
186 Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e);
187 Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
188 // put the MUX into the array
189 Vec_IntPush( vNodes, Kit_Mux2Int(Mux) );
190 }
191 assert( Vec_IntSize(vNodes) == nNodes );
192 // reset signatures
193 for ( i = 0; i < nNodes; i++ )
194 dd->ppNodes[i]->s = dd->nSignCur;
195 return 1;
196}
Cloud_DagCollect
int Cloud_DagCollect(CloudManager *dd, CloudNode *n)
Definition cloud.c:772
Cloud_DagSize
int Cloud_DagSize(CloudManager *dd, CloudNode *n)
Definition cloud.c:721
Cloud_Regular
#define Cloud_Regular(p)
Definition cloud.h:185
Cloud_IsComplement
#define Cloud_IsComplement(p)
Definition cloud.h:188
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_CreateCloudFromTruth()

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 209 of file kitCloud.c.

210{
211 CloudNode * pFunc;
212 Cloud_Restart( dd );
213 pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
214 Vec_IntClear( vNodes );
215 return Kit_CreateCloud( dd, pFunc, vNodes );
216}
Cloud_Restart
void Cloud_Restart(CloudManager *dd)
Definition cloud.c:166
CloudNode
struct cloudNode CloudNode
Definition cloud.h:55
Kit_CreateCloud
int Kit_CreateCloud(CloudManager *dd, CloudNode *pFunc, Vec_Int_t *vNodes)
Definition kitCloud.c:167
Kit_TruthToCloud
CloudNode * Kit_TruthToCloud(CloudManager *dd, unsigned *pTruth, int nVars)
FUNCTION DECLARATIONS ///.
Definition kitCloud.c:148
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthCofSupports()

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 310 of file kitCloud.c.

311{
312 Kit_Mux_t Mux;
313 unsigned * puSuppAll;
314 unsigned * pThis = NULL; // Suppress "might be used uninitialized"
315 unsigned * pFan0, * pFan1;
316 int i, v, Var, Entry, nSupps;
317 nSupps = 2 * nVars;
318
319 // extend storage
320 if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
321 Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
322 puSuppAll = (unsigned *)Vec_IntArray( vMemory );
323 // clear storage for the const node
324 memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
325 // compute supports from nodes
326 Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
327 {
328 Mux = Kit_Int2Mux(Entry);
329 Var = nVars - 1 - Mux.v;
330 pFan0 = puSuppAll + nSupps * Mux.e;
331 pFan1 = puSuppAll + nSupps * Mux.t;
332 pThis = puSuppAll + nSupps * i;
333 for ( v = 0; v < nSupps; v++ )
334 pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
335 assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
336 assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
337 pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
338 pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
339 }
340 // copy the result
341 memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
342 // compute the inverse
343
344 // extend storage
345 if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
346 Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
347 puSuppAll = (unsigned *)Vec_IntArray( vMemory );
348 // clear storage for the const node
349 memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
350 // compute supports from nodes
351 Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
352 {
353 Mux = Kit_Int2Mux(Entry);
354// Var = nVars - 1 - Mux.v;
355 Var = Mux.v;
356 pFan0 = puSuppAll + nSupps * Mux.e;
357 pFan1 = puSuppAll + nSupps * Mux.t;
358 pThis = puSuppAll + nSupps * i;
359 for ( v = 0; v < nSupps; v++ )
360 pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
361 assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
362 assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
363 pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
364 pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
365 }
366
367 // merge supports
368 for ( Var = 0; Var < nSupps; Var++ )
369 puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
370}
Var
int Var
Definition exorList.c:228
memcpy
char * memcpy()
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthCompose()

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 263 of file kitCloud.c.

265{
266 CloudNode * pFunc;
267 unsigned * pThis, * pFan0, * pFan1;
268 Kit_Mux_t Mux;
269 int i, Entry, RetValue;
270 // derive BDD from truth table
271 Cloud_Restart( dd );
272 pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
273 // convert it into nodes
274 RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
275 if ( RetValue == 0 )
276 printf( "Kit_TruthCompose(): Internal failure!!!\n" );
277 // verify the result
278// pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
279// if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
280// printf( "Failed!\n" );
281 // compute truth table from the BDD
282 assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
283 pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
284 Kit_TruthFill( pThis, nVarsAll );
285 Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
286 {
287 Mux = Kit_Int2Mux(Entry);
288 pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
289 pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
290 pThis = (unsigned *)Vec_PtrEntry( vStore, i );
291 Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
292 }
293 // complement the result
294 if ( Mux.i )
295 Kit_TruthNot( pThis, pThis, nVarsAll );
296 return pThis;
297}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthToCloud()

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

FUNCTION DECLARATIONS ///.

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

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file kitCloud.c.

149{
150 CloudNode * pRes;
151 pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
152// printf( "%d/%d ", Count, Cloud_DagSize(dd, pRes) );
153 return pRes;
154}
Kit_TruthToCloud_rec
CloudNode * Kit_TruthToCloud_rec(CloudManager *dd, unsigned *pTruth, int nVars, int nVarsAll)
Definition kitCloud.c:109
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthToCloud5_rec()

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 59 of file kitCloud.c.

60{
61 static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
62 CloudNode * pCof0, * pCof1;
63 unsigned uCof0, uCof1;
64 assert( nVars <= 5 );
65 if ( uTruth == 0 )
66 return dd->zero;
67 if ( uTruth == ~0 )
68 return dd->one;
69 if ( nVars == 1 )
70 {
71 if ( uTruth == uVars[0] )
72 return dd->vars[nVarsAll-1];
73 if ( uTruth == ~uVars[0] )
74 return Cloud_Not(dd->vars[nVarsAll-1]);
75 assert( 0 );
76 }
77// Count++;
78 assert( nVars > 1 );
79 uCof0 = uTruth & ~uVars[nVars-1];
80 uCof1 = uTruth & uVars[nVars-1];
81 uCof0 |= uCof0 << (1<<(nVars-1));
82 uCof1 |= uCof1 >> (1<<(nVars-1));
83 if ( uCof0 == uCof1 )
84 return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
85 if ( uCof0 == ~uCof1 )
86 {
87 pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
88 pCof1 = Cloud_Not( pCof0 );
89 }
90 else
91 {
92 pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
93 pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll );
94 }
95 return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
96}
Cloud_MakeNode
CloudNode * Cloud_MakeNode(CloudManager *dd, CloudVar v, CloudNode *t, CloudNode *e)
Definition cloud.c:254
Cloud_Not
#define Cloud_Not(p)
Definition cloud.h:186
Kit_TruthToCloud5_rec
CloudNode * Kit_TruthToCloud5_rec(CloudManager *dd, unsigned uTruth, int nVars, int nVarsAll)
FUNCTION DEFINITIONS ///.
Definition kitCloud.c:59
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthToCloud_rec()

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 109 of file kitCloud.c.

110{
111 CloudNode * pCof0, * pCof1;
112 unsigned * pTruth0, * pTruth1;
113 if ( nVars <= 5 )
114 return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll );
115 if ( Kit_TruthIsConst0(pTruth, nVars) )
116 return dd->zero;
117 if ( Kit_TruthIsConst1(pTruth, nVars) )
118 return dd->one;
119// Count++;
120 pTruth0 = pTruth;
121 pTruth1 = pTruth + Kit_TruthWordNum(nVars-1);
122 if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) )
123 return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
124 if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) )
125 {
126 pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
127 pCof1 = Cloud_Not( pCof0 );
128 }
129 else
130 {
131 pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
132 pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll );
133 }
134 return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
135}
Here is the call graph for this function:
Here is the caller graph for this function: