mirror of https://github.com/YosysHQ/abc.git
New command "&genlutcas".
This commit is contained in:
Alan Mishchenko
parent
6cab944535
commit
0a650c18cf
|
|
@ -0,0 +1,149 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [giaLutCas.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Scalable AIG package.]
|
||||
|
||||
Synopsis [LUT cascade generator.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: giaLutCas.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "gia.h"
|
||||
#include "sat/cnf/cnf.h"
|
||||
#include "misc/util/utilTruth.h"
|
||||
#include "sat/cadical/cadicalSolver.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Gia_LutCasSort( char * pStr, int iStart, int nChars )
|
||||
{
|
||||
int i, j;
|
||||
for ( i = iStart; i < iStart + nChars - 1; i++ )
|
||||
for ( j = i + 1; j < iStart + nChars; j++ )
|
||||
if ( pStr[i] > pStr[j] )
|
||||
ABC_SWAP( char, pStr[i], pStr[j] );
|
||||
}
|
||||
char * Gia_LutCasPerm( int nVars, int nLuts, int LutSize )
|
||||
{
|
||||
assert( nVars <= 26 && nLuts <= 100 );
|
||||
int nStrLen = nLuts * LutSize;
|
||||
char * pRes = ABC_CALLOC( char, nStrLen+1 );
|
||||
int i, j, iVar, pPerm[26], nVarCount[100] = {0};
|
||||
// create a random permutation
|
||||
for ( i = 0; i < nVars; i++ )
|
||||
pPerm[i] = i;
|
||||
for ( i = nVars - 1; i > 0; i-- ) {
|
||||
j = rand() % (i + 1);
|
||||
ABC_SWAP( int, pPerm[i], pPerm[j] );
|
||||
}
|
||||
// assign the first variable
|
||||
for ( i = 0; i < nLuts; i++ ) {
|
||||
pRes[i * LutSize] = i ? '_' : 'a' + pPerm[0];
|
||||
nVarCount[i] = 1;
|
||||
}
|
||||
// First pass: distribute each variable (starting from the second in permutation) to at least one LUT
|
||||
for ( i = 1; i < nVars; i++ ) {
|
||||
// Find a LUT with space that doesn't have this variable
|
||||
int Tries = 0, iLut = rand() % nLuts;
|
||||
while ( nVarCount[iLut] >= LutSize && Tries++ < nLuts )
|
||||
iLut = (iLut + 1) % nLuts;
|
||||
// the variables are unique - no need to check this
|
||||
pRes[iLut * LutSize + nVarCount[iLut]] = 'a' + pPerm[i];
|
||||
nVarCount[iLut]++;
|
||||
}
|
||||
// Second pass: fill remaining slots with random variables (cycling through permutation)
|
||||
for ( i = 0; i < nLuts; i++ ) {
|
||||
while ( nVarCount[i] < LutSize ) {
|
||||
iVar = pPerm[rand() % nVars];
|
||||
// Check this LUT already has this variable
|
||||
for ( j = 0; j < nVarCount[i]; j++ )
|
||||
if ( pRes[i * LutSize + j] == 'a' + iVar )
|
||||
break;
|
||||
if ( j == nVarCount[i] ) { // does not have
|
||||
pRes[i * LutSize + nVarCount[i]] = 'a' + iVar;
|
||||
nVarCount[i]++;
|
||||
}
|
||||
}
|
||||
}
|
||||
// Sort inputs within each LUT (skip '_' for non-first LUTs)
|
||||
Gia_LutCasSort( pRes, 0, LutSize );
|
||||
for ( i = 1; i < nLuts; i++ )
|
||||
Gia_LutCasSort( pRes + i * LutSize, 1, LutSize-1 );
|
||||
return pRes;
|
||||
}
|
||||
int Gia_ManLutCasGen_rec( Gia_Man_t * pNew, Vec_Int_t * vCtrls, int iCtrl, Vec_Int_t * vDatas, int Shift )
|
||||
{
|
||||
if ( iCtrl-- == 0 )
|
||||
return Vec_IntEntry( vDatas, Shift );
|
||||
int iLit0 = Gia_ManLutCasGen_rec( pNew, vCtrls, iCtrl, vDatas, Shift );
|
||||
int iLit1 = Gia_ManLutCasGen_rec( pNew, vCtrls, iCtrl, vDatas, Shift + (1<<iCtrl));
|
||||
return Gia_ManAppendMux( pNew, Vec_IntEntry(vCtrls, iCtrl), iLit1, iLit0 );
|
||||
}
|
||||
Gia_Man_t * Gia_ManLutCasGen( int nVars, int nLuts, int LutSize, int Seed, int fVerbose )
|
||||
{
|
||||
srand(Seed);
|
||||
char * pPerm = Gia_LutCasPerm( nVars, nLuts, LutSize );
|
||||
int nParams = nLuts * (1 << LutSize);
|
||||
printf( "Generating AIG with %d parameters and %d inputs using fanin assignment %s.\n", nParams, nVars, pPerm );
|
||||
Gia_Man_t * pNew = Gia_ManStart( nParams + nVars );
|
||||
pNew->pName = Abc_UtilStrsav( pPerm );
|
||||
Vec_Int_t * vDatas = Vec_IntAlloc( nParams );
|
||||
Vec_Int_t * vCtrls = Vec_IntAlloc( nVars );
|
||||
for ( int i = 0; i < nParams; i++ )
|
||||
Vec_IntPush( vDatas, Gia_ManAppendCi(pNew) );
|
||||
for ( int i = 0; i < nVars; i++ )
|
||||
Vec_IntPush( vCtrls, Gia_ManAppendCi(pNew) );
|
||||
Vec_Int_t * vLits = Vec_IntStart( LutSize );
|
||||
Vec_IntWriteEntry( vLits, 0, Vec_IntEntry(vCtrls, (int)(pPerm[0]-'a')) );
|
||||
char * pCur = pPerm;
|
||||
for ( int i = 0; i < nLuts; i++ ) {
|
||||
pCur++;
|
||||
for ( int k = 1; k < LutSize; k++ )
|
||||
Vec_IntWriteEntry( vLits, k, Vec_IntEntry(vCtrls, (int)(*pCur++ - 'a')) );
|
||||
Vec_IntWriteEntry( vLits, 0, Gia_ManLutCasGen_rec(pNew, vLits, LutSize, vDatas, i * (1 << LutSize)) );
|
||||
}
|
||||
Gia_ManAppendCo( pNew, Vec_IntEntry(vLits, 0) );
|
||||
Vec_IntFree( vDatas );
|
||||
Vec_IntFree( vCtrls );
|
||||
Vec_IntFree( vLits );
|
||||
ABC_FREE( pPerm );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -50,6 +50,7 @@ SRC += src/aig/gia/giaAig.c \
|
|||
src/aig/gia/giaJf.c \
|
||||
src/aig/gia/giaKf.c \
|
||||
src/aig/gia/giaLf.c \
|
||||
src/aig/gia/giaLutCas.c \
|
||||
src/aig/gia/giaMf.c \
|
||||
src/aig/gia/giaMan.c \
|
||||
src/aig/gia/giaMem.c \
|
||||
|
|
|
|||
|
|
@ -580,6 +580,7 @@ static int Abc_CommandAbc9FFTest ( Abc_Frame_t * pAbc, int argc, cha
|
|||
static int Abc_CommandAbc9Qbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9QVar ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9GenQbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9GenLutCas ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9HomoQbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9SatFx ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9SatClp ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
|
@ -1402,6 +1403,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "ABC9", "&qbf", Abc_CommandAbc9Qbf, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&qvar", Abc_CommandAbc9QVar, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&genqbf", Abc_CommandAbc9GenQbf, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&genlutcas", Abc_CommandAbc9GenLutCas, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&homoqbf", Abc_CommandAbc9HomoQbf, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&satfx", Abc_CommandAbc9SatFx, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&satclp", Abc_CommandAbc9SatClp, 0 );
|
||||
|
|
@ -51659,6 +51661,126 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandAbc9GenLutCas( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern Gia_Man_t * Gia_ManLutCasGen( int nVars, int nLuts, int LutSize, int Seed, int fVerbose );
|
||||
int nVars = 8;
|
||||
int nLuts = 2;
|
||||
int LutSize = 6;
|
||||
int Seed = 0;
|
||||
int fVerbose = 0;
|
||||
int c;
|
||||
Gia_Man_t * pTemp;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "NMKSvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'N':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
nVars = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( nVars < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'M':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
nLuts = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( nLuts < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'K':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
LutSize = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( LutSize < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'S':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
Seed = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( Seed < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( nVars <= LutSize )
|
||||
{
|
||||
Abc_Print( -1, "The number of inputs (%d) should be more than LUT size (%d).\n", nVars, LutSize );
|
||||
return 1;
|
||||
}
|
||||
if ( nVars > 100 )
|
||||
{
|
||||
Abc_Print( -1, "The number of inputs (%d) should be less than 100.\n", nVars );
|
||||
return 1;
|
||||
}
|
||||
if ( nLuts < 2 || nLuts > 100 )
|
||||
{
|
||||
Abc_Print( -1, "The LUT count (%d) should be morein the range [2;100].\n", nLuts );
|
||||
return 1;
|
||||
}
|
||||
if ( LutSize < 2 || LutSize > 12 )
|
||||
{
|
||||
Abc_Print( -1, "The LUT size (%d) should be in the range [2;12].\n", LutSize );
|
||||
return 1;
|
||||
}
|
||||
if ( nVars > (nLuts-1)*(LutSize-1) + LutSize )
|
||||
{
|
||||
Abc_Print( -1, "Function with %d variables is too large for a cascade composed of %d connected %d-LUTs.\n", nVars, nLuts, LutSize );
|
||||
return 1;
|
||||
}
|
||||
pTemp = Gia_ManLutCasGen( nVars, nLuts, LutSize, Seed, fVerbose );
|
||||
Abc_FrameUpdateGia( pAbc, pTemp );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &genlutcas[-NMKS num] [-vh]\n" );
|
||||
Abc_Print( -2, "\t generates single-rail LUT cascade\n" );
|
||||
Abc_Print( -2, "\t-N num : the number of primary inputs [default = %d]\n", nVars );
|
||||
Abc_Print( -2, "\t-M num : the number of LUTs [default = %d]\n", nLuts );
|
||||
Abc_Print( -2, "\t-K num : the LUT size [default = %d]\n", LutSize );
|
||||
Abc_Print( -2, "\t-S num : the random seed [default = %d]\n", Seed );
|
||||
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
|
|||
|
|
@ -35,12 +35,12 @@ bool Internal::stabilizing () {
|
|||
STOP (stable);
|
||||
else
|
||||
STOP (unstable);
|
||||
const int64_t delta_conflicts =
|
||||
stats.conflicts - last.stabilize.conflicts;
|
||||
//const int64_t delta_conflicts =
|
||||
// stats.conflicts - last.stabilize.conflicts;
|
||||
const int64_t delta_ticks =
|
||||
stats.ticks.search[stable] - last.stabilize.ticks;
|
||||
const char *current_mode = stable ? "stable" : "unstable";
|
||||
const char *next_mode = stable ? "unstable" : "stable";
|
||||
//const char *current_mode = stable ? "stable" : "unstable";
|
||||
//const char *next_mode = stable ? "unstable" : "stable";
|
||||
PHASE ("stabilizing", stats.stabphases,
|
||||
"reached %s stabilization limit %" PRId64 " after %" PRId64
|
||||
" conflicts and %" PRId64 " ticks at %" PRId64
|
||||
|
|
|
|||
Loading…
Reference in New Issue