abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Structures | Typedefs | Functions
abcMv.c File Reference
#include "base/abc/abc.h"
#include "misc/extra/extraBdd.h"

Go to the source code of this file.

Data Structures

struct  Mv_Man_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Mv_Man_t_ 		Mv_Man_t
 DECLARATIONS ///. More...
 

Functions

static void Abc_MvDecompose (Mv_Man_t *p)
 
static void Abc_MvPrintStats (Mv_Man_t *p)
 
static void Abc_MvRead (Mv_Man_t *p)
 
static void Abc_MvDeref (Mv_Man_t *p)
 
static DdNode * Abc_MvReadCube (DdManager *dd, char *pLine, int nVars)
 
void Abc_MvExperiment ()
 FUNCTION DEFINITIONS ///. More...
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Mv_Man_t_ Mv_Man_t

DECLARATIONS ///.

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

FileName [abcMv.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Multi-valued decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
abcMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 31 of file abcMv.c.

Function Documentation

void Abc_MvDecompose ( Mv_Man_t *  p)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 290 of file abcMv.c.

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 }
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Llb_Mgr_t_::dd
DdManager * dd
Definition: llb3Image.c:52
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Cudd_Cofactor
DdNode * Cudd_Cofactor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddCof.c:123
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void Abc_MvDeref ( Mv_Man_t *  p)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file abcMv.c.

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 }
Llb_Mgr_t_::dd
DdManager * dd
Definition: llb3Image.c:52
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Abc_MvExperiment ( )

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file abcMv.c.

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 }
memset
char * memset()
CUDD_UNIQUE_SLOTS
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:97
Abc_MvDecompose
static void Abc_MvDecompose(Mv_Man_t *p)
Definition: abcMv.c:290
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Mv_Man_t
typedefABC_NAMESPACE_IMPL_START struct Mv_Man_t_ Mv_Man_t
DECLARATIONS ///.
Definition: abcMv.c:31
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:98
Abc_MvRead
static void Abc_MvRead(Mv_Man_t *p)
Definition: abcMv.c:153
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition: extraBddMisc.c:223
Abc_MvPrintStats
static void Abc_MvPrintStats(Mv_Man_t *p)
Definition: abcMv.c:97
Cudd_Init
DdManager * Cudd_Init(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory)
Definition: cuddInit.c:125
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_MvDeref
static void Abc_MvDeref(Mv_Man_t *p)
Definition: abcMv.c:264
void Abc_MvPrintStats ( Mv_Man_t *  p)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file abcMv.c.

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 }
Llb_Mgr_t_::dd
DdManager * dd
Definition: llb3Image.c:52
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cudd_SupportSize
int Cudd_SupportSize(DdManager *dd, DdNode *f)
Definition: cuddUtil.c:857
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
void Abc_MvRead ( Mv_Man_t *  p)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file abcMv.c.

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 }
Llb_Mgr_t_::dd
DdManager * dd
Definition: llb3Image.c:52
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Cudd_CountMinterm
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cudd_ReadLogicZero
DdNode * Cudd_ReadLogicZero(DdManager *dd)
Definition: cuddAPI.c:1058
Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Abc_MvReadCube
static DdNode * Abc_MvReadCube(DdManager *dd, char *pLine, int nVars)
Definition: abcMv.c:121
assert
#define assert(ex)
Definition: util_old.h:213
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
DdNode * Abc_MvReadCube ( DdManager *  dd,
char *  pLine,
int  nVars 
)
static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file abcMv.c.

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 }
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Cudd_ReadOne
DdNode * Cudd_ReadOne(DdManager *dd)
Definition: cuddAPI.c:987
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
assert
#define assert(ex)
Definition: util_old.h:213
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129