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

Improvements to the QBF solver.

This commit is contained in:
Alan Mishchenko 2011-10-24 18:05:45 +08:00
parent 88c36d9d65
commit f96f3fa583
3 changed files with 59 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -8170,7 +8170,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c;
int nVars;
int nVars; // the number of variables
int nLutSize; // the size of LUTs
int nLuts; // the number of LUTs
int fAdder;
int fSorter;
int fMesh;
@ -8196,7 +8198,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
fRandom = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmftrvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NKLasmftrvh" ) ) != EOF )
{
switch ( c )
{
@ -8211,6 +8213,28 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nVars < 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;
}
nLutSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLutSize < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
nLuts = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLuts < 0 )
goto usage;
break;
case 'a':
fAdder ^= 1;
break;
@ -8253,7 +8277,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
else if ( fMesh )
Abc_GenMesh( FileName, nVars );
else if ( fFpga )
Abc_GenFpga( FileName, 4, 3, 10 );
Abc_GenFpga( FileName, nLutSize, nLuts, nVars );
// Abc_GenFpga( FileName, 2, 2, 3 );
// Abc_GenFpga( FileName, 3, 2, 5 );
else if ( fOneHot )
@ -8265,9 +8289,11 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: gen [-N num] [-asmftrvh] <file>\n" );
Abc_Print( -2, "usage: gen [-NKL num] [-asmftrvh] <file>\n" );
Abc_Print( -2, "\t generates simple circuits\n" );
Abc_Print( -2, "\t-N num : the number of variables [default = %d]\n", nVars );
Abc_Print( -2, "\t-K num : the LUT size (to be used with switch -f) [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-L num : the LUT count (to be used with switch -f) [default = %d]\n", nLuts );
Abc_Print( -2, "\t-a : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );
Abc_Print( -2, "\t-s : generate a sorter [default = %s]\n", fSorter? "yes": "no" );
Abc_Print( -2, "\t-m : generate a mesh [default = %s]\n", fMesh? "yes": "no" );
@ -11053,8 +11079,8 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: qbf [-P num] [-vh]\n" );
Abc_Print( -2, "\t solves a quantified intean formula problem EpVxM(p,x)\n" );
Abc_Print( -2, "\t-P num : number of paramters (should be the first PIs) [default = %d]\n", nPars );
Abc_Print( -2, "\t solves QBF problem EpVxM(p,x)\n" );
Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars );
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;

24
src/base/abci/abcGen.c
View File

@ -424,6 +424,7 @@ void Abc_WriteKLut( FILE * pFile, int nLutSize )
***********************************************************************/
void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
{
int fGenerateFunc = 1;
FILE * pFile;
int nVarsLut = (1 << nLutSize); // the number of LUT variables
int nVarsLog = Extra_Base2Log( nVars + nLuts - 1 ); // the number of encoding vars
@ -440,7 +441,11 @@ void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
fprintf( pFile, ".inputs" );
for ( i = 0; i < nParsLut; i++ )
{
if ( i % (1 << nLutSize) == 0 && i != (nLuts - 1) * (1 << nLutSize) )
continue;
fprintf( pFile, " pl%02d", i );
}
fprintf( pFile, "\n" );
fprintf( pFile, ".inputs" );
@ -454,11 +459,28 @@ void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
fprintf( pFile, "\n" );
fprintf( pFile, ".outputs" );
fprintf( pFile, " v%02d", nVars + nLuts - 1 );
// fprintf( pFile, " v%02d", nVars + nLuts - 1 );
fprintf( pFile, " out" );
fprintf( pFile, "\n" );
fprintf( pFile, ".names Gnd\n" );
fprintf( pFile, " 0\n" );
// generate function
if ( fGenerateFunc )
{
fprintf( pFile, ".names v%02d func out\n", nVars + nLuts - 1 );
fprintf( pFile, "00 1\n11 1\n" );
fprintf( pFile, ".names" );
for ( i = 0; i < nVars; i++ )
fprintf( pFile, " v%02d", i );
fprintf( pFile, " func\n" );
for ( i = 0; i < nVars; i++ )
fprintf( pFile, "1" );
fprintf( pFile, " 1\n" );
}
else
fprintf( pFile, ".names v%02d out\n1 1\n", nVars + nLuts - 1 );
// generate LUTs
for ( i = 0; i < nLuts; i++ )
{

7
src/base/abci/abcQbf.c
View File

@ -89,7 +89,8 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose )
{
// solve the synthesis instance
clkS = clock();
RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
// RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0 );
clkS = clock() - clkS;
if ( RetValue == 0 )
Abc_NtkModelToVector( pNtkSyn, vPiValues );
@ -143,8 +144,8 @@ clkV = clock() - clkV;
printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
printf( " " );
// ABC_PRTn( "Syn", clkS );
ABC_PRT( "Ver", clkV );
ABC_PRT( "Syn", clkS );
// ABC_PRT( "Ver", clkV );
}
}
Abc_NtkDelete( pNtkSyn );