ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
lpkInt.h File Reference
#include "base/abc/abc.h"
#include "bool/kit/kit.h"
#include "map/if/if.h"
#include "lpk.h"
Include dependency graph for lpkInt.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Lpk_Cut_t_
 
struct  Lpk_Man_t_
 
struct  Lpk_Fun_t_
 
struct  Lpk_Res_t_
 

Macros

#define LPK_SIZE_MAX   100
 INCLUDES ///.
 
#define LPK_CUTS_MAX   10000
 
#define Lpk_CutForEachLeaf(pNtk, pCut, pObj, i)
 MACRO DEFINITIONS ///.
 
#define Lpk_CutForEachNode(pNtk, pCut, pObj, i)
 
#define Lpk_CutForEachNodeReverse(pNtk, pCut, pObj, i)
 
#define Lpk_SuppForEachVar(Supp, Var)
 

Typedefs

typedef struct Lpk_Man_t_ Lpk_Man_t
 
typedef struct Lpk_Cut_t_ Lpk_Cut_t
 
typedef struct Lpk_Fun_t_ Lpk_Fun_t
 
typedef struct Lpk_Res_t_ Lpk_Res_t
 

Functions

Abc_Obj_tLpk_Decompose (Lpk_Man_t *pMan, Abc_Ntk_t *pNtk, Vec_Ptr_t *vLeaves, unsigned *pTruth, unsigned *puSupps, int nLutK, int AreaLim, int DelayLim)
 FUNCTION DECLARATIONS ///.
 
Lpk_Res_tLpk_DsdAnalize (Lpk_Man_t *pMan, Lpk_Fun_t *p, int nShared)
 
Lpk_Fun_tLpk_DsdSplit (Lpk_Man_t *pMan, Lpk_Fun_t *p, char *pCofVars, int nCofVars, unsigned uBoundSet)
 
Lpk_Res_tLpk_MuxAnalize (Lpk_Man_t *pMan, Lpk_Fun_t *p)
 DECLARATIONS ///.
 
Lpk_Fun_tLpk_MuxSplit (Lpk_Man_t *pMan, Lpk_Fun_t *p, int Var, int Pol)
 
Lpk_Fun_tLpk_FunAlloc (int nVars)
 DECLARATIONS ///.
 
void Lpk_FunFree (Lpk_Fun_t *p)
 
Lpk_Fun_tLpk_FunCreate (Abc_Ntk_t *pNtk, Vec_Ptr_t *vLeaves, unsigned *pTruth, int nLutK, int AreaLim, int DelayLim)
 
Lpk_Fun_tLpk_FunDup (Lpk_Fun_t *p, unsigned *pTruth)
 
int Lpk_FunSuppMinimize (Lpk_Fun_t *p)
 
void Lpk_FunComputeCofSupps (Lpk_Fun_t *p)
 
int Lpk_SuppDelay (unsigned uSupp, int *pDelays)
 
int Lpk_SuppToVars (unsigned uBoundSet, char *pVars)
 
unsigned * Lpk_CutTruth (Lpk_Man_t *p, Lpk_Cut_t *pCut, int fInv)
 
int Lpk_NodeCuts (Lpk_Man_t *p)
 
Lpk_Man_tLpk_ManStart (Lpk_Par_t *pPars)
 DECLARATIONS ///.
 
void Lpk_ManStop (Lpk_Man_t *p)
 
If_Obj_tLpk_MapPrime (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
 
If_Obj_tLpk_MapTree_rec (Lpk_Man_t *p, Kit_DsdNtk_t *pNtk, If_Obj_t **ppLeaves, int iLit, If_Obj_t *pResult)
 
If_Obj_tLpk_MapTreeMulti (Lpk_Man_t *p, unsigned *pTruth, int nLeaves, If_Obj_t **ppLeaves)
 
If_Obj_tLpk_MapTreeMux_rec (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
 
If_Obj_tLpk_MapSuppRedDec_rec (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
 
unsigned Lpk_MapSuppRedDecSelect (Lpk_Man_t *p, unsigned *pTruth, int nVars, int *piVar, int *piVarReused)
 

Macro Definition Documentation

◆ Lpk_CutForEachLeaf

#define Lpk_CutForEachLeaf ( pNtk,
pCut,
pObj,
i )
Value:
for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )

MACRO DEFINITIONS ///.

ITERATORS ///

Definition at line 190 of file lpkInt.h.

190#define Lpk_CutForEachLeaf( pNtk, pCut, pObj, i ) \
191 for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )

◆ Lpk_CutForEachNode

#define Lpk_CutForEachNode ( pNtk,
pCut,
pObj,
i )
Value:
for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )

Definition at line 192 of file lpkInt.h.

192#define Lpk_CutForEachNode( pNtk, pCut, pObj, i ) \
193 for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )

◆ Lpk_CutForEachNodeReverse

#define Lpk_CutForEachNodeReverse ( pNtk,
pCut,
pObj,
i )
Value:
for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )

Definition at line 194 of file lpkInt.h.

194#define Lpk_CutForEachNodeReverse( pNtk, pCut, pObj, i ) \
195 for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )

◆ LPK_CUTS_MAX

#define LPK_CUTS_MAX   10000

Definition at line 48 of file lpkInt.h.

◆ LPK_SIZE_MAX

#define LPK_SIZE_MAX   100

INCLUDES ///.

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

FileName [lpkInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
lpkInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 47 of file lpkInt.h.

◆ Lpk_SuppForEachVar

#define Lpk_SuppForEachVar ( Supp,
Var )
Value:
for ( Var = 0; Var < 16; Var++ )\
if ( !(Supp & (1<<Var)) ) {} else
int Var
Definition exorList.c:228

Definition at line 196 of file lpkInt.h.

196#define Lpk_SuppForEachVar( Supp, Var )\
197 for ( Var = 0; Var < 16; Var++ )\
198 if ( !(Supp & (1<<Var)) ) {} else

Typedef Documentation

◆ Lpk_Cut_t

typedef struct Lpk_Cut_t_ Lpk_Cut_t

Definition at line 51 of file lpkInt.h.

◆ Lpk_Fun_t

typedef struct Lpk_Fun_t_ Lpk_Fun_t

Definition at line 144 of file lpkInt.h.

◆ Lpk_Man_t

typedef struct Lpk_Man_t_ Lpk_Man_t

Definition at line 50 of file lpkInt.h.

◆ Lpk_Res_t

typedef struct Lpk_Res_t_ Lpk_Res_t

Definition at line 163 of file lpkInt.h.

Function Documentation

◆ Lpk_CutTruth()

unsigned * Lpk_CutTruth ( Lpk_Man_t * p,
Lpk_Cut_t * pCut,
int fInv )
extern

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

Synopsis [Computes the truth able of one cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file lpkCut.c.

176{
177 Hop_Man_t * pManHop = (Hop_Man_t *)p->pNtk->pManFunc;
178 Hop_Obj_t * pObjHop;
179 Abc_Obj_t * pObj = NULL; // Suppress "might be used uninitialized"
180 Abc_Obj_t * pFanin;
181 unsigned * pTruth = NULL; // Suppress "might be used uninitialized"
182 int i, k, iCount = 0;
183// Lpk_NodePrintCut( p, pCut );
184 assert( pCut->nNodes > 0 );
185
186 // initialize the leaves
187 Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
188 pObj->pCopy = (Abc_Obj_t *)Vec_PtrEntry( p->vTtElems, fInv? pCut->nLeaves-1-i : i );
189
190 // construct truth table in the topological order
191 Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
192 {
193 // get the local AIG
194 pObjHop = Hop_Regular((Hop_Obj_t *)pObj->pData);
195 // clean the data field of the nodes in the AIG subgraph
196 Hop_ObjCleanData_rec( pObjHop );
197 // set the initial truth tables at the fanins
198 Abc_ObjForEachFanin( pObj, pFanin, k )
199 {
200 assert( ((unsigned)(ABC_PTRUINT_T)pFanin->pCopy) & 0xffff0000 );
201 Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
202 }
203 // compute the truth table of internal nodes
204 pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
205 if ( Hop_IsComplement((Hop_Obj_t *)pObj->pData) )
206 Kit_TruthNot( pTruth, pTruth, pCut->nLeaves );
207 // set the truth table at the node
208 pObj->pCopy = (Abc_Obj_t *)pTruth;
209 }
210
211 // make sure direct truth table is stored elsewhere (assuming the first call for direct truth!!!)
212 if ( fInv == 0 )
213 {
214 pTruth = (unsigned *)Vec_PtrEntry( p->vTtNodes, iCount++ );
215 Kit_TruthCopy( pTruth, (unsigned *)(ABC_PTRUINT_T)pObj->pCopy, pCut->nLeaves );
216 }
217 assert( iCount <= Vec_PtrSize(p->vTtNodes) );
218 return pTruth;
219}
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition abc.h:527
Cube * p
Definition exorList.c:222
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
void Hop_ObjCleanData_rec(Hop_Obj_t *pObj)
Definition hopUtil.c:88
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
unsigned * Lpk_CutTruth_rec(Hop_Man_t *pMan, Hop_Obj_t *pObj, int nVars, Vec_Ptr_t *vTtNodes, int *piCount)
Definition lpkCut.c:138
#define Lpk_CutForEachNodeReverse(pNtk, pCut, pObj, i)
Definition lpkInt.h:194
#define Lpk_CutForEachLeaf(pNtk, pCut, pObj, i)
MACRO DEFINITIONS ///.
Definition lpkInt.h:190
void * pData
Definition abc.h:145
Abc_Obj_t * pCopy
Definition abc.h:148
unsigned nNodes
Definition lpkInt.h:56
unsigned nLeaves
Definition lpkInt.h:55
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_Decompose()

Abc_Obj_t * Lpk_Decompose ( Lpk_Man_t * p,
Abc_Ntk_t * pNtk,
Vec_Ptr_t * vLeaves,
unsigned * pTruth,
unsigned * puSupps,
int nLutK,
int AreaLim,
int DelayLim )
extern

FUNCTION DECLARATIONS ///.

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

Synopsis [Decomposes the function using recursive MUX decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 258 of file lpkAbcDec.c.

259{
260 Lpk_Fun_t * pFun;
261 Abc_Obj_t * pObjNew = NULL;
262 int nLeaves = Vec_PtrSize( vLeaves );
263 pFun = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
264 if ( puSupps[0] || puSupps[1] )
265 {
266/*
267 int i;
268 Lpk_FunComputeCofSupps( pFun );
269 for ( i = 0; i < nLeaves; i++ )
270 {
271 assert( pFun->puSupps[2*i+0] == puSupps[2*i+0] );
272 assert( pFun->puSupps[2*i+1] == puSupps[2*i+1] );
273 }
274*/
275 memcpy( pFun->puSupps, puSupps, sizeof(unsigned) * 2 * nLeaves );
276 pFun->fSupports = 1;
277 }
278 Lpk_FunSuppMinimize( pFun );
279 if ( pFun->nVars <= pFun->nLutK )
280 pObjNew = Lpk_ImplementFun( p, pNtk, vLeaves, pFun );
281 else if ( Lpk_Decompose_rec(p, pFun) )
282 pObjNew = Lpk_Implement( p, pNtk, vLeaves, nLeaves );
283 Lpk_DecomposeClean( vLeaves, nLeaves );
284 return pObjNew;
285}
ABC_NAMESPACE_IMPL_START Abc_Obj_t * Lpk_ImplementFun(Lpk_Man_t *pMan, Abc_Ntk_t *pNtk, Vec_Ptr_t *vLeaves, Lpk_Fun_t *p)
DECLARATIONS ///.
Definition lpkAbcDec.c:45
int Lpk_Decompose_rec(Lpk_Man_t *pMan, Lpk_Fun_t *p)
Definition lpkAbcDec.c:147
void Lpk_DecomposeClean(Vec_Ptr_t *vLeaves, int nLeavesOld)
Definition lpkAbcDec.c:238
Abc_Obj_t * Lpk_Implement(Lpk_Man_t *pMan, Abc_Ntk_t *pNtk, Vec_Ptr_t *vLeaves, int nLeavesOld)
Definition lpkAbcDec.c:120
int Lpk_FunSuppMinimize(Lpk_Fun_t *p)
Definition lpkAbcUtil.c:143
Lpk_Fun_t * Lpk_FunCreate(Abc_Ntk_t *pNtk, Vec_Ptr_t *vLeaves, unsigned *pTruth, int nLutK, int AreaLim, int DelayLim)
Definition lpkAbcUtil.c:80
struct Lpk_Fun_t_ Lpk_Fun_t
Definition lpkInt.h:144
unsigned nLutK
Definition lpkInt.h:150
unsigned nVars
Definition lpkInt.h:149
unsigned fSupports
Definition lpkInt.h:152
unsigned puSupps[32]
Definition lpkInt.h:155
char * memcpy()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_DsdAnalize()

Lpk_Res_t * Lpk_DsdAnalize ( Lpk_Man_t * pMan,
Lpk_Fun_t * p,
int nShared )
extern

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

Synopsis [Performs DSD-based decomposition of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file lpkAbcDsd.c.

453{
454 static Lpk_Res_t Res0, * pRes0 = &Res0;
455 static Lpk_Res_t Res1, * pRes1 = &Res1;
456 static Lpk_Res_t Res2, * pRes2 = &Res2;
457 static Lpk_Res_t Res3, * pRes3 = &Res3;
458 int fUseBackLooking = 1;
459 Lpk_Res_t * pRes = NULL;
460 Vec_Int_t * vBSets;
461 Kit_DsdNtk_t * pNtks[8] = {NULL};
462 char pCofVars[5];
463 int i;
464
465 assert( p->nLutK >= 3 );
466 assert( nShared >= 0 && nShared <= 3 );
467 assert( p->uSupp == Kit_BitMask(p->nVars) );
468
469 // try decomposition without cofactoring
470 pNtks[0] = Kit_DsdDecomposeExpand( Lpk_FunTruth( p, 0 ), p->nVars );
471 if ( pMan->pPars->fVerbose )
472 pMan->nBlocks[ Kit_DsdNonDsdSizeMax(pNtks[0]) ]++;
473 vBSets = Lpk_ComputeBoundSets( pNtks[0], p->nLutK );
474 Lpk_FunCompareBoundSets( p, vBSets, 0, 0xFFFF, Lpk_DsdLateArriving(p), pRes0 );
475 Vec_IntFree( vBSets );
476
477 // check the result
478 if ( pRes0->nBSVars == (int)p->nLutK )
479 { pRes = pRes0; goto finish; }
480 if ( pRes0->nBSVars == (int)p->nLutK - 1 )
481 { pRes = pRes0; goto finish; }
482 if ( nShared == 0 )
483 goto finish;
484
485 // prepare storage
486 Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth( p, 0 ), p->nVars );
487
488 // cofactor 1 time
489 if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 1, pRes1 ) )
490 goto finish;
491 assert( pRes1->nBSVars <= (int)p->nLutK - 1 );
492 if ( pRes1->nBSVars == (int)p->nLutK - 1 )
493 { pRes = pRes1; goto finish; }
494 if ( pRes0->nBSVars == (int)p->nLutK - 2 )
495 { pRes = pRes0; goto finish; }
496 if ( pRes1->nBSVars == (int)p->nLutK - 2 )
497 { pRes = pRes1; goto finish; }
498 if ( nShared == 1 )
499 goto finish;
500
501 // cofactor 2 times
502 if ( p->nLutK >= 4 )
503 {
504 if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 2, pRes2 ) )
505 goto finish;
506 assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
507 if ( pRes2->nBSVars == (int)p->nLutK - 2 )
508 { pRes = pRes2; goto finish; }
509 if ( fUseBackLooking )
510 {
511 if ( pRes0->nBSVars == (int)p->nLutK - 3 )
512 { pRes = pRes0; goto finish; }
513 if ( pRes1->nBSVars == (int)p->nLutK - 3 )
514 { pRes = pRes1; goto finish; }
515 }
516 if ( pRes2->nBSVars == (int)p->nLutK - 3 )
517 { pRes = pRes2; goto finish; }
518 if ( nShared == 2 )
519 goto finish;
520 assert( nShared == 3 );
521 }
522
523 // cofactor 3 times
524 if ( p->nLutK >= 5 )
525 {
526 if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 3, pRes3 ) )
527 goto finish;
528 assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
529 if ( pRes3->nBSVars == (int)p->nLutK - 3 )
530 { pRes = pRes3; goto finish; }
531 if ( fUseBackLooking )
532 {
533 if ( pRes0->nBSVars == (int)p->nLutK - 4 )
534 { pRes = pRes0; goto finish; }
535 if ( pRes1->nBSVars == (int)p->nLutK - 4 )
536 { pRes = pRes1; goto finish; }
537 if ( pRes2->nBSVars == (int)p->nLutK - 4 )
538 { pRes = pRes2; goto finish; }
539 }
540 if ( pRes3->nBSVars == (int)p->nLutK - 4 )
541 { pRes = pRes3; goto finish; }
542 }
543
544finish:
545 // free the networks
546 for ( i = 0; i < (1<<nShared); i++ )
547 if ( pNtks[i] )
548 Kit_DsdNtkFree( pNtks[i] );
549 // choose the best under these conditions
550 return pRes;
551}
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
int Kit_DsdNonDsdSizeMax(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:1212
Kit_DsdNtk_t * Kit_DsdDecomposeExpand(unsigned *pTruth, int nVars)
Definition kitDsd.c:2331
void Kit_DsdNtkFree(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:164
struct Kit_DsdNtk_t_ Kit_DsdNtk_t
Definition kit.h:124
Vec_Int_t * Lpk_ComputeBoundSets(Kit_DsdNtk_t *p, int nSizeMax)
Definition lpkAbcDsd.c:162
unsigned Lpk_DsdLateArriving(Lpk_Fun_t *p)
Definition lpkAbcDsd.c:352
int Lpk_DsdAnalizeOne(Lpk_Fun_t *p, unsigned *ppTruths[5][16], Kit_DsdNtk_t *pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t *pRes)
Definition lpkAbcDsd.c:372
void Lpk_FunCompareBoundSets(Lpk_Fun_t *p, Vec_Int_t *vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t *pRes)
Definition lpkAbcDsd.c:276
struct Lpk_Res_t_ Lpk_Res_t
Definition lpkInt.h:163
unsigned * ppTruths[5][16]
Definition lpkInt.h:104
int nBlocks[17]
Definition lpkInt.h:123
Lpk_Par_t * pPars
Definition lpkInt.h:72
int nBSVars
Definition lpkInt.h:166
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_DsdSplit()

Lpk_Fun_t * Lpk_DsdSplit ( Lpk_Man_t * pMan,
Lpk_Fun_t * p,
char * pCofVars,
int nCofVars,
unsigned uBoundSet )
extern

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

Synopsis [Splits the function into two subfunctions using DSD.]

Description []

SideEffects []

SeeAlso []

Definition at line 564 of file lpkAbcDsd.c.

565{
566 Lpk_Fun_t * pNew;
567 Kit_DsdNtk_t * pNtkDec;
568 int i, k, iVacVar, nCofs;
569 // prepare storage
570 Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth(p, 0), p->nVars );
571 // get the vacuous variable
572 iVacVar = Kit_WordFindFirstBit( uBoundSet );
573 // compute the cofactors
574 for ( i = 0; i < nCofVars; i++ )
575 for ( k = 0; k < (1<<i); k++ )
576 {
577 Kit_TruthCofactor0New( pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
578 Kit_TruthCofactor1New( pMan->ppTruths[i+1][2*k+1], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
579 }
580 // decompose each cofactor w.r.t. the bound set
581 nCofs = (1<<nCofVars);
582 for ( k = 0; k < nCofs; k++ )
583 {
584 pNtkDec = Kit_DsdDecomposeExpand( pMan->ppTruths[nCofVars][k], p->nVars );
585 Kit_DsdTruthPartialTwo( pMan->pDsdMan, pNtkDec, uBoundSet, iVacVar, pMan->ppTruths[nCofVars+1][k], pMan->ppTruths[nCofVars+1][nCofs+k] );
586 Kit_DsdNtkFree( pNtkDec );
587 }
588 // compute the composition/decomposition functions (they will be in pMan->ppTruths[1][0]/pMan->ppTruths[1][1])
589 for ( i = nCofVars; i >= 1; i-- )
590 for ( k = 0; k < (1<<i); k++ )
591 Kit_TruthMuxVar( pMan->ppTruths[i][k], pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i+1][2*k+1], p->nVars, pCofVars[i-1] );
592
593 // derive the new component (decomposition function)
594 pNew = Lpk_FunDup( p, pMan->ppTruths[1][1] );
595 // update the old component (composition function)
596 Kit_TruthCopy( Lpk_FunTruth(p, 0), pMan->ppTruths[1][0], p->nVars );
597 p->uSupp = Kit_TruthSupport( Lpk_FunTruth(p, 0), p->nVars );
598 p->pFanins[iVacVar] = pNew->Id;
599 p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
600 // support minimize both
601 p->fSupports = 0;
603 Lpk_FunSuppMinimize( pNew );
604 // update delay and area requirements
605 pNew->nDelayLim = p->pDelays[iVacVar];
606 pNew->nAreaLim = 1;
607 p->nAreaLim = p->nAreaLim - 1;
608 return pNew;
609}
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition kitTruth.c:346
void Kit_TruthMuxVar(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition kitTruth.c:1069
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_DsdTruthPartialTwo(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthCo, unsigned *pTruthDec)
Definition kitDsd.c:1090
Lpk_Fun_t * Lpk_FunDup(Lpk_Fun_t *p, unsigned *pTruth)
Definition lpkAbcUtil.c:114
int Lpk_SuppDelay(unsigned uSupp, int *pDelays)
Definition lpkAbcUtil.c:215
int pDelays[16]
Definition lpkInt.h:157
unsigned nAreaLim
Definition lpkInt.h:151
unsigned nDelayLim
Definition lpkInt.h:156
unsigned uSupp
Definition lpkInt.h:154
unsigned Id
Definition lpkInt.h:148
Kit_DsdMan_t * pDsdMan
Definition lpkInt.h:107
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_FunAlloc()

Lpk_Fun_t * Lpk_FunAlloc ( int nVars)
extern

DECLARATIONS ///.

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

FileName [lpkAbcUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis [Procedures working on decomposed functions.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Allocates the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file lpkAbcUtil.c.

46{
47 Lpk_Fun_t * p;
48 p = (Lpk_Fun_t *)ABC_ALLOC( char, sizeof(Lpk_Fun_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars) * 3 );
49 memset( p, 0, sizeof(Lpk_Fun_t) );
50 return p;
51}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_FunComputeCofSupps()

void Lpk_FunComputeCofSupps ( Lpk_Fun_t * p)
extern

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

Synopsis [Computes cofactors w.r.t. each variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file lpkAbcUtil.c.

187{
188 unsigned * pTruth = Lpk_FunTruth( p, 0 );
189 unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
190 unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
191 int Var;
192 assert( p->fSupports == 0 );
193// Lpk_SuppForEachVar( p->uSupp, Var )
194 for ( Var = 0; Var < (int)p->nVars; Var++ )
195 {
196 Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var );
197 Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var );
198 p->puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars );
199 p->puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars );
200 }
201 p->fSupports = 1;
202}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_FunCreate()

Lpk_Fun_t * Lpk_FunCreate ( Abc_Ntk_t * pNtk,
Vec_Ptr_t * vLeaves,
unsigned * pTruth,
int nLutK,
int AreaLim,
int DelayLim )
extern

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

Synopsis [Creates the starting function.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file lpkAbcUtil.c.

81{
82 Lpk_Fun_t * p;
83 Abc_Obj_t * pNode;
84 int i;
85 p = Lpk_FunAlloc( Vec_PtrSize(vLeaves) );
86 p->Id = Vec_PtrSize(vLeaves);
87 p->vNodes = vLeaves;
88 p->nVars = Vec_PtrSize(vLeaves);
89 p->nLutK = nLutK;
90 p->nAreaLim = AreaLim;
91 p->nDelayLim = DelayLim;
92 p->uSupp = Kit_TruthSupport( pTruth, p->nVars );
93 Kit_TruthCopy( Lpk_FunTruth(p,0), pTruth, p->nVars );
94 Vec_PtrForEachEntry( Abc_Obj_t *, vLeaves, pNode, i )
95 {
96 p->pFanins[i] = i;
97 p->pDelays[i] = pNode->Level;
98 }
99 Vec_PtrPush( p->vNodes, p );
100 return p;
101}
ABC_NAMESPACE_IMPL_START Lpk_Fun_t * Lpk_FunAlloc(int nVars)
DECLARATIONS ///.
Definition lpkAbcUtil.c:45
unsigned Level
Definition abc.h:142
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_FunDup()

Lpk_Fun_t * Lpk_FunDup ( Lpk_Fun_t * p,
unsigned * pTruth )
extern

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

Synopsis [Creates the new function with the given truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file lpkAbcUtil.c.

115{
116 Lpk_Fun_t * pNew;
117 pNew = Lpk_FunAlloc( p->nVars );
118 pNew->Id = Vec_PtrSize(p->vNodes);
119 pNew->vNodes = p->vNodes;
120 pNew->nVars = p->nVars;
121 pNew->nLutK = p->nLutK;
122 pNew->nAreaLim = p->nAreaLim;
123 pNew->nDelayLim = p->nDelayLim;
124 pNew->uSupp = Kit_TruthSupport( pTruth, p->nVars );
125 Kit_TruthCopy( Lpk_FunTruth(pNew,0), pTruth, p->nVars );
126 memcpy( pNew->pFanins, p->pFanins, 16 );
127 memcpy( pNew->pDelays, p->pDelays, sizeof(int)*16 );
128 Vec_PtrPush( p->vNodes, pNew );
129 return pNew;
130}
char pFanins[16]
Definition lpkInt.h:158
Vec_Ptr_t * vNodes
Definition lpkInt.h:147
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_FunFree()

void Lpk_FunFree ( Lpk_Fun_t * p)
extern

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

Synopsis [Deletes the function]

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file lpkAbcUtil.c.

65{
66 ABC_FREE( p );
67}
#define ABC_FREE(obj)
Definition abc_global.h:267
Here is the caller graph for this function:

◆ Lpk_FunSuppMinimize()

int Lpk_FunSuppMinimize ( Lpk_Fun_t * p)
extern

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

Synopsis [Minimizes support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file lpkAbcUtil.c.

144{
145 int i, k, nVarsNew;
146 // compress the truth table
147 if ( p->uSupp == Kit_BitMask(p->nVars) )
148 return 0;
149 // invalidate support info
150 p->fSupports = 0;
151//Extra_PrintBinary( stdout, &p->uSupp, p->nVars ); printf( "\n" );
152 // minimize support
153 nVarsNew = Kit_WordCountOnes(p->uSupp);
154 Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 );
155 k = 0;
156 Lpk_SuppForEachVar( p->uSupp, i )
157 {
158 p->pFanins[k] = p->pFanins[i];
159 p->pDelays[k] = p->pDelays[i];
160/*
161 if ( p->fSupports )
162 {
163 p->puSupps[2*k+0] = p->puSupps[2*i+0];
164 p->puSupps[2*k+1] = p->puSupps[2*i+1];
165 }
166*/
167 k++;
168 }
169 assert( k == nVarsNew );
170 p->nVars = k;
171 p->uSupp = Kit_BitMask(p->nVars);
172 return 1;
173}
void Kit_TruthShrink(unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
Definition kitTruth.c:200
#define Lpk_SuppForEachVar(Supp, Var)
Definition lpkInt.h:196
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_ManStart()

Lpk_Man_t * Lpk_ManStart ( Lpk_Par_t * pPars)
extern

DECLARATIONS ///.

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

FileName [lpkMan.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
lpkMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file lpkMan.c.

46{
47 Lpk_Man_t * p;
48 int i, nWords;
49 assert( pPars->nLutsMax <= 16 );
50 assert( pPars->nVarsMax > 0 && pPars->nVarsMax <= 16 );
51 p = ABC_ALLOC( Lpk_Man_t, 1 );
52 memset( p, 0, sizeof(Lpk_Man_t) );
53 p->pPars = pPars;
54 p->nCutsMax = LPK_CUTS_MAX;
55 p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
56 p->vTtNodes = Vec_PtrAllocSimInfo( 1024, Abc_TruthWordNum(pPars->nVarsMax) );
57 p->vCover = Vec_IntAlloc( 1 << 12 );
58 p->vLeaves = Vec_PtrAlloc( 32 );
59 p->vTemp = Vec_PtrAlloc( 32 );
60 for ( i = 0; i < 8; i++ )
61 p->vSets[i] = Vec_IntAlloc(100);
62 p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 );
63 p->vMemory = Vec_IntAlloc( 1024 * 32 );
64 p->vBddDir = Vec_IntAlloc( 256 );
65 p->vBddInv = Vec_IntAlloc( 256 );
66 // allocate temporary storage for truth tables
67 nWords = Kit_TruthWordNum(pPars->nVarsMax);
68 p->ppTruths[0][0] = ABC_ALLOC( unsigned, 32 * nWords );
69 p->ppTruths[1][0] = p->ppTruths[0][0] + 1 * nWords;
70 for ( i = 1; i < 2; i++ )
71 p->ppTruths[1][i] = p->ppTruths[1][0] + i * nWords;
72 p->ppTruths[2][0] = p->ppTruths[1][0] + 2 * nWords;
73 for ( i = 1; i < 4; i++ )
74 p->ppTruths[2][i] = p->ppTruths[2][0] + i * nWords;
75 p->ppTruths[3][0] = p->ppTruths[2][0] + 4 * nWords;
76 for ( i = 1; i < 8; i++ )
77 p->ppTruths[3][i] = p->ppTruths[3][0] + i * nWords;
78 p->ppTruths[4][0] = p->ppTruths[3][0] + 8 * nWords;
79 for ( i = 1; i < 16; i++ )
80 p->ppTruths[4][i] = p->ppTruths[4][0] + i * nWords;
81 return p;
82}
int nWords
Definition abcNpn.c:127
Kit_DsdMan_t * Kit_DsdManAlloc(int nVars, int nNodes)
DECLARATIONS ///.
Definition kitDsd.c:46
#define LPK_CUTS_MAX
Definition lpkInt.h:48
struct Lpk_Man_t_ Lpk_Man_t
Definition lpkInt.h:50
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_ManStop()

void Lpk_ManStop ( Lpk_Man_t * p)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file lpkMan.c.

96{
97 int i;
98 ABC_FREE( p->ppTruths[0][0] );
99 Vec_IntFree( p->vBddDir );
100 Vec_IntFree( p->vBddInv );
101 Vec_IntFree( p->vMemory );
102 Kit_DsdManFree( p->pDsdMan );
103 for ( i = 0; i < 8; i++ )
104 Vec_IntFree(p->vSets[i]);
105 if ( p->pIfMan )
106 {
107 void * pPars = p->pIfMan->pPars;
108 If_ManStop( p->pIfMan );
109 ABC_FREE( pPars );
110 }
111 if ( p->vLevels )
112 Vec_VecFree( p->vLevels );
113 if ( p->vVisited )
114 Vec_VecFree( p->vVisited );
115 Vec_PtrFree( p->vLeaves );
116 Vec_PtrFree( p->vTemp );
117 Vec_IntFree( p->vCover );
118 Vec_PtrFree( p->vTtElems );
119 Vec_PtrFree( p->vTtNodes );
120 ABC_FREE( p );
121}
void If_ManStop(If_Man_t *p)
Definition ifMan.c:212
void Kit_DsdManFree(Kit_DsdMan_t *p)
Definition kitDsd.c:72
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_MapPrime()

If_Obj_t * Lpk_MapPrime ( Lpk_Man_t * p,
unsigned * pTruth,
int nVars,
If_Obj_t ** ppLeaves )
extern

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

Synopsis [Strashes one logic node using its SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file lpkMap.c.

80{
81 Kit_Graph_t * pGraph;
82 Kit_Node_t * pNode;
83 If_Obj_t * pRes;
84 int i;
85 // derive the factored form
86 pGraph = Kit_TruthToGraph( pTruth, nVars, p->vCover );
87 if ( pGraph == NULL )
88 return NULL;
89 // collect the fanins
90 Kit_GraphForEachLeaf( pGraph, pNode, i )
91 pNode->pFunc = ppLeaves[i];
92 // perform strashing
93 pRes = Lpk_MapPrimeInternal( p->pIfMan, pGraph );
94 pRes = If_NotCond( pRes, Kit_GraphIsComplement(pGraph) );
95 Kit_GraphFree( pGraph );
96 return pRes;
97}
struct If_Obj_t_ If_Obj_t
Definition if.h:79
struct Kit_Graph_t_ Kit_Graph_t
Definition kit.h:88
struct Kit_Node_t_ Kit_Node_t
Definition kit.h:69
void Kit_GraphFree(Kit_Graph_t *pGraph)
Definition kitGraph.c:132
#define Kit_GraphForEachLeaf(pGraph, pLeaf, i)
Definition kit.h:505
Kit_Graph_t * Kit_TruthToGraph(unsigned *pTruth, int nVars, Vec_Int_t *vMemory)
Definition kitGraph.c:356
ABC_NAMESPACE_IMPL_START If_Obj_t * Lpk_MapPrimeInternal(If_Man_t *pIfMan, Kit_Graph_t *pGraph)
DECLARATIONS ///.
Definition lpkMap.c:45
void * pFunc
Definition kit.h:76
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_MapSuppRedDec_rec()

If_Obj_t * Lpk_MapSuppRedDec_rec ( Lpk_Man_t * p,
unsigned * pTruth,
int nVars,
If_Obj_t ** ppLeaves )
extern

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

Synopsis [Implements support-reducing decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file lpkMux.c.

134{
135 Kit_DsdNtk_t * pNtkDec, * pNtkComp, * ppNtks[2], * pTemp;
136 If_Obj_t * pObjNew;
137 unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 );
138 unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 );
139 unsigned * pDec0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 2 );
140 unsigned * pDec1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 3 );
141 unsigned * pDec = (unsigned *)Vec_PtrEntry( p->vTtNodes, 4 );
142 unsigned * pCo00 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 5 );
143 unsigned * pCo01 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 6 );
144 unsigned * pCo10 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 7 );
145 unsigned * pCo11 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 8 );
146 unsigned * pCo0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 9 );
147 unsigned * pCo1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 10 );
148 unsigned * pCo = (unsigned *)Vec_PtrEntry( p->vTtNodes, 11 );
149 int TrueMint0, TrueMint1, FalseMint0, FalseMint1;
150 int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
151
152 // determine if supp-red decomposition exists
153 uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
154 if ( uSubsets == 0 )
155 return NULL;
156 p->nCalledSRed++;
157
158 // get the cofactors
159 Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
160 Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
161
162 // get the bound sets
163 uSubset0 = uSubsets & 0xFFFF;
164 uSubset1 = uSubsets >> 16;
165
166 // compute the decomposed functions
167 ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
168 ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
169 ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
170 ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
171 Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 );
172 Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 );
173// Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[0], uSubset0, iVarReused, pCo0, pDec0 );
174// Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[1], uSubset1, iVarReused, pCo1, pDec1 );
175 Kit_DsdNtkFree( ppNtks[0] );
176 Kit_DsdNtkFree( ppNtks[1] );
177//Kit_DsdPrintFromTruth( pDec0, nVars );
178//Kit_DsdPrintFromTruth( pDec1, nVars );
179 // get the decomposed function
180 Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
181
182 // find any true assignments of the decomposed functions
183 TrueMint0 = Kit_TruthFindFirstBit( pDec0, nVars );
184 TrueMint1 = Kit_TruthFindFirstBit( pDec1, nVars );
185 assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
186 // find any false assignments of the decomposed functions
187 FalseMint0 = Kit_TruthFindFirstZero( pDec0, nVars );
188 FalseMint1 = Kit_TruthFindFirstZero( pDec1, nVars );
189 assert( FalseMint0 >= 0 && FalseMint1 >= 0 );
190
191 // cofactor the cofactors according to these minterms
192 Kit_TruthCopy( pCo00, pCof0, nVars );
193 Kit_TruthCopy( pCo01, pCof0, nVars );
194 for ( i = 0; i < nVars; i++ )
195 if ( uSubset0 & (1 << i) )
196 {
197 if ( FalseMint0 & (1 << i) )
198 Kit_TruthCofactor1( pCo00, nVars, i );
199 else
200 Kit_TruthCofactor0( pCo00, nVars, i );
201 if ( TrueMint0 & (1 << i) )
202 Kit_TruthCofactor1( pCo01, nVars, i );
203 else
204 Kit_TruthCofactor0( pCo01, nVars, i );
205 }
206 Kit_TruthCopy( pCo10, pCof1, nVars );
207 Kit_TruthCopy( pCo11, pCof1, nVars );
208 for ( i = 0; i < nVars; i++ )
209 if ( uSubset1 & (1 << i) )
210 {
211 if ( FalseMint1 & (1 << i) )
212 Kit_TruthCofactor1( pCo10, nVars, i );
213 else
214 Kit_TruthCofactor0( pCo10, nVars, i );
215 if ( TrueMint1 & (1 << i) )
216 Kit_TruthCofactor1( pCo11, nVars, i );
217 else
218 Kit_TruthCofactor0( pCo11, nVars, i );
219 }
220
221 // derive the functions by composing them with the new variable (iVarReused)
222 Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
223 Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
224//Kit_DsdPrintFromTruth( pCo0, nVars );
225//Kit_DsdPrintFromTruth( pCo1, nVars );
226
227 // derive the composition function
228 Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
229
230 // process the decomposed function
231 pNtkDec = Kit_DsdDecompose( pDec, nVars );
232 pNtkComp = Kit_DsdDecompose( pCo, nVars );
233//Kit_DsdPrint( stdout, pNtkDec );
234//Kit_DsdPrint( stdout, pNtkComp );
235//printf( "cofactored variable %c\n", 'a' + iVar );
236//printf( "reused variable %c\n", 'a' + iVarReused );
237
238 ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
239 pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
240
241 Kit_DsdNtkFree( pNtkDec );
242 Kit_DsdNtkFree( pNtkComp );
243 return pObjNew;
244}
Kit_DsdNtk_t * Kit_DsdDecompose(unsigned *pTruth, int nVars)
Definition kitDsd.c:2315
void Kit_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:368
void Kit_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:470
Kit_DsdNtk_t * Kit_DsdExpand(Kit_DsdNtk_t *p)
Definition kitDsd.c:1452
void Kit_DsdTruthPartial(Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned *pTruthRes, unsigned uSupp)
Definition kitDsd.c:1108
unsigned Lpk_MapSuppRedDecSelect(Lpk_Man_t *p, unsigned *pTruth, int nVars, int *piVar, int *piVarReused)
Definition lpkSets.c:323
If_Obj_t * Lpk_MapTree_rec(Lpk_Man_t *p, Kit_DsdNtk_t *pNtk, If_Obj_t **ppLeaves, int iLit, If_Obj_t *pResult)
Definition lpkMap.c:110
unsigned short Root
Definition kit.h:130
Here is the call graph for this function:
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 )
extern

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}
void Kit_DsdPrint(FILE *pFile, Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:375
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
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
typedefABC_NAMESPACE_IMPL_START struct Lpk_Set_t_ Lpk_Set_t
DECLARATIONS ///.
Definition lpkSets.c:30
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:

◆ Lpk_MapTree_rec()

If_Obj_t * Lpk_MapTree_rec ( Lpk_Man_t * p,
Kit_DsdNtk_t * pNtk,
If_Obj_t ** ppLeaves,
int iLit,
If_Obj_t * pResult )
extern

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

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file lpkMap.c.

111{
112 Kit_DsdObj_t * pObj;
113 If_Obj_t * pObjNew = NULL, * pObjNew2 = NULL, * pFansNew[16];
114 unsigned i, iLitFanin;
115
116 assert( iLit >= 0 );
117
118 // consider the case of a gate
119 pObj = Kit_DsdNtkObj( pNtk, Abc_Lit2Var(iLit) );
120 if ( pObj == NULL )
121 {
122 pObjNew = ppLeaves[Abc_Lit2Var(iLit)];
123 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
124 }
125 if ( pObj->Type == KIT_DSD_CONST1 )
126 {
127 return If_NotCond( If_ManConst1(p->pIfMan), Abc_LitIsCompl(iLit) );
128 }
129 if ( pObj->Type == KIT_DSD_VAR )
130 {
131 pObjNew = ppLeaves[Abc_Lit2Var(pObj->pFans[0])];
132 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) ^ Abc_LitIsCompl(pObj->pFans[0]) );
133 }
134 if ( pObj->Type == KIT_DSD_AND )
135 {
136 assert( pObj->nFans == 2 );
137 pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
138 pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
139 if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
140 return NULL;
141 pObjNew = If_ManCreateAnd( p->pIfMan, pFansNew[0], pFansNew[1] );
142 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
143 }
144 if ( pObj->Type == KIT_DSD_XOR )
145 {
146 int fCompl = Abc_LitIsCompl(iLit);
147 assert( pObj->nFans == 2 );
148 pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
149 pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
150 if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
151 return NULL;
152 fCompl ^= If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
153 pObjNew = If_ManCreateXor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) );
154 return If_NotCond( pObjNew, fCompl );
155 }
156 assert( pObj->Type == KIT_DSD_PRIME );
157 p->nBlocks[pObj->nFans]++;
158
159 // solve for the inputs
160 Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
161 {
162 if ( i == 0 )
163 pFansNew[i] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
164 else
165 pFansNew[i] = Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
166 if ( pFansNew[i] == NULL )
167 return NULL;
168 }
169/*
170 if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
171 {
172 pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
173 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
174 }
175*/
176/*
177 if ( (int)pObj->nFans > p->pPars->nLutSize )
178 {
179 pObjNew2 = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
180// if ( pObjNew2 )
181// return If_NotCond( pObjNew2, Abc_LitIsCompl(iLit) );
182 }
183*/
184
185 // find best cofactoring variable
186 if ( p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
187 {
188 pObjNew2 = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
189 if ( pObjNew2 )
190 return If_NotCond( pObjNew2, Abc_LitIsCompl(iLit) );
191 }
192
193 pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
194
195 // add choice
196 if ( pObjNew && pObjNew2 )
197 {
198 If_ObjSetChoice( If_Regular(pObjNew), If_Regular(pObjNew2) );
199 If_ManCreateChoice( p->pIfMan, If_Regular(pObjNew) );
200 }
201 return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
202}
void If_ManCreateChoice(If_Man_t *p, If_Obj_t *pRepr)
Definition ifMan.c:460
If_Obj_t * If_ManCreateXor(If_Man_t *p, If_Obj_t *pFan0, If_Obj_t *pFan1)
Definition ifMan.c:422
If_Obj_t * If_ManCreateAnd(If_Man_t *p, If_Obj_t *pFan0, If_Obj_t *pFan1)
Definition ifMan.c:384
@ KIT_DSD_XOR
Definition kit.h:106
@ KIT_DSD_CONST1
Definition kit.h:103
@ KIT_DSD_PRIME
Definition kit.h:107
@ KIT_DSD_AND
Definition kit.h:105
@ KIT_DSD_VAR
Definition kit.h:104
struct Kit_DsdObj_t_ Kit_DsdObj_t
Definition kit.h:111
#define Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
Definition kit.h:160
If_Obj_t * Lpk_MapSuppRedDec_rec(Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
Definition lpkMux.c:133
If_Obj_t * Lpk_MapPrime(Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
Definition lpkMap.c:79
If_Obj_t * Lpk_MapTree_rec(Lpk_Man_t *p, Kit_DsdNtk_t *pNtk, If_Obj_t **ppLeaves, int iLit, If_Obj_t *pResult)
Definition lpkMap.c:110
unsigned Type
Definition kit.h:115
unsigned nFans
Definition kit.h:119
unsigned short pFans[0]
Definition kit.h:120
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_MapTreeMulti()

If_Obj_t * Lpk_MapTreeMulti ( Lpk_Man_t * p,
unsigned * pTruth,
int nVars,
If_Obj_t ** ppLeaves )
extern

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

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 347 of file lpkMulti.c.

348{
349 static int Counter = 0;
350 If_Obj_t * pResult;
351 Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
352 Kit_DsdObj_t * pRoot;
353 int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16];
354 int i, k, nCBars, nSize, nMemSize;
355 unsigned * ppCofs[4][8], uSupport;
356 char pTable[16][16] = {
357 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
358 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
359 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
360 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
361 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
362 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
363 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
364 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
365 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
366 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
367 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
368 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
369 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
370 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
371 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
372 {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
373 };
374 int fVerbose = p->pPars->fVeryVerbose;
375
376 Counter++;
377// printf( "Run %d.\n", Counter );
378
379 // allocate storage for cofactors
380 nMemSize = Kit_TruthWordNum(nVars);
381 ppCofs[0][0] = ABC_ALLOC( unsigned, 32 * nMemSize );
382 nSize = 0;
383 for ( i = 0; i < 4; i++ )
384 for ( k = 0; k < 8; k++ )
385 ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
386 assert( nSize == 32 );
387
388 // find the best cofactoring variables
389 nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
390// nCBars = 2;
391// piCofVar[0] = 0;
392// piCofVar[1] = 1;
393
394
395 // copy the function
396 Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
397
398 // decompose w.r.t. these variables
399 for ( k = 0; k < nCBars; k++ )
400 {
401 nSize = (1 << k);
402 for ( i = 0; i < nSize; i++ )
403 {
404 Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
405 Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
406 }
407 }
408 nSize = (1 << nCBars);
409 // compute DSD networks
410 for ( i = 0; i < nSize; i++ )
411 {
412 ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
413 ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
414 Kit_DsdNtkFree( pTemp );
415 if ( fVerbose )
416 {
417 printf( "Cof%d%d: ", nCBars, i );
418 Kit_DsdPrint( stdout, ppNtks[i] );
419 }
420 }
421
422 // compute variable frequences
423 for ( i = 0; i < nSize; i++ )
424 {
425 uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
426 for ( k = 0; k < nVars; k++ )
427 if ( uSupport & (1<<k) )
428 pFreqs[k]++;
429 }
430
431 // find common variable order
432 for ( i = 0; i < nSize; i++ )
433 {
434 Kit_DsdGetSupports( ppNtks[i] );
435 Lpk_CreateVarOrder( ppNtks[i], pTable );
436 }
437 Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose );
438 // update priorities with frequences
439 for ( i = 0; i < nVars; i++ )
440 pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i;
441
442 if ( fVerbose )
443 printf( "After restructuring with priority:\n" );
444
445 // transform all networks according to the variable order
446 for ( i = 0; i < nSize; i++ )
447 {
448 ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
449 Kit_DsdNtkFree( pTemp );
450 Kit_DsdGetSupports( ppNtks[i] );
451 assert( ppNtks[i]->pSupps[0] <= 0xFFFF );
452 // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
453 Kit_DsdRotate( ppNtks[i], pFreqs );
454 // print the resulting networks
455 if ( fVerbose )
456 {
457 printf( "Cof%d%d: ", nCBars, i );
458 Kit_DsdPrint( stdout, ppNtks[i] );
459 }
460 }
461
462 for ( i = 0; i < nSize; i++ )
463 {
464 // collect the roots
465 pRoot = Kit_DsdNtkRoot(ppNtks[i]);
466 if ( pRoot->Type == KIT_DSD_CONST1 )
467 piLits[i] = Abc_LitIsCompl(ppNtks[i]->Root)? -2: -1;
468 else if ( pRoot->Type == KIT_DSD_VAR )
469 piLits[i] = Abc_LitNotCond( pRoot->pFans[0], Abc_LitIsCompl(ppNtks[i]->Root) );
470 else
471 piLits[i] = ppNtks[i]->Root;
472 }
473
474
475 // recursively construct AIG for mapping
476 p->fCofactoring = 1;
477 pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios );
478 p->fCofactoring = 0;
479
480 if ( fVerbose )
481 printf( "\n" );
482
483 // verify the transformations
484 nSize = (1 << nCBars);
485 for ( i = 0; i < nSize; i++ )
486 Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] );
487 // mux the truth tables
488 for ( k = nCBars-1; k >= 0; k-- )
489 {
490 nSize = (1 << k);
491 for ( i = 0; i < nSize; i++ )
492 Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] );
493 }
494 if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) )
495 printf( "Verification failed.\n" );
496
497
498 // free the networks
499 for ( i = 0; i < 8; i++ )
500 if ( ppNtks[i] )
501 Kit_DsdNtkFree( ppNtks[i] );
502 ABC_FREE( ppCofs[0][0] );
503
504 return pResult;
505}
void Kit_DsdTruth(Kit_DsdNtk_t *pNtk, unsigned *pTruthRes)
Definition kitDsd.c:1069
int Kit_DsdCofactoring(unsigned *pTruth, int nVars, int *pCofVars, int nLimit, int fVerbose)
Definition kitDsd.c:2679
Kit_DsdNtk_t * Kit_DsdShrink(Kit_DsdNtk_t *p, int pPrios[])
Definition kitDsd.c:1634
unsigned Kit_DsdGetSupports(Kit_DsdNtk_t *p)
Definition kitDsd.c:1763
void Kit_DsdRotate(Kit_DsdNtk_t *p, int pFreqs[])
Definition kitDsd.c:1672
If_Obj_t * Lpk_MapTreeMulti_rec(Lpk_Man_t *p, Kit_DsdNtk_t **ppNtks, int *piLits, int *piCofVar, int nCBars, If_Obj_t **ppLeaves, int nLeaves, int *pPrio)
Definition lpkMulti.c:272
void Lpk_CreateCommonOrder(char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose)
Definition lpkMulti.c:87
ABC_NAMESPACE_IMPL_START void Lpk_CreateVarOrder(Kit_DsdNtk_t *pNtk, char pTable[][16])
DECLARATIONS ///.
Definition lpkMulti.c:45
Here is the call graph for this function:

◆ Lpk_MapTreeMux_rec()

If_Obj_t * Lpk_MapTreeMux_rec ( Lpk_Man_t * p,
unsigned * pTruth,
int nVars,
If_Obj_t ** ppLeaves )
extern

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

Synopsis [Maps the function by the best cofactoring.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file lpkMux.c.

90{
91 unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 );
92 unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 );
93 If_Obj_t * pObj0, * pObj1;
94 Kit_DsdNtk_t * ppNtks[2];
95 int iBestVar;
96 assert( nVars > 3 );
97 p->fCalledOnce = 1;
98 // cofactor w.r.t. the best variable
99 iBestVar = Lpk_MapTreeBestCofVar( p, pTruth, nVars, pCof0, pCof1 );
100 if ( iBestVar == -1 )
101 return NULL;
102 // decompose the functions
103 ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
104 ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
105 if ( p->pPars->fVeryVerbose )
106 {
107 printf( "Cofactoring w.r.t. var %c (%d -> %d+%d supp vars):\n",
108 'a'+iBestVar, nVars, Kit_TruthSupportSize(pCof0, nVars), Kit_TruthSupportSize(pCof1, nVars) );
109 Kit_DsdPrintExpanded( ppNtks[0] );
110 Kit_DsdPrintExpanded( ppNtks[1] );
111 }
112 // map the DSD structures
113 pObj0 = Lpk_MapTree_rec( p, ppNtks[0], ppLeaves, ppNtks[0]->Root, NULL );
114 pObj1 = Lpk_MapTree_rec( p, ppNtks[1], ppLeaves, ppNtks[1]->Root, NULL );
115 Kit_DsdNtkFree( ppNtks[0] );
116 Kit_DsdNtkFree( ppNtks[1] );
117 return If_ManCreateMux( p->pIfMan, pObj0, pObj1, ppLeaves[iBestVar] );
118}
If_Obj_t * If_ManCreateMux(If_Man_t *p, If_Obj_t *pFan0, If_Obj_t *pFan1, If_Obj_t *pCtrl)
Definition ifMan.c:441
int Kit_TruthSupportSize(unsigned *pTruth, int nVars)
Definition kitTruth.c:327
void Kit_DsdPrintExpanded(Kit_DsdNtk_t *pNtk)
Definition kitDsd.c:472
ABC_NAMESPACE_IMPL_START int Lpk_MapTreeBestCofVar(Lpk_Man_t *p, unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
DECLARATIONS ///.
Definition lpkMux.c:45
Here is the call graph for this function:

◆ Lpk_MuxAnalize()

Lpk_Res_t * Lpk_MuxAnalize ( Lpk_Man_t * pMan,
Lpk_Fun_t * p )
extern

DECLARATIONS ///.

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

FileName [lpkAbcMux.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis [LUT-decomposition based on recursive MUX decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Checks the possibility of MUX decomposition.]

Description [Returns the best variable to use for MUX decomposition.]

SideEffects []

SeeAlso []

Definition at line 45 of file lpkAbcMux.c.

46{
47 static Lpk_Res_t Res, * pRes = &Res;
48 int nSuppSize0, nSuppSize1, nSuppSizeS, nSuppSizeL;
49 int Var, Area, Polarity, Delay, Delay0, Delay1, DelayA, DelayB;
50 memset( pRes, 0, sizeof(Lpk_Res_t) );
51 assert( p->uSupp == Kit_BitMask(p->nVars) );
52 assert( p->fSupports );
53 // derive the delay and area after MUX-decomp with each var - and find the best var
54 pRes->Variable = -1;
55 Lpk_SuppForEachVar( p->uSupp, Var )
56 {
57 nSuppSize0 = Kit_WordCountOnes(p->puSupps[2*Var+0]);
58 nSuppSize1 = Kit_WordCountOnes(p->puSupps[2*Var+1]);
59 assert( nSuppSize0 < (int)p->nVars );
60 assert( nSuppSize1 < (int)p->nVars );
61 if ( nSuppSize0 < 1 || nSuppSize1 < 1 )
62 continue;
63//printf( "%d %d ", nSuppSize0, nSuppSize1 );
64 if ( nSuppSize0 <= (int)p->nLutK - 2 && nSuppSize1 <= (int)p->nLutK - 2 )
65 {
66 // include cof var into 0-block
67 DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
68 DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1] , p->pDelays );
69 Delay0 = Abc_MaxInt( DelayA, DelayB + 1 );
70 // include cof var into 1-block
71 DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
72 DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0] , p->pDelays );
73 Delay1 = Abc_MaxInt( DelayA, DelayB + 1 );
74 // get the best delay
75 Delay = Abc_MinInt( Delay0, Delay1 );
76 Area = 2;
77 Polarity = (int)(Delay == Delay1);
78 }
79 else if ( nSuppSize0 <= (int)p->nLutK - 2 )
80 {
81 DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
82 DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1] , p->pDelays );
83 Delay = Abc_MaxInt( DelayA, DelayB + 1 );
84 Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
85 Polarity = 0;
86 }
87 else if ( nSuppSize1 <= (int)p->nLutK - 2 )
88 {
89 DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
90 DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0] , p->pDelays );
91 Delay = Abc_MaxInt( DelayA, DelayB + 1 );
92 Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
93 Polarity = 1;
94 }
95 else if ( nSuppSize0 <= (int)p->nLutK )
96 {
97 DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
98 DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0] , p->pDelays );
99 Delay = Abc_MaxInt( DelayA, DelayB + 1 );
100 Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK );
101 Polarity = 1;
102 }
103 else if ( nSuppSize1 <= (int)p->nLutK )
104 {
105 DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
106 DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1] , p->pDelays );
107 Delay = Abc_MaxInt( DelayA, DelayB + 1 );
108 Area = 1 + Lpk_LutNumLuts( nSuppSize0+2, p->nLutK );
109 Polarity = 0;
110 }
111 else
112 {
113 // include cof var into 0-block
114 DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
115 DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1] , p->pDelays );
116 Delay0 = Abc_MaxInt( DelayA, DelayB + 1 );
117 // include cof var into 1-block
118 DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
119 DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0] , p->pDelays );
120 Delay1 = Abc_MaxInt( DelayA, DelayB + 1 );
121 // get the best delay
122 Delay = Abc_MinInt( Delay0, Delay1 );
123 if ( Delay == Delay0 )
124 Area = Lpk_LutNumLuts( nSuppSize0+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
125 else
126 Area = Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
127 Polarity = (int)(Delay == Delay1);
128 }
129 // find the best variable
130 if ( Delay > (int)p->nDelayLim )
131 continue;
132 if ( Area > (int)p->nAreaLim )
133 continue;
134 nSuppSizeS = Abc_MinInt( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity );
135 nSuppSizeL = Abc_MaxInt( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity );
136 if ( nSuppSizeL > (int)p->nVars )
137 continue;
138 if ( pRes->Variable == -1 || pRes->AreaEst > Area ||
139 (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL > nSuppSizeS + nSuppSizeL) ||
140 (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL == nSuppSizeS + nSuppSizeL && pRes->DelayEst > Delay) )
141 {
142 pRes->Variable = Var;
143 pRes->Polarity = Polarity;
144 pRes->AreaEst = Area;
145 pRes->DelayEst = Delay;
146 pRes->nSuppSizeS = nSuppSizeS;
147 pRes->nSuppSizeL = nSuppSizeL;
148 }
149 }
150 return pRes->Variable == -1 ? NULL : pRes;
151}
int nSuppSizeS
Definition lpkInt.h:170
int Variable
Definition lpkInt.h:174
int Polarity
Definition lpkInt.h:175
int DelayEst
Definition lpkInt.h:172
int AreaEst
Definition lpkInt.h:173
int nSuppSizeL
Definition lpkInt.h:171
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_MuxSplit()

Lpk_Fun_t * Lpk_MuxSplit ( Lpk_Man_t * pMan,
Lpk_Fun_t * p,
int Var,
int Pol )
extern

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

Synopsis [Transforms the function decomposed by the MUX decomposition.]

Description [Returns the best variable to use for MUX decomposition.]

SideEffects []

SeeAlso []

Definition at line 164 of file lpkAbcMux.c.

165{
166 Lpk_Fun_t * pNew;
167 unsigned * pTruth = Lpk_FunTruth( p, 0 );
168 unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
169 unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
170// unsigned uSupp;
171 int iVarVac;
172 assert( Var >= 0 && Var < (int)p->nVars );
173 assert( p->nAreaLim >= 2 );
174 assert( p->uSupp == Kit_BitMask(p->nVars) );
175 Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var );
176 Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var );
177/*
178uSupp = Kit_TruthSupport( pTruth, p->nVars );
179Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" );
180uSupp = Kit_TruthSupport( pTruth0, p->nVars );
181Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" );
182uSupp = Kit_TruthSupport( pTruth1, p->nVars );
183Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n\n" );
184*/
185 // derive the new component
186 pNew = Lpk_FunDup( p, Pol ? pTruth0 : pTruth1 );
187 // update the support of the old component
188 p->uSupp = Kit_TruthSupport( Pol ? pTruth1 : pTruth0, p->nVars );
189 p->uSupp |= (1 << Var);
190 // update the truth table of the old component
191 iVarVac = Kit_WordFindFirstBit( ~p->uSupp );
192 assert( iVarVac < (int)p->nVars );
193 p->uSupp |= (1 << iVarVac);
194 Kit_TruthIthVar( pTruth, p->nVars, iVarVac );
195 if ( Pol )
196 Kit_TruthMuxVar( pTruth, pTruth, pTruth1, p->nVars, Var );
197 else
198 Kit_TruthMuxVar( pTruth, pTruth0, pTruth, p->nVars, Var );
199 assert( p->uSupp == Kit_TruthSupport(pTruth, p->nVars) );
200 // set the decomposed variable
201 p->pFanins[iVarVac] = pNew->Id;
202 p->pDelays[iVarVac] = p->nDelayLim - 1;
203 // support minimize both
204 p->fSupports = 0;
206 Lpk_FunSuppMinimize( pNew );
207 // update delay and area requirements
208 pNew->nDelayLim = p->nDelayLim - 1;
209 if ( pNew->nVars <= pNew->nLutK )
210 {
211 pNew->nAreaLim = 1;
212 p->nAreaLim = p->nAreaLim - 1;
213 }
214 else if ( p->nVars <= p->nLutK )
215 {
216 pNew->nAreaLim = p->nAreaLim - 1;
217 p->nAreaLim = 1;
218 }
219 else if ( p->nVars < pNew->nVars )
220 {
221 pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
222 p->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
223 }
224 else // if ( pNew->nVars < p->nVars )
225 {
226 pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
227 p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
228 }
229 pNew->fMark = 1;
230 return pNew;
231}
unsigned fMark
Definition lpkInt.h:153
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_NodeCuts()

int Lpk_NodeCuts ( Lpk_Man_t * p)
extern

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

Synopsis [Computes the set of all cuts.]

Description []

SideEffects []

SeeAlso []

Definition at line 619 of file lpkCut.c.

620{
621 Lpk_Cut_t * pCut, * pCut2;
622 int i, k, Temp, nMffc, fChanges;
623 //int nSupp;
624
625 // mark the MFFC of the node with the current trav ID
626 Vec_PtrClear( p->vTemp );
627 nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj, p->vTemp );
628 assert( nMffc > 0 );
629 if ( nMffc == 1 )
630 return 0;
631/*
632 // count the leaves
633 nSupp = Lpk_CountSupp( p->pNtk, p->vTemp );
634 if ( nMffc > 10 && nSupp <= 10 )
635 printf( "Obj = %4d : Supp = %4d. Mffc = %4d.\n", p->pObj->Id, nSupp, nMffc );
636*/
637 // initialize the first cut
638 pCut = p->pCuts; p->nCuts = 1;
639 pCut->nNodes = 0;
640 pCut->nNodesDup = 0;
641 pCut->nLeaves = 1;
642 pCut->pLeaves[0] = p->pObj->Id;
643 // assign the signature
644 Lpk_NodeCutSignature( pCut );
645
646 // perform the cut computation
647 for ( i = 0; i < p->nCuts; i++ )
648 {
649 pCut = p->pCuts + i;
650 if ( pCut->nLeaves == 0 )
651 continue;
652
653 // try to expand the fanins of this cut
654 for ( k = 0; k < (int)pCut->nLeaves; k++ )
655 {
656 // create a new cut
657 Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
658 // quit if the number of cuts has exceeded the limit
659 if ( p->nCuts == LPK_CUTS_MAX )
660 break;
661 }
662 if ( p->nCuts == LPK_CUTS_MAX )
663 break;
664 }
665 if ( p->nCuts == LPK_CUTS_MAX )
666 p->nNodesOver++;
667
668 // record the impact of this node
669 if ( p->pPars->fSatur )
671
672 // compress the cuts by removing empty ones, those with negative Weight, and decomposable ones
673 p->nEvals = 0;
674 for ( i = 0; i < p->nCuts; i++ )
675 {
676 pCut = p->pCuts + i;
677 if ( pCut->nLeaves < 2 )
678 continue;
679 // compute the minimum number of LUTs needed to implement this cut
680 // V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
681 pCut->nLuts = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize );
682// pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup - 1) / pCut->nLuts; //p->pPars->nLutsMax;
683 pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
684 if ( pCut->Weight <= 1.001 )
685// if ( pCut->Weight <= 0.999 )
686 continue;
687 pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
688 if ( pCut->fHasDsd )
689 continue;
690 p->pEvals[p->nEvals++] = i;
691
692// if ( pCut->nLeaves <= 9 && pCut->nNodes > 15 )
693// printf( "%5d : Obj = %4d Leaves = %4d Nodes = %4d LUTs = %4d\n", i, p->pObj->Id, pCut->nLeaves, pCut->nNodes, pCut->nLuts );
694 }
695 if ( p->nEvals == 0 )
696 return 0;
697
698 // sort the cuts by Weight
699 do {
700 fChanges = 0;
701 for ( i = 0; i < p->nEvals - 1; i++ )
702 {
703 pCut = p->pCuts + p->pEvals[i];
704 pCut2 = p->pCuts + p->pEvals[i+1];
705 if ( pCut->Weight >= pCut2->Weight - 0.001 )
706 continue;
707 Temp = p->pEvals[i];
708 p->pEvals[i] = p->pEvals[i+1];
709 p->pEvals[i+1] = Temp;
710 fChanges = 1;
711 }
712 } while ( fChanges );
713/*
714 for ( i = 0; i < p->nEvals; i++ )
715 {
716 pCut = p->pCuts + p->pEvals[i];
717 printf( "Cut %3d : W = %5.2f.\n", i, pCut->Weight );
718 }
719 printf( "\n" );
720*/
721 return 1;
722}
ABC_DLL int Abc_NodeMffcLabel(Abc_Obj_t *pNode, Vec_Ptr_t *vNodes)
Definition abcRefs.c:439
void Lpk_NodeCutsOne(Lpk_Man_t *p, Lpk_Cut_t *pCut, int Node)
Definition lpkCut.c:477
int Lpk_NodeCutsCheckDsd(Lpk_Man_t *p, Lpk_Cut_t *pCut)
Definition lpkCut.c:275
void Lpk_NodeCutSignature(Lpk_Cut_t *pCut)
Definition lpkCut.c:453
void Lpk_NodeRecordImpact(Lpk_Man_t *p)
Definition lpkCut.c:233
struct Lpk_Cut_t_ Lpk_Cut_t
Definition lpkInt.h:51
unsigned nLuts
Definition lpkInt.h:58
float Weight
Definition lpkInt.h:63
int pLeaves[LPK_SIZE_MAX]
Definition lpkInt.h:65
unsigned nNodesDup
Definition lpkInt.h:57
unsigned fHasDsd
Definition lpkInt.h:60
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Lpk_SuppDelay()

int Lpk_SuppDelay ( unsigned uSupp,
int * pDelays )
extern

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

Synopsis [Get the delay of the bound set.]

Description []

SideEffects []

SeeAlso []

Definition at line 215 of file lpkAbcUtil.c.

216{
217 int Delay, Var;
218 Delay = 0;
219 Lpk_SuppForEachVar( uSupp, Var )
220 Delay = Abc_MaxInt( Delay, pDelays[Var] );
221 return Delay + 1;
222}
Here is the caller graph for this function:

◆ Lpk_SuppToVars()

int Lpk_SuppToVars ( unsigned uBoundSet,
char * pVars )
extern

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

Synopsis [Converts support into variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file lpkAbcUtil.c.

236{
237 int i, nVars = 0;
238 Lpk_SuppForEachVar( uBoundSet, i )
239 pVars[nVars++] = i;
240 return nVars;
241}