Skip to content

A
abc
Commit 3d6eac52 by Alan Mishchenko
Options

Changes to LUT mappers.

parent de48fd79
Showing with 710 additions and 255 deletions
src/base/abci/abc.c
...@@ -231,6 +231,10 @@ static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, cha ...@@ -231,6 +231,10 @@ static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, cha
//static int Abc_CommandFpgaFast ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandFpgaFast ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIf ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIfif ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIfif ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDsdSave ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDsdLoad ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDsdFree ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDsdPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -784,6 +788,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -784,6 +788,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga", Abc_CommandFpgaFast, 1 ); // Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga", Abc_CommandFpgaFast, 1 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "if", Abc_CommandIf, 1 ); Cmd_CommandAdd( pAbc, "FPGA mapping", "if", Abc_CommandIf, 1 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "ifif", Abc_CommandIfif, 1 ); Cmd_CommandAdd( pAbc, "FPGA mapping", "ifif", Abc_CommandIfif, 1 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "dsd_save", Abc_CommandDsdSave, 0 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "dsd_load", Abc_CommandDsdLoad, 0 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "dsd_free", Abc_CommandDsdFree, 0 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "dsd_ps", Abc_CommandDsdPs, 0 );
// Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 ); // Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
...@@ -15088,6 +15096,29 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -15088,6 +15096,29 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fUsePerm = 1; pPars->fUsePerm = 1;
} }
if ( pPars->fUseDsd )
{
int LutSize = (pPars->pLutStruct && pPars->pLutStruct[2] == 0)? pPars->pLutStruct[0] - '0' : 0;
If_DsdMan_t * p = (If_DsdMan_t *)Abc_FrameReadManDsd();
if ( pPars->pLutStruct && pPars->pLutStruct[2] != 0 )
{
printf( "DSD only works for LUT structures XY.\n" );
return 0;
}
if ( p && pPars->nLutSize > If_DsdManVarNum(p) )
{
printf( "DSD manager has incompatible number of variables.\n" );
return 0;
}
if ( p && LutSize != If_DsdManLutSize(p) )
{
printf( "DSD manager has different LUT size.\n" );
return 0;
}
if ( p == NULL )
Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, LutSize) );
}
if ( pPars->fUserRecLib ) if ( pPars->fUserRecLib )
{ {
assert( Abc_NtkRecIsRunning3() ); assert( Abc_NtkRecIsRunning3() );
...@@ -15322,6 +15353,210 @@ usage: ...@@ -15322,6 +15353,210 @@ usage:
return 1; return 1;
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDsdSave( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char * FileName;
char ** pArgvNew;
int nArgcNew;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( !Abc_FrameReadManDsd() )
{
Abc_Print( -1, "The DSD manager is not started.\n" );
return 1;
}
pArgvNew = argv + globalUtilOptind;
nArgcNew = argc - globalUtilOptind;
if ( nArgcNew != 1 )
{
Abc_Print( -1, "File name is not given on the command line.\n" );
return 1;
}
// get the input file name
FileName = (nArgcNew == 1) ? pArgvNew[0] : NULL;
If_DsdManSave( (If_DsdMan_t *)Abc_FrameReadManDsd(), FileName );
return 0;
usage:
Abc_Print( -2, "usage: dsd_save [-h] <file>\n" );
Abc_Print( -2, "\t saves DSD manager into a file\n");
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : (optional) file name to write\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDsdLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char * FileName, * pTemp;
char ** pArgvNew;
int c, nArgcNew;
FILE * pFile;
If_DsdMan_t * pDsdMan;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
pArgvNew = argv + globalUtilOptind;
nArgcNew = argc - globalUtilOptind;
if ( nArgcNew != 1 )
{
Abc_Print( -1, "File name is not given on the command line.\n" );
return 1;
}
// get the input file name
FileName = pArgvNew[0];
// fix the wrong symbol
for ( pTemp = FileName; *pTemp; pTemp++ )
if ( *pTemp == '>' )
*pTemp = '\\';
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
pDsdMan = If_DsdManLoad(FileName);
if ( pDsdMan == NULL )
return 1;
Abc_FrameSetManDsd( pDsdMan );
return 0;
usage:
Abc_Print( -2, "usage: dsd_load [-h] <file>\n" );
Abc_Print( -2, "\t loads DSD manager from file\n");
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : file name to read\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDsdFree( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( !Abc_FrameReadManDsd() )
{
Abc_Print( 1, "The DSD manager is not started.\n" );
return 0;
}
Abc_FrameSetManDsd( NULL );
return 0;
usage:
Abc_Print( -2, "usage: dsd_ps [-h]\n" );
Abc_Print( -2, "\t deletes DSD manager\n" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c, fPrintLib = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
{
switch ( c )
{
case 'p':
fPrintLib ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( !Abc_FrameReadManDsd() )
{
Abc_Print( 1, "The DSD manager is not started.\n" );
return 0;
}
If_DsdManPrint( (If_DsdMan_t *)Abc_FrameReadManDsd(), NULL, 0 );
return 0;
usage:
Abc_Print( -2, "usage: dsd_ps [-h]\n" );
Abc_Print( -2, "\t prints statistics of DSD manager\n" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function************************************************************* /**Function*************************************************************
src/base/abci/abcIf.c
...@@ -137,6 +137,15 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) ...@@ -137,6 +137,15 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
if ( pPars->fPower ) if ( pPars->fPower )
Abc_NtkIfComputeSwitching( pNtk, pIfMan ); Abc_NtkIfComputeSwitching( pNtk, pIfMan );
// create DSD manager
if ( pPars->fUseDsd )
{
If_DsdMan_t * p = (If_DsdMan_t *)Abc_FrameReadManDsd();
assert( pPars->nLutSize <= If_DsdManVarNum(p) );
assert( (pPars->pLutStruct == NULL && If_DsdManLutSize(p) == 0) || (pPars->pLutStruct && pPars->pLutStruct[0] - '0' == If_DsdManLutSize(p)) );
pIfMan->pIfDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
}
// perform FPGA mapping // perform FPGA mapping
if ( !If_ManPerformMapping( pIfMan ) ) if ( !If_ManPerformMapping( pIfMan ) )
{ {
......
src/base/main/main.h
...@@ -106,6 +106,8 @@ extern ABC_DLL void * Abc_FrameReadLibVer(); ...@@ -106,6 +106,8 @@ extern ABC_DLL void * Abc_FrameReadLibVer();
extern ABC_DLL void * Abc_FrameReadLibScl(); extern ABC_DLL void * Abc_FrameReadLibScl();
extern ABC_DLL void * Abc_FrameReadManDd(); extern ABC_DLL void * Abc_FrameReadManDd();
extern ABC_DLL void * Abc_FrameReadManDec(); extern ABC_DLL void * Abc_FrameReadManDec();
extern ABC_DLL void * Abc_FrameReadManDsd();
extern ABC_DLL char * Abc_FrameReadFlag( char * pFlag ); extern ABC_DLL char * Abc_FrameReadFlag( char * pFlag );
extern ABC_DLL int Abc_FrameIsFlagEnabled( char * pFlag ); extern ABC_DLL int Abc_FrameIsFlagEnabled( char * pFlag );
extern ABC_DLL int Abc_FrameIsBatchMode(); extern ABC_DLL int Abc_FrameIsBatchMode();
...@@ -138,6 +140,7 @@ extern ABC_DLL void Abc_FrameSetFlag( char * pFlag, char * pValue ); ...@@ -138,6 +140,7 @@ extern ABC_DLL void Abc_FrameSetFlag( char * pFlag, char * pValue );
extern ABC_DLL void Abc_FrameSetCex( Abc_Cex_t * pCex ); extern ABC_DLL void Abc_FrameSetCex( Abc_Cex_t * pCex );
extern ABC_DLL void Abc_FrameSetNFrames( int nFrames ); extern ABC_DLL void Abc_FrameSetNFrames( int nFrames );
extern ABC_DLL void Abc_FrameSetStatus( int Status ); extern ABC_DLL void Abc_FrameSetStatus( int Status );
extern ABC_DLL void Abc_FrameSetManDsd( void * pMan );
extern ABC_DLL int Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum ); extern ABC_DLL int Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
......
src/base/main/mainFrame.c
...@@ -22,6 +22,7 @@ ...@@ -22,6 +22,7 @@
#include "mainInt.h" #include "mainInt.h"
#include "bool/dec/dec.h" #include "bool/dec/dec.h"
#include "misc/extra/extraBdd.h" #include "misc/extra/extraBdd.h"
#include "map/if/if.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
...@@ -59,6 +60,7 @@ void * Abc_FrameReadLibVer() { return s_GlobalFr ...@@ -59,6 +60,7 @@ void * Abc_FrameReadLibVer() { return s_GlobalFr
void * Abc_FrameReadLibScl() { return s_GlobalFrame->pLibScl; } void * Abc_FrameReadLibScl() { return s_GlobalFrame->pLibScl; }
void * Abc_FrameReadManDd() { if ( s_GlobalFrame->dd == NULL ) s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); return s_GlobalFrame->dd; } void * Abc_FrameReadManDd() { if ( s_GlobalFrame->dd == NULL ) s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); return s_GlobalFrame->dd; }
void * Abc_FrameReadManDec() { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart(); return s_GlobalFrame->pManDec; } void * Abc_FrameReadManDec() { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart(); return s_GlobalFrame->pManDec; }
void * Abc_FrameReadManDsd() { return s_GlobalFrame->pManDsd; }
char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagReadByName( s_GlobalFrame, pFlag ); } char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagReadByName( s_GlobalFrame, pFlag ); }
int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFrame->nFrames; } int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFrame->nFrames; }
...@@ -85,6 +87,7 @@ void Abc_FrameSetFlag( char * pFlag, char * pValue ) { Cmd_FlagUpdateVal ...@@ -85,6 +87,7 @@ void Abc_FrameSetFlag( char * pFlag, char * pValue ) { Cmd_FlagUpdateVal
void Abc_FrameSetCex( Abc_Cex_t * pCex ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex; } void Abc_FrameSetCex( Abc_Cex_t * pCex ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->pCex = pCex; }
void Abc_FrameSetNFrames( int nFrames ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->nFrames = nFrames; } void Abc_FrameSetNFrames( int nFrames ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->nFrames = nFrames; }
void Abc_FrameSetStatus( int Status ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->Status = Status; } void Abc_FrameSetStatus( int Status ) { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->Status = Status; }
void Abc_FrameSetManDsd( void * pMan ) { if (s_GlobalFrame->pManDsd) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd, 0); s_GlobalFrame->pManDsd = pMan; }
int Abc_FrameIsBatchMode() { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0; } int Abc_FrameIsBatchMode() { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0; }
...@@ -194,6 +197,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) ...@@ -194,6 +197,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
if ( p->pSave2 ) Aig_ManStop( (Aig_Man_t *)p->pSave2 ); if ( p->pSave2 ) Aig_ManStop( (Aig_Man_t *)p->pSave2 );
if ( p->pSave3 ) Aig_ManStop( (Aig_Man_t *)p->pSave3 ); if ( p->pSave3 ) Aig_ManStop( (Aig_Man_t *)p->pSave3 );
if ( p->pSave4 ) Aig_ManStop( (Aig_Man_t *)p->pSave4 ); if ( p->pSave4 ) Aig_ManStop( (Aig_Man_t *)p->pSave4 );
if ( p->pManDsd ) If_DsdManFree( (If_DsdMan_t *)p->pManDsd, 0 );
if ( p->vPlugInComBinPairs ) if ( p->vPlugInComBinPairs )
{ {
char * pTemp; char * pTemp;
......
src/base/main/mainInt.h
...@@ -84,6 +84,7 @@ struct Abc_Frame_t_ ...@@ -84,6 +84,7 @@ struct Abc_Frame_t_
Vec_Ptr_t * vStore; // networks to be used by choice Vec_Ptr_t * vStore; // networks to be used by choice
// decomposition package // decomposition package
void * pManDec; // decomposition manager void * pManDec; // decomposition manager
void * pManDsd; // decomposition manager
DdManager * dd; // temporary BDD package DdManager * dd; // temporary BDD package
// libraries for mapping // libraries for mapping
void * pLibLut; // the current LUT library void * pLibLut; // the current LUT library
......
src/map/if/if.h
...@@ -517,12 +517,18 @@ extern int If_CluCheckExt( void * p, word * pTruth, int nVars, int n ...@@ -517,12 +517,18 @@ extern int If_CluCheckExt( void * p, word * pTruth, int nVars, int n
extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot, extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int nLutLeaf, int nLutLeaf2, int nLutRoot,
char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 ); char * pLut0, char * pLut1, char * pLut2, word * pFunc0, word * pFunc1, word * pFunc2 );
/*=== ifDsd.c =============================================================*/ /*=== ifDsd.c =============================================================*/
extern If_DsdMan_t * If_DsdManAlloc( int nLutSize ); extern If_DsdMan_t * If_DsdManAlloc( int nVars, int nLutSize );
extern void If_DsdManDump( If_DsdMan_t * p ); extern void If_DsdManDump( If_DsdMan_t * p );
extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ); extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose );
extern void If_DsdManFree( If_DsdMan_t * p, int fVerbose ); extern void If_DsdManFree( If_DsdMan_t * p, int fVerbose );
extern void If_DsdManSave( If_DsdMan_t * p, char * pFileName );
extern If_DsdMan_t * If_DsdManLoad( char * pFileName );
extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct ); extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
extern char * If_DsdManFileName( If_DsdMan_t * p );
extern int If_DsdManVarNum( If_DsdMan_t * p );
extern int If_DsdManLutSize( If_DsdMan_t * p );
extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ); extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose );
/*=== ifLib.c =============================================================*/ /*=== ifLib.c =============================================================*/
extern If_LibLut_t * If_LibLutRead( char * FileName ); extern If_LibLut_t * If_LibLutRead( char * FileName );
extern If_LibLut_t * If_LibLutDup( If_LibLut_t * p ); extern If_LibLut_t * If_LibLutDup( If_LibLut_t * p );
......
src/map/if/ifDsd.c
...@@ -53,7 +53,9 @@ struct If_DsdObj_t_ ...@@ -53,7 +53,9 @@ struct If_DsdObj_t_
struct If_DsdMan_t_ struct If_DsdMan_t_
{ {
char * pStore; // input/output file
int nVars; // max var number int nVars; // max var number
int LutSize; // LUT size
int nWords; // word number int nWords; // word number
int nBins; // table size int nBins; // table size
unsigned * pBins; // hash table unsigned * pBins; // hash table
...@@ -116,7 +118,7 @@ static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) ...@@ -116,7 +118,7 @@ static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Sorting DSD literals.] Synopsis []
Description [] Description []
...@@ -125,114 +127,21 @@ static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) ...@@ -125,114 +127,21 @@ static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 ) char * If_DsdManFileName( If_DsdMan_t * p )
{ {
If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0)); return p->pStore;
If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1));
int i, Res;
if ( If_DsdObjType(p0) < If_DsdObjType(p1) )
return -1;
if ( If_DsdObjType(p0) > If_DsdObjType(p1) )
return 1;
if ( If_DsdObjType(p0) < IF_DSD_AND )
return 0;
if ( If_DsdObjFaninNum(p0) < If_DsdObjFaninNum(p1) )
return -1;
if ( If_DsdObjFaninNum(p0) > If_DsdObjFaninNum(p1) )
return 1;
for ( i = 0; i < If_DsdObjFaninNum(p0); i++ )
{
Res = If_DsdObjCompare( p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) );
if ( Res != 0 )
return Res;
}
if ( Abc_LitIsCompl(iLit0) < Abc_LitIsCompl(iLit1) )
return -1;
if ( Abc_LitIsCompl(iLit0) > Abc_LitIsCompl(iLit1) )
return 1;
return 0;
} }
void If_DsdObjSort( Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm ) int If_DsdManVarNum( If_DsdMan_t * p )
{ {
int i, j, best_i; return p->nVars;
for ( i = 0; i < nLits-1; i++ )
{
best_i = i;
for ( j = i+1; j < nLits; j++ )
if ( If_DsdObjCompare(p, pLits[best_i], pLits[j]) == 1 )
best_i = j;
if ( i == best_i )
continue;
ABC_SWAP( int, pLits[i], pLits[best_i] );
if ( pPerm )
ABC_SWAP( int, pPerm[i], pPerm[best_i] );
}
} }
int If_DsdManLutSize( If_DsdMan_t * p )
/**Function*************************************************************
Synopsis [Creating DSD objects.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
{ {
int nWords = If_DsdObjWordNum( nFans + (int)(Type == DAU_DSD_PRIME) ); return p->LutSize;
If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
If_DsdObjClean( pObj );
pObj->Type = Type;
pObj->nFans = nFans;
pObj->Id = Vec_PtrSize( p->vObjs );
pObj->fMark = 0;
pObj->Count = 0;
Vec_PtrPush( p->vObjs, pObj );
Vec_IntPush( p->vNexts, 0 );
return pObj;
} }
int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId ) int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
{ {
If_DsdObj_t * pObj, * pFanin; return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) );
int i, iPrev = -1;
// check structural canonicity
assert( Type != DAU_DSD_MUX || nLits == 3 );
assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[0]) );
assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[1]) || !Abc_LitIsCompl(pLits[2]) );
// check that leaves are in good order
if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
{
for ( i = 0; i < nLits; i++ )
{
pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[i]) );
assert( Type != DAU_DSD_AND || Abc_LitIsCompl(pLits[i]) || If_DsdObjType(pFanin) != DAU_DSD_AND );
assert( Type != DAU_DSD_XOR || If_DsdObjType(pFanin) != DAU_DSD_XOR );
assert( iPrev == -1 || If_DsdObjCompare(p->vObjs, iPrev, pLits[i]) <= 0 );
iPrev = pLits[i];
}
}
if ( Vec_PtrSize(p->vObjs) % p->nBins == 0 )
printf( "Warning: The number of objects in If_DsdObjCreate() is more than the number of bins.\n" );
// create new node
pObj = If_DsdObjAlloc( p, Type, nLits );
if ( Type == DAU_DSD_PRIME )
If_DsdObjSetTruth( p, pObj, truthId );
assert( pObj->nSupp == 0 );
for ( i = 0; i < nLits; i++ )
{
pObj->pFans[i] = pLits[i];
pObj->nSupp += If_DsdVecLitSuppSize(p->vObjs, pLits[i]);
}
/*
{
extern void If_DsdManPrintOne( If_DsdMan_t * p, int iDsdLit, int * pPermLits );
If_DsdManPrintOne( p, If_DsdObj2Lit(pObj), NULL );
}
*/
return pObj->Id;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -258,11 +167,29 @@ static inline word ** If_ManDsdTtElems() ...@@ -258,11 +167,29 @@ static inline word ** If_ManDsdTtElems()
} }
return pTtElems; return pTtElems;
} }
If_DsdMan_t * If_DsdManAlloc( int nVars ) If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
{
int nWords = If_DsdObjWordNum( nFans + (int)(Type == DAU_DSD_PRIME) );
If_DsdObj_t * pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
If_DsdObjClean( pObj );
pObj->Type = Type;
pObj->nFans = nFans;
pObj->Id = Vec_PtrSize( p->vObjs );
pObj->fMark = 0;
pObj->Count = 0;
Vec_PtrPush( p->vObjs, pObj );
Vec_IntPush( p->vNexts, 0 );
return pObj;
}
If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
{ {
If_DsdMan_t * p; int v; If_DsdMan_t * p; int v;
char pFileName[10];
sprintf( pFileName, "%02d.dsd", nVars );
p = ABC_CALLOC( If_DsdMan_t, 1 ); p = ABC_CALLOC( If_DsdMan_t, 1 );
p->pStore = Abc_UtilStrsav( pFileName );
p->nVars = nVars; p->nVars = nVars;
p->LutSize = LutSize;
p->nWords = Abc_TtWordNum( nVars ); p->nWords = Abc_TtWordNum( nVars );
p->nBins = Abc_PrimeCudd( 1000000 ); p->nBins = Abc_PrimeCudd( 1000000 );
p->pBins = ABC_CALLOC( unsigned, p->nBins ); p->pBins = ABC_CALLOC( unsigned, p->nBins );
...@@ -284,8 +211,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) ...@@ -284,8 +211,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
{ {
int v; int v;
// If_DsdManDump( p ); // If_DsdManDump( p );
if ( fVerbose )
If_DsdManPrint( p, NULL, 0 ); If_DsdManPrint( p, NULL, 0 );
Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars );
if ( fVerbose ) if ( fVerbose )
{ {
Abc_PrintTime( 1, "Time DSD ", p->timeDsd ); Abc_PrintTime( 1, "Time DSD ", p->timeDsd );
...@@ -293,6 +220,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) ...@@ -293,6 +220,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
Abc_PrintTime( 1, "Time check ", p->timeCheck ); Abc_PrintTime( 1, "Time check ", p->timeCheck );
Abc_PrintTime( 1, "Time verify", p->timeVerify ); Abc_PrintTime( 1, "Time verify", p->timeVerify );
} }
if ( fVerbose )
Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars );
for ( v = 2; v < p->nVars; v++ ) for ( v = 2; v < p->nVars; v++ )
ABC_FREE( p->pSched[v] ); ABC_FREE( p->pSched[v] );
Vec_VecFree( (Vec_Vec_t *)p->vTtDecs ); Vec_VecFree( (Vec_Vec_t *)p->vTtDecs );
...@@ -302,9 +231,46 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) ...@@ -302,9 +231,46 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
Vec_IntFreeP( &p->vNexts ); Vec_IntFreeP( &p->vNexts );
Vec_PtrFreeP( &p->vObjs ); Vec_PtrFreeP( &p->vObjs );
Mem_FlexStop( p->pMem, 0 ); Mem_FlexStop( p->pMem, 0 );
ABC_FREE( p->pStore );
ABC_FREE( p->pBins ); ABC_FREE( p->pBins );
ABC_FREE( p ); ABC_FREE( p );
} }
void If_DsdManDump( If_DsdMan_t * p )
{
char * pFileName = "dss_tts.txt";
FILE * pFile;
If_DsdObj_t * pObj;
int i;
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\".\n", pFileName );
return;
}
If_DsdVecForEachObj( p->vObjs, pObj, i )
{
if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
continue;
fprintf( pFile, "0x" );
Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), p->nVars );
fprintf( pFile, "\n" );
printf( " " );
Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
}
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Printing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_DsdManHashProfile( If_DsdMan_t * p ) void If_DsdManHashProfile( If_DsdMan_t * p )
{ {
If_DsdObj_t * pObj; If_DsdObj_t * pObj;
...@@ -367,6 +333,7 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char ...@@ -367,6 +333,7 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char
fprintf( pFile, "%6d : ", iObjId ); fprintf( pFile, "%6d : ", iObjId );
fprintf( pFile, "%2d ", If_DsdVecObjSuppSize(p->vObjs, iObjId) ); fprintf( pFile, "%2d ", If_DsdVecObjSuppSize(p->vObjs, iObjId) );
fprintf( pFile, "%8d ", If_DsdVecObjRef(p->vObjs, iObjId) ); fprintf( pFile, "%8d ", If_DsdVecObjRef(p->vObjs, iObjId) );
fprintf( pFile, "%d ", If_DsdVecObjMark(p->vObjs, iObjId) );
If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp ); If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp );
if ( fNewLine ) if ( fNewLine )
fprintf( pFile, "\n" ); fprintf( pFile, "\n" );
...@@ -400,7 +367,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) ...@@ -400,7 +367,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) ); fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) ); fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) ); fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// If_DsdManHashProfile( p ); // If_DsdManHashProfile( p );
// If_DsdManDump( p ); // If_DsdManDump( p );
// return; // return;
...@@ -416,57 +383,6 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) ...@@ -416,57 +383,6 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
if ( pFileName ) if ( pFileName )
fclose( pFile ); fclose( pFile );
} }
void If_DsdManDump( If_DsdMan_t * p )
{
char * pFileName = "dss_tts.txt";
FILE * pFile;
If_DsdObj_t * pObj;
int i;
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\".\n", pFileName );
return;
}
If_DsdVecForEachObj( p->vObjs, pObj, i )
{
if ( If_DsdObjType(pObj) != IF_DSD_PRIME )
continue;
fprintf( pFile, "0x" );
Abc_TtPrintHexRev( pFile, If_DsdObjTruth(p, pObj), p->nVars );
fprintf( pFile, "\n" );
printf( " " );
Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
}
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Collect nodes of the tree.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
{
int i, iFanin;
If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id );
if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR )
return;
If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes );
Vec_IntPush( vNodes, Id );
}
void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
{
Vec_IntClear( vNodes );
If_DsdManCollect_rec( p, Id, vNodes );
}
/**Function************************************************************* /**Function*************************************************************
...@@ -481,7 +397,6 @@ void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes ) ...@@ -481,7 +397,6 @@ void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
***********************************************************************/ ***********************************************************************/
static inline unsigned If_DsdObjHashKey( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId ) static inline unsigned If_DsdObjHashKey( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
{ {
// static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
static int s_Primes[24] = { 1049, 1297, 1559, 1823, 2089, 2371, 2663, 2909, static int s_Primes[24] = { 1049, 1297, 1559, 1823, 2089, 2371, 2663, 2909,
3221, 3517, 3779, 4073, 4363, 4663, 4973, 5281, 3221, 3517, 3779, 4073, 4363, 4663, 4973, 5281,
5573, 5861, 6199, 6481, 6803, 7109, 7477, 7727 }; 5573, 5861, 6199, 6481, 6803, 7109, 7477, 7727 };
...@@ -512,6 +427,43 @@ unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLit ...@@ -512,6 +427,43 @@ unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLit
p->nUniqueMisses++; p->nUniqueMisses++;
return pSpot; return pSpot;
} }
int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
{
If_DsdObj_t * pObj, * pFanin;
int i, iPrev = -1;
// check structural canonicity
assert( Type != DAU_DSD_MUX || nLits == 3 );
assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[0]) );
assert( Type != DAU_DSD_MUX || !Abc_LitIsCompl(pLits[1]) || !Abc_LitIsCompl(pLits[2]) );
// check that leaves are in good order
if ( Type == DAU_DSD_AND || Type == DAU_DSD_XOR )
{
for ( i = 0; i < nLits; i++ )
{
pFanin = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[i]) );
assert( Type != DAU_DSD_AND || Abc_LitIsCompl(pLits[i]) || If_DsdObjType(pFanin) != DAU_DSD_AND );
assert( Type != DAU_DSD_XOR || If_DsdObjType(pFanin) != DAU_DSD_XOR );
assert( iPrev == -1 || If_DsdObjCompare(p->vObjs, iPrev, pLits[i]) <= 0 );
iPrev = pLits[i];
}
}
if ( Vec_PtrSize(p->vObjs) % p->nBins == 0 )
printf( "Warning: The number of objects in If_DsdObjCreate() is more than the number of bins.\n" );
// create new node
pObj = If_DsdObjAlloc( p, Type, nLits );
if ( Type == DAU_DSD_PRIME )
If_DsdObjSetTruth( p, pObj, truthId );
assert( pObj->nSupp == 0 );
for ( i = 0; i < nLits; i++ )
{
pObj->pFans[i] = pLits[i];
pObj->nSupp += If_DsdVecLitSuppSize(p->vObjs, pLits[i]);
}
// check decomposability
if ( p->LutSize && !If_DsdManCheckXY(p, Abc_Var2Lit(pObj->Id, 0), p->LutSize, 0, 0) )
If_DsdVecObjSetMark( p->vObjs, pObj->Id );
return pObj->Id;
}
int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth ) int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word * pTruth )
{ {
int truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem, pTruth) : -1; int truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem, pTruth) : -1;
...@@ -536,6 +488,146 @@ p->timeCheck += Abc_Clock() - clk; ...@@ -536,6 +488,146 @@ p->timeCheck += Abc_Clock() - clk;
/**Function************************************************************* /**Function*************************************************************
Synopsis [Saving/loading DSD manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_DsdManSave( If_DsdMan_t * p, char * pFileName )
{
If_DsdObj_t * pObj;
Vec_Int_t * vSets;
char * pBuffer = "dsd0";
word * pTruth;
int i, Num;
FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" );
if ( pFile == NULL )
{
printf( "Writing DSD manager file \"%s\" has failed.\n", pFileName ? pFileName : p->pStore );
return;
}
fwrite( pBuffer, 4, 1, pFile );
Num = p->nVars;
fwrite( &Num, 4, 1, pFile );
Num = p->LutSize;
fwrite( &Num, 4, 1, pFile );
Num = Vec_PtrSize(p->vObjs);
fwrite( &Num, 4, 1, pFile );
Vec_PtrForEachEntryStart( If_DsdObj_t *, p->vObjs, pObj, i, 2 )
{
Num = If_DsdObjWordNum( pObj->nFans + (int)(pObj->Type == DAU_DSD_PRIME) );
fwrite( &Num, 4, 1, pFile );
fwrite( pObj, sizeof(word)*Num, 1, pFile );
}
assert( Vec_MemEntryNum(p->vTtMem) == Vec_PtrSize(p->vTtDecs) );
Num = Vec_MemEntryNum(p->vTtMem);
fwrite( &Num, 4, 1, pFile );
Vec_MemForEachEntry( p->vTtMem, pTruth, i )
fwrite( pTruth, sizeof(word)*p->nWords, 1, pFile );
Vec_PtrForEachEntry( Vec_Int_t *, p->vTtDecs, vSets, i )
{
Num = Vec_IntSize(vSets);
fwrite( &Num, 4, 1, pFile );
fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
}
fclose( pFile );
}
If_DsdMan_t * If_DsdManLoad( char * pFileName )
{
If_DsdMan_t * p;
If_DsdObj_t * pObj;
Vec_Int_t * vSets;
char pBuffer[10];
unsigned * pSpot;
word * pTruth;
int i, Num;
FILE * pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
printf( "Reading DSD manager file \"%s\" has failed.\n", pFileName );
return NULL;
}
fread( pBuffer, 4, 1, pFile );
if ( pBuffer[0] != 'd' && pBuffer[1] != 's' && pBuffer[2] != 'd' && pBuffer[3] != '0' )
{
printf( "Unrecognized format of file \"%s\".\n", pFileName );
return NULL;
}
fread( &Num, 4, 1, pFile );
p = If_DsdManAlloc( Num, 0 );
ABC_FREE( p->pStore );
p->pStore = Abc_UtilStrsav( pFileName );
fread( &Num, 4, 1, pFile );
p->LutSize = Num;
fread( &Num, 4, 1, pFile );
assert( Num >= 2 );
Vec_PtrFillExtra( p->vObjs, Num, NULL );
Vec_IntFill( p->vNexts, Num, 0 );
for ( i = 2; i < Vec_PtrSize(p->vObjs); i++ )
{
fread( &Num, 4, 1, pFile );
pObj = (If_DsdObj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * Num );
fread( pObj, sizeof(word)*Num, 1, pFile );
Vec_PtrWriteEntry( p->vObjs, i, pObj );
pSpot = If_DsdObjHashLookup( p, pObj->Type, pObj->pFans, pObj->nFans, If_DsdObjTruthId(p, pObj) );
assert( *pSpot == 0 );
*pSpot = pObj->Id;
}
fread( &Num, 4, 1, pFile );
pTruth = ABC_ALLOC( word, p->nWords );
for ( i = 0; i < Num; i++ )
{
fread( pTruth, sizeof(word)*p->nWords, 1, pFile );
Vec_MemHashInsert( p->vTtMem, pTruth );
}
ABC_FREE( pTruth );
assert( Num == Vec_MemEntryNum(p->vTtMem) );
for ( i = 0; i < Vec_MemEntryNum(p->vTtMem); i++ )
{
fread( &Num, 4, 1, pFile );
vSets = Vec_IntAlloc( Num );
fread( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile );
vSets->nSize = Num;
Vec_PtrPush( p->vTtDecs, vSets );
}
assert( Vec_MemEntryNum(p->vTtMem) == Vec_PtrSize(p->vTtDecs) );
fclose( pFile );
return p;
}
/**Function*************************************************************
Synopsis [Collect nodes of the tree.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
{
int i, iFanin;
If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id );
if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR )
return;
If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes );
Vec_IntPush( vNodes, Id );
}
void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
{
Vec_IntClear( vNodes );
If_DsdManCollect_rec( p, Id, vNodes );
}
/**Function*************************************************************
Synopsis [] Synopsis []
Description [] Description []
...@@ -620,6 +712,61 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi ...@@ -620,6 +712,61 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
/**Function************************************************************* /**Function*************************************************************
Synopsis [Sorting DSD literals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_DsdObjCompare( Vec_Ptr_t * p, int iLit0, int iLit1 )
{
If_DsdObj_t * p0 = If_DsdVecObj(p, Abc_Lit2Var(iLit0));
If_DsdObj_t * p1 = If_DsdVecObj(p, Abc_Lit2Var(iLit1));
int i, Res;
if ( If_DsdObjType(p0) < If_DsdObjType(p1) )
return -1;
if ( If_DsdObjType(p0) > If_DsdObjType(p1) )
return 1;
if ( If_DsdObjType(p0) < IF_DSD_AND )
return 0;
if ( If_DsdObjFaninNum(p0) < If_DsdObjFaninNum(p1) )
return -1;
if ( If_DsdObjFaninNum(p0) > If_DsdObjFaninNum(p1) )
return 1;
for ( i = 0; i < If_DsdObjFaninNum(p0); i++ )
{
Res = If_DsdObjCompare( p, If_DsdObjFaninLit(p0, i), If_DsdObjFaninLit(p1, i) );
if ( Res != 0 )
return Res;
}
if ( Abc_LitIsCompl(iLit0) < Abc_LitIsCompl(iLit1) )
return -1;
if ( Abc_LitIsCompl(iLit0) > Abc_LitIsCompl(iLit1) )
return 1;
return 0;
}
void If_DsdObjSort( Vec_Ptr_t * p, int * pLits, int nLits, int * pPerm )
{
int i, j, best_i;
for ( i = 0; i < nLits-1; i++ )
{
best_i = i;
for ( j = i+1; j < nLits; j++ )
if ( If_DsdObjCompare(p, pLits[best_i], pLits[j]) == 1 )
best_i = j;
if ( i == best_i )
continue;
ABC_SWAP( int, pLits[i], pLits[best_i] );
if ( pPerm )
ABC_SWAP( int, pPerm[i], pPerm[best_i] );
}
}
/**Function*************************************************************
Synopsis [Performs DSD operation.] Synopsis [Performs DSD operation.]
Description [] Description []
...@@ -697,13 +844,26 @@ int If_DsdManOperation2( If_DsdMan_t * p, int Type, int * pLits, int nLits ) ...@@ -697,13 +844,26 @@ int If_DsdManOperation2( If_DsdMan_t * p, int Type, int * pLits, int nLits )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int If_DsdManComputeFirstArray( If_DsdMan_t * p, int * pLits, int nLits, int * pFirsts )
{
int i, nSSize = 0;
for ( i = 0; i < nLits; i++ )
{
pFirsts[i] = nSSize;
nSSize += If_DsdVecLitSuppSize(p->vObjs, pLits[i]);
}
return nSSize;
}
int If_DsdManComputeFirst( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pFirsts )
{
return If_DsdManComputeFirstArray( p, pObj->pFans, pObj->nFans, pFirsts );
}
int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth ) int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth )
{ {
If_DsdObj_t * pObj, * pFanin; If_DsdObj_t * pObj, * pFanin;
unsigned char pPermNew[DAU_MAX_VAR]; unsigned char pPermNew[DAU_MAX_VAR];
int nChildren = 0, pChildren[DAU_MAX_VAR], pBegEnd[DAU_MAX_VAR]; int nChildren = 0, pChildren[DAU_MAX_VAR], pBegEnd[DAU_MAX_VAR];
int i, k, j, Id, iFanin, fComplFan, fCompl = 0, nSSize = 0; int i, k, j, Id, iFanin, fComplFan, fCompl = 0, nSSize = 0;
// abctime clk;
if ( Type == IF_DSD_AND ) if ( Type == IF_DSD_AND )
{ {
for ( k = 0; k < nLits; k++ ) for ( k = 0; k < nLits; k++ )
...@@ -813,11 +973,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig ...@@ -813,11 +973,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
int i, uCanonPhase, pFirsts[DAU_MAX_VAR]; int i, uCanonPhase, pFirsts[DAU_MAX_VAR];
uCanonPhase = Abc_TtCanonicize( pTruth, nLits, pCanonPerm ); uCanonPhase = Abc_TtCanonicize( pTruth, nLits, pCanonPerm );
fCompl = ((uCanonPhase >> nLits) & 1); fCompl = ((uCanonPhase >> nLits) & 1);
for ( i = 0; i < nLits; i++ ) nSSize = If_DsdManComputeFirstArray( p, pLits, nLits, pFirsts );
{
pFirsts[i] = nSSize;
nSSize += If_DsdVecLitSuppSize(p->vObjs, pLits[i]);
}
for ( j = i = 0; i < nLits; i++ ) for ( j = i = 0; i < nLits; i++ )
{ {
int iLitNew = Abc_LitNotCond( pLits[(int)pCanonPerm[i]], ((uCanonPhase>>i)&1) ); int iLitNew = Abc_LitNotCond( pLits[(int)pCanonPerm[i]], ((uCanonPhase>>i)&1) );
...@@ -873,7 +1029,6 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p ...@@ -873,7 +1029,6 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p
fCompl = 1; fCompl = 1;
(*p)++; (*p)++;
} }
// assert( !((**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9')) );
if ( **p >= 'a' && **p <= 'z' ) // var if ( **p >= 'a' && **p <= 'z' ) // var
{ {
pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl ); pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl );
...@@ -952,6 +1107,23 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char ...@@ -952,6 +1107,23 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
// create signature of the support of the node
unsigned If_DsdSign_rec( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pnSupp )
{
unsigned uSign = 0; int i;
If_DsdObj_t * pFanin;
if ( If_DsdObjType(pObj) == IF_DSD_VAR )
return (1 << (2*(*pnSupp)++));
If_DsdObjForEachFanin( p->vObjs, pObj, pFanin, i )
uSign |= If_DsdSign_rec( p, pFanin, pnSupp );
return uSign;
}
unsigned If_DsdSign( If_DsdMan_t * p, If_DsdObj_t * pObj, int iFan, int iFirst, int fShared )
{
If_DsdObj_t * pFanin = If_DsdObjFanin( p->vObjs, pObj, iFan );
unsigned uSign = If_DsdSign_rec( p, pFanin, &iFirst );
return fShared ? (uSign << 1) | uSign : uSign;
}
// collect supports of the node // collect supports of the node
void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes ) void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
{ {
...@@ -960,10 +1132,10 @@ void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes ) ...@@ -960,10 +1132,10 @@ void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
pSSizes[i] = If_DsdObjSuppSize(pFanin); pSSizes[i] = If_DsdObjSuppSize(pFanin);
} }
// checks if there is a way to package some fanins // checks if there is a way to package some fanins
int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose ) unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
{ {
int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
int nFans = If_DsdObjFaninNum(pObj); int nFans = If_DsdObjFaninNum(pObj), pFirsts[DAU_MAX_VAR];
assert( pObj->nFans > 2 ); assert( pObj->nFans > 2 );
assert( If_DsdObjSuppSize(pObj) > LutSize ); assert( If_DsdObjSuppSize(pObj) > LutSize );
If_DsdManGetSuppSizes( p, pObj, pSSizes ); If_DsdManGetSuppSizes( p, pObj, pSSizes );
...@@ -976,7 +1148,10 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int ...@@ -976,7 +1148,10 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int
SizeOut = pObj->nSupp - SizeIn; SizeOut = pObj->nSupp - SizeIn;
if ( SizeIn > LutSize || SizeOut > LimitOut ) if ( SizeIn > LutSize || SizeOut > LimitOut )
continue; continue;
return (1 << i[0]) | (1 << i[1]); if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0);
} }
if ( pObj->nFans == 3 ) if ( pObj->nFans == 3 )
return 0; return 0;
...@@ -988,7 +1163,10 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int ...@@ -988,7 +1163,10 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int
SizeOut = pObj->nSupp - SizeIn; SizeOut = pObj->nSupp - SizeIn;
if ( SizeIn > LutSize || SizeOut > LimitOut ) if ( SizeIn > LutSize || SizeOut > LimitOut )
continue; continue;
return (1 << i[0]) | (1 << i[1]) | (1 << i[2]); if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0);
} }
if ( pObj->nFans == 4 ) if ( pObj->nFans == 4 )
return 0; return 0;
...@@ -1001,14 +1179,17 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int ...@@ -1001,14 +1179,17 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int
SizeOut = pObj->nSupp - SizeIn; SizeOut = pObj->nSupp - SizeIn;
if ( SizeIn > LutSize || SizeOut > LimitOut ) if ( SizeIn > LutSize || SizeOut > LimitOut )
continue; continue;
return (1 << i[0]) | (1 << i[1]) | (1 << i[2]) | (1 << i[3]); if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0) | If_DsdSign(p, pObj, i[3], pFirsts[i[3]], 0);
} }
return 0; return 0;
} }
// checks if there is a way to package some fanins // checks if there is a way to package some fanins
int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose ) unsigned If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
{ {
int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
assert( If_DsdObjFaninNum(pObj) == 3 ); assert( If_DsdObjFaninNum(pObj) == 3 );
assert( If_DsdObjSuppSize(pObj) > LutSize ); assert( If_DsdObjSuppSize(pObj) > LutSize );
If_DsdManGetSuppSizes( p, pObj, pSSizes ); If_DsdManGetSuppSizes( p, pObj, pSSizes );
...@@ -1019,21 +1200,27 @@ int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int Lu ...@@ -1019,21 +1200,27 @@ int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int Lu
SizeOut = pSSizes[2]; SizeOut = pSSizes[2];
if ( SizeIn <= LutSize && SizeOut <= LimitOut ) if ( SizeIn <= LutSize && SizeOut <= LimitOut )
{ {
return 1; if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 1, pFirsts[1], 0);
} }
// second input // second input
SizeIn = pSSizes[0] + pSSizes[2]; SizeIn = pSSizes[0] + pSSizes[2];
SizeOut = pSSizes[1]; SizeOut = pSSizes[1];
if ( SizeIn <= LutSize && SizeOut <= LimitOut ) if ( SizeIn <= LutSize && SizeOut <= LimitOut )
{ {
return 1; if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 2, pFirsts[2], 0);
} }
return 0; return 0;
} }
// checks if there is a way to package some fanins // checks if there is a way to package some fanins
int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose ) unsigned If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
{ {
int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR]; int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
int truthId = If_DsdObjTruthId( p, pObj ); int truthId = If_DsdObjTruthId( p, pObj );
int nFans = If_DsdObjFaninNum(pObj); int nFans = If_DsdObjFaninNum(pObj);
Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId); Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId);
...@@ -1066,11 +1253,29 @@ Dau_DecPrintSets( vSets, nFans ); ...@@ -1066,11 +1253,29 @@ Dau_DecPrintSets( vSets, nFans );
break; break;
} }
if ( v == nFans ) if ( v == nFans )
return set; {
unsigned uSign;
if ( !fDerive )
return ~0;
uSign = 0;
If_DsdManComputeFirst( p, pObj, pFirsts );
for ( v = 0; v < nFans; v++ )
{
int Value = ((set >> (v << 1)) & 3);
if ( Value == 0 )
{}
else if ( Value == 1 )
uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 0);
else if ( Value == 3 )
uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 1);
else assert( Value == 0 );
}
return uSign;
}
} }
return 0; return 0;
} }
int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
{ {
If_DsdObj_t * pObj, * pTemp; int i, Mask; If_DsdObj_t * pObj, * pTemp; int i, Mask;
pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) ); pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
...@@ -1080,7 +1285,7 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) ...@@ -1080,7 +1285,7 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
{ {
if ( fVerbose ) if ( fVerbose )
printf( " Trivial\n" ); printf( " Trivial\n" );
return 1; return ~0;
} }
If_DsdManCollect( p, pObj->Id, p->vNodes ); If_DsdManCollect( p, pObj->Id, p->vNodes );
If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
...@@ -1090,12 +1295,12 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) ...@@ -1090,12 +1295,12 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
printf( " Dec using node " ); printf( " Dec using node " );
if ( fVerbose ) if ( fVerbose )
If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 ); If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 );
return 1; return ~0;
} }
If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize ) if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize )
{ {
if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) ) if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
{ {
if ( fVerbose ) if ( fVerbose )
printf( " " ); printf( " " );
...@@ -1103,13 +1308,13 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) ...@@ -1103,13 +1308,13 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
Abc_TtPrintBinary( (word *)&Mask, 4 ); Abc_TtPrintBinary( (word *)&Mask, 4 );
if ( fVerbose ) if ( fVerbose )
printf( " Using multi-input AND/XOR node\n" ); printf( " Using multi-input AND/XOR node\n" );
return 1; return Mask;
} }
} }
If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize ) if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize )
{ {
if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) ) if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
{ {
if ( fVerbose ) if ( fVerbose )
printf( " " ); printf( " " );
...@@ -1117,13 +1322,13 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) ...@@ -1117,13 +1322,13 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
Abc_TtPrintBinary( (word *)&Mask, 4 ); Abc_TtPrintBinary( (word *)&Mask, 4 );
if ( fVerbose ) if ( fVerbose )
printf( " Using multi-input MUX node\n" ); printf( " Using multi-input MUX node\n" );
return 1; return Mask;
} }
} }
If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i ) If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize ) if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize )
{ {
if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) ) if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
{ {
if ( fVerbose ) if ( fVerbose )
printf( " " ); printf( " " );
...@@ -1131,19 +1336,14 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose ) ...@@ -1131,19 +1336,14 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
Dau_DecPrintSet( Mask, If_DsdObjFaninNum(pTemp), 0 ); Dau_DecPrintSet( Mask, If_DsdObjFaninNum(pTemp), 0 );
if ( fVerbose ) if ( fVerbose )
printf( " Using prime node\n" ); printf( " Using prime node\n" );
return 1; return Mask;
} }
} }
if ( fVerbose ) if ( fVerbose )
printf( " UNDEC\n" ); printf( " UNDEC\n" );
// If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 ); // If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
return 0; return 0;
} }
int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize )
{
return 1;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -1156,9 +1356,9 @@ int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize ) ...@@ -1156,9 +1356,9 @@ int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ) unsigned If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
{ {
return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) ); return ~0;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -1183,17 +1383,6 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char ...@@ -1183,17 +1383,6 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
clk = Abc_Clock(); clk = Abc_Clock();
nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd ); nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd );
p->timeDsd += Abc_Clock() - clk; p->timeDsd += Abc_Clock() - clk;
/*
if ( nLeaves <= 6 )
{
word pCopy2[DAU_MAX_WORD], t;
char pDsd2[DAU_MAX_STR];
Abc_TtCopy( pCopy2, pTruth, p->nWords, 0 );
nSizeNonDec = Dau_DsdDecompose( pCopy2, nLeaves, 0, 1, pDsd2 );
t = Dau_Dsd6ToTruth( pDsd2 );
assert( t == *pTruth );
}
*/
// if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") ) // if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
// { // {
// int x = 0; // int x = 0;
...@@ -1217,18 +1406,9 @@ p->timeVerify += Abc_Clock() - clk; ...@@ -1217,18 +1406,9 @@ p->timeVerify += Abc_Clock() - clk;
printf( "%s\n", pDsd ); printf( "%s\n", pDsd );
Dau_DsdPrintFromTruth( pTruth, nLeaves ); Dau_DsdPrintFromTruth( pTruth, nLeaves );
Dau_DsdPrintFromTruth( pRes, nLeaves ); Dau_DsdPrintFromTruth( pRes, nLeaves );
// Kit_DsdPrintFromTruth( (unsigned *)pTruth, nLeaves ); printf( "\n" );
// Kit_DsdPrintFromTruth( (unsigned *)pRes, nLeaves ); printf( "\n" );
If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 ); If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
printf( "\n" ); printf( "\n" );
} }
if ( pLutStruct && If_DsdVecObjRef(p->vObjs, Abc_Lit2Var(iDsd)) )
{
int LutSize = (int)(pLutStruct[0] - '0');
assert( pLutStruct[2] == 0 ); // XY
if ( !If_DsdManCheckXY( p, iDsd, LutSize, 0 ) )
If_DsdVecObjSetMark( p->vObjs, Abc_Lit2Var(iDsd) );
}
If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) ); If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) );
return iDsd; return iDsd;
} }
......
src/map/if/ifMan.c
...@@ -85,7 +85,6 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) ...@@ -85,7 +85,6 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
p->puTempW = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words ) : NULL; p->puTempW = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words ) : NULL;
if ( pPars->fUseDsd ) if ( pPars->fUseDsd )
{ {
p->pIfDsdMan = If_DsdManAlloc( pPars->nLutSize );
p->vTtDsds = Vec_IntAlloc( 1000 ); p->vTtDsds = Vec_IntAlloc( 1000 );
Vec_IntPush( p->vTtDsds, 0 ); Vec_IntPush( p->vTtDsds, 0 );
Vec_IntPush( p->vTtDsds, 2 ); Vec_IntPush( p->vTtDsds, 2 );
...@@ -142,6 +141,15 @@ void If_ManRestart( If_Man_t * p ) ...@@ -142,6 +141,15 @@ void If_ManRestart( If_Man_t * p )
***********************************************************************/ ***********************************************************************/
void If_ManStop( If_Man_t * p ) void If_ManStop( If_Man_t * p )
{ {
/*
if ( p->pIfDsdMan )
{
If_DsdMan_t * pNew;
If_DsdManSave( p->pIfDsdMan, NULL );
pNew = If_DsdManLoad( If_DsdManFileName(p->pIfDsdMan) );
If_DsdManFree( pNew, 1 );
}
*/
{ {
// extern void If_CluHashFindMedian( If_Man_t * p ); // extern void If_CluHashFindMedian( If_Man_t * p );
// extern void If_CluHashTableCheck( If_Man_t * p ); // extern void If_CluHashTableCheck( If_Man_t * p );
...@@ -158,11 +166,13 @@ void If_ManStop( If_Man_t * p ) ...@@ -158,11 +166,13 @@ void If_ManStop( If_Man_t * p )
Abc_Print( 1, "Useless cuts %2d = %9d (out of %9d) (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) ); Abc_Print( 1, "Useless cuts %2d = %9d (out of %9d) (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) );
Abc_Print( 1, "Useless cuts all = %9d (out of %9d) (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) ); Abc_Print( 1, "Useless cuts all = %9d (out of %9d) (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) );
} }
if ( p->pPars->fVerbose && p->nCuts5 ) // if ( p->pPars->fVerbose && p->nCuts5 )
Abc_Print( 1, "Statistics about 5-cuts: Total = %d Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 ); // Abc_Print( 1, "Statistics about 5-cuts: Total = %d Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 );
if ( p->pPars->fUseDsd ) // if ( p->pPars->fUseDsd )
If_DsdManFree( p->pIfDsdMan, p->pPars->fVerbose ); // If_DsdManFree( p->pIfDsdMan, p->pPars->fVerbose );
if ( p->pPars->fUseDsd ) if ( p->pIfDsdMan )
p->pIfDsdMan = NULL;
if ( p->pPars->fUseDsd && (p->nCountNonDec[0] || p->nCountNonDec[1]) )
printf( "NonDec0 = %d. NonDec1 = %d.\n", p->nCountNonDec[0], p->nCountNonDec[1] ); printf( "NonDec0 = %d. NonDec1 = %d.\n", p->nCountNonDec[0], p->nCountNonDec[1] );
// Abc_PrintTime( 1, "Truth", p->timeTruth ); // Abc_PrintTime( 1, "Truth", p->timeTruth );
// Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp ); // Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp );
......
src/map/if/ifMap.c
...@@ -217,11 +217,38 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep ...@@ -217,11 +217,38 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
// abctime clk = Abc_Clock(); // abctime clk = Abc_Clock();
If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 ); If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
// p->timeTruth += Abc_Clock() - clk; // p->timeTruth += Abc_Clock() - clk;
if ( p->pPars->fUseDsd )
{
int truthId = Abc_Lit2Var(pCut->iCutFunc);
if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 )
{
pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
// printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) );
while ( Vec_IntSize(p->vTtDsds) <= truthId )
{
Vec_IntPush( p->vTtDsds, -1 );
for ( v = 0; v < p->pPars->nLutSize; v++ )
Vec_StrPush( p->vTtPerms, IF_BIG_CHAR );
}
Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
for ( v = 0; v < (int)pCut->nLeaves; v++ )
Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] );
}
else
{
pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
for ( v = 0; v < (int)pCut->nLeaves; v++ )
pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v );
}
}
// run user functions // run user functions
pCut->fUseless = 0; pCut->fUseless = 0;
if ( p->pPars->pFuncCell ) if ( p->pPars->pFuncCell )
{ {
assert( pCut->nLimit >= 4 && pCut->nLimit <= 16 ); assert( pCut->nLimit >= 4 && pCut->nLimit <= 16 );
if ( p->pPars->fUseDsd )
pCut->fUseless = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
else
pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(p, pCut), pCut->nLimit, pCut->nLeaves, p->pPars->pLutStruct ); pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(p, pCut), pCut->nLimit, pCut->nLeaves, p->pPars->pLutStruct );
p->nCutsUselessAll += pCut->fUseless; p->nCutsUselessAll += pCut->fUseless;
p->nCutsUseless[pCut->nLeaves] += pCut->fUseless; p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
...@@ -251,29 +278,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep ...@@ -251,29 +278,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
p->nCuts5a++; p->nCuts5a++;
} }
} }
/*
if ( p->pPars->fUseDsd ) if ( p->pPars->fUseDsd )
{ {
int truthId = Abc_Lit2Var(pCut->iCutFunc);
if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 )
{
pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
// printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) );
while ( Vec_IntSize(p->vTtDsds) <= truthId )
{
Vec_IntPush( p->vTtDsds, -1 );
for ( v = 0; v < p->pPars->nLutSize; v++ )
Vec_StrPush( p->vTtPerms, IF_BIG_CHAR );
}
Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
for ( v = 0; v < (int)pCut->nLeaves; v++ )
Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] );
}
else
{
pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
for ( v = 0; v < (int)pCut->nLeaves; v++ )
pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v );
}
if ( p->pPars->pLutStruct ) if ( p->pPars->pLutStruct )
{ {
int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ); int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
...@@ -283,7 +290,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep ...@@ -283,7 +290,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
p->nCountNonDec[0]++; p->nCountNonDec[0]++;
if ( !pCut->fUseless && Value ) if ( !pCut->fUseless && Value )
p->nCountNonDec[1]++; p->nCountNonDec[1]++;
/*
// if ( pCut->fUseless && !Value ) // if ( pCut->fUseless && !Value )
// printf( "Old does not work. New works.\n" ); // printf( "Old does not work. New works.\n" );
if ( !pCut->fUseless && Value ) if ( !pCut->fUseless && Value )
...@@ -307,14 +314,14 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep ...@@ -307,14 +314,14 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
z = If_Dec6Perform( t, 1 ); z = If_Dec6Perform( t, 1 );
If_DecPrintConfig( z ); If_DecPrintConfig( z );
s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 1 ); s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 0, 1 );
printf( "Confirm %d\n", s ); printf( "Confirm %d\n", s );
s = 0; s = 0;
} }
*/
} }
} }
} }
*/
} }
// compute the application-specific cost and depth // compute the application-specific cost and depth
......
src/map/if/ifSat.c
...@@ -204,46 +204,46 @@ void If_ManSatTest() ...@@ -204,46 +204,46 @@ void If_ManSatTest()
uSet = (3 << 0) | (1 << 2) | (1 << 4); uSet = (3 << 0) | (1 << 2) | (1 << 4);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (1 << 0) | (3 << 2) | (1 << 4); uSet = (1 << 0) | (3 << 2) | (1 << 4);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (1 << 0) | (1 << 2) | (3 << 4); uSet = (1 << 0) | (1 << 2) | (3 << 4);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (3 << 0) | (1 << 2) | (1 << 6); uSet = (3 << 0) | (1 << 2) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (1 << 0) | (3 << 2) | (1 << 6); uSet = (1 << 0) | (3 << 2) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (1 << 0) | (1 << 2) | (3 << 6); uSet = (1 << 0) | (1 << 2) | (3 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (3 << 0) | (1 << 4) | (1 << 6); uSet = (3 << 0) | (1 << 4) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (1 << 0) | (3 << 4) | (1 << 6); uSet = (1 << 0) | (3 << 4) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (1 << 0) | (1 << 4) | (3 << 6); uSet = (1 << 0) | (1 << 4) | (3 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (3 << 2) | (1 << 4) | (1 << 6); uSet = (3 << 2) | (1 << 4) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (1 << 2) | (3 << 4) | (1 << 6); uSet = (1 << 2) | (3 << 4) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
uSet = (1 << 2) | (1 << 4) | (3 << 6); uSet = (1 << 2) | (1 << 4) | (3 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits ); RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue ); printf( "%d (%d)", RetValue, sat_solver_nconflicts(p) );
printf( "\n" ); printf( "\n" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment