1 /**CFile****************************************************************
2
3 FileName [ivyDsd.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [And-Inverter Graph package.]
8
9 Synopsis [Disjoint-support decomposition.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - May 11, 2006.]
16
17 Revision [$Id: ivyDsd.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "ivy.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 // decomposition types
31 typedef enum {
32 IVY_DEC_PI, // 0: var
33 IVY_DEC_CONST1, // 1: CONST1
34 IVY_DEC_BUF, // 2: BUF
35 IVY_DEC_AND, // 3: AND
36 IVY_DEC_EXOR, // 4: EXOR
37 IVY_DEC_MUX, // 5: MUX
38 IVY_DEC_MAJ, // 6: MAJ
39 IVY_DEC_PRIME // 7: undecomposable
40 } Ivy_DecType_t;
41
42 typedef struct Ivy_Dec_t_ Ivy_Dec_t;
43 struct Ivy_Dec_t_
44 {
45 unsigned Type : 4; // the node type (PI, CONST1, AND, EXOR, MUX, PRIME)
46 unsigned fCompl : 1; // shows if node is complemented (root node only)
47 unsigned nFans : 3; // the number of fanins
48 unsigned Fan0 : 4; // fanin 0
49 unsigned Fan1 : 4; // fanin 1
50 unsigned Fan2 : 4; // fanin 2
51 unsigned Fan3 : 4; // fanin 3
52 unsigned Fan4 : 4; // fanin 4
53 unsigned Fan5 : 4; // fanin 5
54 };
55
Ivy_DecToInt(Ivy_Dec_t m)56 static inline int Ivy_DecToInt( Ivy_Dec_t m ) { union { Ivy_Dec_t x; int y; } v; v.x = m; return v.y; }
Ivy_IntToDec(int m)57 static inline Ivy_Dec_t Ivy_IntToDec( int m ) { union { Ivy_Dec_t x; int y; } v; v.y = m; return v.x; }
Ivy_DecClear(Ivy_Dec_t * pNode)58 static inline void Ivy_DecClear( Ivy_Dec_t * pNode ) { *pNode = Ivy_IntToDec(0); }
59
60 //static inline int Ivy_DecToInt( Ivy_Dec_t Node ) { return *((int *)&Node); }
61 //static inline Ivy_Dec_t Ivy_IntToDec( int Node ) { return *((Ivy_Dec_t *)&Node); }
62 //static inline void Ivy_DecClear( Ivy_Dec_t * pNode ) { *((int *)pNode) = 0; }
63
64
65 static unsigned s_Masks[6][2] = {
66 { 0x55555555, 0xAAAAAAAA },
67 { 0x33333333, 0xCCCCCCCC },
68 { 0x0F0F0F0F, 0xF0F0F0F0 },
69 { 0x00FF00FF, 0xFF00FF00 },
70 { 0x0000FFFF, 0xFFFF0000 },
71 { 0x00000000, 0xFFFFFFFF }
72 };
73
Ivy_TruthWordCountOnes(unsigned uWord)74 static inline int Ivy_TruthWordCountOnes( unsigned uWord )
75 {
76 uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
77 uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
78 uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
79 uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
80 return (uWord & 0x0000FFFF) + (uWord>>16);
81 }
82
Ivy_TruthCofactorIsConst(unsigned uTruth,int Var,int Cof,int Const)83 static inline int Ivy_TruthCofactorIsConst( unsigned uTruth, int Var, int Cof, int Const )
84 {
85 if ( Const == 0 )
86 return (uTruth & s_Masks[Var][Cof]) == 0;
87 else
88 return (uTruth & s_Masks[Var][Cof]) == s_Masks[Var][Cof];
89 }
90
Ivy_TruthCofactorIsOne(unsigned uTruth,int Var)91 static inline int Ivy_TruthCofactorIsOne( unsigned uTruth, int Var )
92 {
93 return (uTruth & s_Masks[Var][0]) == 0;
94 }
95
Ivy_TruthCofactor(unsigned uTruth,int Var)96 static inline unsigned Ivy_TruthCofactor( unsigned uTruth, int Var )
97 {
98 unsigned uCofactor = uTruth & s_Masks[Var >> 1][(Var & 1) == 0];
99 int Shift = (1 << (Var >> 1));
100 if ( Var & 1 )
101 return uCofactor | (uCofactor << Shift);
102 return uCofactor | (uCofactor >> Shift);
103 }
104
Ivy_TruthCofactor2(unsigned uTruth,int Var0,int Var1)105 static inline unsigned Ivy_TruthCofactor2( unsigned uTruth, int Var0, int Var1 )
106 {
107 return Ivy_TruthCofactor( Ivy_TruthCofactor(uTruth, Var0), Var1 );
108 }
109
110 // returns 1 if the truth table depends on this var (var is regular interger var)
Ivy_TruthDepends(unsigned uTruth,int Var)111 static inline int Ivy_TruthDepends( unsigned uTruth, int Var )
112 {
113 return Ivy_TruthCofactor(uTruth, Var << 1) != Ivy_TruthCofactor(uTruth, (Var << 1) | 1);
114 }
115
Ivy_DecSetVar(Ivy_Dec_t * pNode,int iNum,unsigned Var)116 static inline void Ivy_DecSetVar( Ivy_Dec_t * pNode, int iNum, unsigned Var )
117 {
118 assert( iNum >= 0 && iNum <= 5 );
119 switch( iNum )
120 {
121 case 0: pNode->Fan0 = Var; break;
122 case 1: pNode->Fan1 = Var; break;
123 case 2: pNode->Fan2 = Var; break;
124 case 3: pNode->Fan3 = Var; break;
125 case 4: pNode->Fan4 = Var; break;
126 case 5: pNode->Fan5 = Var; break;
127 }
128 }
129
Ivy_DecGetVar(Ivy_Dec_t * pNode,int iNum)130 static inline unsigned Ivy_DecGetVar( Ivy_Dec_t * pNode, int iNum )
131 {
132 assert( iNum >= 0 && iNum <= 5 );
133 switch( iNum )
134 {
135 case 0: return pNode->Fan0;
136 case 1: return pNode->Fan1;
137 case 2: return pNode->Fan2;
138 case 3: return pNode->Fan3;
139 case 4: return pNode->Fan4;
140 case 5: return pNode->Fan5;
141 }
142 return ~0;
143 }
144
145 static int Ivy_TruthDecompose_rec( unsigned uTruth, Vec_Int_t * vTree );
146 static int Ivy_TruthRecognizeMuxMaj( unsigned uTruth, int * pSupp, int nSupp, Vec_Int_t * vTree );
147
148 //int nTruthDsd;
149
150 ////////////////////////////////////////////////////////////////////////
151 /// FUNCTION DEFINITIONS ///
152 ////////////////////////////////////////////////////////////////////////
153
154 /**Function*************************************************************
155
156 Synopsis [Computes DSD of truth table of 5 variables or less.]
157
158 Description [Returns 1 if the function is a constant or is fully
159 DSD decomposable using AND/EXOR/MUX gates.]
160
161 SideEffects []
162
163 SeeAlso []
164
165 ***********************************************************************/
Ivy_TruthDsd(unsigned uTruth,Vec_Int_t * vTree)166 int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree )
167 {
168 Ivy_Dec_t Node;
169 int i, RetValue;
170 // set the PI variables
171 Vec_IntClear( vTree );
172 for ( i = 0; i < 5; i++ )
173 Vec_IntPush( vTree, 0 );
174 // check if it is a constant
175 if ( uTruth == 0 || ~uTruth == 0 )
176 {
177 Ivy_DecClear( &Node );
178 Node.Type = IVY_DEC_CONST1;
179 Node.fCompl = (uTruth == 0);
180 Vec_IntPush( vTree, Ivy_DecToInt(Node) );
181 return 1;
182 }
183 // perform the decomposition
184 RetValue = Ivy_TruthDecompose_rec( uTruth, vTree );
185 if ( RetValue == -1 )
186 return 0;
187 // get the topmost node
188 if ( (RetValue >> 1) < 5 )
189 { // add buffer
190 Ivy_DecClear( &Node );
191 Node.Type = IVY_DEC_BUF;
192 Node.fCompl = (RetValue & 1);
193 Node.Fan0 = ((RetValue >> 1) << 1);
194 Vec_IntPush( vTree, Ivy_DecToInt(Node) );
195 }
196 else if ( RetValue & 1 )
197 { // check if the topmost node has to be complemented
198 Node = Ivy_IntToDec( Vec_IntPop(vTree) );
199 assert( Node.fCompl == 0 );
200 Node.fCompl = (RetValue & 1);
201 Vec_IntPush( vTree, Ivy_DecToInt(Node) );
202 }
203 if ( uTruth != Ivy_TruthDsdCompute(vTree) )
204 printf( "Verification failed.\n" );
205 return 1;
206 }
207
208 /**Function*************************************************************
209
210 Synopsis [Computes DSD of truth table.]
211
212 Description [Returns the number of topmost decomposition node.]
213
214 SideEffects []
215
216 SeeAlso []
217
218 ***********************************************************************/
Ivy_TruthDecompose_rec(unsigned uTruth,Vec_Int_t * vTree)219 int Ivy_TruthDecompose_rec( unsigned uTruth, Vec_Int_t * vTree )
220 {
221 Ivy_Dec_t Node;
222 int Supp[5], Vars0[5], Vars1[5], Vars2[5], * pVars = NULL;
223 int nSupp, Count0, Count1, Count2, nVars = 0, RetValue, fCompl = 0, i;
224 unsigned uTruthCof, uCof0, uCof1;
225
226 // get constant confactors
227 Count0 = Count1 = Count2 = nSupp = 0;
228 for ( i = 0; i < 5; i++ )
229 {
230 if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 0) )
231 Vars0[Count0++] = (i << 1) | 0;
232 else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 0) )
233 Vars0[Count0++] = (i << 1) | 1;
234 else if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 1) )
235 Vars1[Count1++] = (i << 1) | 0;
236 else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 1) )
237 Vars1[Count1++] = (i << 1) | 1;
238 else
239 {
240 uCof0 = Ivy_TruthCofactor( uTruth, (i << 1) | 1 );
241 uCof1 = Ivy_TruthCofactor( uTruth, (i << 1) | 0 );
242 if ( uCof0 == ~uCof1 )
243 Vars2[Count2++] = (i << 1) | 0;
244 else if ( uCof0 != uCof1 )
245 Supp[nSupp++] = i;
246 }
247 }
248 assert( Count0 == 0 || Count1 == 0 );
249 assert( Count0 == 0 || Count2 == 0 );
250 assert( Count1 == 0 || Count2 == 0 );
251
252 // consider the case of a single variable
253 if ( Count0 == 1 && nSupp == 0 )
254 return Vars0[0];
255
256 // consider more complex decompositions
257 if ( Count0 == 0 && Count1 == 0 && Count2 == 0 )
258 return Ivy_TruthRecognizeMuxMaj( uTruth, Supp, nSupp, vTree );
259
260 // extract the nodes
261 Ivy_DecClear( &Node );
262 if ( Count0 > 0 )
263 nVars = Count0, pVars = Vars0, Node.Type = IVY_DEC_AND, fCompl = 0;
264 else if ( Count1 > 0 )
265 nVars = Count1, pVars = Vars1, Node.Type = IVY_DEC_AND, fCompl = 1, uTruth = ~uTruth;
266 else if ( Count2 > 0 )
267 nVars = Count2, pVars = Vars2, Node.Type = IVY_DEC_EXOR, fCompl = 0;
268 else
269 assert( 0 );
270 Node.nFans = nVars+(nSupp>0);
271
272 // compute cofactor
273 uTruthCof = uTruth;
274 for ( i = 0; i < nVars; i++ )
275 {
276 uTruthCof = Ivy_TruthCofactor( uTruthCof, pVars[i] );
277 Ivy_DecSetVar( &Node, i, pVars[i] );
278 }
279
280 if ( Node.Type == IVY_DEC_EXOR )
281 fCompl ^= ((Node.nFans & 1) == 0);
282
283 if ( nSupp > 0 )
284 {
285 assert( uTruthCof != 0 && ~uTruthCof != 0 );
286 // call recursively
287 RetValue = Ivy_TruthDecompose_rec( uTruthCof, vTree );
288 // quit if non-decomposable
289 if ( RetValue == -1 )
290 return -1;
291 // remove the complement from the child if the node is EXOR
292 if ( Node.Type == IVY_DEC_EXOR && (RetValue & 1) )
293 {
294 fCompl ^= 1;
295 RetValue ^= 1;
296 }
297 // set the new decomposition
298 Ivy_DecSetVar( &Node, nVars, RetValue );
299 }
300 else if ( Node.Type == IVY_DEC_EXOR )
301 fCompl ^= (uTruthCof == 0);
302
303 Vec_IntPush( vTree, Ivy_DecToInt(Node) );
304 return ((Vec_IntSize(vTree)-1) << 1) | fCompl;
305 }
306
307 /**Function*************************************************************
308
309 Synopsis [Returns a non-negative number if the truth table is a MUX.]
310
311 Description [If the truth table is a MUX, returns the variable as follows:
312 first, control variable; second, positive cofactor; third, negative cofactor.]
313
314 SideEffects []
315
316 SeeAlso []
317
318 ***********************************************************************/
Ivy_TruthRecognizeMuxMaj(unsigned uTruth,int * pSupp,int nSupp,Vec_Int_t * vTree)319 int Ivy_TruthRecognizeMuxMaj( unsigned uTruth, int * pSupp, int nSupp, Vec_Int_t * vTree )
320 {
321 Ivy_Dec_t Node;
322 int i, k, RetValue0, RetValue1;
323 unsigned uCof0, uCof1, Num;
324 char Count[3];
325 assert( nSupp >= 3 );
326 // start the node
327 Ivy_DecClear( &Node );
328 Node.Type = IVY_DEC_MUX;
329 Node.nFans = 3;
330 // try each of the variables
331 for ( i = 0; i < nSupp; i++ )
332 {
333 // get the cofactors with respect to these variables
334 uCof0 = Ivy_TruthCofactor( uTruth, (pSupp[i] << 1) | 1 );
335 uCof1 = Ivy_TruthCofactor( uTruth, pSupp[i] << 1 );
336 // go through all other variables and make sure
337 // each of them belongs to the support of one cofactor
338 for ( k = 0; k < nSupp; k++ )
339 {
340 if ( k == i )
341 continue;
342 if ( Ivy_TruthDepends(uCof0, pSupp[k]) && Ivy_TruthDepends(uCof1, pSupp[k]) )
343 break;
344 }
345 if ( k < nSupp )
346 continue;
347 // MUX decomposition exists
348 RetValue0 = Ivy_TruthDecompose_rec( uCof0, vTree );
349 if ( RetValue0 == -1 )
350 break;
351 RetValue1 = Ivy_TruthDecompose_rec( uCof1, vTree );
352 if ( RetValue1 == -1 )
353 break;
354 // both of them exist; create the node
355 Ivy_DecSetVar( &Node, 0, pSupp[i] << 1 );
356 Ivy_DecSetVar( &Node, 1, RetValue1 );
357 Ivy_DecSetVar( &Node, 2, RetValue0 );
358 Vec_IntPush( vTree, Ivy_DecToInt(Node) );
359 return ((Vec_IntSize(vTree)-1) << 1) | 0;
360 }
361 // check majority gate
362 if ( nSupp > 3 )
363 return -1;
364 if ( Ivy_TruthWordCountOnes(uTruth) != 16 )
365 return -1;
366 // this is a majority gate; determine polarity
367 Node.Type = IVY_DEC_MAJ;
368 Count[0] = Count[1] = Count[2] = 0;
369 for ( i = 0; i < 8; i++ )
370 {
371 Num = 0;
372 for ( k = 0; k < 3; k++ )
373 if ( i & (1 << k) )
374 Num |= (1 << pSupp[k]);
375 assert( Num < 32 );
376 if ( (uTruth & (1 << Num)) == 0 )
377 continue;
378 for ( k = 0; k < 3; k++ )
379 if ( i & (1 << k) )
380 Count[k]++;
381 }
382 assert( Count[0] == 1 || Count[0] == 3 );
383 assert( Count[1] == 1 || Count[1] == 3 );
384 assert( Count[2] == 1 || Count[2] == 3 );
385 Ivy_DecSetVar( &Node, 0, (pSupp[0] << 1)|(Count[0] == 1) );
386 Ivy_DecSetVar( &Node, 1, (pSupp[1] << 1)|(Count[1] == 1) );
387 Ivy_DecSetVar( &Node, 2, (pSupp[2] << 1)|(Count[2] == 1) );
388 Vec_IntPush( vTree, Ivy_DecToInt(Node) );
389 return ((Vec_IntSize(vTree)-1) << 1) | 0;
390 }
391
392
393 /**Function*************************************************************
394
395 Synopsis [Computes truth table of decomposition tree for verification.]
396
397 Description []
398
399 SideEffects []
400
401 SeeAlso []
402
403 ***********************************************************************/
Ivy_TruthDsdCompute_rec(int iNode,Vec_Int_t * vTree)404 unsigned Ivy_TruthDsdCompute_rec( int iNode, Vec_Int_t * vTree )
405 {
406 unsigned uTruthChild, uTruthTotal;
407 int Var, i;
408 // get the node
409 Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
410 // compute the node function
411 if ( Node.Type == IVY_DEC_CONST1 )
412 return s_Masks[5][ !Node.fCompl ];
413 if ( Node.Type == IVY_DEC_PI )
414 return s_Masks[iNode][ !Node.fCompl ];
415 if ( Node.Type == IVY_DEC_BUF )
416 {
417 uTruthTotal = Ivy_TruthDsdCompute_rec( Node.Fan0 >> 1, vTree );
418 return Node.fCompl? ~uTruthTotal : uTruthTotal;
419 }
420 if ( Node.Type == IVY_DEC_AND )
421 {
422 uTruthTotal = s_Masks[5][1];
423 for ( i = 0; i < (int)Node.nFans; i++ )
424 {
425 Var = Ivy_DecGetVar( &Node, i );
426 uTruthChild = Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
427 uTruthTotal = (Var & 1)? uTruthTotal & ~uTruthChild : uTruthTotal & uTruthChild;
428 }
429 return Node.fCompl? ~uTruthTotal : uTruthTotal;
430 }
431 if ( Node.Type == IVY_DEC_EXOR )
432 {
433 uTruthTotal = 0;
434 for ( i = 0; i < (int)Node.nFans; i++ )
435 {
436 Var = Ivy_DecGetVar( &Node, i );
437 uTruthTotal ^= Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
438 assert( (Var & 1) == 0 );
439 }
440 return Node.fCompl? ~uTruthTotal : uTruthTotal;
441 }
442 assert( Node.fCompl == 0 );
443 if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
444 {
445 unsigned uTruthChildC, uTruthChild1, uTruthChild0;
446 int VarC, Var1, Var0;
447 VarC = Ivy_DecGetVar( &Node, 0 );
448 Var1 = Ivy_DecGetVar( &Node, 1 );
449 Var0 = Ivy_DecGetVar( &Node, 2 );
450 uTruthChildC = Ivy_TruthDsdCompute_rec( VarC >> 1, vTree );
451 uTruthChild1 = Ivy_TruthDsdCompute_rec( Var1 >> 1, vTree );
452 uTruthChild0 = Ivy_TruthDsdCompute_rec( Var0 >> 1, vTree );
453 assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
454 uTruthChildC = (VarC & 1)? ~uTruthChildC : uTruthChildC;
455 uTruthChild1 = (Var1 & 1)? ~uTruthChild1 : uTruthChild1;
456 uTruthChild0 = (Var0 & 1)? ~uTruthChild0 : uTruthChild0;
457 if ( Node.Type == IVY_DEC_MUX )
458 return (uTruthChildC & uTruthChild1) | (~uTruthChildC & uTruthChild0);
459 else
460 return (uTruthChildC & uTruthChild1) | (uTruthChildC & uTruthChild0) | (uTruthChild1 & uTruthChild0);
461 }
462 assert( 0 );
463 return 0;
464 }
465
466
467 /**Function*************************************************************
468
469 Synopsis [Computes truth table of decomposition tree for verification.]
470
471 Description []
472
473 SideEffects []
474
475 SeeAlso []
476
477 ***********************************************************************/
Ivy_TruthDsdCompute(Vec_Int_t * vTree)478 unsigned Ivy_TruthDsdCompute( Vec_Int_t * vTree )
479 {
480 return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree );
481 }
482
483 /**Function*************************************************************
484
485 Synopsis [Prints the decomposition tree.]
486
487 Description []
488
489 SideEffects []
490
491 SeeAlso []
492
493 ***********************************************************************/
Ivy_TruthDsdPrint_rec(FILE * pFile,int iNode,Vec_Int_t * vTree)494 void Ivy_TruthDsdPrint_rec( FILE * pFile, int iNode, Vec_Int_t * vTree )
495 {
496 int Var, i;
497 // get the node
498 Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
499 // compute the node function
500 if ( Node.Type == IVY_DEC_CONST1 )
501 fprintf( pFile, "Const1%s", (Node.fCompl? "\'" : "") );
502 else if ( Node.Type == IVY_DEC_PI )
503 fprintf( pFile, "%c%s", 'a' + iNode, (Node.fCompl? "\'" : "") );
504 else if ( Node.Type == IVY_DEC_BUF )
505 {
506 Ivy_TruthDsdPrint_rec( pFile, Node.Fan0 >> 1, vTree );
507 fprintf( pFile, "%s", (Node.fCompl? "\'" : "") );
508 }
509 else if ( Node.Type == IVY_DEC_AND )
510 {
511 fprintf( pFile, "AND(" );
512 for ( i = 0; i < (int)Node.nFans; i++ )
513 {
514 Var = Ivy_DecGetVar( &Node, i );
515 Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
516 fprintf( pFile, "%s", (Var & 1)? "\'" : "" );
517 if ( i != (int)Node.nFans-1 )
518 fprintf( pFile, "," );
519 }
520 fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
521 }
522 else if ( Node.Type == IVY_DEC_EXOR )
523 {
524 fprintf( pFile, "EXOR(" );
525 for ( i = 0; i < (int)Node.nFans; i++ )
526 {
527 Var = Ivy_DecGetVar( &Node, i );
528 Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
529 if ( i != (int)Node.nFans-1 )
530 fprintf( pFile, "," );
531 assert( (Var & 1) == 0 );
532 }
533 fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
534 }
535 else if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
536 {
537 int VarC, Var1, Var0;
538 assert( Node.fCompl == 0 );
539 VarC = Ivy_DecGetVar( &Node, 0 );
540 Var1 = Ivy_DecGetVar( &Node, 1 );
541 Var0 = Ivy_DecGetVar( &Node, 2 );
542 fprintf( pFile, "%s", (Node.Type == IVY_DEC_MUX)? "MUX(" : "MAJ(" );
543 Ivy_TruthDsdPrint_rec( pFile, VarC >> 1, vTree );
544 fprintf( pFile, "%s", (VarC & 1)? "\'" : "" );
545 fprintf( pFile, "," );
546 Ivy_TruthDsdPrint_rec( pFile, Var1 >> 1, vTree );
547 fprintf( pFile, "%s", (Var1 & 1)? "\'" : "" );
548 fprintf( pFile, "," );
549 Ivy_TruthDsdPrint_rec( pFile, Var0 >> 1, vTree );
550 fprintf( pFile, "%s", (Var0 & 1)? "\'" : "" );
551 fprintf( pFile, ")" );
552 }
553 else assert( 0 );
554 }
555
556
557 /**Function*************************************************************
558
559 Synopsis [Prints the decomposition tree.]
560
561 Description []
562
563 SideEffects []
564
565 SeeAlso []
566
567 ***********************************************************************/
Ivy_TruthDsdPrint(FILE * pFile,Vec_Int_t * vTree)568 void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree )
569 {
570 fprintf( pFile, "F = " );
571 Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree );
572 fprintf( pFile, "\n" );
573 }
574
575 /**Function*************************************************************
576
577 Synopsis [Implement DSD in the AIG.]
578
579 Description []
580
581 SideEffects []
582
583 SeeAlso []
584
585 ***********************************************************************/
Ivy_ManDsdConstruct_rec(Ivy_Man_t * p,Vec_Int_t * vFront,int iNode,Vec_Int_t * vTree)586 Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNode, Vec_Int_t * vTree )
587 {
588 Ivy_Obj_t * pResult, * pChild, * pNodes[16];
589 int Var, i;
590 // get the node
591 Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
592 // compute the node function
593 if ( Node.Type == IVY_DEC_CONST1 )
594 return Ivy_NotCond( Ivy_ManConst1(p), Node.fCompl );
595 if ( Node.Type == IVY_DEC_PI )
596 {
597 pResult = Ivy_ManObj( p, Vec_IntEntry(vFront, iNode) );
598 return Ivy_NotCond( pResult, Node.fCompl );
599 }
600 if ( Node.Type == IVY_DEC_BUF )
601 {
602 pResult = Ivy_ManDsdConstruct_rec( p, vFront, Node.Fan0 >> 1, vTree );
603 return Ivy_NotCond( pResult, Node.fCompl );
604 }
605 if ( Node.Type == IVY_DEC_AND || Node.Type == IVY_DEC_EXOR )
606 {
607 for ( i = 0; i < (int)Node.nFans; i++ )
608 {
609 Var = Ivy_DecGetVar( &Node, i );
610 assert( Node.Type == IVY_DEC_AND || (Var & 1) == 0 );
611 pChild = Ivy_ManDsdConstruct_rec( p, vFront, Var >> 1, vTree );
612 pChild = Ivy_NotCond( pChild, (Var & 1) );
613 pNodes[i] = pChild;
614 }
615
616 // Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
617
618 pResult = Ivy_Multi( p, pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
619 return Ivy_NotCond( pResult, Node.fCompl );
620 }
621 assert( Node.fCompl == 0 );
622 if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
623 {
624 int VarC, Var1, Var0;
625 VarC = Ivy_DecGetVar( &Node, 0 );
626 Var1 = Ivy_DecGetVar( &Node, 1 );
627 Var0 = Ivy_DecGetVar( &Node, 2 );
628 pNodes[0] = Ivy_ManDsdConstruct_rec( p, vFront, VarC >> 1, vTree );
629 pNodes[1] = Ivy_ManDsdConstruct_rec( p, vFront, Var1 >> 1, vTree );
630 pNodes[2] = Ivy_ManDsdConstruct_rec( p, vFront, Var0 >> 1, vTree );
631 assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
632 pNodes[0] = Ivy_NotCond( pNodes[0], (VarC & 1) );
633 pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) );
634 pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) );
635 if ( Node.Type == IVY_DEC_MUX )
636 return Ivy_Mux( p, pNodes[0], pNodes[1], pNodes[2] );
637 else
638 return Ivy_Maj( p, pNodes[0], pNodes[1], pNodes[2] );
639 }
640 assert( 0 );
641 return 0;
642 }
643
644 /**Function*************************************************************
645
646 Synopsis [Implement DSD in the AIG.]
647
648 Description []
649
650 SideEffects []
651
652 SeeAlso []
653
654 ***********************************************************************/
Ivy_ManDsdConstruct(Ivy_Man_t * p,Vec_Int_t * vFront,Vec_Int_t * vTree)655 Ivy_Obj_t * Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree )
656 {
657 int Entry, i;
658 // implement latches on the frontier (TEMPORARY!!!)
659 Vec_IntForEachEntry( vFront, Entry, i )
660 Vec_IntWriteEntry( vFront, i, Ivy_LeafId(Entry) );
661 // recursively construct the tree
662 return Ivy_ManDsdConstruct_rec( p, vFront, Vec_IntSize(vTree)-1, vTree );
663 }
664
665
666
667 /**Function*************************************************************
668
669 Synopsis []
670
671 Description []
672
673 SideEffects []
674
675 SeeAlso []
676
677 ***********************************************************************/
Ivy_TruthDsdComputePrint(unsigned uTruth)678 void Ivy_TruthDsdComputePrint( unsigned uTruth )
679 {
680 static Vec_Int_t * vTree = NULL;
681 if ( vTree == NULL )
682 vTree = Vec_IntAlloc( 12 );
683 if ( Ivy_TruthDsd( uTruth, vTree ) )
684 Ivy_TruthDsdPrint( stdout, vTree );
685 else
686 printf( "Undecomposable\n" );
687 }
688
689 /**Function*************************************************************
690
691 Synopsis []
692
693 Description []
694
695 SideEffects []
696
697 SeeAlso []
698
699 ***********************************************************************/
Ivy_TruthTestOne(unsigned uTruth)700 void Ivy_TruthTestOne( unsigned uTruth )
701 {
702 static int Counter = 0;
703 static Vec_Int_t * vTree = NULL;
704 // decompose
705 if ( vTree == NULL )
706 vTree = Vec_IntAlloc( 12 );
707
708 if ( !Ivy_TruthDsd( uTruth, vTree ) )
709 {
710 // printf( "Undecomposable\n" );
711 }
712 else
713 {
714 // nTruthDsd++;
715 printf( "%5d : ", Counter++ );
716 Extra_PrintBinary( stdout, &uTruth, 32 );
717 printf( " " );
718 Ivy_TruthDsdPrint( stdout, vTree );
719 if ( uTruth != Ivy_TruthDsdCompute(vTree) )
720 printf( "Verification failed.\n" );
721 }
722 // Vec_IntFree( vTree );
723 }
724
725 #if 0
726
727 /**Function*************************************************************
728
729 Synopsis []
730
731 Description []
732
733 SideEffects []
734
735 SeeAlso []
736
737 ***********************************************************************/
738 void Ivy_TruthTest()
739 {
740 FILE * pFile;
741 char Buffer[100];
742 unsigned uTruth;
743 int i;
744
745 pFile = fopen( "npn4.txt", "r" );
746 for ( i = 0; i < 222; i++ )
747 // pFile = fopen( "npn5.txt", "r" );
748 // for ( i = 0; i < 616126; i++ )
749 {
750 fscanf( pFile, "%s", Buffer );
751 Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
752 // Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
753 uTruth |= (uTruth << 16);
754 // uTruth = ~uTruth;
755 Ivy_TruthTestOne( uTruth );
756 }
757 fclose( pFile );
758 }
759
760 /**Function*************************************************************
761
762 Synopsis []
763
764 Description []
765
766 SideEffects []
767
768 SeeAlso []
769
770 ***********************************************************************/
771 void Ivy_TruthTest3()
772 {
773 FILE * pFile;
774 char Buffer[100];
775 unsigned uTruth;
776 int i;
777
778 pFile = fopen( "npn3.txt", "r" );
779 for ( i = 0; i < 14; i++ )
780 {
781 fscanf( pFile, "%s", Buffer );
782 Extra_ReadHexadecimal( &uTruth, Buffer+2, 3 );
783 uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24);
784 Ivy_TruthTestOne( uTruth );
785 }
786 fclose( pFile );
787 }
788
789 /**Function*************************************************************
790
791 Synopsis []
792
793 Description []
794
795 SideEffects []
796
797 SeeAlso []
798
799 ***********************************************************************/
800 void Ivy_TruthTest5()
801 {
802 FILE * pFile;
803 char Buffer[100];
804 unsigned uTruth;
805 int i;
806
807 // pFile = fopen( "npn4.txt", "r" );
808 // for ( i = 0; i < 222; i++ )
809 pFile = fopen( "npn5.txt", "r" );
810 for ( i = 0; i < 616126; i++ )
811 {
812 fscanf( pFile, "%s", Buffer );
813 // Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
814 Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
815 // uTruth |= (uTruth << 16);
816 // uTruth = ~uTruth;
817 Ivy_TruthTestOne( uTruth );
818 }
819 fclose( pFile );
820 }
821
822 #endif
823
824
825 ////////////////////////////////////////////////////////////////////////
826 /// END OF FILE ///
827 ////////////////////////////////////////////////////////////////////////
828
829
830 ABC_NAMESPACE_IMPL_END
831
832