1 /**CFile****************************************************************
2
3 FileName [kitCloud.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Computation kit.]
8
9 Synopsis [Procedures using BDD package CLOUD.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - Dec 6, 2006.]
16
17 Revision [$Id: kitCloud.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "kit.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 // internal representation of the function to be decomposed
31 typedef struct Kit_Mux_t_ Kit_Mux_t;
32 struct Kit_Mux_t_
33 {
34 unsigned v : 5; // variable
35 unsigned t : 12; // then edge
36 unsigned e : 12; // else edge
37 unsigned c : 1; // complemented attr of else edge
38 unsigned i : 1; // complemented attr of top node
39 };
40
Kit_Mux2Int(Kit_Mux_t m)41 static inline int Kit_Mux2Int( Kit_Mux_t m ) { union { Kit_Mux_t x; int y; } v; v.x = m; return v.y; }
Kit_Int2Mux(int m)42 static inline Kit_Mux_t Kit_Int2Mux( int m ) { union { Kit_Mux_t x; int y; } v; v.y = m; return v.x; }
43
44 ////////////////////////////////////////////////////////////////////////
45 /// FUNCTION DEFINITIONS ///
46 ////////////////////////////////////////////////////////////////////////
47
48 /**Function*************************************************************
49
50 Synopsis [Derive BDD from the truth table for 5 variable functions.]
51
52 Description []
53
54 SideEffects []
55
56 SeeAlso []
57
58 ***********************************************************************/
Kit_TruthToCloud5_rec(CloudManager * dd,unsigned uTruth,int nVars,int nVarsAll)59 CloudNode * Kit_TruthToCloud5_rec( CloudManager * dd, unsigned uTruth, int nVars, int nVarsAll )
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 }
97
98 /**Function********************************************************************
99
100 Synopsis [Compute BDD for the truth table.]
101
102 Description []
103
104 SideEffects []
105
106 SeeAlso []
107
108 ******************************************************************************/
Kit_TruthToCloud_rec(CloudManager * dd,unsigned * pTruth,int nVars,int nVarsAll)109 CloudNode * Kit_TruthToCloud_rec( CloudManager * dd, unsigned * pTruth, int nVars, int nVarsAll )
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 }
136
137 /**Function********************************************************************
138
139 Synopsis [Compute BDD for the truth table.]
140
141 Description []
142
143 SideEffects []
144
145 SeeAlso []
146
147 ******************************************************************************/
Kit_TruthToCloud(CloudManager * dd,unsigned * pTruth,int nVars)148 CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars )
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 }
155
156 /**Function********************************************************************
157
158 Synopsis [Transforms the array of BDDs into the integer array.]
159
160 Description []
161
162 SideEffects []
163
164 SeeAlso []
165
166 ******************************************************************************/
Kit_CreateCloud(CloudManager * dd,CloudNode * pFunc,Vec_Int_t * vNodes)167 int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes )
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 }
197
198 /**Function********************************************************************
199
200 Synopsis [Transforms the array of BDDs into the integer array.]
201
202 Description []
203
204 SideEffects []
205
206 SeeAlso []
207
208 ******************************************************************************/
Kit_CreateCloudFromTruth(CloudManager * dd,unsigned * pTruth,int nVars,Vec_Int_t * vNodes)209 int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes )
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 }
217
218 /**Function*************************************************************
219
220 Synopsis [Computes composition of truth tables.]
221
222 Description []
223
224 SideEffects []
225
226 SeeAlso []
227
228 ***********************************************************************/
Kit_CloudToTruth(Vec_Int_t * vNodes,int nVars,Vec_Ptr_t * vStore,int fInv)229 unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv )
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 }
251
252 /**Function*************************************************************
253
254 Synopsis [Computes composition of truth tables.]
255
256 Description []
257
258 SideEffects []
259
260 SeeAlso []
261
262 ***********************************************************************/
Kit_TruthCompose(CloudManager * dd,unsigned * pTruth,int nVars,unsigned ** pInputs,int nVarsAll,Vec_Ptr_t * vStore,Vec_Int_t * vNodes)263 unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars,
264 unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes )
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 }
298
299 /**Function********************************************************************
300
301 Synopsis [Compute BDD for the truth table.]
302
303 Description []
304
305 SideEffects []
306
307 SeeAlso []
308
309 ******************************************************************************/
Kit_TruthCofSupports(Vec_Int_t * vBddDir,Vec_Int_t * vBddInv,int nVars,Vec_Int_t * vMemory,unsigned * puSupps)310 void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps )
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 }
371
372 ////////////////////////////////////////////////////////////////////////
373 /// END OF FILE ///
374 ////////////////////////////////////////////////////////////////////////
375
376
377 ABC_NAMESPACE_IMPL_END
378
379