abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
lpkSets.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [lpkSets.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Fast Boolean matching for LUT structures.]
8 
9  Synopsis []
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - April 28, 2007.]
16 
17  Revision [$Id: lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "lpkInt.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 typedef struct Lpk_Set_t_ Lpk_Set_t;
31 struct Lpk_Set_t_
32 {
33  char iVar; // the cofactoring variable
34  char Over; // the overlap in supports
35  char SRed; // the support reduction
36  char Size; // the size of the boundset
37  unsigned uSubset0; // the first subset (with removed)
38  unsigned uSubset1; // the second subset (with removed)
39 };
40 
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44 
45 /**Function*************************************************************
46 
47  Synopsis [Recursively computes decomposable subsets.]
48 
49  Description []
50 
51  SideEffects []
52 
53  SeeAlso []
54 
55 ***********************************************************************/
56 unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
57 {
58  unsigned i, iLitFanin, uSupport, uSuppCur;
59  Kit_DsdObj_t * pObj;
60  // consider the case of simple gate
61  pObj = Kit_DsdNtkObj( p, Abc_Lit2Var(iLit) );
62  if ( pObj == NULL )
63  return (1 << Abc_Lit2Var(iLit));
64  if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
65  {
66  unsigned uSupps[16], Limit, s;
67  uSupport = 0;
68  Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
69  {
70  uSupps[i] = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
71  uSupport |= uSupps[i];
72  }
73  // create all subsets, except empty and full
74  Limit = (1 << pObj->nFans) - 1;
75  for ( s = 1; s < Limit; s++ )
76  {
77  uSuppCur = 0;
78  for ( i = 0; i < pObj->nFans; i++ )
79  if ( s & (1 << i) )
80  uSuppCur |= uSupps[i];
81  Vec_IntPush( vSets, uSuppCur );
82  }
83  return uSupport;
84  }
85  assert( pObj->Type == KIT_DSD_PRIME );
86  // get the cumulative support of all fanins
87  uSupport = 0;
88  Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
89  {
90  uSuppCur = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
91  uSupport |= uSuppCur;
92  Vec_IntPush( vSets, uSuppCur );
93  }
94  return uSupport;
95 }
96 
97 /**Function*************************************************************
98 
99  Synopsis [Computes the set of subsets of decomposable variables.]
100 
101  Description []
102 
103  SideEffects []
104 
105  SeeAlso []
106 
107 ***********************************************************************/
108 unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
109 {
110  unsigned uSupport, Entry;
111  int Number, i;
112  assert( p->nVars <= 16 );
113  Vec_IntClear( vSets );
114  Vec_IntPush( vSets, 0 );
115  if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
116  return 0;
117  if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
118  {
119  uSupport = ( 1 << Abc_Lit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
120  Vec_IntPush( vSets, uSupport );
121  return uSupport;
122  }
123  uSupport = Lpk_ComputeSets_rec( p, p->Root, vSets );
124  assert( (uSupport & 0xFFFF0000) == 0 );
125  Vec_IntPush( vSets, uSupport );
126  // set the remaining variables
127  Vec_IntForEachEntry( vSets, Number, i )
128  {
129  Entry = Number;
130  Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
131  }
132  return uSupport;
133 }
134 
135 /**Function*************************************************************
136 
137  Synopsis [Prints the sets of subsets.]
138 
139  Description []
140 
141  SideEffects []
142 
143  SeeAlso []
144 
145 ***********************************************************************/
146 static void Lpk_PrintSetOne( int uSupport )
147 {
148  unsigned k;
149  for ( k = 0; k < 16; k++ )
150  if ( uSupport & (1<<k) )
151  printf( "%c", 'a'+k );
152  printf( " " );
153 }
154 /**Function*************************************************************
155 
156  Synopsis [Prints the sets of subsets.]
157 
158  Description []
159 
160  SideEffects []
161 
162  SeeAlso []
163 
164 ***********************************************************************/
165 static void Lpk_PrintSets( Vec_Int_t * vSets )
166 {
167  unsigned uSupport;
168  int Number, i;
169  printf( "Subsets(%d): ", Vec_IntSize(vSets) );
170  Vec_IntForEachEntry( vSets, Number, i )
171  {
172  uSupport = Number;
173  Lpk_PrintSetOne( uSupport );
174  }
175  printf( "\n" );
176 }
177 
178 /**Function*************************************************************
179 
180  Synopsis [Computes maximal support reducing bound-sets.]
181 
182  Description []
183 
184  SideEffects []
185 
186  SeeAlso []
187 
188 ***********************************************************************/
189 void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCofVar,
190  Lpk_Set_t * pStore, int * pSize, int nSizeLimit )
191 {
192  static int nTravId = 0; // the number of the times this is visited
193  static int TravId[1<<16] = {0}; // last visited
194  static char SRed[1<<16]; // best support reduction
195  static char Over[1<<16]; // best overlaps
196  static unsigned Parents[1<<16]; // best set of parents
197  static unsigned short Used[1<<16]; // storage for used subsets
198  int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s;
199  unsigned Entry, Entry0, Entry1;
200  unsigned uSupp, uSupp0, uSupp1, uSuppTotal;
201  Lpk_Set_t * pEntry;
202 
203  if ( nTravId == (1 << 30) )
204  memset( TravId, 0, sizeof(int) * (1 << 16) );
205 
206  // collect support reducing subsets
207  nUsed = 0;
208  nTravId++;
209  uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar);
210  Vec_IntForEachEntry( vSets0, Entry0, i )
211  Vec_IntForEachEntry( vSets1, Entry1, k )
212  {
213  uSupp0 = (Entry0 & 0xFFFF);
214  uSupp1 = (Entry1 & 0xFFFF);
215  // skip trivial
216  if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal )
217  continue;
218  if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) )
219  continue;
220  // get the entry
221  Entry = Entry0 | Entry1;
222  uSupp = Entry & 0xFFFF;
223  // set the bound set size
224  nSuppSize = Kit_WordCountOnes( uSupp );
225  // get the number of overlapping vars
226  nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) );
227  // get the support reduction
228  nSuppRed = nSuppSize - 1 - nSuppOver;
229  // only consider support-reducing subsets
230  if ( nSuppRed <= 0 )
231  continue;
232  // check if this support is already used
233  if ( TravId[uSupp] < nTravId )
234  {
235  Used[nUsed++] = uSupp;
236 
237  TravId[uSupp] = nTravId;
238  SRed[uSupp] = nSuppRed;
239  Over[uSupp] = nSuppOver;
240  Parents[uSupp] = (k << 16) | i;
241  }
242  else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed )
243  {
244  TravId[uSupp] = nTravId;
245  SRed[uSupp] = nSuppRed;
246  Over[uSupp] = nSuppOver;
247  Parents[uSupp] = (k << 16) | i;
248  }
249  }
250 
251  // find the minimum overlap
252  nMinOver = 1000;
253  for ( s = 0; s < nUsed; s++ )
254  if ( nMinOver > Over[Used[s]] )
255  nMinOver = Over[Used[s]];
256 
257 
258  // collect the accumulated ones
259  for ( s = 0; s < nUsed; s++ )
260  if ( Over[Used[s]] == nMinOver )
261  {
262  // save the entry
263  if ( *pSize == nSizeLimit )
264  return;
265  pEntry = pStore + (*pSize)++;
266 
267  i = Parents[Used[s]] & 0xFFFF;
268  k = Parents[Used[s]] >> 16;
269 
270  pEntry->uSubset0 = Vec_IntEntry(vSets0, i);
271  pEntry->uSubset1 = Vec_IntEntry(vSets1, k);
272  Entry = pEntry->uSubset0 | pEntry->uSubset1;
273 
274  // record the cofactoring variable
275  pEntry->iVar = iCofVar;
276  // set the bound set size
277  pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF );
278  // get the number of overlapping vars
279  pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
280  // get the support reduction
281  pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
282  assert( pEntry->SRed > 0 );
283  }
284 }
285 
286 /**Function*************************************************************
287 
288  Synopsis [Prints one set.]
289 
290  Description []
291 
292  SideEffects []
293 
294  SeeAlso []
295 
296 ***********************************************************************/
297 void Lpk_MapSuppPrintSet( Lpk_Set_t * pSet, int i )
298 {
299  unsigned Entry;
300  Entry = pSet->uSubset0 | pSet->uSubset1;
301  printf( "%2d : ", i );
302  printf( "Var = %c ", 'a' + pSet->iVar );
303  printf( "Size = %2d ", pSet->Size );
304  printf( "Over = %2d ", pSet->Over );
305  printf( "SRed = %2d ", pSet->SRed );
306  Lpk_PrintSetOne( Entry );
307  printf( " " );
308  Lpk_PrintSetOne( Entry >> 16 );
309  printf( "\n" );
310 }
311 
312 /**Function*************************************************************
313 
314  Synopsis [Evaluates the cofactors.]
315 
316  Description []
317 
318  SideEffects []
319 
320  SeeAlso []
321 
322 ***********************************************************************/
323 unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused )
324 {
325  static int nStoreSize = 256;
326  static Lpk_Set_t pStore[256], * pSet, * pSetBest;
327  Kit_DsdNtk_t * ppNtks[2], * pTemp;
328  Vec_Int_t * vSets0 = p->vSets[0];
329  Vec_Int_t * vSets1 = p->vSets[1];
330  unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 );
331  unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 );
332  int nSets, i, SizeMax;//, SRedMax;
333  unsigned Entry;
334  int fVerbose = p->pPars->fVeryVerbose;
335 // int fVerbose = 0;
336 
337  // collect decomposable subsets for each pair of cofactors
338  if ( fVerbose )
339  {
340  printf( "\nExploring support-reducing bound-sets of function:\n" );
341  Kit_DsdPrintFromTruth( pTruth, nVars );
342  }
343  nSets = 0;
344  for ( i = 0; i < nVars; i++ )
345  {
346  if ( fVerbose )
347  printf( "Evaluating variable %c:\n", 'a'+i );
348  // evaluate the cofactor pair
349  Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
350  Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
351  // decompose and expand
352  ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
353  ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
354  ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
355  ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
356  if ( fVerbose )
357  Kit_DsdPrint( stdout, ppNtks[0] );
358  if ( fVerbose )
359  Kit_DsdPrint( stdout, ppNtks[1] );
360  // compute subsets
361  Lpk_ComputeSets( ppNtks[0], vSets0 );
362  Lpk_ComputeSets( ppNtks[1], vSets1 );
363  // print subsets
364  if ( fVerbose )
365  Lpk_PrintSets( vSets0 );
366  if ( fVerbose )
367  Lpk_PrintSets( vSets1 );
368  // free the networks
369  Kit_DsdNtkFree( ppNtks[0] );
370  Kit_DsdNtkFree( ppNtks[1] );
371  // evaluate the pair
372  Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize );
373  }
374 
375  // print the results
376  if ( fVerbose )
377  printf( "\n" );
378  if ( fVerbose )
379  for ( i = 0; i < nSets; i++ )
380  Lpk_MapSuppPrintSet( pStore + i, i );
381 
382  // choose the best subset
383  SizeMax = 0;
384  pSetBest = NULL;
385  for ( i = 0; i < nSets; i++ )
386  {
387  pSet = pStore + i;
388  if ( pSet->Size > p->pPars->nLutSize - 1 )
389  continue;
390  if ( SizeMax < pSet->Size )
391  {
392  pSetBest = pSet;
393  SizeMax = pSet->Size;
394  }
395  }
396 /*
397  // if the best is not choosen, select the one with largest reduction
398  SRedMax = 0;
399  if ( pSetBest == NULL )
400  {
401  for ( i = 0; i < nSets; i++ )
402  {
403  pSet = pStore + i;
404  if ( SRedMax < pSet->SRed )
405  {
406  pSetBest = pSet;
407  SRedMax = pSet->SRed;
408  }
409  }
410  }
411 */
412  if ( pSetBest == NULL )
413  {
414  if ( fVerbose )
415  printf( "Could not select a subset.\n" );
416  return 0;
417  }
418  else
419  {
420  if ( fVerbose )
421  printf( "Selected the following subset:\n" );
422  if ( fVerbose )
423  Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
424  }
425 
426  // prepare the return result
427  // get the remaining variables
428  Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16));
429  // get the variables to be removed
430  Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry;
431  // make sure there are some - otherwise it is not supp-red
432  assert( Entry );
433  // remember the first such variable
434  *piVarReused = Kit_WordFindFirstBit( Entry );
435  *piVar = pSetBest->iVar;
436  return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF);
437 }
438 
439 ////////////////////////////////////////////////////////////////////////
440 /// END OF FILE ///
441 ////////////////////////////////////////////////////////////////////////
442 
443 
445 
char * memset()
unsigned Type
Definition: kit.h:112
char iVar
Definition: lpkSets.c:33
void Lpk_ComposeSets(Vec_Int_t *vSets0, Vec_Int_t *vSets1, int nVars, int iCofVar, Lpk_Set_t *pStore, int *pSize, int nSizeLimit)
Definition: lpkSets.c:189
static Kit_DsdObj_t * Kit_DsdNtkRoot(Kit_DsdNtk_t *pNtk)
Definition: kit.h:151
Lpk_Par_t * pPars
Definition: lpkInt.h:72
static void Lpk_PrintSets(Vec_Int_t *vSets)
Definition: lpkSets.c:165
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Kit_WordHasOneBit(unsigned uWord)
Definition: kit.h:239
unsigned nFans
Definition: kit.h:116
static Kit_DsdObj_t * Kit_DsdNtkObj(Kit_DsdNtk_t *pNtk, int Id)
Definition: kit.h:150
Vec_Int_t * vSets[8]
Definition: lpkInt.h:105
unsigned short Root
Definition: kit.h:127
unsigned Lpk_ComputeSets_rec(Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets)
FUNCTION DEFINITIONS ///.
Definition: lpkSets.c:56
typedefABC_NAMESPACE_IMPL_START struct Lpk_Set_t_ Lpk_Set_t
DECLARATIONS ///.
Definition: lpkSets.c:30
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition: kitDsd.c:490
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition: kit.h:157
Vec_Ptr_t * vTtNodes
Definition: lpkInt.h:98
Kit_DsdNtk_t * Kit_DsdDecompose(unsigned *pTruth, int nVars)
Definition: kitDsd.c:2314
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:521
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
unsigned Lpk_MapSuppRedDecSelect(Lpk_Man_t *p, unsigned *pTruth, int nVars, int *piVar, int *piVarReused)
Definition: lpkSets.c:323
static void Lpk_PrintSetOne(int uSupport)
Definition: lpkSets.c:146
void Kit_DsdPrint(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:374
char Size
Definition: lpkSets.c:36
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition: kitTruth.c:573
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
char Over
Definition: lpkSets.c:34
void Lpk_MapSuppPrintSet(Lpk_Set_t *pSet, int i)
Definition: lpkSets.c:297
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
unsigned uSubset1
Definition: lpkSets.c:38
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Kit_WordFindFirstBit(unsigned uWord)
Definition: kit.h:231
unsigned uSubset0
Definition: lpkSets.c:37
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition: kitDsd.c:163
#define assert(ex)
Definition: util_old.h:213
static int Kit_WordCountOnes(unsigned uWord)
Definition: kit.h:243
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Kit_DsdNtk_t * Kit_DsdExpand(Kit_DsdNtk_t *p)
Definition: kitDsd.c:1451
char SRed
Definition: lpkSets.c:35
unsigned short nVars
Definition: kit.h:124
static unsigned Kit_BitMask(int nBits)
Definition: kit.h:225
unsigned Lpk_ComputeSets(Kit_DsdNtk_t *p, Vec_Int_t *vSets)
Definition: lpkSets.c:108