abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcMv.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [abcMv.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Network and node package.]
8 
9  Synopsis [Multi-valued decomposition.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: abcMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/abc/abc.h"
22 #include "misc/extra/extraBdd.h"
23 
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 typedef struct Mv_Man_t_ Mv_Man_t;
32 struct Mv_Man_t_
33 {
34  int nInputs; // the number of 4-valued input variables
35  int nFuncs; // the number of 4-valued functions
36  DdManager * dd; // representation of functions
37  DdNode * bValues[15][4]; // representation of i-sets
38  DdNode * bValueDcs[15][4]; // representation of i-sets don't-cares
39  DdNode * bFuncs[15]; // representation of functions
40 };
41 
42 static void Abc_MvDecompose( Mv_Man_t * p );
43 static void Abc_MvPrintStats( Mv_Man_t * p );
44 static void Abc_MvRead( Mv_Man_t * p );
45 static void Abc_MvDeref( Mv_Man_t * p );
46 static DdNode * Abc_MvReadCube( DdManager * dd, char * pLine, int nVars );
47 
48 ////////////////////////////////////////////////////////////////////////
49 /// FUNCTION DEFINITIONS ///
50 ////////////////////////////////////////////////////////////////////////
51 
52 /**Function*************************************************************
53 
54  Synopsis []
55 
56  Description []
57 
58  SideEffects []
59 
60  SeeAlso []
61 
62 ***********************************************************************/
64 {
65  Mv_Man_t * p;
66  // get the functions
67  p = ABC_ALLOC( Mv_Man_t, 1 );
68  memset( p, 0, sizeof(Mv_Man_t) );
69  p->dd = Cudd_Init( 32, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
70  p->nFuncs = 15;
71  p->nInputs = 9;
72  Abc_MvRead( p );
73  // process the functions
74  Abc_MvPrintStats( p );
75 // Cudd_ReduceHeap( p->dd, CUDD_REORDER_SYMM_SIFT, 1 );
76 // Abc_MvPrintStats( p );
77  // try detecting support reducing bound set
78  Abc_MvDecompose( p );
79 
80  // remove the manager
81  Abc_MvDeref( p );
82  Extra_StopManager( p->dd );
83  ABC_FREE( p );
84 }
85 
86 /**Function*************************************************************
87 
88  Synopsis []
89 
90  Description []
91 
92  SideEffects []
93 
94  SeeAlso []
95 
96 ***********************************************************************/
98 {
99  int i, v;
100  for ( i = 0; i < 15; i++ )
101  {
102  printf( "%2d : ", i );
103  printf( "%3d (%2d) ", Cudd_DagSize(p->bFuncs[i])-1, Cudd_SupportSize(p->dd, p->bFuncs[i]) );
104  for ( v = 0; v < 4; v++ )
105  printf( "%d = %3d (%2d) ", v, Cudd_DagSize(p->bValues[i][v])-1, Cudd_SupportSize(p->dd, p->bValues[i][v]) );
106  printf( "\n" );
107  }
108 }
109 
110 /**Function*************************************************************
111 
112  Synopsis []
113 
114  Description []
115 
116  SideEffects []
117 
118  SeeAlso []
119 
120 ***********************************************************************/
121 DdNode * Abc_MvReadCube( DdManager * dd, char * pLine, int nVars )
122 {
123  DdNode * bCube, * bVar, * bTemp;
124  int i;
125  bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube );
126  for ( i = 0; i < nVars; i++ )
127  {
128  if ( pLine[i] == '-' )
129  continue;
130  else if ( pLine[i] == '0' ) // 0
131  bVar = Cudd_Not( Cudd_bddIthVar(dd, 29-i) );
132  else if ( pLine[i] == '1' ) // 1
133  bVar = Cudd_bddIthVar(dd, 29-i);
134  else assert(0);
135  bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube );
136  Cudd_RecursiveDeref( dd, bTemp );
137  }
138  Cudd_Deref( bCube );
139  return bCube;
140 }
141 
142 /**Function*************************************************************
143 
144  Synopsis []
145 
146  Description []
147 
148  SideEffects []
149 
150  SeeAlso []
151 
152 ***********************************************************************/
154 {
155  FILE * pFile;
156  char Buffer[1000], * pLine;
157  DdNode * bCube, * bTemp, * bProd, * bVar0, * bVar1, * bCubeSum;
158  int i, v;
159 
160  // start the cube
161  bCubeSum = Cudd_ReadLogicZero(p->dd); Cudd_Ref( bCubeSum );
162 
163  // start the values
164  for ( i = 0; i < 15; i++ )
165  for ( v = 0; v < 4; v++ )
166  {
167  p->bValues[i][v] = Cudd_ReadLogicZero(p->dd); Cudd_Ref( p->bValues[i][v] );
168  p->bValueDcs[i][v] = Cudd_ReadLogicZero(p->dd); Cudd_Ref( p->bValueDcs[i][v] );
169  }
170 
171  // read the file
172  pFile = fopen( "input.pla", "r" );
173  while ( fgets( Buffer, 1000, pFile ) )
174  {
175  if ( Buffer[0] == '#' )
176  continue;
177  if ( Buffer[0] == '.' )
178  {
179  if ( Buffer[1] == 'e' )
180  break;
181  continue;
182  }
183 
184  // get the cube
185  bCube = Abc_MvReadCube( p->dd, Buffer, 18 ); Cudd_Ref( bCube );
186 
187  // add it to the values of the output functions
188  pLine = Buffer + 19;
189  for ( i = 0; i < 15; i++ )
190  {
191  if ( pLine[2*i] == '-' && pLine[2*i+1] == '-' )
192  {
193  for ( v = 0; v < 4; v++ )
194  {
195  p->bValueDcs[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValueDcs[i][v], bCube ); Cudd_Ref( p->bValueDcs[i][v] );
196  Cudd_RecursiveDeref( p->dd, bTemp );
197  }
198  continue;
199  }
200  else if ( pLine[2*i] == '0' && pLine[2*i+1] == '0' ) // 0
201  v = 0;
202  else if ( pLine[2*i] == '1' && pLine[2*i+1] == '0' ) // 1
203  v = 1;
204  else if ( pLine[2*i] == '0' && pLine[2*i+1] == '1' ) // 2
205  v = 2;
206  else if ( pLine[2*i] == '1' && pLine[2*i+1] == '1' ) // 3
207  v = 3;
208  else assert( 0 );
209  // add the value
210  p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], bCube ); Cudd_Ref( p->bValues[i][v] );
211  Cudd_RecursiveDeref( p->dd, bTemp );
212  }
213 
214  // add the cube
215  bCubeSum = Cudd_bddOr( p->dd, bTemp = bCubeSum, bCube ); Cudd_Ref( bCubeSum );
216  Cudd_RecursiveDeref( p->dd, bTemp );
217  Cudd_RecursiveDeref( p->dd, bCube );
218  }
219 
220  // add the complement of the domain to all values
221  for ( i = 0; i < 15; i++ )
222  for ( v = 0; v < 4; v++ )
223  {
224  if ( p->bValues[i][v] == Cudd_Not(Cudd_ReadOne(p->dd)) )
225  continue;
226  p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], p->bValueDcs[i][v] ); Cudd_Ref( p->bValues[i][v] );
227  Cudd_RecursiveDeref( p->dd, bTemp );
228  p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], Cudd_Not(bCubeSum) ); Cudd_Ref( p->bValues[i][v] );
229  Cudd_RecursiveDeref( p->dd, bTemp );
230  }
231  printf( "Domain = %5.2f %%.\n", 100.0*Cudd_CountMinterm(p->dd, bCubeSum, 32)/Cudd_CountMinterm(p->dd, Cudd_ReadOne(p->dd), 32) );
232  Cudd_RecursiveDeref( p->dd, bCubeSum );
233 
234  // create each output function
235  for ( i = 0; i < 15; i++ )
236  {
237  p->bFuncs[i] = Cudd_ReadLogicZero(p->dd); Cudd_Ref( p->bFuncs[i] );
238  for ( v = 0; v < 4; v++ )
239  {
240  bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 30), ((v & 1) == 0) );
241  bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 31), ((v & 2) == 0) );
242  bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 ); Cudd_Ref( bCube );
243  bProd = Cudd_bddAnd( p->dd, p->bValues[i][v], bCube ); Cudd_Ref( bProd );
244  Cudd_RecursiveDeref( p->dd, bCube );
245  // add the value
246  p->bFuncs[i] = Cudd_bddOr( p->dd, bTemp = p->bFuncs[i], bProd ); Cudd_Ref( p->bFuncs[i] );
247  Cudd_RecursiveDeref( p->dd, bTemp );
248  Cudd_RecursiveDeref( p->dd, bProd );
249  }
250  }
251 }
252 
253 /**Function*************************************************************
254 
255  Synopsis []
256 
257  Description []
258 
259  SideEffects []
260 
261  SeeAlso []
262 
263 ***********************************************************************/
265 {
266  int i, v;
267  for ( i = 0; i < 15; i++ )
268  for ( v = 0; v < 4; v++ )
269  {
270  Cudd_RecursiveDeref( p->dd, p->bValues[i][v] );
271  Cudd_RecursiveDeref( p->dd, p->bValueDcs[i][v] );
272  }
273  for ( i = 0; i < 15; i++ )
274  Cudd_RecursiveDeref( p->dd, p->bFuncs[i] );
275 }
276 
277 
278 
279 /**Function*************************************************************
280 
281  Synopsis []
282 
283  Description []
284 
285  SideEffects []
286 
287  SeeAlso []
288 
289 ***********************************************************************/
291 {
292  DdNode * bCofs[16], * bVarCube1, * bVarCube2, * bVarCube, * bCube, * bVar0, * bVar1;//, * bRes;
293  int k, i1, i2, v1, v2;//, c1, c2, Counter;
294 
295  bVar0 = Cudd_bddIthVar(p->dd, 30);
296  bVar1 = Cudd_bddIthVar(p->dd, 31);
297  bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 ); Cudd_Ref( bCube );
298 
299  for ( k = 0; k < p->nFuncs; k++ )
300  {
301  printf( "FUNCTION %d\n", k );
302  for ( i1 = 0; i1 < p->nFuncs; i1++ )
303  for ( i2 = i1+1; i2 < p->nFuncs; i2++ )
304  {
305  Vec_Ptr_t * vCofs;
306 
307  for ( v1 = 0; v1 < 4; v1++ )
308  {
309  bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1 ), ((v1 & 1) == 0) );
310  bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1-1), ((v1 & 2) == 0) );
311  bVarCube1 = Cudd_bddAnd( p->dd, bVar0, bVar1 ); Cudd_Ref( bVarCube1 );
312  for ( v2 = 0; v2 < 4; v2++ )
313  {
314  bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2 ), ((v2 & 1) == 0) );
315  bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2-1), ((v2 & 2) == 0) );
316  bVarCube2 = Cudd_bddAnd( p->dd, bVar0, bVar1 ); Cudd_Ref( bVarCube2 );
317  bVarCube = Cudd_bddAnd( p->dd, bVarCube1, bVarCube2 ); Cudd_Ref( bVarCube );
318  bCofs[v1 * 4 + v2] = Cudd_Cofactor( p->dd, p->bFuncs[k], bVarCube ); Cudd_Ref( bCofs[v1 * 4 + v2] );
319  Cudd_RecursiveDeref( p->dd, bVarCube );
320  Cudd_RecursiveDeref( p->dd, bVarCube2 );
321  }
322  Cudd_RecursiveDeref( p->dd, bVarCube1 );
323  }
324 /*
325  // check the compatibility of cofactors
326  Counter = 0;
327  for ( c1 = 0; c1 < 16; c1++ )
328  {
329  for ( c2 = 0; c2 <= c1; c2++ )
330  printf( " " );
331  for ( c2 = c1+1; c2 < 16; c2++ )
332  {
333  bRes = Cudd_bddAndAbstract( p->dd, bCofs[c1], bCofs[c2], bCube ); Cudd_Ref( bRes );
334  if ( bRes == Cudd_ReadOne(p->dd) )
335  {
336  printf( "+" );
337  Counter++;
338  }
339  else
340  {
341  printf( " " );
342  }
343  Cudd_RecursiveDeref( p->dd, bRes );
344  }
345  printf( "\n" );
346  }
347 */
348 
349  vCofs = Vec_PtrAlloc( 16 );
350  for ( v1 = 0; v1 < 4; v1++ )
351  for ( v2 = 0; v2 < 4; v2++ )
352  Vec_PtrPushUnique( vCofs, bCofs[v1 * 4 + v2] );
353  printf( "%d ", Vec_PtrSize(vCofs) );
354  Vec_PtrFree( vCofs );
355 
356  // free the cofactors
357  for ( v1 = 0; v1 < 4; v1++ )
358  for ( v2 = 0; v2 < 4; v2++ )
359  Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );
360 
361  printf( "\n" );
362 // printf( "%2d, %2d : %3d\n", i1, i2, Counter );
363  }
364  }
365 
366  Cudd_RecursiveDeref( p->dd, bCube );
367 }
368 
369 ////////////////////////////////////////////////////////////////////////
370 /// END OF FILE ///
371 ////////////////////////////////////////////////////////////////////////
372 
373 
375 
char * memset()
int nFuncs
Definition: abcMv.c:35
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
DdNode * bFuncs[15]
Definition: abcMv.c:39
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
static void Abc_MvDecompose(Mv_Man_t *p)
Definition: abcMv.c:290
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
Definition: cudd.h:278
#define Cudd_Not(node)
Definition: cudd.h:367
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DdNode * Cudd_ReadLogicZero(DdManager *dd)
Definition: cuddAPI.c:1058
typedefABC_NAMESPACE_IMPL_START struct Mv_Man_t_ Mv_Man_t
DECLARATIONS ///.
Definition: abcMv.c:31
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
static void Abc_MvRead(Mv_Man_t *p)
Definition: abcMv.c:153
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static void Abc_MvPrintStats(Mv_Man_t *p)
Definition: abcMv.c:97
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
void Abc_MvExperiment()
FUNCTION DEFINITIONS ///.
Definition: abcMv.c:63
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
int nInputs
Definition: abcMv.c:34
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
DdNode * bValues[15][4]
Definition: abcMv.c:37
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
DdNode * bValueDcs[15][4]
Definition: abcMv.c:38
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdManager * dd
Definition: abcMv.c:36
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
static DdNode * Abc_MvReadCube(DdManager *dd, char *pLine, int nVars)
Definition: abcMv.c:121
#define assert(ex)
Definition: util_old.h:213
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
static void Abc_MvDeref(Mv_Man_t *p)
Definition: abcMv.c:264
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223