abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ivyDsd.c
Go to the documentation of this file.
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 
56 static inline int Ivy_DecToInt( Ivy_Dec_t m ) { union { Ivy_Dec_t x; int y; } v; v.x = m; return v.y; }
57 static inline Ivy_Dec_t Ivy_IntToDec( int m ) { union { Ivy_Dec_t x; int y; } v; v.y = m; return v.x; }
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 
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 
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 
91 static inline int Ivy_TruthCofactorIsOne( unsigned uTruth, int Var )
92 {
93  return (uTruth & s_Masks[Var][0]) == 0;
94 }
95 
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 
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)
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 
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 
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 ***********************************************************************/
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 ***********************************************************************/
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;
223  int nSupp, Count0, Count1, Count2, nVars, RetValue, fCompl, 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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 
Ivy_TruthDsdPrint
void Ivy_TruthDsdPrint(FILE *pFile, Vec_Int_t *vTree)
Definition: ivyDsd.c:568
Ivy_TruthDsd
int Ivy_TruthDsd(unsigned uTruth, Vec_Int_t *vTree)
FUNCTION DEFINITIONS ///.
Definition: ivyDsd.c:166
Ivy_ManConst1
static Ivy_Obj_t * Ivy_ManConst1(Ivy_Man_t *p)
Definition: ivy.h:199
IVY_AND
Definition: ivy.h:58
Ivy_Dec_t_::Fan0
unsigned Fan0
Definition: ivyDsd.c:48
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ivy_Dec_t_::Fan1
unsigned Fan1
Definition: ivyDsd.c:49
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Ivy_Dec_t_::nFans
unsigned nFans
Definition: ivyDsd.c:47
Ivy_Mux
Ivy_Obj_t * Ivy_Mux(Ivy_Man_t *p, Ivy_Obj_t *pC, Ivy_Obj_t *p1, Ivy_Obj_t *p0)
Definition: ivyOper.c:158
Ivy_Dec_t_
Definition: ivyDsd.c:43
Ivy_TruthDsdPrint_rec
void Ivy_TruthDsdPrint_rec(FILE *pFile, int iNode, Vec_Int_t *vTree)
Definition: ivyDsd.c:494
Ivy_DecGetVar
static unsigned Ivy_DecGetVar(Ivy_Dec_t *pNode, int iNum)
Definition: ivyDsd.c:130
Ivy_TruthDsdComputePrint
void Ivy_TruthDsdComputePrint(unsigned uTruth)
Definition: ivyDsd.c:678
Ivy_Dec_t_::Type
unsigned Type
Definition: ivyDsd.c:45
Ivy_TruthRecognizeMuxMaj
static int Ivy_TruthRecognizeMuxMaj(unsigned uTruth, int *pSupp, int nSupp, Vec_Int_t *vTree)
Definition: ivyDsd.c:319
Ivy_LeafId
static int Ivy_LeafId(int Leaf)
Definition: ivy.h:215
Ivy_TruthTestOne
void Ivy_TruthTestOne(unsigned uTruth)
Definition: ivyDsd.c:700
Ivy_Dec_t_::Fan3
unsigned Fan3
Definition: ivyDsd.c:51
Ivy_IntToDec
static Ivy_Dec_t Ivy_IntToDec(int m)
Definition: ivyDsd.c:57
Ivy_TruthCofactorIsOne
static int Ivy_TruthCofactorIsOne(unsigned uTruth, int Var)
Definition: ivyDsd.c:91
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Ivy_TruthCofactor2
static unsigned Ivy_TruthCofactor2(unsigned uTruth, int Var0, int Var1)
Definition: ivyDsd.c:105
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Ivy_ManObj
static Ivy_Obj_t * Ivy_ManObj(Ivy_Man_t *p, int i)
Definition: ivy.h:203
Ivy_TruthDsdCompute_rec
unsigned Ivy_TruthDsdCompute_rec(int iNode, Vec_Int_t *vTree)
Definition: ivyDsd.c:404
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Ivy_ManDsdConstruct_rec
Ivy_Obj_t * Ivy_ManDsdConstruct_rec(Ivy_Man_t *p, Vec_Int_t *vFront, int iNode, Vec_Int_t *vTree)
Definition: ivyDsd.c:586
Ivy_Multi
Ivy_Obj_t * Ivy_Multi(Ivy_Man_t *p, Ivy_Obj_t **pArgs, int nArgs, Ivy_Type_t Type)
Definition: ivyOper.c:246
Vec_IntPop
static int Vec_IntPop(Vec_Int_t *p)
Definition: extraZddTrunc.c:110
Ivy_DecToInt
static int Ivy_DecToInt(Ivy_Dec_t m)
Definition: ivyDsd.c:56
Ivy_Obj_t_
Definition: ivy.h:73
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Counter
static int Counter
Definition: extraBddMisc.c:1877
Ivy_TruthCofactorIsConst
static int Ivy_TruthCofactorIsConst(unsigned uTruth, int Var, int Cof, int Const)
Definition: ivyDsd.c:83
Extra_ReadHexadecimal
int Extra_ReadHexadecimal(unsigned Sign[], char *pString, int nVars)
Definition: extraUtilFile.c:540
Ivy_Dec_t_::Fan2
unsigned Fan2
Definition: ivyDsd.c:50
Ivy_DecSetVar
static void Ivy_DecSetVar(Ivy_Dec_t *pNode, int iNum, unsigned Var)
Definition: ivyDsd.c:116
Ivy_TruthDepends
static int Ivy_TruthDepends(unsigned uTruth, int Var)
Definition: ivyDsd.c:111
Ivy_TruthDsdCompute
unsigned Ivy_TruthDsdCompute(Vec_Int_t *vTree)
Definition: ivyDsd.c:478
Ivy_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_ Ivy_Man_t
INCLUDES ///.
Definition: ivy.h:46
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Ivy_DecType_t
Ivy_DecType_t
DECLARATIONS ///.
Definition: ivyDsd.c:31
IVY_EXOR
Definition: ivy.h:59
Ivy_TruthDecompose_rec
static int Ivy_TruthDecompose_rec(unsigned uTruth, Vec_Int_t *vTree)
Definition: ivyDsd.c:219
Ivy_TruthCofactor
static unsigned Ivy_TruthCofactor(unsigned uTruth, int Var)
Definition: ivyDsd.c:96
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Ivy_DecClear
static void Ivy_DecClear(Ivy_Dec_t *pNode)
Definition: ivyDsd.c:58
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition: extraUtilFile.c:497
Ivy_NotCond
static Ivy_Obj_t * Ivy_NotCond(Ivy_Obj_t *p, int c)
Definition: ivy.h:195
Minisat::Var
int Var
Definition: SolverTypes.h:42
Ivy_TruthWordCountOnes
static int Ivy_TruthWordCountOnes(unsigned uWord)
Definition: ivyDsd.c:74
assert
#define assert(ex)
Definition: util_old.h:213
Ivy_Maj
Ivy_Obj_t * Ivy_Maj(Ivy_Man_t *p, Ivy_Obj_t *pA, Ivy_Obj_t *pB, Ivy_Obj_t *pC)
Definition: ivyOper.c:209
Ivy_ManDsdConstruct
Ivy_Obj_t * Ivy_ManDsdConstruct(Ivy_Man_t *p, Vec_Int_t *vFront, Vec_Int_t *vTree)
Definition: ivyDsd.c:655
s_Masks
static unsigned s_Masks[6][2]
Definition: ivyDsd.c:65
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Ivy_Dec_t_::Fan5
unsigned Fan5
Definition: ivyDsd.c:53
Ivy_Dec_t_::Fan4
unsigned Fan4
Definition: ivyDsd.c:52
Ivy_Dec_t_::fCompl
unsigned fCompl
Definition: ivyDsd.c:46