luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc70705

This commit is contained in:
Alan Mishchenko 2007-07-05 08:01:00 -07:00
parent a8db621dc9
commit 0c1e87bc9a
25 changed files with 3330 additions and 1957 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
Makefile
View File

@ -6,12 +6,21 @@ CP := cp
PROG := abc
MODULES := src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/ver \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco src/aig/mem src/aig/ec \
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo src/bdd/cas \
src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \
src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim src/opt/ret src/opt/res src/opt/kit \
MODULES := src/base/abc src/base/abci src/base/cmd \
src/base/io src/base/main src/base/ver \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
src/aig/ec \
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
src/bdd/parse src/bdd/reo src/bdd/cas \
src/map/fpga src/map/mapper src/map/mio \
src/map/super src/map/if \
src/misc/extra src/misc/mvc src/misc/st src/misc/util \
src/misc/espresso src/misc/nm src/misc/vec \
src/misc/hash \
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr \
src/opt/sim src/opt/ret src/opt/res src/opt/kit \
src/opt/lpk \
src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
src/phys/place

48
abc.dsp
View File

@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\opt\lpk" /I "src\opt\bdc" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\opt\lpk" /I "src\opt\bdc" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
@ -230,10 +230,6 @@ SOURCE=.\src\base\abci\abcDsd.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcDsdRes.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcEspresso.c
# End Source File
# Begin Source File
@ -1937,6 +1933,46 @@ SOURCE=.\src\opt\bdc\bdcInt.h
SOURCE=.\src\opt\bdc\bdcTable.c
# End Source File
# End Group
# Begin Group "lpk"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\lpk\lpk.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkCore.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkCut.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkInt.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkMan.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkMap.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkMulti.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkMux.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\lpk\lpkSets.c
# End Source File
# End Group
# End Group
# Begin Group "map"

5
abc.rc
View File

@ -31,6 +31,7 @@ alias fsto fraig_store
alias fres fraig_restore
alias ft fraig_trust
alias lp lutpack
alias pd print_dsd
alias pex print_exdc -d
alias pf print_factor
alias pfan print_fanio
@ -169,6 +170,8 @@ alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
alias bug "r pj1_if3.blif; lp"
alias table "r lutexp.baf; test"
alias t "r c.blif; st; wc c.cnf"
#alias t "r c.blif; st; wc c.cnf"
#alias t "r test/dsdmap6.blif; lutpack -vw; cec"
alias t "r i10_if4.blif; lp"

17
src/base/abc/abc.h
View File

@ -227,23 +227,6 @@ struct Abc_Lib_t_
void * pGenlib; // the genlib library used to map this design
};
typedef struct Lut_Par_t_ Lut_Par_t;
struct Lut_Par_t_
{
// user-controlled parameters
int nLutsMax; // (N) the maximum number of LUTs in the structure
int nLutsOver; // (Q) the maximum number of LUTs not in the MFFC
int nVarsShared; // (S) the maximum number of shared variables (crossbars)
int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis
int fSatur; // iterate till saturation
int fZeroCost; // accept zero-cost replacements
int fVerbose; // the verbosiness flag
int fVeryVerbose; // additional verbose info printout
// internal parameters
int nLutSize; // (K) the LUT size (determined by the input network)
int nVarsMax; // (V) the largest number of variables: V = N * (K-1) + 1
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////

28
src/base/abc/abcFunc.c
View File

@ -881,12 +881,20 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V
Hop_Obj_t * pObj;
unsigned * pTruth, * pTruth2;
int i, nWords, nNodes;
Vec_Ptr_t * vTtElems;
// if the number of variables is more than 8, allocate truth tables
if ( nVars > 8 )
vTtElems = Vec_PtrAllocTruthTables( nVars );
else
vTtElems = NULL;
// clear the data fields and set marks
nNodes = Abc_ConvertAigToTruth_rec1( pRoot );
// prepare memory
nWords = Hop_TruthWordNum( nVars );
Vec_IntClear( vTruth );
Vec_IntGrow( vTruth, nWords * nNodes );
Vec_IntGrow( vTruth, nWords * (nNodes+1) );
pTruth = Vec_IntFetch( vTruth, nWords );
// check the case of a constant
if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
@ -900,21 +908,33 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V
}
// set elementary truth tables at the leaves
assert( nVars <= Hop_ManPiNum(p) );
assert( Hop_ManPiNum(p) <= 8 );
// assert( Hop_ManPiNum(p) <= 8 );
if ( fMsbFirst )
{
Hop_ManForEachPi( p, pObj, i )
pObj->pData = (void *)uTruths[nVars-1-i];
{
if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
else
pObj->pData = (void *)uTruths[nVars-1-i];
}
}
else
{
Hop_ManForEachPi( p, pObj, i )
pObj->pData = (void *)uTruths[i];
{
if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, i);
else
pObj->pData = (void *)uTruths[i];
}
}
// clear the marks and compute the truth table
pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
// copy the result
Extra_TruthCopy( pTruth, pTruth2, nVars );
if ( vTtElems )
Vec_PtrFree( vTtElems );
return pTruth;
}

64
src/base/abci/abc.c
View File

@ -26,7 +26,7 @@
#include "fpga.h"
#include "if.h"
#include "res.h"
//#include "dar.h"
#include "lpk.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -1509,23 +1509,37 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
int fUseLibrary;
int fCofactor;
int nCofLevel;
extern void Kit_DsdTest( unsigned * pTruth, int nVars );
extern void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fUseLibrary = 1;
nCofLevel = 1;
fCofactor = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Nch" ) ) != EOF )
{
switch ( c )
{
case 'l':
fUseLibrary ^= 1;
case 'N':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nCofLevel = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nCofLevel < 0 )
goto usage;
break;
case 'c':
fCofactor ^= 1;
break;
case 'h':
goto usage;
@ -1549,16 +1563,16 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
// convert it to truth table
{
Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
Vec_Int_t * vMemory = Vec_IntAlloc( 10000 );
Vec_Int_t * vMemory = Vec_IntAlloc(0);
unsigned * pTruth;
if ( !Abc_ObjIsNode(pObj) )
{
fprintf( pErr, "The fanin of the first PO node does not have a logic function.\n" );
return 1;
}
if ( Abc_ObjFaninNum(pObj) > 8 )
if ( Abc_ObjFaninNum(pObj) > 16 )
{
fprintf( pErr, "Currently works only for up to 8 inputs.\n" );
fprintf( pErr, "Currently works only for up to 16 inputs.\n" );
return 1;
}
pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
@ -1566,16 +1580,20 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
printf( "\n" );
Kit_DsdTest( pTruth, Abc_ObjFaninNum(pObj) );
if ( fCofactor )
Kit_DsdPrintCofactors( pTruth, Abc_ObjFaninNum(pObj), nCofLevel, 1 );
else
Kit_DsdTest( pTruth, Abc_ObjFaninNum(pObj) );
Vec_IntFree( vMemory );
}
return 0;
usage:
fprintf( pErr, "usage: print_dsd [-h]\n" );
fprintf( pErr, "\t print DSD formula for a single-output function with less than 16 variables\n" );
// fprintf( pErr, "\t-l : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "usage: print_dsd [-ch] [-N num]\n" );
fprintf( pErr, "\t print DSD formula for a single-output function with less than 16 variables\n" );
fprintf( pErr, "\t-c : toggle recursive cofactoring [default = %s]\n", fCofactor? "yes": "no" );
fprintf( pErr, "\t-N num : the number of levels to cofactor [default = %d]\n", nCofLevel );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -2906,26 +2924,22 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
Lut_Par_t Pars, * pPars = &Pars;
Lpk_Par_t Pars, * pPars = &Pars;
int c;
extern int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars );
// printf( "Implementation of this command is not finished.\n" );
// return 1;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
memset( pPars, 0, sizeof(Lut_Par_t) );
memset( pPars, 0, sizeof(Lpk_Par_t) );
pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure
pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC
pPars->nVarsShared = 3; // (S) the maximum number of shared variables (crossbars)
pPars->nGrowthLevel = 1;
pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars)
pPars->nGrowthLevel = 9; // (L) the maximum number of increased levels
pPars->fSatur = 1;
pPars->fZeroCost = 0;
pPars->fVerbose = 0;
pPars->fVerbose = 1;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszvwh" ) ) != EOF )
@ -3007,7 +3021,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
if ( !Abc_LutResynthesize( pNtk, pPars ) )
if ( !Lpk_Resynthesize( pNtk, pPars ) )
{
fprintf( pErr, "Resynthesis has failed.\n" );
return 1;

1774
src/base/abci/abcDsdRes.c
View File

File diff suppressed because it is too large Load Diff

6
src/base/abci/abcIf.c
View File

@ -145,8 +145,8 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
Extra_ProgressBarUpdate( pProgress, i, "Initial" );
// add the node to the mapper
pNode->pCopy = (Abc_Obj_t *)If_ManCreateAnd( pIfMan,
(If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode),
(If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
If_NotCond( (If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
// set up the choice node
if ( Abc_AigNodeIsChoice( pNode ) )
{
@ -162,7 +162,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
// set the primary outputs without copying the phase
Abc_NtkForEachCo( pNtk, pNode, i )
If_ManCreateCo( pIfMan, (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
If_ManCreateCo( pIfMan, If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
return pIfMan;
}

1
src/base/abci/module.make
View File

@ -11,7 +11,6 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDebug.c \
src/base/abci/abcDress.c \
src/base/abci/abcDsd.c \
src/base/abci/abcDsdRes.c \
src/base/abci/abcEspresso.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFpga.c \

2
src/base/io/io.c
View File

@ -715,7 +715,7 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
int fHex;
int c;
fHex = 0;
fHex = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "xh" ) ) != EOF )
{

13
src/map/if/if.h
View File

@ -212,6 +212,11 @@ struct If_Obj_t_
If_Cut_t CutBest; // the best cut selected
};
static inline If_Obj_t * If_Regular( If_Obj_t * p ) { return (If_Obj_t *)((unsigned long)(p) & ~01); }
static inline If_Obj_t * If_Not( If_Obj_t * p ) { return (If_Obj_t *)((unsigned long)(p) ^ 01); }
static inline If_Obj_t * If_NotCond( If_Obj_t * p, int c ) { return (If_Obj_t *)((unsigned long)(p) ^ (c)); }
static inline int If_IsComplement( If_Obj_t * p ) { return (int )(((unsigned long)p) & 01); }
static inline int If_ManCiNum( If_Man_t * p ) { return p->nObjs[IF_CI]; }
static inline int If_ManCoNum( If_Man_t * p ) { return p->nObjs[IF_CO]; }
static inline int If_ManAndNum( If_Man_t * p ) { return p->nObjs[IF_AND]; }
@ -334,10 +339,10 @@ extern If_Man_t * If_ManStart( If_Par_t * pPars );
extern void If_ManRestart( If_Man_t * p );
extern void If_ManStop( If_Man_t * p );
extern If_Obj_t * If_ManCreateCi( If_Man_t * p );
extern If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
extern If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
extern If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 );
extern If_Obj_t * If_ManCreateMnux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl );
extern If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver );
extern If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 );
extern If_Obj_t * If_ManCreateXor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 );
extern If_Obj_t * If_ManCreateMux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl );
extern void If_ManCreateChoice( If_Man_t * p, If_Obj_t * pRepr );
extern void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId );
extern void If_ManSetupCiCutSets( If_Man_t * p );

39
src/map/if/ifMan.c
View File

@ -175,13 +175,13 @@ If_Obj_t * If_ManCreateCi( If_Man_t * p )
SeeAlso []
***********************************************************************/
If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 )
If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver )
{
If_Obj_t * pObj;
pObj = If_ManSetupObj( p );
pObj->Type = IF_CO;
pObj->fCompl0 = fCompl0;
Vec_PtrPush( p->vCos, pObj );
pObj->Type = IF_CO;
pObj->fCompl0 = If_IsComplement(pDriver); pDriver = If_Regular(pDriver);
pObj->pFanin0 = pDriver; pDriver->nRefs++;
p->nObjs[IF_CO]++;
return pObj;
@ -198,17 +198,26 @@ If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 )
SeeAlso []
***********************************************************************/
If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 )
If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
{
If_Obj_t * pObj;
// perform constant propagation
if ( pFan0 == pFan1 )
return pFan0;
if ( pFan0 == If_Not(pFan1) )
return If_Not(p->pConst1);
if ( If_Regular(pFan0) == p->pConst1 )
return pFan0 == p->pConst1 ? pFan1 : If_Not(p->pConst1);
if ( If_Regular(pFan1) == p->pConst1 )
return pFan1 == p->pConst1 ? pFan0 : If_Not(p->pConst1);
// get memory for the new object
pObj = If_ManSetupObj( p );
pObj->Type = IF_AND;
pObj->fCompl0 = fCompl0;
pObj->fCompl1 = fCompl1;
pObj->fCompl0 = If_IsComplement(pFan0); pFan0 = If_Regular(pFan0);
pObj->fCompl1 = If_IsComplement(pFan1); pFan1 = If_Regular(pFan1);
pObj->pFanin0 = pFan0; pFan0->nRefs++; pFan0->nVisits++; pFan0->nVisitsCopy++;
pObj->pFanin1 = pFan1; pFan1->nRefs++; pFan1->nVisits++; pFan1->nVisitsCopy++;
pObj->fPhase = (fCompl0 ^ pFan0->fPhase) & (fCompl1 ^ pFan1->fPhase);
pObj->fPhase = (pObj->fCompl0 ^ pFan0->fPhase) & (pObj->fCompl1 ^ pFan1->fPhase);
pObj->Level = 1 + IF_MAX( pFan0->Level, pFan1->Level );
if ( p->nLevelMax < (int)pObj->Level )
p->nLevelMax = (int)pObj->Level;
@ -227,12 +236,12 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_
SeeAlso []
***********************************************************************/
If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
If_Obj_t * If_ManCreateXor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
{
If_Obj_t * pRes1, * pRes2;
pRes1 = If_ManCreateAnd( p, pFan0, 0, pFan1, 1 );
pRes2 = If_ManCreateAnd( p, pFan0, 1, pFan1, 0 );
return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 );
pRes1 = If_ManCreateAnd( p, If_Not(pFan0), pFan1 );
pRes2 = If_ManCreateAnd( p, pFan0, If_Not(pFan1) );
return If_Not( If_ManCreateAnd( p, If_Not(pRes1), If_Not(pRes2) ) );
}
/**Function*************************************************************
@ -246,12 +255,12 @@ If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
SeeAlso []
***********************************************************************/
If_Obj_t * If_ManCreateMnux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl )
If_Obj_t * If_ManCreateMux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl )
{
If_Obj_t * pRes1, * pRes2;
pRes1 = If_ManCreateAnd( p, pFan0, 0, pCtrl, 1 );
pRes2 = If_ManCreateAnd( p, pFan1, 0, pCtrl, 0 );
return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 );
pRes1 = If_ManCreateAnd( p, pFan0, If_Not(pCtrl) );
pRes2 = If_ManCreateAnd( p, pFan1, pCtrl );
return If_Not( If_ManCreateAnd( p, If_Not(pRes1), If_Not(pRes2) ) );
}
/**Function*************************************************************

15
src/opt/kit/kit.h
View File

@ -159,6 +159,7 @@ static inline unsigned Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )
#define KIT_MIN(a,b) (((a) < (b))? (a) : (b))
#define KIT_MAX(a,b) (((a) > (b))? (a) : (b))
#define KIT_INFINITY (100000000)
#ifndef ALLOC
#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
@ -235,6 +236,10 @@ static inline int Kit_WordFindFirstBit( unsigned uWord )
return i;
return -1;
}
static inline int Kit_WordHasOneBit( unsigned uWord )
{
return (uWord & (uWord - 1)) == 0;
}
static inline int Kit_WordCountOnes( unsigned uWord )
{
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
@ -250,6 +255,14 @@ static inline int Kit_TruthCountOnes( unsigned * pIn, int nVars )
Counter += Kit_WordCountOnes(pIn[w]);
return Counter;
}
static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars )
{
int w;
for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
if ( pIn[w] )
return Kit_WordFindFirstBit(pIn[w]);
return -1;
}
static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
@ -433,7 +446,9 @@ extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nV
/*=== kitDsd.c ==========================================================*/
extern Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
extern void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
extern void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );

496
src/opt/kit/kitDsd.c
View File

@ -47,7 +47,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
p->nVars = nVars;
p->nWords = Kit_TruthWordNum( p->nVars );
p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
p->vTtNodes = Vec_PtrAllocSimInfo( 64, p->nWords );
p->vTtNodes = Vec_PtrAllocSimInfo( 1024, p->nWords );
return p;
}
@ -260,6 +260,25 @@ void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk )
fprintf( pFile, "\n" );
}
/**Function*************************************************************
Synopsis [Print the DSD formula.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
{
Kit_DsdNtk_t * pTemp;
pTemp = Kit_DsdExpand( pNtk );
Kit_DsdPrint( stdout, pNtk );
Kit_DsdNtkFree( pTemp );
}
/**Function*************************************************************
Synopsis [Derives the truth table of the DSD node.]
@ -384,6 +403,26 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
return pTruthRes;
}
/**Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
{
Kit_DsdMan_t * p;
unsigned * pTruth;
p = Kit_DsdManAlloc( pNtk->nVars );
pTruth = Kit_DsdTruthCompute( p, pNtk );
Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
Kit_DsdManFree( p );
}
/**Function*************************************************************
@ -551,29 +590,25 @@ void Kit_DsdExpandCollectXor_rec( Kit_DsdNtk_t * p, int iLit, int * piLitsNew, i
int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
{
unsigned * pTruth, * pTruthNew;
unsigned i, fCompl, iLitFanin, piLitsNew[16], nLitsNew = 0;
unsigned i, iLitFanin, piLitsNew[16], nLitsNew = 0;
Kit_DsdObj_t * pObj, * pObjNew;
// remember the complement
fCompl = Kit_DsdLitIsCompl(iLit);
iLit = Kit_DsdLitRegular(iLit);
assert( !Kit_DsdLitIsCompl(iLit) );
// consider the case of simple gate
pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
return Kit_DsdLitNotCond( iLit, fCompl );
return iLit;
if ( pObj->Type == KIT_DSD_AND )
{
Kit_DsdExpandCollectAnd_rec( p, iLit, piLitsNew, &nLitsNew );
Kit_DsdExpandCollectAnd_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew );
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
for ( i = 0; i < pObjNew->nFans; i++ )
pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] );
return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
}
if ( pObj->Type == KIT_DSD_XOR )
{
Kit_DsdExpandCollectXor_rec( p, iLit, piLitsNew, &nLitsNew );
int fCompl = Kit_DsdLitIsCompl(iLit);
Kit_DsdExpandCollectXor_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew );
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
for ( i = 0; i < pObjNew->nFans; i++ )
{
@ -602,7 +637,7 @@ int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
}
}
// if the incoming phase is complemented, absorb it into the prime node
if ( fCompl )
if ( Kit_DsdLitIsCompl(iLit) )
Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
return Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
@ -655,46 +690,48 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
SeeAlso []
***********************************************************************/
void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], int piLitsNew[], int nVars )
void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned char * piLits, int nVars, int piLitsRes[] )
{
int nSuppSizes[16], Priority[16], pOrder[16], Temp[16];
int i, k, iVarBest, SuppMax, PrioMin;
int nSuppSizes[16], Priority[16], pOrder[16];
int i, k, iVarBest, SuppMax, PrioMax;
// compute support sizes and priorities of the components
for ( i = 0; i < nVars; i++ )
{
Temp[i] = piLitsNew[i];
assert( uSupps[i] );
pOrder[i] = i;
Priority[i] = 16;
nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
Priority[i] = KIT_INFINITY;
for ( k = 0; k < 16; k++ )
if ( uSupps[i] & (1 << k) )
Priority[i] = KIT_MIN( Priority[i], pPrios[k] );
assert( Priority[i] != 16 );
nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
}
// find the component by with largest size and smallest priority
// sort the components by pririty
Extra_BubbleSort( pOrder, Priority, nVars, 0 );
// find the component by with largest size and lowest priority
iVarBest = -1;
SuppMax = 0;
PrioMin = 16;
SuppMax = 0;
PrioMax = 0;
for ( i = 0; i < nVars; i++ )
{
if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMin > Priority[i]) )
if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMax < Priority[i]) )
{
SuppMax = nSuppSizes[i];
PrioMin = Priority[i];
SuppMax = nSuppSizes[i];
PrioMax = Priority[i];
iVarBest = i;
}
}
// sort the components by pririty
Extra_BubbleSort( pOrder, Priority, nVars, 1 );
assert( iVarBest != -1 );
// copy the resulting literals
k = 0;
piLitsNew[k++] = piLitsNew[iVarBest];
piLitsRes[k++] = piLits[iVarBest];
for ( i = 0; i < nVars; i++ )
{
if ( pOrder[i] == iVarBest )
continue;
piLitsNew[k++] = piLitsNew[pOrder[i]];
piLitsRes[k++] = piLits[pOrder[i]];
}
assert( k == nVars );
}
/**Function*************************************************************
@ -713,76 +750,52 @@ int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPri
Kit_DsdObj_t * pObj, * pObjNew;
unsigned * pTruth, * pTruthNew;
unsigned i, piLitsNew[16], uSupps[16];
int fCompl, iLitFanin, iLitNew;
// remember the complement
fCompl = Kit_DsdLitIsCompl(iLit);
iLit = Kit_DsdLitRegular(iLit);
assert( !Kit_DsdLitIsCompl(iLit) );
int iLitFanin, iLitNew;
// consider the case of simple gate
pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
return Kit_DsdLitNotCond( iLit, fCompl );
return iLit;
if ( pObj->Type == KIT_DSD_AND )
{
if ( pObj->nFans == 2 )
// get the supports
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
// put the largest component last
// sort other components in the decreasing order of priority of their vars
Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
// construct the two-input node network
iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
for ( i = 1; i < pObj->nFans; i++ )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
pObjNew->pFans[1] = iLitNew;
iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
else
{
// get the supports
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
piLitsNew[i] = iLitFanin;
uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
}
// put the largest component first
// sort other components in the increasing order of the highest variable
Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
for ( i = 1; i < pObj->nFans; i++ )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
pObjNew->pFans[0] = iLitNew;
pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
}
return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
}
if ( pObj->Type == KIT_DSD_XOR )
{
if ( pObj->nFans == 2 )
// get the supports
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
assert( !Kit_DsdLitIsCompl(iLitFanin) );
uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
}
// put the largest component last
// sort other components in the decreasing order of priority of their vars
Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
// construct the two-input node network
iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
for ( i = 1; i < pObj->nFans; i++ )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
pObjNew->pFans[1] = iLitNew;
iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
else
{
// get the supports
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
piLitsNew[i] = iLitFanin;
uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
}
// put the largest component first
// sort other components in the increasing order of the highest variable
Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
for ( i = 1; i < pObj->nFans; i++ )
{
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
pObjNew->pFans[0] = iLitNew;
pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
}
return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
}
assert( pObj->Type == KIT_DSD_PRIME );
@ -804,7 +817,7 @@ int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPri
}
}
// if the incoming phase is complemented, absorb it into the prime node
if ( fCompl )
if ( Kit_DsdLitIsCompl(iLit) )
Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
return Kit_DsdVar2Lit( pObjNew->Id, 0 );
}
@ -877,22 +890,26 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
Weights[k] = 0;
for ( v = 0; v < 16; v++ )
if ( uSuppFanin & (1 << v) )
Weights[k] += pFreqs[v];
Weights[k] += pFreqs[v] - 1;
}
// find the most frequent fanin
WeightMax = FaninMax = 0;
WeightMax = 0;
FaninMax = -1;
for ( k = 0; k < pObj->nFans; k++ )
if ( WeightMax < Weights[k] )
{
WeightMax = Weights[k];
FaninMax = k;
}
assert( k < pObj->nFans );
// no need to reorder if there are no frequent fanins
if ( FaninMax == -1 )
continue;
// move the fanins number k to the first place
nSwaps = 0;
pIn = Kit_DsdObjTruth(pObj);
pOut = p->pSupps;
for ( v = k-1; v >= 0; v-- )
pOut = p->pMem;
// for ( v = FaninMax; v < ((int)pObj->nFans)-1; v++ )
for ( v = FaninMax-1; v >= 0; v-- )
{
// swap the fanins
Temp = pObj->pFans[v];
@ -903,11 +920,38 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
pTemp = pIn; pIn = pOut; pOut = pTemp;
nSwaps++;
}
if ( nSwaps & 1)
Kit_TruthCopy( pIn, pOut, pObj->nFans );
if ( nSwaps & 1 )
Kit_TruthCopy( pOut, pIn, pObj->nFans );
}
}
/**Function*************************************************************
Synopsis [Compute the support.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Kit_DsdGetSupports_rec( Kit_DsdNtk_t * p, int iLit )
{
Kit_DsdObj_t * pObj;
unsigned uSupport, k;
int iFaninLit;
pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
return Kit_DsdLitSupport( p, iLit );
uSupport = 0;
Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
uSupport |= Kit_DsdGetSupports_rec( p, iFaninLit );
p->pSupps[pObj->Id - p->nVars] = uSupport;
assert( uSupport <= 0xFFFF );
return uSupport;
}
/**Function*************************************************************
Synopsis [Compute the support.]
@ -921,17 +965,24 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
***********************************************************************/
void Kit_DsdGetSupports( Kit_DsdNtk_t * p )
{
Kit_DsdObj_t * pObj;
unsigned uSupport, k;
int iFaninLit, i;
Kit_DsdObj_t * pRoot;
assert( p->pSupps == NULL );
p->pSupps = ALLOC( unsigned, p->nNodes );
Kit_DsdNtkForEachObj( p, pObj, i )
// consider simple special cases
pRoot = Kit_DsdNtkRoot(p);
if ( pRoot->Type == KIT_DSD_CONST1 )
{
uSupport = 0;
Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
uSupport |= Kit_DsdLitSupport( p, iFaninLit );
p->pSupps[pObj->Id - p->nVars] = uSupport;
}
assert( p->nNodes == 1 );
p->pSupps[0] = 0;
}
if ( pRoot->Type == KIT_DSD_VAR )
{
assert( p->nNodes == 1 );
p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] );
}
else
Kit_DsdGetSupports_rec( p, p->Root );
assert( p->pSupps[0] <= 0xFFFF );
}
/**Function*************************************************************
@ -1772,6 +1823,251 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit
return nStep;
}
/**Function*************************************************************
Synopsis [Canonical decomposition into completely DSD-structure.]
Description [Returns the number of cofactoring steps. Also returns
the cofactoring variables in pVars.]
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose )
{
Kit_DsdNtk_t * ppNtks[32] = {0}, * pTemp;
unsigned * ppCofs[5][16];
int piCofVar[5];
int nPrimeSizeMax, nPrimeSizeCur, nSuppSizeMax;
int i, k, v1, v2, v3, v4, s, nSteps, nSize, nMemSize;
assert( nCofLevel < 5 );
// print the function
ppNtks[0] = Kit_DsdDecompose( pTruth, nVars );
ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
Kit_DsdNtkFree( pTemp );
if ( fVerbose )
Kit_DsdPrint( stdout, ppNtks[0] );
Kit_DsdNtkFree( ppNtks[0] );
// allocate storage for cofactors
nMemSize = Kit_TruthWordNum(nVars);
ppCofs[0][0] = ALLOC( unsigned, 80 * nMemSize );
nSize = 0;
for ( i = 0; i < 5; i++ )
for ( k = 0; k < 16; k++ )
ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
assert( nSize == 80 );
// copy the function
Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
if ( nCofLevel == 1 )
for ( v1 = 0; v1 < nVars; v1++ )
{
nSteps = 0;
piCofVar[nSteps++] = v1;
printf( " Variables { " );
for ( i = 0; i < nSteps; i++ )
printf( "%c ", 'a' + piCofVar[i] );
printf( "}\n" );
// single cofactors
for ( s = 1; s <= nSteps; s++ )
{
for ( k = 0; k < s; k++ )
{
nSize = (1 << k);
for ( i = 0; i < nSize; i++ )
{
Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
}
}
}
// compute DSD networks
nSize = (1 << nSteps);
nPrimeSizeMax = 0;
nSuppSizeMax = 0;
for ( i = 0; i < nSize; i++ )
{
ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
Kit_DsdNtkFree( pTemp );
if ( fVerbose )
{
printf( "Cof%d%d: ", nSteps, i );
Kit_DsdPrint( stdout, ppNtks[i] );
}
// compute the largest non-decomp block
nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
Kit_DsdNtkFree( ppNtks[i] );
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
}
printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
}
if ( nCofLevel == 2 )
for ( v1 = 0; v1 < nVars; v1++ )
for ( v2 = v1+1; v2 < nVars; v2++ )
{
nSteps = 0;
piCofVar[nSteps++] = v1;
piCofVar[nSteps++] = v2;
printf( " Variables { " );
for ( i = 0; i < nSteps; i++ )
printf( "%c ", 'a' + piCofVar[i] );
printf( "}\n" );
// single cofactors
for ( s = 1; s <= nSteps; s++ )
{
for ( k = 0; k < s; k++ )
{
nSize = (1 << k);
for ( i = 0; i < nSize; i++ )
{
Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
}
}
}
// compute DSD networks
nSize = (1 << nSteps);
nPrimeSizeMax = 0;
nSuppSizeMax = 0;
for ( i = 0; i < nSize; i++ )
{
ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
Kit_DsdNtkFree( pTemp );
if ( fVerbose )
{
printf( "Cof%d%d: ", nSteps, i );
Kit_DsdPrint( stdout, ppNtks[i] );
}
// compute the largest non-decomp block
nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
Kit_DsdNtkFree( ppNtks[i] );
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
}
printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
}
if ( nCofLevel == 3 )
for ( v1 = 0; v1 < nVars; v1++ )
for ( v2 = v1+1; v2 < nVars; v2++ )
for ( v3 = v2+1; v3 < nVars; v3++ )
{
nSteps = 0;
piCofVar[nSteps++] = v1;
piCofVar[nSteps++] = v2;
piCofVar[nSteps++] = v3;
printf( " Variables { " );
for ( i = 0; i < nSteps; i++ )
printf( "%c ", 'a' + piCofVar[i] );
printf( "}\n" );
// single cofactors
for ( s = 1; s <= nSteps; s++ )
{
for ( k = 0; k < s; k++ )
{
nSize = (1 << k);
for ( i = 0; i < nSize; i++ )
{
Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
}
}
}
// compute DSD networks
nSize = (1 << nSteps);
nPrimeSizeMax = 0;
nSuppSizeMax = 0;
for ( i = 0; i < nSize; i++ )
{
ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
Kit_DsdNtkFree( pTemp );
if ( fVerbose )
{
printf( "Cof%d%d: ", nSteps, i );
Kit_DsdPrint( stdout, ppNtks[i] );
}
// compute the largest non-decomp block
nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
Kit_DsdNtkFree( ppNtks[i] );
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
}
printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
}
if ( nCofLevel == 4 )
for ( v1 = 0; v1 < nVars; v1++ )
for ( v2 = v1+1; v2 < nVars; v2++ )
for ( v3 = v2+1; v3 < nVars; v3++ )
for ( v4 = v3+1; v4 < nVars; v4++ )
{
nSteps = 0;
piCofVar[nSteps++] = v1;
piCofVar[nSteps++] = v2;
piCofVar[nSteps++] = v3;
piCofVar[nSteps++] = v4;
printf( " Variables { " );
for ( i = 0; i < nSteps; i++ )
printf( "%c ", 'a' + piCofVar[i] );
printf( "}\n" );
// single cofactors
for ( s = 1; s <= nSteps; s++ )
{
for ( k = 0; k < s; k++ )
{
nSize = (1 << k);
for ( i = 0; i < nSize; i++ )
{
Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
}
}
}
// compute DSD networks
nSize = (1 << nSteps);
nPrimeSizeMax = 0;
nSuppSizeMax = 0;
for ( i = 0; i < nSize; i++ )
{
ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
Kit_DsdNtkFree( pTemp );
if ( fVerbose )
{
printf( "Cof%d%d: ", nSteps, i );
Kit_DsdPrint( stdout, ppNtks[i] );
}
// compute the largest non-decomp block
nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]);
nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
Kit_DsdNtkFree( ppNtks[i] );
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
}
printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
}
free( ppCofs[0][0] );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

82
src/opt/lpk/lpk.h Normal file
View File

@ -0,0 +1,82 @@
/**CFile****************************************************************
FileName [lpk.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Fast Boolean matching for LUT structures.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: lpk.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __LPK_H__
#define __LPK_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Lpk_Par_t_ Lpk_Par_t;
struct Lpk_Par_t_
{
// user-controlled parameters
int nLutsMax; // (N) the maximum number of LUTs in the structure
int nLutsOver; // (Q) the maximum number of LUTs not in the MFFC
int nVarsShared; // (S) the maximum number of shared variables (crossbars)
int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis
int fSatur; // iterate till saturation
int fZeroCost; // accept zero-cost replacements
int fVerbose; // the verbosiness flag
int fVeryVerbose; // additional verbose info printout
// internal parameters
int nLutSize; // (K) the LUT size (determined by the input network)
int nVarsMax; // (V) the largest number of variables: V = N * (K-1) + 1
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== lpkCore.c ========================================================*/
extern int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

280
src/opt/lpk/lpkCore.c Normal file
View File

@ -0,0 +1,280 @@
/**CFile****************************************************************
FileName [lpkCore.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: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns 1 if at least one entry has changed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pTemp;
int i;
vNodes = Vec_VecEntry( p->vVisited, iNode );
if ( Vec_PtrSize(vNodes) == 0 )
return 1;
Vec_PtrForEachEntry( vNodes, pTemp, i )
{
// check if the node has changed
pTemp = Abc_NtkObj( p->pNtk, (int)pTemp );
if ( pTemp == NULL )
return 1;
// check if the number of fanouts has changed
// if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) )
// return 1;
i++;
}
return 0;
}
/**Function*************************************************************
Synopsis [Performs resynthesis for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_ResynthesizeNode( Lpk_Man_t * p )
{
Kit_DsdNtk_t * pDsdNtk;
Lpk_Cut_t * pCut;
unsigned * pTruth;
void * pDsd = NULL;
int i, RetValue, clk;
Lpk_Cut_t * pCutMax;
// compute the cuts
clk = clock();
if ( !Lpk_NodeCuts( p ) )
{
p->timeCuts += clock() - clk;
return 0;
}
p->timeCuts += clock() - clk;
// find the max volume cut
pCutMax = NULL;
for ( i = 0; i < p->nEvals; i++ )
{
pCut = p->pCuts + p->pEvals[i];
if ( pCutMax == NULL || pCutMax->nNodes < pCut->nNodes )
pCutMax = pCut;
}
assert( pCutMax != NULL );
if ( p->pPars->fVeryVerbose )
printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
// try the good cuts
p->nCutsTotal += p->nCuts;
p->nCutsUseful += p->nEvals;
for ( i = 0; i < p->nEvals; i++ )
{
// get the cut
pCut = p->pCuts + p->pEvals[i];
if ( pCut != pCutMax )
continue;
// compute the truth table
clk = clock();
pTruth = Lpk_CutTruth( p, pCut );
p->timeTruth += clock() - clk;
clk = clock();
pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize );
p->timeEval += clock() - clk;
if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work
{
Kit_DsdNtkFree( pDsdNtk );
continue;
}
if ( p->pPars->fVeryVerbose )
{
printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
Kit_DsdPrint( stdout, pDsdNtk );
}
// update the network
clk = clock();
RetValue = Lpk_CutExplore( p, pCut, pDsdNtk );
Kit_DsdNtkFree( pDsdNtk );
p->timeMap += clock() - clk;
if ( RetValue )
break;
}
return 1;
}
/**Function*************************************************************
Synopsis [Performs resynthesis for one network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
{
ProgressBar * pProgress;
Lpk_Man_t * p;
Abc_Obj_t * pObj;
double Delta;
int i, Iter, nNodes, nNodesPrev, clk = clock();
assert( Abc_NtkIsLogic(pNtk) );
// get the number of inputs
pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
// adjust the number of crossbars based on LUT size
if ( pPars->nVarsShared > pPars->nLutSize - 2 )
pPars->nVarsShared = pPars->nLutSize - 2;
// get the max number of LUTs tried
pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1
while ( pPars->nVarsMax > 16 )
{
pPars->nLutsMax--;
pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1;
}
if ( pPars->fVerbose )
{
printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
}
// convert logic to AIGs
Abc_NtkToAig( pNtk );
// start the manager
p = Lpk_ManStart( pPars );
p->pNtk = pNtk;
p->nNodesTotal = Abc_NtkNodeNum(pNtk);
p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes
if ( p->pPars->fSatur )
p->vVisited = Vec_VecStart( 0 );
// iterate over the network
nNodesPrev = p->nNodesTotal;
for ( Iter = 1; ; Iter++ )
{
// expand storage for changed nodes
if ( p->pPars->fSatur )
Vec_VecExpand( p->vVisited, Abc_NtkObjNumMax(pNtk) + 1 );
// consider all nodes
nNodes = Abc_NtkObjNumMax(pNtk);
if ( !pPars->fVeryVerbose )
pProgress = Extra_ProgressBarStart( stdout, nNodes );
Abc_NtkForEachNode( pNtk, pObj, i )
{
// skip all except the final node
// if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
// continue;
if ( i >= nNodes )
break;
if ( !pPars->fVeryVerbose )
Extra_ProgressBarUpdate( pProgress, i, NULL );
// skip the nodes that did not change
if ( p->pPars->fSatur && !Lpk_NodeHasChanged(p, pObj->Id) )
continue;
// resynthesize
p->pObj = pObj;
Lpk_ResynthesizeNode( p );
if ( p->nChanges == 3 )
break;
}
if ( !pPars->fVeryVerbose )
Extra_ProgressBarStop( pProgress );
// check the increase
Delta = 100.00 * (nNodesPrev - Abc_NtkNodeNum(pNtk)) / p->nNodesTotal;
if ( Delta < 0.05 )
break;
nNodesPrev = Abc_NtkNodeNum(pNtk);
if ( !p->pPars->fSatur )
break;
break;
}
if ( pPars->fVerbose )
{
printf( "N = %5d (%3d) Cut = %5d (%4d) Change = %5d Gain = %5d (%5.2f %%) Iter = %2d\n",
p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter );
printf( "Non_DSD blocks: " );
for ( i = 3; i <= pPars->nVarsMax; i++ )
if ( p->nBlocks[i] )
printf( "%d=%d ", i, p->nBlocks[i] );
printf( "\n" );
p->timeTotal = clock() - clk;
p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
PRTP( "Cuts ", p->timeCuts, p->timeTotal );
PRTP( "Truth ", p->timeTruth, p->timeTotal );
PRTP( "Eval ", p->timeEval, p->timeTotal );
PRTP( "Map ", p->timeMap, p->timeTotal );
PRTP( "Other ", p->timeOther, p->timeTotal );
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
}
Lpk_ManStop( p );
// check the resulting network
if ( !Abc_NtkCheck( pNtk ) )
{
printf( "Lpk_Resynthesize: The network check has failed.\n" );
return 0;
}
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

584
src/opt/lpk/lpkCut.c Normal file
View File

@ -0,0 +1,584 @@
/**CFile****************************************************************
FileName [lpkCut.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: lpkCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the truth able of one cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount )
{
unsigned * pTruth, * pTruth0, * pTruth1;
assert( !Hop_IsComplement(pObj) );
if ( pObj->pData )
{
assert( ((unsigned)pObj->pData) & 0xffff0000 );
return pObj->pData;
}
// get the plan for a new truth table
pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ );
if ( Hop_ObjIsConst1(pObj) )
Extra_TruthFill( pTruth, nVars );
else
{
assert( Hop_ObjIsAnd(pObj) );
// compute the truth tables of the fanins
pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount );
pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount );
// creat the truth table of the node
Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
}
pObj->pData = pTruth;
return pTruth;
}
/**Function*************************************************************
Synopsis [Computes the truth able of one cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut )
{
Hop_Man_t * pManHop = p->pNtk->pManFunc;
Hop_Obj_t * pObjHop;
Abc_Obj_t * pObj, * pFanin;
unsigned * pTruth;
int i, k, iCount = 0;
// Lpk_NodePrintCut( p, pCut );
// initialize the leaves
Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
pObj->pCopy = Vec_PtrEntry( p->vTtElems, i );
// construct truth table in the topological order
Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
{
// get the local AIG
pObjHop = Hop_Regular(pObj->pData);
// clean the data field of the nodes in the AIG subgraph
Hop_ObjCleanData_rec( pObjHop );
// set the initial truth tables at the fanins
Abc_ObjForEachFanin( pObj, pFanin, k )
{
assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
}
// compute the truth table of internal nodes
pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
if ( Hop_IsComplement(pObj->pData) )
Extra_TruthNot( pTruth, pTruth, pCut->nLeaves );
// set the truth table at the node
pObj->pCopy = (Abc_Obj_t *)pTruth;
}
return pTruth;
}
/**Function*************************************************************
Synopsis [Returns 1 if at least one entry has changed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_NodeRecordImpact( Lpk_Man_t * p )
{
Lpk_Cut_t * pCut;
Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id );
Abc_Obj_t * pNode;
int i, k;
// collect the nodes that impact the given node
Vec_PtrClear( vNodes );
for ( i = 0; i < p->nCuts; i++ )
{
pCut = p->pCuts + i;
for ( k = 0; k < (int)pCut->nLeaves; k++ )
{
pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] );
if ( pNode->fMarkC )
continue;
pNode->fMarkC = 1;
Vec_PtrPush( vNodes, (void *)pNode->Id );
Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) );
}
}
// clear the marks
Vec_PtrForEachEntry( vNodes, pNode, i )
{
pNode = Abc_NtkObj( p->pNtk, (int)pNode );
pNode->fMarkC = 0;
i++;
}
//printf( "%d ", Vec_PtrSize(vNodes) );
}
/**Function*************************************************************
Synopsis [Returns 1 if the cut has structural DSD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
{
Abc_Obj_t * pObj, * pFanin;
int i, k, nCands, fLeavesOnly, RetValue;
assert( pCut->nLeaves > 0 );
// clear ref counters
memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves );
// mark cut leaves
Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
{
assert( pObj->fMarkA == 0 );
pObj->fMarkA = 1;
pObj->pCopy = (void *)i;
}
// ref leaves pointed from the internal nodes
nCands = 0;
Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
{
fLeavesOnly = 1;
Abc_ObjForEachFanin( pObj, pFanin, k )
if ( pFanin->fMarkA )
p->pRefs[(int)pFanin->pCopy]++;
else
fLeavesOnly = 0;
if ( fLeavesOnly )
p->pCands[nCands++] = pObj->Id;
}
// look at the nodes that only point to the leaves
RetValue = 0;
for ( i = 0; i < nCands; i++ )
{
pObj = Abc_NtkObj( p->pNtk, p->pCands[i] );
Abc_ObjForEachFanin( pObj, pFanin, k )
{
assert( pFanin->fMarkA == 1 );
if ( p->pRefs[(int)pFanin->pCopy] > 1 )
break;
}
if ( k == Abc_ObjFaninNum(pObj) )
{
RetValue = 1;
break;
}
}
// unmark cut leaves
Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
pObj->fMarkA = 0;
return RetValue;
}
/**Function*************************************************************
Synopsis [Returns 1 if pDom is contained in pCut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Lpk_NodeCutsOneDominance( Lpk_Cut_t * pDom, Lpk_Cut_t * pCut )
{
int i, k;
for ( i = 0; i < (int)pDom->nLeaves; i++ )
{
for ( k = 0; k < (int)pCut->nLeaves; k++ )
if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
break;
if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
return 0;
}
// every node in pDom is contained in pCut
return 1;
}
/**Function*************************************************************
Synopsis [Check if the cut exists.]
Description [Returns 1 if the cut exists.]
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_NodeCutsOneFilter( Lpk_Cut_t * pCuts, int nCuts, Lpk_Cut_t * pCutNew )
{
Lpk_Cut_t * pCut;
int i, k;
assert( pCutNew->uSign[0] || pCutNew->uSign[1] );
// try to find the cut
for ( i = 0; i < nCuts; i++ )
{
pCut = pCuts + i;
if ( pCut->nLeaves == 0 )
continue;
if ( pCut->nLeaves == pCutNew->nLeaves )
{
if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] )
{
for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] )
break;
if ( k == (int)pCutNew->nLeaves )
return 1;
}
continue;
}
if ( pCut->nLeaves < pCutNew->nLeaves )
{
// skip the non-contained cuts
if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] )
continue;
if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] )
continue;
// check containment seriously
if ( Lpk_NodeCutsOneDominance( pCut, pCutNew ) )
return 1;
continue;
}
// check potential containment of other cut
// skip the non-contained cuts
if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] )
continue;
if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] )
continue;
// check containment seriously
if ( Lpk_NodeCutsOneDominance( pCutNew, pCut ) )
pCut->nLeaves = 0; // removed
}
return 0;
}
/**Function*************************************************************
Synopsis [Prints the given cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_NodePrintCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fLeavesOnly )
{
Abc_Obj_t * pObj;
int i;
if ( !fLeavesOnly )
printf( "LEAVES:\n" );
Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
printf( "%d,", pObj->Id );
if ( !fLeavesOnly )
{
printf( "\nNODES:\n" );
Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
{
printf( "%d,", pObj->Id );
assert( Abc_ObjIsNode(pObj) );
}
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis [Set the cut signature.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_NodeCutSignature( Lpk_Cut_t * pCut )
{
unsigned i;
pCut->uSign[0] = pCut->uSign[1] = 0;
for ( i = 0; i < pCut->nLeaves; i++ )
{
pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31));
if ( i != pCut->nLeaves - 1 )
assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] );
}
}
/**Function*************************************************************
Synopsis [Computes the set of all cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
{
Lpk_Cut_t * pCutNew;
Abc_Obj_t * pObj, * pFanin;
int i, k, j, nLeavesNew;
/*
printf( "Exploring cut " );
Lpk_NodePrintCut( p, pCut, 1 );
printf( "with node %d\n", Node );
*/
// check if the cut can stand adding one more internal node
if ( pCut->nNodes == LPK_SIZE_MAX )
return;
// if the node is a PI, quit
pObj = Abc_NtkObj( p->pNtk, Node );
if ( Abc_ObjIsCi(pObj) )
return;
assert( Abc_ObjIsNode(pObj) );
assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
// if the node is not in the MFFC, check the limit
if ( !Abc_NodeIsTravIdCurrent(pObj) )
{
if ( (int)pCut->nNodesDup == p->pPars->nLutsOver )
return;
assert( (int)pCut->nNodesDup < p->pPars->nLutsOver );
}
// check the possibility of adding this node using the signature
nLeavesNew = pCut->nLeaves - 1;
Abc_ObjForEachFanin( pObj, pFanin, i )
{
if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) )
continue;
if ( ++nLeavesNew > p->pPars->nVarsMax )
return;
}
// initialize the set of leaves to the nodes in the cut
assert( p->nCuts < LPK_CUTS_MAX );
pCutNew = p->pCuts + p->nCuts;
/*
if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 )
{
int x = 0;
printf( "Start:\n" );
Lpk_NodePrintCut( p, pCut );
}
*/
pCutNew->nLeaves = 0;
for ( i = 0; i < (int)pCut->nLeaves; i++ )
if ( pCut->pLeaves[i] != Node )
pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i];
// add new nodes
Abc_ObjForEachFanin( pObj, pFanin, i )
{
// find the place where this node belongs
for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
if ( pCutNew->pLeaves[k] >= pFanin->Id )
break;
if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id )
continue;
// check if there is room
if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax )
return;
// move all the nodes
for ( j = pCutNew->nLeaves; j > k; j-- )
pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1];
pCutNew->pLeaves[k] = pFanin->Id;
pCutNew->nLeaves++;
assert( pCutNew->nLeaves <= LPK_SIZE_MAX );
}
/*
printf( " Trying cut: " );
Lpk_NodePrintCut( p, pCutNew, 1 );
printf( "\n" );
*/
// skip the contained cuts
Lpk_NodeCutSignature( pCutNew );
if ( Lpk_NodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
return;
// update the set of internal nodes
assert( pCut->nNodes < LPK_SIZE_MAX );
memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
pCutNew->nNodes = pCut->nNodes;
pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
// add the marked node
pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj);
/*
if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
{
int x = 0;
printf( "Finish:\n" );
Lpk_NodePrintCut( p, pCutNew );
}
*/
// add the cut to storage
assert( p->nCuts < LPK_CUTS_MAX );
p->nCuts++;
assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
/*
printf( " Creating cut: " );
Lpk_NodePrintCut( p, pCutNew, 1 );
printf( "\n" );
*/
}
/**Function*************************************************************
Synopsis [Computes the set of all cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_NodeCuts( Lpk_Man_t * p )
{
Lpk_Cut_t * pCut, * pCut2;
int i, k, Temp, nMffc, fChanges;
// mark the MFFC of the node with the current trav ID
nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj );
assert( nMffc > 0 );
if ( nMffc == 1 )
return 0;
// initialize the first cut
pCut = p->pCuts; p->nCuts = 1;
pCut->nNodes = 0;
pCut->nNodesDup = 0;
pCut->nLeaves = 1;
pCut->pLeaves[0] = p->pObj->Id;
// assign the signature
Lpk_NodeCutSignature( pCut );
// perform the cut computation
for ( i = 0; i < p->nCuts; i++ )
{
pCut = p->pCuts + i;
if ( pCut->nLeaves == 0 )
continue;
// try to expand the fanins of this cut
for ( k = 0; k < (int)pCut->nLeaves; k++ )
{
// create a new cut
Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
// quit if the number of cuts has exceeded the limit
if ( p->nCuts == LPK_CUTS_MAX )
break;
}
if ( p->nCuts == LPK_CUTS_MAX )
break;
}
if ( p->nCuts == LPK_CUTS_MAX )
p->nNodesOver++;
// record the impact of this node
if ( p->pPars->fSatur )
Lpk_NodeRecordImpact( p );
// compress the cuts by removing empty ones, those with negative Weight, and decomposable ones
p->nEvals = 0;
for ( i = 0; i < p->nCuts; i++ )
{
pCut = p->pCuts + i;
if ( pCut->nLeaves < 2 )
continue;
// compute the number of LUTs neede to implement this cut
// V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 );
pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
if ( pCut->Weight <= 1.0 )
continue;
pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
if ( pCut->fHasDsd )
continue;
p->pEvals[p->nEvals++] = i;
}
if ( p->nEvals == 0 )
return 0;
// sort the cuts by Weight
do {
fChanges = 0;
for ( i = 0; i < p->nEvals - 1; i++ )
{
pCut = p->pCuts + p->pEvals[i];
pCut2 = p->pCuts + p->pEvals[i+1];
if ( pCut->Weight >= pCut2->Weight )
continue;
Temp = p->pEvals[i];
p->pEvals[i] = p->pEvals[i+1];
p->pEvals[i+1] = Temp;
fChanges = 1;
}
} while ( fChanges );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

161
src/opt/lpk/lpkInt.h Normal file
View File

@ -0,0 +1,161 @@
/**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 $]
***********************************************************************/
#ifndef __LPK_INT_H__
#define __LPK_INT_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "abc.h"
#include "kit.h"
#include "if.h"
#include "lpk.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
#define LPK_SIZE_MAX 24 // the largest size of the function
#define LPK_CUTS_MAX 512 // the largest number of cuts considered
typedef struct Lpk_Man_t_ Lpk_Man_t;
typedef struct Lpk_Cut_t_ Lpk_Cut_t;
struct Lpk_Cut_t_
{
unsigned nLeaves : 6; // (L) the number of leaves
unsigned nNodes : 6; // (M) the number of nodes
unsigned nNodesDup : 6; // (Q) nodes outside of MFFC
unsigned nLuts : 6; // (N) the number of LUTs to try
unsigned unused : 6; // unused
unsigned fHasDsd : 1; // set to 1 if the cut has structural DSD (and so cannot be used)
unsigned fMark : 1; // multipurpose mark
unsigned uSign[2]; // the signature
float Weight; // the weight of the cut: (M - Q)/N(V) (the larger the better)
int Gain; // the gain achieved using this cut
int pLeaves[LPK_SIZE_MAX]; // the leaves of the cut
int pNodes[LPK_SIZE_MAX]; // the nodes of the cut
};
struct Lpk_Man_t_
{
// parameters
Lpk_Par_t * pPars; // the set of parameters
// current representation
Abc_Ntk_t * pNtk; // the network
Abc_Obj_t * pObj; // the node to resynthesize
// cut representation
int nMffc; // the size of MFFC of the node
int nCuts; // the total number of cuts
int nCutsMax; // the largest possible number of cuts
int nEvals; // the number of good cuts
Lpk_Cut_t pCuts[LPK_CUTS_MAX]; // the storage for cuts
int pEvals[LPK_CUTS_MAX]; // the good cuts
// visited nodes
Vec_Vec_t * vVisited;
// mapping manager
If_Man_t * pIfMan;
Vec_Int_t * vCover;
Vec_Vec_t * vLevels;
// temporary variables
int fCofactoring; // working in the cofactoring mode
int fCalledOnce; // limits the depth of MUX cofactoring
int pRefs[LPK_SIZE_MAX]; // fanin reference counters
int pCands[LPK_SIZE_MAX]; // internal nodes pointing only to the leaves
// truth table representation
Vec_Ptr_t * vTtElems; // elementary truth tables
Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes
// variable sets
Vec_Int_t * vSets[8];
// statistics
int nNodesTotal; // total number of nodes
int nNodesOver; // nodes with cuts over the limit
int nCutsTotal; // total number of cuts
int nCutsUseful; // useful cuts
int nGainTotal; // the gain in LUTs
int nChanges; // the number of changed nodes
// counter of non-DSD blocks
int nBlocks[17];
// rutime
int timeCuts;
int timeTruth;
int timeEval;
int timeMap;
int timeOther;
int timeTotal;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
#define Lpk_CutForEachLeaf( pNtk, pCut, pObj, i ) \
for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )
#define Lpk_CutForEachNode( pNtk, pCut, pObj, i ) \
for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )
#define Lpk_CutForEachNodeReverse( pNtk, pCut, pObj, i ) \
for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== lpkCut.c =========================================================*/
extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut );
extern int Lpk_NodeCuts( Lpk_Man_t * p );
/*=== lpkMap.c =========================================================*/
extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars );
extern void Lpk_ManStop( Lpk_Man_t * p );
/*=== lpkMap.c =========================================================*/
extern int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk );
extern If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
extern If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult );
/*=== lpkMulti.c =======================================================*/
extern If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves );
/*=== lpkMux.c =========================================================*/
extern If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
extern If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
/*=== lpkSets.c =========================================================*/
extern unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

96
src/opt/lpk/lpkMan.c Normal file
View File

@ -0,0 +1,96 @@
/**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 $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
{
Lpk_Man_t * p;
int i;
assert( pPars->nLutsMax <= 16 );
assert( pPars->nVarsMax > 0 );
p = ALLOC( Lpk_Man_t, 1 );
memset( p, 0, sizeof(Lpk_Man_t) );
p->pPars = pPars;
p->nCutsMax = LPK_CUTS_MAX;
p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) );
p->vCover = Vec_IntAlloc( 1 << 12 );
for ( i = 0; i < 8; i++ )
p->vSets[i] = Vec_IntAlloc(100);
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_ManStop( Lpk_Man_t * p )
{
int i;
for ( i = 0; i < 8; i++ )
Vec_IntFree(p->vSets[i]);
if ( p->pIfMan )
{
void * pPars = p->pIfMan->pPars;
If_ManStop( p->pIfMan );
free( pPars );
}
if ( p->vLevels )
Vec_VecFree( p->vLevels );
if ( p->vVisited )
Vec_VecFree( p->vVisited );
Vec_IntFree( p->vCover );
Vec_PtrFree( p->vTtElems );
Vec_PtrFree( p->vTtNodes );
free( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

349
src/opt/lpk/lpkMap.c Normal file
View File

@ -0,0 +1,349 @@
/**CFile****************************************************************
FileName [lpkMap.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: lpkMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_IfManStart( Lpk_Man_t * p )
{
If_Par_t * pPars;
assert( p->pIfMan == NULL );
// set defaults
pPars = ALLOC( If_Par_t, 1 );
memset( pPars, 0, sizeof(If_Par_t) );
// user-controlable paramters
pPars->nLutSize = p->pPars->nLutSize;
pPars->nCutsMax = 16;
pPars->nFlowIters = 0; // 1
pPars->nAreaIters = 0; // 1
pPars->DelayTarget = -1;
pPars->fPreprocess = 0;
pPars->fArea = 1;
pPars->fFancy = 0;
pPars->fExpRed = 0; //
pPars->fLatchPaths = 0;
pPars->fSeqMap = 0;
pPars->fVerbose = 0;
// internal parameters
pPars->fTruth = 0;
pPars->fUsePerm = 0;
pPars->nLatches = 0;
pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
pPars->pTimesArr = NULL;
pPars->pTimesArr = NULL;
pPars->fUseBdds = 0;
pPars->fUseSops = 0;
pPars->fUseCnfs = 0;
pPars->fUseMv = 0;
// start the mapping manager and set its parameters
p->pIfMan = If_ManStart( pPars );
If_ManSetupSetAll( p->pIfMan, 1000 );
p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
}
/**Function*************************************************************
Synopsis [Transforms the decomposition graph into the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * Lpk_MapPrimeInternal( If_Man_t * pIfMan, Kit_Graph_t * pGraph )
{
Kit_Node_t * pNode;
If_Obj_t * pAnd0, * pAnd1;
int i;
// check for constant function
if ( Kit_GraphIsConst(pGraph) )
return If_ManConst1(pIfMan);
// check for a literal
if ( Kit_GraphIsVar(pGraph) )
return Kit_GraphVar(pGraph)->pFunc;
// build the AIG nodes corresponding to the AND gates of the graph
Kit_GraphForEachNode( pGraph, pNode, i )
{
pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
pNode->pFunc = If_ManCreateAnd( pIfMan,
If_NotCond( If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl ),
If_NotCond( If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl ) );
}
return pNode->pFunc;
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
Kit_Graph_t * pGraph;
Kit_Node_t * pNode;
If_Obj_t * pRes;
int i;
// derive the factored form
pGraph = Kit_TruthToGraph( pTruth, nVars, p->vCover );
if ( pGraph == NULL )
return NULL;
// collect the fanins
Kit_GraphForEachLeaf( pGraph, pNode, i )
pNode->pFunc = ppLeaves[i];
// perform strashing
pRes = Lpk_MapPrimeInternal( p->pIfMan, pGraph );
pRes = If_NotCond( pRes, Kit_GraphIsComplement(pGraph) );
Kit_GraphFree( pGraph );
return pRes;
}
/**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
{
extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
Kit_DsdObj_t * pRoot;
If_Obj_t * pDriver, * ppLeaves[16];
Abc_Obj_t * pLeaf, * pObjNew;
int nGain, i;
// int nOldShared;
// check special cases
pRoot = Kit_DsdNtkRoot( pNtk );
if ( pRoot->Type == KIT_DSD_CONST1 )
{
if ( Kit_DsdLitIsCompl(pNtk->Root) )
pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
else
pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
// perform replacement
pObjNew->Level = p->pObj->Level;
Abc_ObjReplace( p->pObj, pObjNew );
Res_UpdateNetworkLevel( pObjNew, p->vLevels );
p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
return 1;
}
if ( pRoot->Type == KIT_DSD_VAR )
{
pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
// perform replacement
pObjNew->Level = p->pObj->Level;
Abc_ObjReplace( p->pObj, pObjNew );
Res_UpdateNetworkLevel( pObjNew, p->vLevels );
p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
return 1;
}
assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
// start the mapping manager
if ( p->pIfMan == NULL )
Lpk_IfManStart( p );
// prepare the mapping manager
If_ManRestart( p->pIfMan );
// create the PI variables
for ( i = 0; i < p->pPars->nVarsMax; i++ )
ppLeaves[i] = If_ManCreateCi( p->pIfMan );
// set the arrival times
Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
// prepare the PI cuts
If_ManSetupCiCutSets( p->pIfMan );
// create the internal nodes
p->fCalledOnce = 0;
pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
if ( pDriver == NULL )
return 0;
// create the PO node
If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
// perform mapping
p->pIfMan->pPars->fAreaOnly = 1;
If_ManPerformMappingComb( p->pIfMan );
// compute the gain in area
nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
if ( p->pPars->fVeryVerbose )
printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n",
pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level );
// quit if there is no gain
if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
return 0;
// quit if depth increases too much
if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel )
return 0;
// perform replacement
p->nGainTotal += nGain;
p->nChanges++;
// prepare the mapping manager
If_ManCleanNodeCopy( p->pIfMan );
If_ManCleanCutData( p->pIfMan );
// set the PIs of the cut
Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
// get the area of mapping
pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
// perform replacement
pObjNew->Level = p->pObj->Level;
Abc_ObjReplace( p->pObj, pObjNew );
Res_UpdateNetworkLevel( pObjNew, p->vLevels );
return 1;
}
/**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult )
{
Kit_DsdObj_t * pObj;
If_Obj_t * pObjNew, * pFansNew[16];
unsigned i, iLitFanin;
assert( iLit >= 0 );
// consider the case of a gate
pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
{
pObjNew = ppLeaves[Kit_DsdLit2Var(iLit)];
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
}
if ( pObj->Type == KIT_DSD_CONST1 )
{
return If_NotCond( If_ManConst1(p->pIfMan), Kit_DsdLitIsCompl(iLit) );
}
if ( pObj->Type == KIT_DSD_VAR )
{
pObjNew = ppLeaves[Kit_DsdLit2Var(pObj->pFans[0])];
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ^ Kit_DsdLitIsCompl(pObj->pFans[0]) );
}
if ( pObj->Type == KIT_DSD_AND )
{
assert( pObj->nFans == 2 );
pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
return NULL;
pObjNew = If_ManCreateAnd( p->pIfMan, pFansNew[0], pFansNew[1] );
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
}
if ( pObj->Type == KIT_DSD_XOR )
{
int fCompl = Kit_DsdLitIsCompl(iLit);
assert( pObj->nFans == 2 );
pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
return NULL;
fCompl ^= If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
pObjNew = If_ManCreateXor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) );
return If_NotCond( pObjNew, fCompl );
}
assert( pObj->Type == KIT_DSD_PRIME );
p->nBlocks[pObj->nFans]++;
// solve for the inputs
Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
{
if ( i == 0 )
pFansNew[i] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
else
pFansNew[i] = Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
if ( pFansNew[i] == NULL )
return NULL;
}
/*
if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
{
pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
}
*/
// find best cofactoring variable
if ( pObj->nFans > 3 && !p->fCalledOnce )
// pObjNew = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
pObjNew = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
else
pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

495
src/opt/lpk/lpkMulti.c Normal file
View File

@ -0,0 +1,495 @@
/**CFile****************************************************************
FileName [lpkMulti.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: lpkMulti.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Records variable order.]
Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_CreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] )
{
Kit_DsdObj_t * pObj;
unsigned uSuppFanins, k;
int Above[16], Below[16];
int nAbove, nBelow, iFaninLit, i, x, y;
// iterate through the nodes
Kit_DsdNtkForEachObj( pNtk, pObj, i )
{
// collect fanin support of this node
nAbove = 0;
uSuppFanins = 0;
Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
{
if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
Above[nAbove++] = Kit_DsdLit2Var(iFaninLit);
else
uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
}
// find the below variables
nBelow = 0;
for ( y = 0; y < 16; y++ )
if ( uSuppFanins & (1 << y) )
Below[nBelow++] = y;
// create all pairs
for ( x = 0; x < nAbove; x++ )
for ( y = 0; y < nBelow; y++ )
pTable[Above[x]][Below[y]]++;
}
}
/**Function*************************************************************
Synopsis [Creates commmon variable order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_CreateCommonOrder( char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose )
{
int Score[16] = {0}, pPres[16];
int i, y, x, iVarBest, ScoreMax, PrioCount;
// mark the present variables
for ( i = 0; i < nVars; i++ )
pPres[i] = 1;
// remove cofactored variables
for ( i = 0; i < nCBars; i++ )
pPres[piCofVar[i]] = 0;
// compute scores for each leaf
for ( i = 0; i < nVars; i++ )
{
if ( pPres[i] == 0 )
continue;
for ( y = 0; y < nVars; y++ )
Score[i] += pTable[i][y];
for ( x = 0; x < nVars; x++ )
Score[i] -= pTable[x][i];
}
// print the scores
if ( fVerbose )
{
printf( "Scores: " );
for ( i = 0; i < nVars; i++ )
printf( "%c=%d ", 'a'+i, Score[i] );
printf( " " );
printf( "Prios: " );
}
// derive variable priority
// variables with equal score receive the same priority
for ( i = 0; i < nVars; i++ )
pPrios[i] = 16;
// iterate until variables remain
for ( PrioCount = 1; ; PrioCount++ )
{
// find the present variable with the highest score
iVarBest = -1;
ScoreMax = -100000;
for ( i = 0; i < nVars; i++ )
{
if ( pPres[i] == 0 )
continue;
if ( ScoreMax < Score[i] )
{
ScoreMax = Score[i];
iVarBest = i;
}
}
if ( iVarBest == -1 )
break;
// give the next priority to all vars having this score
if ( fVerbose )
printf( "%d=", PrioCount );
for ( i = 0; i < nVars; i++ )
{
if ( pPres[i] == 0 )
continue;
if ( Score[i] == ScoreMax )
{
pPrios[i] = PrioCount;
pPres[i] = 0;
if ( fVerbose )
printf( "%c", 'a'+i );
}
}
if ( fVerbose )
printf( " " );
}
if ( fVerbose )
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Finds components with the highest priority.]
Description [Returns the number of components selected.]
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_FindHighest( Kit_DsdNtk_t ** ppNtks, int * piLits, int nSize, int * pPrio, int * pDecision )
{
Kit_DsdObj_t * pObj;
unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge;
int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv;
// find individual support and total support
uSuppTotal = 0;
for ( i = 0; i < nSize; i++ )
{
pTriv[i] = 1;
if ( piLits[i] < 0 )
uSupps[i] = 0;
else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) )
uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] );
else
{
pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
if ( pObj->Type == KIT_DSD_PRIME )
{
pTriv[i] = 0;
uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] );
}
else
{
assert( pObj->nFans == 2 );
if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) )
pTriv[i] = 0;
uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] );
}
uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
}
assert( uSupps[i] <= 0xFFFF );
uSuppTotal |= uSupps[i];
}
if ( uSuppTotal == 0 )
return 0;
// find one support variable with the highest priority
PrioMin = ABC_INFINITY;
iVarMax = -1;
for ( i = 0; i < 16; i++ )
if ( uSuppTotal & (1 << i) )
if ( PrioMin > pPrio[i] )
{
PrioMin = pPrio[i];
iVarMax = i;
}
assert( iVarMax != -1 );
// select components, which have this variable
nComps = 0;
fOneNonTriv = 0;
uSuppLarge = 0;
for ( i = 0; i < nSize; i++ )
if ( uSupps[i] & (1<<iVarMax) )
{
if ( pTriv[i] || !fOneNonTriv )
{
if ( !pTriv[i] )
{
uSuppLarge = uSupps[i];
fOneNonTriv = 1;
}
pDecision[i] = 1;
nComps++;
}
else
pDecision[i] = 0;
}
else
pDecision[i] = 0;
// add other non-trivial not-taken components whose support is contained in the current large component support
if ( fOneNonTriv )
for ( i = 0; i < nSize; i++ )
if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 )
{
pDecision[i] = 1;
nComps++;
}
return nComps;
}
/**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 )
{
Kit_DsdObj_t * pObj;
If_Obj_t * pObjsNew[4][8], * pResPrev;
int piLitsNew[8], pDecision[8];
int i, k, nComps, nSize;
// find which of the variables is highest in the order
nSize = (1 << nCBars);
nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision );
if ( nComps == 0 )
return If_Not( If_ManConst1(p->pIfMan) );
// iterate over the nodes
if ( p->pPars->fVeryVerbose )
printf( "Decision: " );
for ( i = 0; i < nSize; i++ )
{
if ( pDecision[i] )
{
if ( p->pPars->fVeryVerbose )
printf( "%d ", i );
assert( piLits[i] >= 0 );
pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
if ( pObj == NULL )
piLitsNew[i] = -2;
else if ( pObj->Type == KIT_DSD_PRIME )
piLitsNew[i] = pObj->pFans[0];
else
piLitsNew[i] = pObj->pFans[1];
}
else
piLitsNew[i] = piLits[i];
}
if ( p->pPars->fVeryVerbose )
printf( "\n" );
// call again
pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio );
// create new set of nodes
for ( i = 0; i < nSize; i++ )
{
if ( pDecision[i] )
pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev );
else if ( piLits[i] == -1 )
pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan);
else if ( piLits[i] == -2 )
pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) );
else
pObjsNew[nCBars][i] = pResPrev;
}
// create MUX using these outputs
for ( k = nCBars; k > 0; k-- )
{
nSize /= 2;
for ( i = 0; i < nSize; i++ )
pObjsNew[k-1][i] = If_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
}
assert( nSize == 1 );
return pObjsNew[0][0];
}
/**Function*************************************************************
Synopsis [Prepares the mapping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
static Counter = 0;
If_Obj_t * pResult;
Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
Kit_DsdObj_t * pRoot;
int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16];
int i, k, nCBars, nSize, nMemSize;
unsigned * ppCofs[4][8], uSupport;
char pTable[16][16] = {0};
int fVerbose = p->pPars->fVeryVerbose;
Counter++;
// printf( "Run %d.\n", Counter );
// allocate storage for cofactors
nMemSize = Kit_TruthWordNum(nVars);
ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
nSize = 0;
for ( i = 0; i < 4; i++ )
for ( k = 0; k < 8; k++ )
ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
assert( nSize == 32 );
// find the best cofactoring variables
nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
// nCBars = 2;
// piCofVar[0] = 0;
// piCofVar[1] = 1;
// copy the function
Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
// decompose w.r.t. these variables
for ( k = 0; k < nCBars; k++ )
{
nSize = (1 << k);
for ( i = 0; i < nSize; i++ )
{
Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
}
}
nSize = (1 << nCBars);
// compute DSD networks
for ( i = 0; i < nSize; i++ )
{
ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
Kit_DsdNtkFree( pTemp );
if ( fVerbose )
{
printf( "Cof%d%d: ", nCBars, i );
Kit_DsdPrint( stdout, ppNtks[i] );
}
}
// compute variable frequences
for ( i = 0; i < nSize; i++ )
{
uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
for ( k = 0; k < nVars; k++ )
if ( uSupport & (1<<k) )
pFreqs[k]++;
}
// find common variable order
for ( i = 0; i < nSize; i++ )
{
Kit_DsdGetSupports( ppNtks[i] );
Lpk_CreateVarOrder( ppNtks[i], pTable );
}
Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose );
// update priorities with frequences
for ( i = 0; i < nVars; i++ )
pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i;
if ( fVerbose )
printf( "After restructuring with priority:\n" );
if ( Counter == 1 )
{
int x = 0;
}
// transform all networks according to the variable order
for ( i = 0; i < nSize; i++ )
{
ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
Kit_DsdNtkFree( pTemp );
Kit_DsdGetSupports( ppNtks[i] );
assert( ppNtks[i]->pSupps[0] <= 0xFFFF );
// undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
Kit_DsdRotate( ppNtks[i], pFreqs );
// print the resulting networks
if ( fVerbose )
{
printf( "Cof%d%d: ", nCBars, i );
Kit_DsdPrint( stdout, ppNtks[i] );
}
}
for ( i = 0; i < nSize; i++ )
{
// collect the roots
pRoot = Kit_DsdNtkRoot(ppNtks[i]);
if ( pRoot->Type == KIT_DSD_CONST1 )
piLits[i] = Kit_DsdLitIsCompl(ppNtks[i]->Root)? -2: -1;
else if ( pRoot->Type == KIT_DSD_VAR )
piLits[i] = Kit_DsdLitNotCond( pRoot->pFans[0], Kit_DsdLitIsCompl(ppNtks[i]->Root) );
else
piLits[i] = ppNtks[i]->Root;
}
// recursively construct AIG for mapping
p->fCofactoring = 1;
pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios );
p->fCofactoring = 0;
if ( fVerbose )
printf( "\n" );
// verify the transformations
nSize = (1 << nCBars);
for ( i = 0; i < nSize; i++ )
Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] );
// mux the truth tables
for ( k = nCBars-1; k >= 0; k-- )
{
nSize = (1 << k);
for ( i = 0; i < nSize; i++ )
Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] );
}
if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) )
printf( "Verification failed.\n" );
// free the networks
for ( i = 0; i < 8; i++ )
if ( ppNtks[i] )
Kit_DsdNtkFree( ppNtks[i] );
free( ppCofs[0][0] );
return pResult;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

257
src/opt/lpk/lpkMux.c Normal file
View File

@ -0,0 +1,257 @@
/**CFile****************************************************************
FileName [lpkMux.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: lpkMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Find the best cofactoring variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
{
// Kit_DsdNtk_t * ppNtks[2], * pTemp;
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
// int nPrimeSizeCur0, nPrimeSizeCur1, nPrimeSizeCur, nPrimeSizeMin;
// iterate through variables
iBestVar = -1;
nSuppSizeMin = ABC_INFINITY;
// nPrimeSizeMin = ABC_INFINITY;
for ( i = 0; i < nVars; i++ )
{
// cofactor the functiona and get support sizes
Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
/*
// check the size of the largest prime components
ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
// compute the largest non-decomp block
nPrimeSizeCur0 = Kit_DsdNonDsdSizeMax(ppNtks[0]);
nPrimeSizeCur1 = Kit_DsdNonDsdSizeMax(ppNtks[1]);
nPrimeSizeCur = KIT_MAX( nPrimeSizeCur0, nPrimeSizeCur1 );
printf( "Evaluating variable %c:\n", 'a'+i );
// Kit_DsdPrintExpanded( ppNtks[0] );
// Kit_DsdPrintExpanded( ppNtks[1] );
ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
Kit_DsdNtkFree( pTemp );
ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );
Kit_DsdNtkFree( pTemp );
Kit_DsdPrint( stdout, ppNtks[0] );
Kit_DsdPrint( stdout, ppNtks[1] );
// Lpk_DsdEvalSets( p, ppNtks[0], ppNtks[1] );
// free the networks
Kit_DsdNtkFree( ppNtks[0] );
Kit_DsdNtkFree( ppNtks[1] );
*/
// compare this variable with other variables
if ( nSuppSizeMin > nSuppSizeCur ) //|| (nSuppSizeMin == nSuppSizeCur && nPrimeSizeMin > nPrimeSizeCur ) )
{
nSuppSizeMin = nSuppSizeCur;
// nPrimeSizeMin = nPrimeSizeCur;
iBestVar = i;
}
}
printf( "\n" );
assert( iBestVar != -1 );
return iBestVar;
}
/**Function*************************************************************
Synopsis [Maps the function by the best cofactoring.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
If_Obj_t * pObj0, * pObj1;
Kit_DsdNtk_t * ppNtks[2];
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
int iBestVar;
assert( nVars > 3 );
p->fCalledOnce = 1;
// cofactor w.r.t. the best variable
iBestVar = Lpk_MapTreeBestVar( p, pTruth, nVars );
Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
// decompose the functions
ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
if ( p->pPars->fVeryVerbose )
{
printf( "Cofactoring w.r.t. var %c (%d -> %d+%d supp vars):\n",
'a'+iBestVar, nVars, Kit_TruthSupportSize(pCof0, nVars), Kit_TruthSupportSize(pCof1, nVars) );
Kit_DsdPrintExpanded( ppNtks[0] );
Kit_DsdPrintExpanded( ppNtks[1] );
}
// map the DSD structures
pObj0 = Lpk_MapTree_rec( p, ppNtks[0], ppLeaves, ppNtks[0]->Root, NULL );
pObj1 = Lpk_MapTree_rec( p, ppNtks[1], ppLeaves, ppNtks[1]->Root, NULL );
Kit_DsdNtkFree( ppNtks[0] );
Kit_DsdNtkFree( ppNtks[1] );
return If_ManCreateMux( p->pIfMan, pObj0, pObj1, ppLeaves[iBestVar] );
}
/**Function*************************************************************
Synopsis [Implements support-reducing decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
Kit_DsdNtk_t * pNtkDec, * pNtkComp;
If_Obj_t * pObjNew;
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
unsigned * pDec0 = Vec_PtrEntry( p->vTtNodes, 2 );
unsigned * pDec1 = Vec_PtrEntry( p->vTtNodes, 3 );
unsigned * pDec = Vec_PtrEntry( p->vTtNodes, 4 );
unsigned * pCo00 = Vec_PtrEntry( p->vTtNodes, 5 );
unsigned * pCo01 = Vec_PtrEntry( p->vTtNodes, 6 );
unsigned * pCo10 = Vec_PtrEntry( p->vTtNodes, 7 );
unsigned * pCo11 = Vec_PtrEntry( p->vTtNodes, 8 );
unsigned * pCo0 = Vec_PtrEntry( p->vTtNodes, 9 );
unsigned * pCo1 = Vec_PtrEntry( p->vTtNodes, 10 );
unsigned * pCo = Vec_PtrEntry( p->vTtNodes, 11 );
int TrueMint0, TrueMint1;
int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
// determine if supp-red decomposition exists
uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
if ( uSubsets == 0 )
return NULL;
// get the bound sets
uSubset0 = uSubsets & 0xFFFF;
uSubset1 = uSubsets >> 16;
// get the cofactors
Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
// find any true assignments of the cofactors
TrueMint0 = Kit_TruthFindFirstBit( pCof0, nVars );
TrueMint1 = Kit_TruthFindFirstBit( pCof1, nVars );
assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
// cofactor the cofactors according to these minterms
Kit_TruthCopy( pDec0, pCof0, nVars );
Kit_TruthCopy( pDec1, pCof1, nVars );
for ( i = 0; i < nVars; i++ )
if ( !(uSubset0 & (1 << i)) )
{
if ( TrueMint0 & (1 << i) )
Kit_TruthCofactor1( pDec0, nVars, i );
else
Kit_TruthCofactor0( pDec0, nVars, i );
}
for ( i = 0; i < nVars; i++ )
if ( !(uSubset1 & (1 << i)) )
{
if ( TrueMint1 & (1 << i) )
Kit_TruthCofactor1( pDec1, nVars, i );
else
Kit_TruthCofactor0( pDec1, nVars, i );
}
// get the decomposed function
Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
// derive the remainders
Kit_TruthAndPhase( pCo00, pCof0, pDec0, nVars, 0, 1 );
Kit_TruthAndPhase( pCo01, pCof0, pDec0, nVars, 0, 0 );
Kit_TruthAndPhase( pCo10, pCof1, pDec1, nVars, 0, 1 );
Kit_TruthAndPhase( pCo11, pCof1, pDec1, nVars, 0, 0 );
// quantify bound set variables
for ( i = 0; i < nVars; i++ )
if ( uSubset0 & (1 << i) )
{
Kit_TruthExist( pCo00, nVars, i );
Kit_TruthExist( pCo01, nVars, i );
}
for ( i = 0; i < nVars; i++ )
if ( uSubset1 & (1 << i) )
{
Kit_TruthExist( pCo10, nVars, i );
Kit_TruthExist( pCo11, nVars, i );
}
// derive the functions by composing them with the new variable (iVarReused)
Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
// derive the composition function
Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
// process the decomposed function
pNtkDec = Kit_DsdDecompose( pDec, nVars );
Kit_DsdPrint( stdout, pNtkDec );
ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
Kit_DsdNtkFree( pNtkDec );
// process the composition function
pNtkComp = Kit_DsdDecompose( pCo, nVars );
Kit_DsdPrint( stdout, pNtkComp );
pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
Kit_DsdNtkFree( pNtkComp );
return pObjNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

399
src/opt/lpk/lpkSets.c Normal file
View File

@ -0,0 +1,399 @@
/**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 $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Lpk_Set_t_ Lpk_Set_t;
struct Lpk_Set_t_
{
char iVar; // the cofactoring variable
char Over; // the overlap in supports
char SRed; // the support reduction
char Size; // the size of the boundset
unsigned uSubset0; // the first subset (with removed)
unsigned uSubset1; // the second subset (with removed)
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Recursively computes decomposable subsets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
{
unsigned i, iLitFanin, uSupport, uSuppCur;
Kit_DsdObj_t * pObj;
// consider the case of simple gate
pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
if ( pObj == NULL )
return (1 << Kit_DsdLit2Var(iLit));
if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
{
unsigned uSupps[16], Limit, s;
uSupport = 0;
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
uSupps[i] = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
uSupport |= uSupps[i];
}
// create all subsets, except empty and full
Limit = (1 << pObj->nFans) - 1;
for ( s = 1; s < Limit; s++ )
{
uSuppCur = 0;
for ( i = 0; i < pObj->nFans; i++ )
if ( s & (1 << i) )
uSuppCur |= uSupps[i];
Vec_IntPush( vSets, uSuppCur );
}
return uSupport;
}
assert( pObj->Type == KIT_DSD_PRIME );
// get the cumulative support of all fanins
uSupport = 0;
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
uSuppCur = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
uSupport |= uSuppCur;
Vec_IntPush( vSets, uSuppCur );
}
return uSupport;
}
/**Function*************************************************************
Synopsis [Computes the set of subsets of decomposable variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
{
unsigned uSupport, Entry, i;
assert( p->nVars <= 16 );
Vec_IntClear( vSets );
Vec_IntPush( vSets, 0 );
if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
return 0;
if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
{
uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
Vec_IntPush( vSets, uSupport );
return uSupport;
}
uSupport = Lpk_ComputeSets_rec( p, p->Root, vSets );
assert( (uSupport & 0xFFFF0000) == 0 );
Vec_IntPush( vSets, uSupport );
// set the remaining variables
Vec_IntForEachEntry( vSets, Entry, i )
Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
return uSupport;
}
/**Function*************************************************************
Synopsis [Prints the sets of subsets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_PrintSetOne( int uSupport )
{
unsigned k;
for ( k = 0; k < 16; k++ )
if ( uSupport & (1<<k) )
printf( "%c", 'a'+k );
printf( " " );
}
/**Function*************************************************************
Synopsis [Prints the sets of subsets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_PrintSets( Vec_Int_t * vSets )
{
unsigned uSupport, i;
printf( "Subsets(%d): ", Vec_IntSize(vSets) );
Vec_IntForEachEntry( vSets, uSupport, i )
Lpk_PrintSetOne( uSupport );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Computes maximal support reducing bound-sets.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCofVar,
Lpk_Set_t * pStore, int * pSize, int nSizeLimit )
{
static int nTravId = 0; // the number of the times this is visited
static int TravId[1<<16] = {0}; // last visited
static char SRed[1<<16]; // best support reduction
static char Over[1<<16]; // best overlaps
static unsigned Parents[1<<16]; // best set of parents
static unsigned short Used[1<<16]; // storage for used subsets
int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s;
unsigned Entry, Entry0, Entry1;
unsigned uSupp, uSupp0, uSupp1, uSuppTotal;
Lpk_Set_t * pEntry;
if ( nTravId == (1 << 30) )
memset( TravId, 0, sizeof(int) * (1 << 16) );
// collect support reducing subsets
nUsed = 0;
nTravId++;
uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar);
Vec_IntForEachEntry( vSets0, Entry0, i )
Vec_IntForEachEntry( vSets1, Entry1, k )
{
uSupp0 = (Entry0 & 0xFFFF);
uSupp1 = (Entry1 & 0xFFFF);
// skip trivial
if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal )
continue;
if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) )
continue;
// get the entry
Entry = Entry0 | Entry1;
uSupp = Entry & 0xFFFF;
// set the bound set size
nSuppSize = Kit_WordCountOnes( uSupp );
// get the number of overlapping vars
nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) );
// get the support reduction
nSuppRed = nSuppSize - 1 - nSuppOver;
// only consider support-reducing subsets
if ( nSuppRed <= 0 )
continue;
// check if this support is already used
if ( TravId[uSupp] < nTravId )
{
Used[nUsed++] = uSupp;
TravId[uSupp] = nTravId;
SRed[uSupp] = nSuppRed;
Over[uSupp] = nSuppOver;
Parents[uSupp] = (k << 16) | i;
}
else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed )
{
TravId[uSupp] = nTravId;
SRed[uSupp] = nSuppRed;
Over[uSupp] = nSuppOver;
Parents[uSupp] = (k << 16) | i;
}
}
// check if there are non-overlapping
nMinOver = 1000;
for ( s = 0; s < nUsed; s++ )
if ( nMinOver > Over[Used[s]] )
nMinOver = Over[Used[s]];
// collect the accumulated ones
for ( s = 0; s < nUsed; s++ )
if ( Over[Used[s]] == nMinOver )
{
// save the entry
if ( *pSize == nSizeLimit )
return;
pEntry = pStore + (*pSize)++;
i = Parents[Used[s]] & 0xFFFF;
k = Parents[Used[s]] >> 16;
pEntry->uSubset0 = Vec_IntEntry(vSets0, i);
pEntry->uSubset1 = Vec_IntEntry(vSets1, k);
Entry = pEntry->uSubset0 | pEntry->uSubset1;
// record the cofactoring variable
pEntry->iVar = iCofVar;
// set the bound set size
pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF );
// get the number of overlapping vars
pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
// get the support reduction
pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
assert( pEntry->SRed > 0 );
}
}
/**Function*************************************************************
Synopsis [Prints one set.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_MapSuppPrintSet( Lpk_Set_t * pSet, int i )
{
unsigned Entry;
Entry = pSet->uSubset0 | pSet->uSubset1;
printf( "%2d : ", i );
printf( "Var = %c ", 'a' + pSet->iVar );
printf( "Size = %2d ", pSet->Size );
printf( "Over = %2d ", pSet->Over );
printf( "SRed = %2d ", pSet->SRed );
Lpk_PrintSetOne( Entry );
printf( " " );
Lpk_PrintSetOne( Entry >> 16 );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Evaluates the cofactors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused )
{
static int nStoreSize = 256;
static Lpk_Set_t pStore[256], * pSet, * pSetBest;
Kit_DsdNtk_t * ppNtks[2], * pTemp;
Vec_Int_t * vSets0 = p->vSets[0];
Vec_Int_t * vSets1 = p->vSets[1];
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
int nSets, i, SizeMax;
unsigned Entry;
// collect decomposable subsets for each pair of cofactors
nSets = 0;
for ( i = 0; i < nVars; i++ )
{
printf( "Evaluating variable %c:\n", 'a'+i );
// evaluate the cofactor pair
Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
// decompose and expand
ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
Kit_DsdPrint( stdout, ppNtks[0] );
Kit_DsdPrint( stdout, ppNtks[1] );
// compute subsets
Lpk_ComputeSets( ppNtks[0], vSets0 );
Lpk_ComputeSets( ppNtks[1], vSets1 );
// print subsets
Lpk_PrintSets( vSets0 );
Lpk_PrintSets( vSets1 );
// free the networks
Kit_DsdNtkFree( ppNtks[0] );
Kit_DsdNtkFree( ppNtks[1] );
// evaluate the pair
Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize );
}
// print the results
printf( "\n" );
for ( i = 0; i < nSets; i++ )
Lpk_MapSuppPrintSet( pStore + i, i );
// choose the best subset
SizeMax = 0;
pSetBest = NULL;
for ( i = 0; i < nSets; i++ )
{
pSet = pStore + i;
if ( pSet->Size > p->pPars->nLutSize - 1 )
continue;
if ( SizeMax < pSet->Size )
{
pSetBest = pSet;
SizeMax = pSet->Size;
}
}
if ( pSetBest == NULL )
{
printf( "Could not select a subset.\n" );
return 0;
}
else
{
printf( "Selected the following subset:\n" );
Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
}
// prepare the return result
// get the remaining variables
Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16));
// get the variables to be removed
Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry;
// make sure there are some - otherwise it is not supp-red
assert( Entry );
// remember the first such variable
*piVarReused = Kit_WordFindFirstBit( Entry );
*piVar = pSetBest->iVar;
return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

48
src/opt/lpk/lpk_.c Normal file
View File

@ -0,0 +1,48 @@
/**CFile****************************************************************
FileName [lpk_.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: lpk_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

7
src/opt/lpk/module.make Normal file
View File

@ -0,0 +1,7 @@
SRC += src/aig/lpk/lpkCore.c \
src/aig/lpk/lpkCut.c \
src/aig/lpk/lpkMan.c \
src/aig/lpk/lpkMap.c \
src/aig/lpk/lpkMulti.c \
src/aig/lpk/lpkMux.c \
src/aig/lpk/lpkSets.c