ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
lpkSets.c File Reference
#include "lpkInt.h"
Include dependency graph for lpkSets.c:

Go to the source code of this file.

Classes

struct  Lpk_Set_t_
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Lpk_Set_t_ Lpk_Set_t
 DECLARATIONS ///.
 

Functions

unsigned Lpk_ComputeSets_rec (Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets)
 FUNCTION DEFINITIONS ///.
 
unsigned Lpk_ComputeSets (Kit_DsdNtk_t *p, Vec_Int_t *vSets)
 
void Lpk_ComposeSets (Vec_Int_t *vSets0, Vec_Int_t *vSets1, int nVars, int iCofVar, Lpk_Set_t *pStore, int *pSize, int nSizeLimit)
 
void Lpk_MapSuppPrintSet (Lpk_Set_t *pSet, int i)
 
unsigned Lpk_MapSuppRedDecSelect (Lpk_Man_t *p, unsigned *pTruth, int nVars, int *piVar, int *piVarReused)
 

Typedef Documentation

◆ Lpk_Set_t

typedef typedefABC_NAMESPACE_IMPL_START struct Lpk_Set_t_ Lpk_Set_t

DECLARATIONS ///.

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

FileName [lpkSets.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]

Definition at line 30 of file lpkSets.c.

Function Documentation

◆ Lpk_ComposeSets()

void Lpk_ComposeSets ( Vec_Int_t * vSets0,
Vec_Int_t * vSets1,
int nVars,
int iCofVar,
Lpk_Set_t * pStore,
int * pSize,
int nSizeLimit )

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

Synopsis [Computes maximal support reducing bound-sets.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file lpkSets.c.

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}
typedefABC_NAMESPACE_IMPL_START struct Lpk_Set_t_ Lpk_Set_t
DECLARATIONS ///.
Definition lpkSets.c:30
#define assert(ex)
Definition util_old.h:213
char * memset()
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_ComputeSets()

unsigned Lpk_ComputeSets ( Kit_DsdNtk_t * p,
Vec_Int_t * vSets )

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

Synopsis [Computes the set of subsets of decomposable variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file lpkSets.c.

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}
Cube * p
Definition exorList.c:222
@ KIT_DSD_CONST1
Definition kit.h:103
@ KIT_DSD_VAR
Definition kit.h:104
unsigned Lpk_ComputeSets_rec(Kit_DsdNtk_t *p, int iLit, Vec_Int_t *vSets)
FUNCTION DEFINITIONS ///.
Definition lpkSets.c:56
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_ComputeSets_rec()

unsigned Lpk_ComputeSets_rec ( Kit_DsdNtk_t * p,
int iLit,
Vec_Int_t * vSets )

FUNCTION DEFINITIONS ///.

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

Synopsis [Recursively computes decomposable subsets.]

Description []

SideEffects []

SeeAlso []

Definition at line 56 of file lpkSets.c.

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}
@ KIT_DSD_XOR
Definition kit.h:106
@ KIT_DSD_PRIME
Definition kit.h:107
@ KIT_DSD_AND
Definition kit.h:105
struct Kit_DsdObj_t_ Kit_DsdObj_t
Definition kit.h:111
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition kit.h:160
unsigned Type
Definition kit.h:115
unsigned nFans
Definition kit.h:119
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_MapSuppPrintSet()

void Lpk_MapSuppPrintSet ( Lpk_Set_t * pSet,
int i )

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

Synopsis [Prints one set.]

Description []

SideEffects []

SeeAlso []

Definition at line 297 of file lpkSets.c.

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}
Here is the caller graph for this function:

◆ Lpk_MapSuppRedDecSelect()

unsigned Lpk_MapSuppRedDecSelect ( Lpk_Man_t * p,
unsigned * pTruth,
int nVars,
int * piVar,
int * piVarReused )

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

Synopsis [Evaluates the cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 323 of file lpkSets.c.

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}
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Kit_DsdNtk_t * Kit_DsdDecompose(unsigned *pTruth, int nVars)
Definition kitDsd.c:2315
void Kit_DsdPrint(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:375
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:573
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:521
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:164
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
struct Kit_DsdNtk_t_ Kit_DsdNtk_t
Definition kit.h:124
Kit_DsdNtk_t * Kit_DsdExpand(Kit_DsdNtk_t *p)
Definition kitDsd.c:1452
unsigned Lpk_ComputeSets(Kit_DsdNtk_t *p, Vec_Int_t *vSets)
Definition lpkSets.c:108
void Lpk_MapSuppPrintSet(Lpk_Set_t *pSet, int i)
Definition lpkSets.c:297
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
Here is the call graph for this function:
Here is the caller graph for this function: