abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fxuCreate.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fxuCreate.c]
4 
5  PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]
6 
7  Synopsis [Create matrix from covers and covers from matrix.]
8 
9  Author [MVSIS Group]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 1.0. Started - February 1, 2003.]
14 
15  Revision [$Id: fxuCreate.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "fxuInt.h"
20 #include "fxu.h"
21 
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// DECLARATIONS ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 static void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder );
30 static int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY );
31 static void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext );
32 static Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode );
33 static int * s_pLits;
34 
35 extern int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
36 
37 ////////////////////////////////////////////////////////////////////////
38 /// FUNCTION DEFINITIONS ///
39 ////////////////////////////////////////////////////////////////////////
40 
41 /**Function*************************************************************
42 
43  Synopsis [Creates the sparse matrix from the array of SOPs.]
44 
45  Description []
46 
47  SideEffects []
48 
49  SeeAlso []
50 
51 ***********************************************************************/
53 {
54  Fxu_Matrix * p;
55  Fxu_Var * pVar;
56  Fxu_Cube * pCubeFirst, * pCubeNew;
57  Fxu_Cube * pCube1, * pCube2;
58  Vec_Int_t * vFanins;
59  char * pSopCover;
60  char * pSopCube;
61  int * pOrder, nBitsMax;
62  int i, v, c;
63  int nCubesTotal;
64  int nPairsTotal;
65  int nPairsStore;
66  int nCubes;
67  int iCube, iPair;
68  int nFanins;
69 
70  // collect all sorts of statistics
71  nCubesTotal = 0;
72  nPairsTotal = 0;
73  nPairsStore = 0;
74  nBitsMax = -1;
75  for ( i = 0; i < pData->nNodesOld; i++ )
76  if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
77  {
78  nCubes = Abc_SopGetCubeNum( pSopCover );
79  nFanins = Abc_SopGetVarNum( pSopCover );
80  assert( nFanins > 1 && nCubes > 0 );
81 
82  nCubesTotal += nCubes;
83  nPairsTotal += nCubes * (nCubes - 1) / 2;
84  nPairsStore += nCubes * nCubes;
85  if ( nBitsMax < nFanins )
86  nBitsMax = nFanins;
87  }
88  if ( nBitsMax <= 0 )
89  {
90  printf( "The current network does not have SOPs to perform extraction.\n" );
91  return NULL;
92  }
93 
94  if ( nPairsStore > 50000000 )
95  {
96  printf( "The problem is too large to be solved by \"fxu\" (%d cubes and %d cube pairs)\n", nCubesTotal, nPairsStore );
97  return NULL;
98  }
99 
100  // start the matrix
101  p = Fxu_MatrixAllocate();
102  // create the column labels
103  p->ppVars = ABC_ALLOC( Fxu_Var *, 2 * (pData->nNodesOld + pData->nNodesExt) );
104  for ( i = 0; i < 2 * pData->nNodesOld; i++ )
105  p->ppVars[i] = Fxu_MatrixAddVar( p );
106 
107  // allocate storage for all cube pairs at once
108  p->pppPairs = ABC_ALLOC( Fxu_Pair **, nCubesTotal + 100 );
109  p->ppPairs = ABC_ALLOC( Fxu_Pair *, nPairsStore + 100 );
110  memset( p->ppPairs, 0, sizeof(Fxu_Pair *) * nPairsStore );
111  iCube = 0;
112  iPair = 0;
113  for ( i = 0; i < pData->nNodesOld; i++ )
114  if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
115  {
116  // get the number of cubes
117  nCubes = Abc_SopGetCubeNum( pSopCover );
118  // get the new var in the matrix
119  pVar = p->ppVars[2*i+1];
120  // assign the pair storage
121  pVar->nCubes = nCubes;
122  if ( nCubes > 0 )
123  {
124  pVar->ppPairs = p->pppPairs + iCube;
125  pVar->ppPairs[0] = p->ppPairs + iPair;
126  for ( v = 1; v < nCubes; v++ )
127  pVar->ppPairs[v] = pVar->ppPairs[v-1] + nCubes;
128  }
129  // update
130  iCube += nCubes;
131  iPair += nCubes * nCubes;
132  }
133  assert( iCube == nCubesTotal );
134  assert( iPair == nPairsStore );
135 
136 
137  // allocate room for the reordered literals
138  pOrder = ABC_ALLOC( int, nBitsMax );
139  // create the rows
140  for ( i = 0; i < pData->nNodesOld; i++ )
141  if ( (pSopCover = (char *)pData->vSops->pArray[i]) )
142  {
143  // get the new var in the matrix
144  pVar = p->ppVars[2*i+1];
145  // here we sort the literals of the cover
146  // in the increasing order of the numbers of the corresponding nodes
147  // because literals should be added to the matrix in this order
148  vFanins = (Vec_Int_t *)pData->vFanins->pArray[i];
149  s_pLits = vFanins->pArray;
150  // start the variable order
151  nFanins = Abc_SopGetVarNum( pSopCover );
152  for ( v = 0; v < nFanins; v++ )
153  pOrder[v] = v;
154  // reorder the fanins
155  qsort( (void *)pOrder, nFanins, sizeof(int),(int (*)(const void *, const void *))Fxu_CreateMatrixLitCompare);
156  assert( s_pLits[ pOrder[0] ] < s_pLits[ pOrder[nFanins-1] ] );
157  // create the corresponding cubes in the matrix
158  pCubeFirst = NULL;
159  c = 0;
160  Abc_SopForEachCube( pSopCover, nFanins, pSopCube )
161  {
162  // create the cube
163  pCubeNew = Fxu_MatrixAddCube( p, pVar, c++ );
164  Fxu_CreateMatrixAddCube( p, pCubeNew, pSopCube, vFanins, pOrder );
165  if ( pCubeFirst == NULL )
166  pCubeFirst = pCubeNew;
167  pCubeNew->pFirst = pCubeFirst;
168  }
169  // set the first cube of this var
170  pVar->pFirst = pCubeFirst;
171  // create the divisors without preprocessing
172  if ( nPairsTotal <= pData->nPairsMax )
173  {
174  for ( pCube1 = pCubeFirst; pCube1; pCube1 = pCube1->pNext )
175  for ( pCube2 = pCube1? pCube1->pNext: NULL; pCube2; pCube2 = pCube2->pNext )
176  Fxu_MatrixAddDivisor( p, pCube1, pCube2 );
177  }
178  }
179  ABC_FREE( pOrder );
180 
181  // consider the case when cube pairs should be preprocessed
182  // before adding them to the set of divisors
183 // if ( pData->fVerbose )
184 // printf( "The total number of cube pairs is %d.\n", nPairsTotal );
185  if ( nPairsTotal > 10000000 )
186  {
187  printf( "The total number of cube pairs of the network is more than 10,000,000.\n" );
188  printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
189  printf( "that the user changes the network by reducing the size of logic node and\n" );
190  printf( "consequently the number of cube pairs to be processed by this command.\n" );
191  printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
192  printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
193  return NULL;
194  }
195  if ( nPairsTotal > pData->nPairsMax )
196  if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
197  return NULL;
198 // if ( pData->fVerbose )
199 // printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
200 
201  if ( p->lVars.nItems > 1000000 )
202  {
203  printf( "The total number of variables is more than 1,000,000.\n" );
204  printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
205  printf( "that the user changes the network by reducing the size of logic node and\n" );
206  printf( "consequently the number of cube pairs to be processed by this command.\n" );
207  printf( "It can be achieved as follows: \"st; if -K <num>\" or \"st; renode -s -K <num>\"\n" );
208  printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
209  return NULL;
210  }
211 
212 
213  // add the var pairs to the heap
214  Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
215 
216  // print stats
217  if ( pData->fVerbose )
218  {
219  double Density;
220  Density = ((double)p->nEntries) / p->lVars.nItems / p->lCubes.nItems;
221  fprintf( stdout, "Matrix: [vars x cubes] = [%d x %d] ",
222  p->lVars.nItems, p->lCubes.nItems );
223  fprintf( stdout, "Lits = %d Density = %.5f%%\n",
224  p->nEntries, Density );
225  fprintf( stdout, "1-cube divs = %6d. (Total = %6d) ", p->lSingles.nItems, p->nSingleTotal );
226  fprintf( stdout, "2-cube divs = %6d. (Total = %6d)", p->nDivsTotal, nPairsTotal );
227  fprintf( stdout, "\n" );
228  }
229 // Fxu_MatrixPrint( stdout, p );
230  return p;
231 }
232 
233 /**Function*************************************************************
234 
235  Synopsis [Adds one cube with literals to the matrix.]
236 
237  Description [Create the cube and literals in the matrix corresponding
238  to the given cube in the SOP cover. Co-singleton transform is performed here.]
239 
240  SideEffects []
241 
242  SeeAlso []
243 
244 ***********************************************************************/
245 void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder )
246 {
247  Fxu_Var * pVar;
248  int Value, i;
249  // add literals to the matrix
250  Abc_CubeForEachVar( pSopCube, Value, i )
251  {
252  Value = pSopCube[pOrder[i]];
253  if ( Value == '0' )
254  {
255  pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] + 1 ]; // CST
256  Fxu_MatrixAddLiteral( p, pCube, pVar );
257  }
258  else if ( Value == '1' )
259  {
260  pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] ]; // CST
261  Fxu_MatrixAddLiteral( p, pCube, pVar );
262  }
263  }
264 }
265 
266 
267 /**Function*************************************************************
268 
269  Synopsis [Creates the new array of Sop covers from the sparse matrix.]
270 
271  Description []
272 
273  SideEffects []
274 
275  SeeAlso []
276 
277 ***********************************************************************/
279 {
280  Fxu_Cube * pCube, * pCubeFirst, * pCubeNext;
281  char * pSopCover;
282  int iNode, n;
283 
284  // get the first cube of the first internal node
285  pCubeFirst = Fxu_CreateCoversFirstCube( p, pData, 0 );
286 
287  // go through the internal nodes
288  for ( n = 0; n < pData->nNodesOld; n++ )
289  if ( (pSopCover = (char *)pData->vSops->pArray[n]) )
290  {
291  // get the number of this node
292  iNode = n;
293  // get the next first cube
294  pCubeNext = Fxu_CreateCoversFirstCube( p, pData, iNode + 1 );
295  // check if there any new variables in these cubes
296  for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
297  if ( pCube->lLits.pTail && pCube->lLits.pTail->iVar >= 2 * pData->nNodesOld )
298  break;
299  if ( pCube != pCubeNext )
300  Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
301  // update the first cube
302  pCubeFirst = pCubeNext;
303  }
304 
305  // add the covers for the extracted nodes
306  for ( n = 0; n < pData->nNodesNew; n++ )
307  {
308  // get the number of this node
309  iNode = pData->nNodesOld + n;
310  // get the next first cube
311  pCubeNext = Fxu_CreateCoversFirstCube( p, pData, iNode + 1 );
312  // the node should be added
313  Fxu_CreateCoversNode( p, pData, iNode, pCubeFirst, pCubeNext );
314  // update the first cube
315  pCubeFirst = pCubeNext;
316  }
317 }
318 
319 /**Function*************************************************************
320 
321  Synopsis [Create Sop covers for one node that has changed.]
322 
323  Description []
324 
325  SideEffects []
326 
327  SeeAlso []
328 
329 ***********************************************************************/
330 void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext )
331 {
332  Vec_Int_t * vInputsNew;
333  char * pSopCover, * pSopCube;
334  Fxu_Var * pVar;
335  Fxu_Cube * pCube;
336  Fxu_Lit * pLit;
337  int iNum, nCubes, v;
338 
339  // collect positive polarity variable in the cubes between pCubeFirst and pCubeNext
341  for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
342  for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
343  {
344  pVar = p->ppVars[ 2 * (pLit->pVar->iVar/2) + 1 ];
345  if ( pVar->pOrder == NULL )
346  Fxu_MatrixRingVarsAdd( p, pVar );
347  }
349 
350  // collect the variable numbers
351  vInputsNew = Vec_IntAlloc( 4 );
352  Fxu_MatrixForEachVarInRing( p, pVar )
353  Vec_IntPush( vInputsNew, pVar->iVar / 2 );
355 
356  // sort the vars by their number
357  Vec_IntSort( vInputsNew, 0 );
358 
359  // mark the vars with their numbers in the sorted array
360  for ( v = 0; v < vInputsNew->nSize; v++ )
361  {
362  p->ppVars[ 2 * vInputsNew->pArray[v] + 0 ]->lLits.nItems = v; // hack - reuse lLits.nItems
363  p->ppVars[ 2 * vInputsNew->pArray[v] + 1 ]->lLits.nItems = v; // hack - reuse lLits.nItems
364  }
365 
366  // count the number of cubes
367  nCubes = 0;
368  for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
369  if ( pCube->lLits.nItems )
370  nCubes++;
371 
372  // allocate room for the new cover
373  pSopCover = Abc_SopStart( pData->pManSop, nCubes, vInputsNew->nSize );
374  // set the correct polarity of the cover
375  if ( iNode < pData->nNodesOld && Abc_SopGetPhase( (char *)pData->vSops->pArray[iNode] ) == 0 )
376  Abc_SopComplement( pSopCover );
377 
378  // add the cubes
379  nCubes = 0;
380  for ( pCube = pCubeFirst; pCube != pCubeNext; pCube = pCube->pNext )
381  {
382  if ( pCube->lLits.nItems == 0 )
383  continue;
384  // get hold of the SOP cube
385  pSopCube = pSopCover + nCubes * (vInputsNew->nSize + 3);
386  // insert literals
387  for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
388  {
389  iNum = pLit->pVar->lLits.nItems; // hack - reuse lLits.nItems
390  assert( iNum < vInputsNew->nSize );
391  if ( pLit->pVar->iVar / 2 < pData->nNodesOld )
392  pSopCube[iNum] = (pLit->pVar->iVar & 1)? '0' : '1'; // reverse CST
393  else
394  pSopCube[iNum] = (pLit->pVar->iVar & 1)? '1' : '0'; // no CST
395  }
396  // count the cube
397  nCubes++;
398  }
399  assert( nCubes == Abc_SopGetCubeNum(pSopCover) );
400 
401  // set the new cover and the array of fanins
402  pData->vSopsNew->pArray[iNode] = pSopCover;
403  pData->vFaninsNew->pArray[iNode] = vInputsNew;
404 }
405 
406 
407 /**Function*************************************************************
408 
409  Synopsis [Adds the var to storage.]
410 
411  Description []
412 
413  SideEffects []
414 
415  SeeAlso []
416 
417 ***********************************************************************/
419 {
420  int v;
421  for ( v = iVar; v < pData->nNodesOld + pData->nNodesNew; v++ )
422  if ( p->ppVars[ 2*v + 1 ]->pFirst )
423  return p->ppVars[ 2*v + 1 ]->pFirst;
424  return NULL;
425 }
426 
427 /**Function*************************************************************
428 
429  Synopsis [Compares the vars by their number.]
430 
431  Description []
432 
433  SideEffects []
434 
435  SeeAlso []
436 
437 ***********************************************************************/
438 int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY )
439 {
440  return s_pLits[*ptrX] - s_pLits[*ptrY];
441 }
442 
443 ////////////////////////////////////////////////////////////////////////
444 /// END OF FILE ///
445 ////////////////////////////////////////////////////////////////////////
447 
char * memset()
int nCubes
Definition: fxuInt.h:216
Definition: fxuInt.h:213
ABC_DLL char * Abc_SopStart(Mem_Flex_t *pMan, int nCubes, int nVars)
Definition: abcSop.c:76
static int * s_pLits
Definition: fxuCreate.c:33
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Fxu_ListLit lLits
Definition: fxuInt.h:219
Fxu_Matrix * Fxu_MatrixAllocate()
DECLARATIONS ///.
Definition: fxuMatrix.c:43
static ABC_NAMESPACE_IMPL_START void Fxu_CreateMatrixAddCube(Fxu_Matrix *p, Fxu_Cube *pCube, char *pSopCube, Vec_Int_t *vFanins, int *pOrder)
DECLARATIONS ///.
Definition: fxuCreate.c:245
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int iVar
Definition: fxuInt.h:215
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Fxu_MatrixAddDivisor(Fxu_Matrix *p, Fxu_Cube *pCube1, Fxu_Cube *pCube2)
Definition: fxuMatrix.c:301
#define Abc_SopForEachCube(pSop, nFanins, pCube)
Definition: abc.h:531
ABC_DLL int Abc_SopGetCubeNum(char *pSop)
Definition: abcSop.c:489
typedefABC_NAMESPACE_HEADER_START struct FxuDataStruct Fxu_Data_t
INCLUDES ///.
Definition: fxu.h:42
Fxu_Lit * pHead
Definition: fxuInt.h:109
#define Fxu_MatrixForEachVarInRing(Matrix, Var)
Definition: fxuInt.h:407
Fxu_Lit * pHNext
Definition: fxuInt.h:233
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
#define Abc_CubeForEachVar(pCube, Value, i)
Definition: abc.h:529
static Fxu_Cube * Fxu_CreateCoversFirstCube(Fxu_Matrix *p, Fxu_Data_t *pData, int iNode)
Definition: fxuCreate.c:418
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
void Fxu_MatrixComputeSingles(Fxu_Matrix *p, int fUse0, int nSingleMax)
FUNCTION DEFINITIONS ///.
Definition: fxuSingle.c:47
void Fxu_MatrixAddLiteral(Fxu_Matrix *p, Fxu_Cube *pCube, Fxu_Var *pVar)
Definition: fxuMatrix.c:205
#define Fxu_MatrixRingVarsStart(Matrix)
Definition: fxuInt.h:386
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Fxu_ListLit lLits
Definition: fxuInt.h:206
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Fxu_Cube * Fxu_MatrixAddCube(Fxu_Matrix *p, Fxu_Var *pVar, int iCube)
Definition: fxuMatrix.c:183
Fxu_Cube * pFirst
Definition: fxuInt.h:217
void Fxu_MatrixRingVarsUnmark(Fxu_Matrix *p)
Definition: fxu.c:206
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define Fxu_MatrixRingVarsAdd(Matrix, Var)
Definition: fxuInt.h:395
Fxu_Cube * pFirst
Definition: fxuInt.h:204
Fxu_Cube * pNext
Definition: fxuInt.h:208
int iVar
Definition: fxuInt.h:228
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Fxu_Lit * pTail
Definition: fxuInt.h:110
ABC_DLL void Abc_SopComplement(char *pSop)
Definition: abcSop.c:600
#define ABC_FREE(obj)
Definition: abc_global.h:232
Fxu_Pair *** ppPairs
Definition: fxuInt.h:218
void Fxu_CreateCovers(Fxu_Matrix *p, Fxu_Data_t *pData)
Definition: fxuCreate.c:278
Fxu_Var * pVar
Definition: fxuInt.h:231
Fxu_Var * pOrder
Definition: fxuInt.h:222
ABC_DLL int Abc_SopGetVarNum(char *pSop)
Definition: abcSop.c:536
int nItems
Definition: fxuInt.h:111
#define Fxu_MatrixRingVarsStop(Matrix)
Definition: fxuInt.h:389
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct FxuMatrix Fxu_Matrix
INCLUDES ///.
Definition: fxuInt.h:63
Definition: fxuInt.h:226
Fxu_Matrix * Fxu_CreateMatrix(Fxu_Data_t *pData)
FUNCTION DEFINITIONS ///.
Definition: fxuCreate.c:52
int Fxu_PreprocessCubePairs(Fxu_Matrix *p, Vec_Ptr_t *vCovers, int nPairsTotal, int nPairsMax)
FUNCTION DEFINITIONS ///.
Definition: fxuReduce.c:53
Fxu_Var * Fxu_MatrixAddVar(Fxu_Matrix *p)
Definition: fxuMatrix.c:161
static int Fxu_CreateMatrixLitCompare(int *ptrX, int *ptrY)
Definition: fxuCreate.c:438
ABC_DLL int Abc_SopGetPhase(char *pSop)
Definition: abcSop.c:556
static void Fxu_CreateCoversNode(Fxu_Matrix *p, Fxu_Data_t *pData, int iNode, Fxu_Cube *pCubeFirst, Fxu_Cube *pCubeNext)
Definition: fxuCreate.c:330