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

Changes to several APIs.

This commit is contained in:
Alan Mishchenko 2019-12-05 09:53:42 -08:00
parent bb33b5978a
commit 1e602492d8
4 changed files with 92 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/giaSim4.c
View File

@ -41,7 +41,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose )
int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose )
{
return 0;
}

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

@ -7128,11 +7128,11 @@ usage:
***********************************************************************/
int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose );
extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose );
char * pFileNames[4] = {NULL, NULL, "out.v", NULL};
int c, fOrder = 0, nWords = 1, fVerbose = 0;
int c, nWords = 4, nBeam = 4, LevL = 0, LevU = 0, fOrder = 0, fFancy = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Wovh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofvh" ) ) != EOF )
{
switch ( c )
{
@ -7147,9 +7147,45 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nWords < 0 )
goto usage;
break;
case 'B':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage;
}
nBeam = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nBeam < 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;
}
LevL = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( LevL < 0 )
goto usage;
break;
case 'U':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-U\" should be followed by an integer.\n" );
goto usage;
}
LevU = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( LevU < 0 )
goto usage;
break;
case 'o':
fOrder ^= 1;
break;
case 'f':
fFancy ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -7167,15 +7203,19 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManRandom(1);
for ( c = 0; c < argc - globalUtilOptind; c++ )
pFileNames[c] = argv[globalUtilOptind+c];
Acb_NtkRunSim( pFileNames, nWords, fOrder, fVerbose );
Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: runsim [-W] [-ovh] [-N <num>] <file1> <file2> <file3>\n" );
Abc_Print( -2, "usage: runsim [-WBLU] [-ofvh] [-N <num>] <file1> <file2> <file3>\n" );
Abc_Print( -2, "\t experimental simulation command\n" );
Abc_Print( -2, "\t-W <num> : the number of words of simulation info [default = %d]\n", nWords );
Abc_Print( -2, "\t-B <num> : the beam width parameter [default = %d]\n", nBeam );
Abc_Print( -2, "\t-L <num> : the lower bound on level [default = %d]\n", LevL );
Abc_Print( -2, "\t-U <num> : the upper bound on level [default = %d]\n", LevU );
Abc_Print( -2, "\t-o : toggle using a different node ordering [default = %s]\n", fOrder? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-f : toggle using experimental feature [default = %s]\n", fFancy? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}

48
src/base/acb/acbFunc.c
View File

@ -888,6 +888,12 @@ Vec_Int_t * Acb_FindSupportStart( sat_solver * pSat, int iFirstDiv, Vec_Int_t *
//printf( "Selecting divisor %d with weight %d\n", i, Vec_IntEntry(vWeights, i) );
fFound = 1;
}
if ( fFound == 0 )
{
Vec_WrdFree( vPats );
Vec_IntFree( vSupp );
return NULL;
}
assert( fFound );
iPat++;
}
@ -1102,7 +1108,10 @@ Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeig
else
vSupp = Acb_FindSupportNext( pSat, iFirstDiv, vWeights, vPats, &nPats );
if ( vSupp == NULL )
break;
{
Vec_IntFree( vSuppBest );
return NULL;
}
//vSupp = Acb_FindSupportMin( pSat, iFirstDiv, vPats, &nPats, vTemp = vSupp );
//Vec_IntFree( vTemp );
if ( vSupp == NULL )
@ -1241,6 +1250,7 @@ Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, in
// find minimum subset
if ( fUseMinAssump )
{
int fUseSuppMin = 1;
// solve in a standard way
abctime clk = Abc_Clock();
nSuppNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
@ -1250,20 +1260,25 @@ Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, in
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// perform minimization
if ( Vec_IntSize(vSupp) > 0 )
if ( fUseSuppMin && Vec_IntSize(vSupp) > 0 )
{
abctime clk = Abc_Clock();
Vec_Int_t * vSupp2 = Vec_IntDup( vSupp );
Vec_Int_t * vTemp, * vWeights = Acb_DeriveWeights( vDivs, pNtkF );
vSupp = Acb_FindSupport( pSat, iDivVar, vWeights, vTemp = vSupp, TimeOut );
Vec_IntFree( vWeights );
Vec_IntFree( vTemp );
if ( vSupp == NULL )
{
printf( "Support minimization timed out after %d sec.\n", TimeOut );
sat_solver_delete( pSat );
return NULL;
printf( "Support minimization did not succeed. " );
//sat_solver_delete( pSat );
vSupp = vSupp2;
}
else
{
Vec_IntFree( vSupp2 );
printf( "Minimized support to %d supp vars. ", Vec_IntSize(vSupp) );
}
printf( "Minimized support to %d supp vars. ", Vec_IntSize(vSupp) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
}
@ -1504,6 +1519,17 @@ char * Acb_EnumerateSatAssigns( sat_solver * pSat, int PivotVar, int FreeVar, Ve
{
if ( iMint == 1000 )
{
//if ( Vec_IntSize(vDivVars) == 0 )
{
printf( "Assuming constant 0 function.\n" );
Vec_StrClear( vTempSop );
Vec_StrPush( vTempSop, ' ' );
Vec_StrPush( vTempSop, '0' );
Vec_StrPush( vTempSop, '\n' );
Vec_StrPush( vTempSop, '\0' );
return Vec_StrReleaseArray(vTempSop);
}
printf( "Reached the limit on the number of cubes (1000).\n" );
Vec_IntFree( vTemp );
Vec_IntFree( vLits );
@ -2039,7 +2065,17 @@ Cnf_Dat_t * Acb_NtkDeriveMiterCnf( Gia_Man_t * p, int iTar, int nTars, int fVerb
Cnf_Dat_t * pCnf; int v;
for ( v = 0; v < iTar; v++ )
{
Gia_Man_t * pTemp;
pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
//pCof = Acb_NtkEcoSynthesize( pTemp = pCof );
//pCof = Gia_ManCompress2( pTemp = pCof, 1, 0 );
pCof = Gia_ManAigSyn2( pTemp = pCof, 0, 1, 0, 100, 0, 0, 0 );
Gia_ManStop( pTemp );
if ( Gia_ManAndNum(pCof) > 10000 )
{
printf( "Quantifying target %3d ", v );
Gia_ManPrintStats( pCof, NULL );
}
assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) );
Gia_ManStop( p );
}

6
src/base/acb/acbUtil.c
View File

@ -764,12 +764,12 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames
SeeAlso []
***********************************************************************/
void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose )
void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose )
{
extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose );
extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose );
extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose );
char * pFileNames[4] = { pFileName[2], pFileName[1], NULL, pFileName[2] };
if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, fOrder, fVerbose ) )
if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, nBeam, LevL, LevU, fOrder, fFancy, fVerbose ) )
Acb_NtkRunEco( pFileNames, 1, fVerbose );
}