Skip to content

A
abc
Commit 83963214 by Alan Mishchenko
Options

Changes to LUT mappers.

parent 5b3d4b7d
Showing with 325 additions and 3 deletions
src/base/abci/abc.c
......@@ -235,6 +235,7 @@ static int Abc_CommandDsdSave ( Abc_Frame_t * pAbc, int argc, cha
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_CommandDsdTune ( 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 );
......@@ -793,6 +794,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
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, "FPGA mapping", "dsd_tune", Abc_CommandDsdTune, 0 );
// Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
......@@ -15559,6 +15561,70 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c, fVerbose = 0, fFast = 0, fSpec = 0, LutSize = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Kfsvh" ) ) != EOF )
{
switch ( c )
{
case 'K':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-K\" should be followed by a floating point number.\n" );
goto usage;
}
LutSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( LutSize < 4 || LutSize > 6 )
goto usage;
break;
case 'f':
fFast ^= 1;
break;
case 's':
fSpec ^= 1;
break;
case 'v':
fVerbose ^= 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_DsdManTune( (If_DsdMan_t *)Abc_FrameReadManDsd(), LutSize, fFast, fSpec, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: dsd_tune [-K num] [-fsvh]\n" );
Abc_Print( -2, "\t tunes DSD manager for the given LUT size\n" );
Abc_Print( -2, "\t-K num : LUT size used for tuning [default = %d]\n", LutSize );
Abc_Print( -2, "\t-f : toggles using fast check [default = %s]\n", fFast? "yes": "no" );
Abc_Print( -2, "\t-s : toggles using specialized check [default = %s]\n", fSpec? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
src/map/if/if.h
......@@ -520,6 +520,7 @@ extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int
extern If_DsdMan_t * If_DsdManAlloc( int nVars, int nLutSize );
extern void If_DsdManDump( If_DsdMan_t * p );
extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose );
extern void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, 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 );
......@@ -574,10 +575,12 @@ extern int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, i
extern void If_ManImproveMapping( If_Man_t * p );
/*=== ifSat.c ==========================================================*/
extern void * If_ManSatBuildXY( int nLutSize );
extern void * If_ManSatBuild55();
extern void * If_ManSatBuildXYZ( int nLutSize );
extern void If_ManSatUnbuild( void * p );
extern int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits );
extern unsigned If_ManSatCheckXYall( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits );
extern unsigned If_ManSatCheck55all( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits );
/*=== ifSeq.c =============================================================*/
extern int If_ManPerformMappingSeq( If_Man_t * p );
/*=== ifTime.c ============================================================*/
......
src/map/if/ifDsd.c
......@@ -20,6 +20,7 @@
#include "if.h"
#include "misc/extra/extra.h"
#include "sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
......@@ -102,6 +103,7 @@ static inline void If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj )
static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return If_DsdVecObj(p, Abc_Lit2Var(pObj->pFans[i])); }
static inline int If_DsdVecObjMark( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->fMark; }
static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 1; }
static inline void If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 0; }
#define If_DsdVecForEachObj( vVec, pObj, i ) \
Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i )
......@@ -365,10 +367,39 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char
fprintf( pFile, "\n" );
assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, iObjId) );
}
void If_DsdManPrintDistrib( If_DsdMan_t * p )
{
If_DsdObj_t * pObj;
int CountAll[IF_MAX_FUNC_LUTSIZE] = {0};
int CountNon[IF_MAX_FUNC_LUTSIZE] = {0};
int i, nVars, CountNonTotal = 0;
If_DsdVecForEachObj( p->vObjs, pObj, i )
{
nVars = If_DsdObjSuppSize(pObj);
CountAll[nVars]++;
if ( !If_DsdVecObjMark(p->vObjs, i) )
continue;
CountNon[nVars]++;
CountNonTotal++;
}
for ( i = 0; i <= p->nVars; i++ )
{
printf( "%3d : ", i );
printf( "All = %8d ", CountAll[i] );
printf( "Non = %8d ", CountNon[i] );
printf( "(%6.2f %%)", 100.0 * CountNon[i] / CountAll[i] );
printf( "\n" );
}
printf( "All : " );
printf( "All = %8d ", Vec_PtrSize(p->vObjs) );
printf( "Non = %8d ", CountNonTotal );
printf( "(%6.2f %%)", 100.0 * CountNonTotal / Vec_PtrSize(p->vObjs) );
printf( "\n" );
}
void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
{
If_DsdObj_t * pObj;
int i, DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0;
int i, DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0, CountMarked = 0;
FILE * pFile;
pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
if ( pFileName && pFile == NULL )
......@@ -382,9 +413,11 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
DsdMax = Abc_MaxInt( DsdMax, pObj->nFans );
CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id );
CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 );
CountMarked += If_DsdVecObjMark( p->vObjs, i );
}
fprintf( pFile, "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) );
fprintf( pFile, "Externally used objects = %8d\n", CountUsed );
fprintf( pFile, "Marked objects = %8d\n", CountMarked );
fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", DsdMax, Vec_MemEntryNum(p->vTtMem) );
fprintf( pFile, "Non-DSD structures = %8d\n", CountNonDsdStr );
fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits );
......@@ -392,11 +425,15 @@ 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 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) );
If_DsdManPrintDistrib( p );
if ( p->timeDsd )
{
Abc_PrintTime( 1, "Time DSD ", p->timeDsd );
Abc_PrintTime( 1, "Time canon ", p->timeCanon-p->timeCheck );
Abc_PrintTime( 1, "Time check ", p->timeCheck );
Abc_PrintTime( 1, "Time check2", p->timeCheck2 );
Abc_PrintTime( 1, "Time verify", p->timeVerify );
}
// If_DsdManHashProfile( p );
// If_DsdManDump( p );
// If_DsdManDumpAll( p );
......@@ -1442,6 +1479,84 @@ void If_DsdManTest()
Vec_IntFree( vSets );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVerbose )
{
ProgressBar * pProgress = NULL;
If_DsdObj_t * pObj;
sat_solver * pSat = NULL;
sat_solver * pSat5 = NULL;
Vec_Int_t * vLits = Vec_IntAlloc( 1000 );
int i, Value, nVars;
word * pTruth;
pSat = (sat_solver *)If_ManSatBuildXY( LutSize );
if ( LutSize == 5 && fSpec )
pSat5 = (sat_solver *)If_ManSatBuild55();
If_DsdVecForEachObj( p->vObjs, pObj, i )
pObj->fMark = 0;
pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(p->vObjs) );
If_DsdVecForEachObj( p->vObjs, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
nVars = If_DsdObjSuppSize(pObj);
if ( nVars <= LutSize )
continue;
if ( LutSize == 5 && fSpec )
{
if ( nVars == 9 )
{
pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
Value = If_ManSatCheck55all( pSat5, pTruth, nVars, vLits );
}
else
{
if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) )
continue;
if ( fFast )
Value = 0;
else
{
pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits );
}
}
}
else
{
if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) )
continue;
if ( fFast )
Value = 0;
else
{
pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL );
Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits );
}
}
if ( Value )
continue;
If_DsdVecObjSetMark( p->vObjs, i );
}
if ( pProgress )
Extra_ProgressBarStop( pProgress );
If_ManSatUnbuild( pSat5 );
If_ManSatUnbuild( pSat );
Vec_IntFree( vLits );
if ( fVerbose )
If_DsdManPrintDistrib( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/map/if/ifSat.c
......@@ -268,6 +268,128 @@ int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsig
}
return 1;
}
int If_ManSatCheck55( void * pSat, word * pTruth, int nVars, int * pPerm9, word * pTBound, word * pTFree, Vec_Int_t * vLits )
{
sat_solver * p = (sat_solver *)pSat;
int v, Value, m, mNew;
int nMintsL = 16;
// remap minterms
Vec_IntFill( vLits, 512, -1 );
for ( m = 0; m < (1 << nVars); m++ )
{
mNew = 0;
for ( v = 0; v < 9; v++ )
{
assert( pPerm9[v] < nVars );
if ( ((m >> pPerm9[v]) & 1) )
mNew |= (1 << v);
}
assert( Vec_IntEntry(vLits, mNew) == -1 );
Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
}
// find assumptions
v = 0;
Vec_IntForEachEntry( vLits, Value, m )
if ( Value >= 0 )
Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) );
Vec_IntShrink( vLits, v );
// run SAT solver
Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
if ( Value != l_True )
return 0;
if ( pTBound && pTFree )
{
// collect config
*pTBound = 0;
for ( m = 0; m < nMintsL; m++ )
if ( sat_solver_var_value(p, m) )
Abc_TtSetBit( pTBound, m );
*pTBound = Abc_Tt6Stretch( *pTBound, 4 );
// collect configs
*pTFree = 0;
for ( m = 0; m < nMintsL; m++ )
if ( sat_solver_var_value(p, nMintsL+m) )
Abc_TtSetBit( pTFree, m );
*pTFree = Abc_Tt6Stretch( *pTFree, 4 );
}
return 1;
}
/**Function*************************************************************
Synopsis [Returns config string for the given truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned If_ManSatCheck55all_int( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits )
{
int Combs[10][5] = {
{0,1,2,3,4},
{0,2,1,3,4},
{0,3,1,2,4},
{0,4,1,2,3},
{1,2,0,3,4},
{1,3,0,2,4},
{1,4,0,2,3},
{2,3,0,1,4},
{2,4,0,1,3},
{3,4,0,1,2}
};
int pPerm9[9], Mark[9], i[6], k, n, c;
assert( nVars == 9 || nVars == 8 || nVars == 7 );
for ( i[0] = 0; i[0] < nVars; i[0]++ )
for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ )
for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ )
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
{
// add remaining ones
n = 5;
for ( k = 0; k < nVars; k++ )
Mark[k] = 0;
for ( k = 0; k < 5; k++ )
Mark[i[k]] = 1;
for ( k = 0; k < nVars; k++ )
if ( Mark[k] == 0 )
pPerm9[n++] = k;
assert( n == nVars );
for ( ; n < 9; n++ )
pPerm9[n] = pPerm9[n-1];
assert( n == 9 );
// current ones
for ( c = 0; c < 10; c++ )
{
for ( n = 0; n < 5; n++ )
pPerm9[n] = i[Combs[c][n]];
// try different combinations
for ( k = 5; k < nVars; k++ )
{
ABC_SWAP( int, pPerm9[5], pPerm9[k] );
if ( If_ManSatCheck55(pSat, pTruth, nVars, pPerm9, NULL, NULL, vLits) )
{
// for ( k = 0; k < 9; k++ )
// printf( "%c", 'a' + pPerm9[k] );
// printf( "\n" );
return 1;
}
ABC_SWAP( int, pPerm9[5], pPerm9[k] );
}
}
}
return 0;
}
unsigned If_ManSatCheck55all( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits )
{
// abctime clk = Abc_Clock();
unsigned Value = If_ManSatCheck55all_int( pSat, pTruth, nVars, vLits );
// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return Value;
}
/**Function*************************************************************
......@@ -408,6 +530,7 @@ unsigned If_ManSatCheckXYall_int( void * pSat, int nLutSize, word * pTruth, int
for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ )
for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ )
{
uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4]));
for ( s[0] = 0; s[0] < nLutSize; s[0]++ )
for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ )
for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ )
......@@ -538,8 +661,7 @@ void If_ManSatTest2()
sat_solver_delete(p);
Vec_IntFree( vLits );
}
void If_ManSatTest()
void If_ManSatTest3()
{
int nVars = 6;
int nLutSize = 4;
......@@ -558,6 +680,22 @@ void If_ManSatTest()
sat_solver_delete(p);
Vec_IntFree( vLits );
}
void If_ManSatTest()
{
int nVars = 9;
sat_solver * p = (sat_solver *)If_ManSatBuild55();
// char * pDsd = "[([(ab)cde]f)ghi]";
// char * pDsd = "[([(hi)cde]f)gab]";
char * pDsd = "[(0123{(hi)cde}f)gab]";
word * pTruth = Dau_DsdToTruth( pDsd, nVars );
Vec_Int_t * vLits = Vec_IntAlloc( 1000 );
if ( If_ManSatCheck55all( p, pTruth, nVars, vLits ) )
printf( "Found!\n" );
else
printf( "Not found!\n" );
sat_solver_delete(p);
Vec_IntFree( vLits );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
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