abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
ivyDsd.c File Reference
#include "ivy.h"

Go to the source code of this file.

Data Structures

struct  Ivy_Dec_t_
 

Typedefs

typedef struct Ivy_Dec_t_ Ivy_Dec_t
 

Enumerations

enum  Ivy_DecType_t {
  IVY_DEC_PI, IVY_DEC_CONST1, IVY_DEC_BUF, IVY_DEC_AND,
  IVY_DEC_EXOR, IVY_DEC_MUX, IVY_DEC_MAJ, IVY_DEC_PRIME
}
 DECLARATIONS ///. More...
 

Functions

static int Ivy_DecToInt (Ivy_Dec_t m)
 
static Ivy_Dec_t Ivy_IntToDec (int m)
 
static void Ivy_DecClear (Ivy_Dec_t *pNode)
 
static int Ivy_TruthWordCountOnes (unsigned uWord)
 
static int Ivy_TruthCofactorIsConst (unsigned uTruth, int Var, int Cof, int Const)
 
static int Ivy_TruthCofactorIsOne (unsigned uTruth, int Var)
 
static unsigned Ivy_TruthCofactor (unsigned uTruth, int Var)
 
static unsigned Ivy_TruthCofactor2 (unsigned uTruth, int Var0, int Var1)
 
static int Ivy_TruthDepends (unsigned uTruth, int Var)
 
static void Ivy_DecSetVar (Ivy_Dec_t *pNode, int iNum, unsigned Var)
 
static unsigned Ivy_DecGetVar (Ivy_Dec_t *pNode, int iNum)
 
static int Ivy_TruthDecompose_rec (unsigned uTruth, Vec_Int_t *vTree)
 
static int Ivy_TruthRecognizeMuxMaj (unsigned uTruth, int *pSupp, int nSupp, Vec_Int_t *vTree)
 
int Ivy_TruthDsd (unsigned uTruth, Vec_Int_t *vTree)
 FUNCTION DEFINITIONS ///. More...
 
unsigned Ivy_TruthDsdCompute_rec (int iNode, Vec_Int_t *vTree)
 
unsigned Ivy_TruthDsdCompute (Vec_Int_t *vTree)
 
void Ivy_TruthDsdPrint_rec (FILE *pFile, int iNode, Vec_Int_t *vTree)
 
void Ivy_TruthDsdPrint (FILE *pFile, Vec_Int_t *vTree)
 
Ivy_Obj_tIvy_ManDsdConstruct_rec (Ivy_Man_t *p, Vec_Int_t *vFront, int iNode, Vec_Int_t *vTree)
 
Ivy_Obj_tIvy_ManDsdConstruct (Ivy_Man_t *p, Vec_Int_t *vFront, Vec_Int_t *vTree)
 
void Ivy_TruthDsdComputePrint (unsigned uTruth)
 
void Ivy_TruthTestOne (unsigned uTruth)
 

Variables

static unsigned s_Masks [6][2]
 

Typedef Documentation

typedef struct Ivy_Dec_t_ Ivy_Dec_t

Definition at line 42 of file ivyDsd.c.

Enumeration Type Documentation

DECLARATIONS ///.

CFile****************************************************************

FileName [ivyDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Disjoint-support decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id:
ivyDsd.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]

Enumerator
IVY_DEC_PI 
IVY_DEC_CONST1 
IVY_DEC_BUF 
IVY_DEC_AND 
IVY_DEC_EXOR 
IVY_DEC_MUX 
IVY_DEC_MAJ 
IVY_DEC_PRIME 

Definition at line 31 of file ivyDsd.c.

31  {
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
Ivy_DecType_t
DECLARATIONS ///.
Definition: ivyDsd.c:31

Function Documentation

static void Ivy_DecClear ( Ivy_Dec_t pNode)
inlinestatic

Definition at line 58 of file ivyDsd.c.

58 { *pNode = Ivy_IntToDec(0); }
static Ivy_Dec_t Ivy_IntToDec(int m)
Definition: ivyDsd.c:57
static unsigned Ivy_DecGetVar ( Ivy_Dec_t pNode,
int  iNum 
)
inlinestatic

Definition at line 130 of file ivyDsd.c.

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 }
unsigned Fan0
Definition: ivyDsd.c:48
unsigned Fan1
Definition: ivyDsd.c:49
unsigned Fan3
Definition: ivyDsd.c:51
unsigned Fan2
Definition: ivyDsd.c:50
#define assert(ex)
Definition: util_old.h:213
unsigned Fan5
Definition: ivyDsd.c:53
unsigned Fan4
Definition: ivyDsd.c:52
static void Ivy_DecSetVar ( Ivy_Dec_t pNode,
int  iNum,
unsigned  Var 
)
inlinestatic

Definition at line 116 of file ivyDsd.c.

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 }
unsigned Fan0
Definition: ivyDsd.c:48
unsigned Fan1
Definition: ivyDsd.c:49
unsigned Fan3
Definition: ivyDsd.c:51
unsigned Fan2
Definition: ivyDsd.c:50
int Var
Definition: SolverTypes.h:42
#define assert(ex)
Definition: util_old.h:213
unsigned Fan5
Definition: ivyDsd.c:53
unsigned Fan4
Definition: ivyDsd.c:52
static int Ivy_DecToInt ( Ivy_Dec_t  m)
inlinestatic

Definition at line 56 of file ivyDsd.c.

56 { union { Ivy_Dec_t x; int y; } v; v.x = m; return v.y; }
static Ivy_Dec_t Ivy_IntToDec ( int  m)
inlinestatic

Definition at line 57 of file ivyDsd.c.

57 { union { Ivy_Dec_t x; int y; } v; v.y = m; return v.x; }
Ivy_Obj_t* Ivy_ManDsdConstruct ( Ivy_Man_t p,
Vec_Int_t vFront,
Vec_Int_t vTree 
)

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

Synopsis [Implement DSD in the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 655 of file ivyDsd.c.

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 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Ivy_LeafId(int Leaf)
Definition: ivy.h:215
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Ivy_Obj_t * Ivy_ManDsdConstruct_rec(Ivy_Man_t *p, Vec_Int_t *vFront, int iNode, Vec_Int_t *vTree)
Definition: ivyDsd.c:586
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Ivy_Obj_t* Ivy_ManDsdConstruct_rec ( Ivy_Man_t p,
Vec_Int_t vFront,
int  iNode,
Vec_Int_t vTree 
)

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

Synopsis [Implement DSD in the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 586 of file ivyDsd.c.

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 }
static Ivy_Obj_t * Ivy_ManConst1(Ivy_Man_t *p)
Definition: ivy.h:199
Definition: ivy.h:58
unsigned Fan0
Definition: ivyDsd.c:48
static Llb_Mgr_t * p
Definition: llb3Image.c:950
unsigned nFans
Definition: ivyDsd.c:47
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
static unsigned Ivy_DecGetVar(Ivy_Dec_t *pNode, int iNum)
Definition: ivyDsd.c:130
unsigned Type
Definition: ivyDsd.c:45
static Ivy_Dec_t Ivy_IntToDec(int m)
Definition: ivyDsd.c:57
static Ivy_Obj_t * Ivy_ManObj(Ivy_Man_t *p, int i)
Definition: ivy.h:203
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
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_Obj_t * Ivy_Multi(Ivy_Man_t *p, Ivy_Obj_t **pArgs, int nArgs, Ivy_Type_t Type)
Definition: ivyOper.c:246
Definition: ivy.h:73
Definition: ivy.h:59
static Ivy_Obj_t * Ivy_NotCond(Ivy_Obj_t *p, int c)
Definition: ivy.h:195
int Var
Definition: SolverTypes.h:42
#define assert(ex)
Definition: util_old.h:213
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
unsigned fCompl
Definition: ivyDsd.c:46
static unsigned Ivy_TruthCofactor ( unsigned  uTruth,
int  Var 
)
inlinestatic

Definition at line 96 of file ivyDsd.c.

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 }
int Var
Definition: SolverTypes.h:42
static unsigned s_Masks[6][2]
Definition: ivyDsd.c:65
static unsigned Ivy_TruthCofactor2 ( unsigned  uTruth,
int  Var0,
int  Var1 
)
inlinestatic

Definition at line 105 of file ivyDsd.c.

106 {
107  return Ivy_TruthCofactor( Ivy_TruthCofactor(uTruth, Var0), Var1 );
108 }
static unsigned Ivy_TruthCofactor(unsigned uTruth, int Var)
Definition: ivyDsd.c:96
static int Ivy_TruthCofactorIsConst ( unsigned  uTruth,
int  Var,
int  Cof,
int  Const 
)
inlinestatic

Definition at line 83 of file ivyDsd.c.

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 }
int Var
Definition: SolverTypes.h:42
static unsigned s_Masks[6][2]
Definition: ivyDsd.c:65
static int Ivy_TruthCofactorIsOne ( unsigned  uTruth,
int  Var 
)
inlinestatic

Definition at line 91 of file ivyDsd.c.

92 {
93  return (uTruth & s_Masks[Var][0]) == 0;
94 }
int Var
Definition: SolverTypes.h:42
static unsigned s_Masks[6][2]
Definition: ivyDsd.c:65
int Ivy_TruthDecompose_rec ( unsigned  uTruth,
Vec_Int_t vTree 
)
static

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

Synopsis [Computes DSD of truth table.]

Description [Returns the number of topmost decomposition node.]

SideEffects []

SeeAlso []

Definition at line 219 of file ivyDsd.c.

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 }
unsigned nFans
Definition: ivyDsd.c:47
unsigned Type
Definition: ivyDsd.c:45
static int Ivy_TruthRecognizeMuxMaj(unsigned uTruth, int *pSupp, int nSupp, Vec_Int_t *vTree)
Definition: ivyDsd.c:319
static int Ivy_DecToInt(Ivy_Dec_t m)
Definition: ivyDsd.c:56
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Ivy_TruthCofactorIsConst(unsigned uTruth, int Var, int Cof, int Const)
Definition: ivyDsd.c:83
static void Ivy_DecSetVar(Ivy_Dec_t *pNode, int iNum, unsigned Var)
Definition: ivyDsd.c:116
static int Ivy_TruthDecompose_rec(unsigned uTruth, Vec_Int_t *vTree)
Definition: ivyDsd.c:219
static unsigned Ivy_TruthCofactor(unsigned uTruth, int Var)
Definition: ivyDsd.c:96
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Ivy_DecClear(Ivy_Dec_t *pNode)
Definition: ivyDsd.c:58
#define assert(ex)
Definition: util_old.h:213
static int Ivy_TruthDepends ( unsigned  uTruth,
int  Var 
)
inlinestatic

Definition at line 111 of file ivyDsd.c.

112 {
113  return Ivy_TruthCofactor(uTruth, Var << 1) != Ivy_TruthCofactor(uTruth, (Var << 1) | 1);
114 }
static unsigned Ivy_TruthCofactor(unsigned uTruth, int Var)
Definition: ivyDsd.c:96
int Var
Definition: SolverTypes.h:42
int Ivy_TruthDsd ( unsigned  uTruth,
Vec_Int_t vTree 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes DSD of truth table of 5 variables or less.]

Description [Returns 1 if the function is a constant or is fully DSD decomposable using AND/EXOR/MUX gates.]

SideEffects []

SeeAlso []

Definition at line 166 of file ivyDsd.c.

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 }
unsigned Fan0
Definition: ivyDsd.c:48
unsigned Type
Definition: ivyDsd.c:45
static Ivy_Dec_t Ivy_IntToDec(int m)
Definition: ivyDsd.c:57
static int Vec_IntPop(Vec_Int_t *p)
static int Ivy_DecToInt(Ivy_Dec_t m)
Definition: ivyDsd.c:56
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
unsigned Ivy_TruthDsdCompute(Vec_Int_t *vTree)
Definition: ivyDsd.c:478
static int Ivy_TruthDecompose_rec(unsigned uTruth, Vec_Int_t *vTree)
Definition: ivyDsd.c:219
static void Ivy_DecClear(Ivy_Dec_t *pNode)
Definition: ivyDsd.c:58
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
unsigned fCompl
Definition: ivyDsd.c:46
unsigned Ivy_TruthDsdCompute ( Vec_Int_t vTree)

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

Synopsis [Computes truth table of decomposition tree for verification.]

Description []

SideEffects []

SeeAlso []

Definition at line 478 of file ivyDsd.c.

479 {
480  return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree );
481 }
unsigned Ivy_TruthDsdCompute_rec(int iNode, Vec_Int_t *vTree)
Definition: ivyDsd.c:404
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
unsigned Ivy_TruthDsdCompute_rec ( int  iNode,
Vec_Int_t vTree 
)

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

Synopsis [Computes truth table of decomposition tree for verification.]

Description []

SideEffects []

SeeAlso []

Definition at line 404 of file ivyDsd.c.

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 }
unsigned Fan0
Definition: ivyDsd.c:48
unsigned nFans
Definition: ivyDsd.c:47
static unsigned Ivy_DecGetVar(Ivy_Dec_t *pNode, int iNum)
Definition: ivyDsd.c:130
unsigned Type
Definition: ivyDsd.c:45
static Ivy_Dec_t Ivy_IntToDec(int m)
Definition: ivyDsd.c:57
unsigned Ivy_TruthDsdCompute_rec(int iNode, Vec_Int_t *vTree)
Definition: ivyDsd.c:404
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
int Var
Definition: SolverTypes.h:42
#define assert(ex)
Definition: util_old.h:213
static unsigned s_Masks[6][2]
Definition: ivyDsd.c:65
unsigned fCompl
Definition: ivyDsd.c:46
void Ivy_TruthDsdComputePrint ( unsigned  uTruth)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 678 of file ivyDsd.c.

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 }
void Ivy_TruthDsdPrint(FILE *pFile, Vec_Int_t *vTree)
Definition: ivyDsd.c:568
int Ivy_TruthDsd(unsigned uTruth, Vec_Int_t *vTree)
FUNCTION DEFINITIONS ///.
Definition: ivyDsd.c:166
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
void Ivy_TruthDsdPrint ( FILE *  pFile,
Vec_Int_t vTree 
)

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

Synopsis [Prints the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 568 of file ivyDsd.c.

569 {
570  fprintf( pFile, "F = " );
571  Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree );
572  fprintf( pFile, "\n" );
573 }
void Ivy_TruthDsdPrint_rec(FILE *pFile, int iNode, Vec_Int_t *vTree)
Definition: ivyDsd.c:494
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void Ivy_TruthDsdPrint_rec ( FILE *  pFile,
int  iNode,
Vec_Int_t vTree 
)

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

Synopsis [Prints the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 494 of file ivyDsd.c.

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 }
unsigned Fan0
Definition: ivyDsd.c:48
unsigned nFans
Definition: ivyDsd.c:47
void Ivy_TruthDsdPrint_rec(FILE *pFile, int iNode, Vec_Int_t *vTree)
Definition: ivyDsd.c:494
static unsigned Ivy_DecGetVar(Ivy_Dec_t *pNode, int iNum)
Definition: ivyDsd.c:130
unsigned Type
Definition: ivyDsd.c:45
static Ivy_Dec_t Ivy_IntToDec(int m)
Definition: ivyDsd.c:57
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
int Var
Definition: SolverTypes.h:42
#define assert(ex)
Definition: util_old.h:213
unsigned fCompl
Definition: ivyDsd.c:46
int Ivy_TruthRecognizeMuxMaj ( unsigned  uTruth,
int *  pSupp,
int  nSupp,
Vec_Int_t vTree 
)
static

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

Synopsis [Returns a non-negative number if the truth table is a MUX.]

Description [If the truth table is a MUX, returns the variable as follows: first, control variable; second, positive cofactor; third, negative cofactor.]

SideEffects []

SeeAlso []

Definition at line 319 of file ivyDsd.c.

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 }
unsigned nFans
Definition: ivyDsd.c:47
unsigned Type
Definition: ivyDsd.c:45
static int Ivy_DecToInt(Ivy_Dec_t m)
Definition: ivyDsd.c:56
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static void Ivy_DecSetVar(Ivy_Dec_t *pNode, int iNum, unsigned Var)
Definition: ivyDsd.c:116
static int Ivy_TruthDepends(unsigned uTruth, int Var)
Definition: ivyDsd.c:111
static int Ivy_TruthDecompose_rec(unsigned uTruth, Vec_Int_t *vTree)
Definition: ivyDsd.c:219
static unsigned Ivy_TruthCofactor(unsigned uTruth, int Var)
Definition: ivyDsd.c:96
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Ivy_DecClear(Ivy_Dec_t *pNode)
Definition: ivyDsd.c:58
static int Ivy_TruthWordCountOnes(unsigned uWord)
Definition: ivyDsd.c:74
#define assert(ex)
Definition: util_old.h:213
void Ivy_TruthTestOne ( unsigned  uTruth)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 700 of file ivyDsd.c.

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 }
void Ivy_TruthDsdPrint(FILE *pFile, Vec_Int_t *vTree)
Definition: ivyDsd.c:568
int Ivy_TruthDsd(unsigned uTruth, Vec_Int_t *vTree)
FUNCTION DEFINITIONS ///.
Definition: ivyDsd.c:166
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Counter
unsigned Ivy_TruthDsdCompute(Vec_Int_t *vTree)
Definition: ivyDsd.c:478
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
static int Ivy_TruthWordCountOnes ( unsigned  uWord)
inlinestatic

Definition at line 74 of file ivyDsd.c.

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 }

Variable Documentation

unsigned s_Masks[6][2]
static
Initial value:
= {
{ 0x55555555, 0xAAAAAAAA },
{ 0x33333333, 0xCCCCCCCC },
{ 0x0F0F0F0F, 0xF0F0F0F0 },
{ 0x00FF00FF, 0xFF00FF00 },
{ 0x0000FFFF, 0xFFFF0000 },
{ 0x00000000, 0xFFFFFFFF }
}

Definition at line 65 of file ivyDsd.c.