Skip to content

A
abc
Commit 30ae05f0 by Alan Mishchenko
Options

Scalable gate-level abstraction.

parent e9af6c3c
Showing with 51 additions and 22 deletions
src/aig/gia/gia.h
......@@ -220,6 +220,7 @@ struct Gia_ParVta_t_
int nLearnedPerce; // percentage of clauses to leave
int nTimeOut; // timeout in seconds
int nRatioMin; // stop when less than this % of object is abstracted
int nRatioMax; // restart when the number of abstracted object is more than this
int fUseTermVars; // use terminal variables
int fUseRollback; // use rollback to the starting number of frames
int fPropFanout; // propagate fanout implications
......
src/aig/gia/giaAbsGla2.c
......@@ -396,8 +396,8 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vIsopMem = Vec_IntAlloc( 100 );
Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
// hash table
p->nTable = 1000003;
p->pTable = ABC_CALLOC( int, 6 * p->nTable ); // 2.4 MB
p->nTable = Abc_PrimeCudd(1<<18);
p->pTable = ABC_CALLOC( int, 6 * p->nTable );
return p;
}
void Ga2_ManReportMemory( Ga2_Man_t * p )
......@@ -408,6 +408,7 @@ void Ga2_ManReportMemory( Ga2_Man_t * p )
double memPro = sat_solver2_memory_proof( p->pSat );
double memMap = Vec_VecMemoryInt( (Vec_Vec_t *)p->vId2Lit );
double memRef = Rnm_ManMemoryUsage( p->pRnm );
double memHash= sizeof(int) * 6 * p->nTable;
double memOth = sizeof(Ga2_Man_t);
memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCnfs );
memOth += Vec_IntMemory( p->vIds );
......@@ -417,12 +418,13 @@ void Ga2_ManReportMemory( Ga2_Man_t * p )
memOth += Vec_IntMemory( p->vLits );
memOth += Vec_IntMemory( p->vIsopMem );
memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
memTot = memAig + memSat + memPro + memMap + memRef + memOth;
memTot = memAig + memSat + memPro + memMap + memRef + memHash + memOth;
ABC_PRMP( "Memory: AIG ", memAig, memTot );
ABC_PRMP( "Memory: SAT ", memSat, memTot );
ABC_PRMP( "Memory: Proof ", memPro, memTot );
ABC_PRMP( "Memory: Map ", memMap, memTot );
ABC_PRMP( "Memory: Refine ", memRef, memTot );
ABC_PRMP( "Memory: Hash ", memHash,memTot );
ABC_PRMP( "Memory: Other ", memOth, memTot );
ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
}
......@@ -435,6 +437,7 @@ void Ga2_ManStop( Ga2_Man_t * p )
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat),
sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat),
p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
if ( p->pPars->fVerbose )
Abc_Print( 1, "Hash hits = %d. Hash misses = %d. Hash overs = %d.\n",
p->nHashHit, p->nHashMiss, p->nHashOver );
......@@ -894,7 +897,7 @@ static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, i
{
int * pLookup, nSize = Vec_IntSize(p->vLits);
assert( Vec_IntSize(p->vLits) < 5 );
assert( Vec_IntEntry(p->vLits, 0) < Vec_IntEntryLast(p->vLits) );
assert( Vec_IntEntry(p->vLits, 0) <= Vec_IntEntryLast(p->vLits) );
assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
for ( i = Vec_IntSize(p->vLits); i < 4; i++ )
Vec_IntPush( p->vLits, GA2_BIG_NUM );
......@@ -928,7 +931,6 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
int fSimple = 0;
Gia_Obj_t * pObj;
int i;
// add variables for the leaves
Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
{
if ( i == p->LimAbs )
......@@ -941,6 +943,7 @@ void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
if ( i >= p->LimAbs )
Ga2_ManAddToAbsOneStatic( p, pObj, f );
// sat_solver2_simplify( p->pSat );
}
void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
......@@ -970,13 +973,14 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
Ga2_ManAddToAbsOneStatic( p, pObj, f );
}
// sat_solver2_simplify( p->pSat );
}
void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues, int nSatVars )
{
Vec_Int_t * vMap;
Gia_Obj_t * pObj;
int i;
int i, k, Entry;
assert( nAbs > 0 );
assert( nValues > 0 );
assert( nSatVars > 0 );
......@@ -1004,9 +1008,17 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues, int nSatVars )
}
Vec_IntShrink( p->vValues, nValues );
Vec_PtrShrink( p->vCnfs, 2 * nValues );
// hack to clear constant
if ( nValues == 1 )
nValues = 0;
// clean mapping for each timeframe
Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
Vec_IntClear( vMap );
{
Vec_IntShrink( vMap, nValues );
Vec_IntForEachEntry( vMap, Entry, k )
if ( Entry >= 2*nSatVars )
Vec_IntWriteEntry( vMap, k, -1 );
}
// shrink SAT variables
p->nSatVars = nSatVars;
}
......@@ -1503,10 +1515,13 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// iterate unrolling
for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
{
int nAbsOld;
// remember the timeframe
p->pPars->iFrame = -1;
// create new SAT solver
Ga2_ManRestart( p );
// remember abstraction size after the last restart
nAbsOld = Vec_IntSize(p->vAbs);
// unroll the circuit
for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
{
......@@ -1534,7 +1549,8 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
continue;
assert( Lit > 1 );
// check for counter-examples
sat_solver2_setnvars( p->pSat, p->nSatVars );
// if ( p->nSatVars > sat_solver2_nvars(p->pSat) )
// sat_solver2_setnvars( p->pSat, p->nSatVars );
nVarsOld = p->nSatVars;
for ( c = 0; ; c++ )
{
......@@ -1646,7 +1662,17 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
iFrameProved = f;
if ( p->pPars->fVeryVerbose )
Abc_Print( 1, "\n" );
break; // temporary
// if abstraction grew more than a certain percentage, force a restart
if ( pPars->nRatioMax == 0 )
break;
if ( Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
{
if ( p->pPars->fVeryVerbose )
Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n",
nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
break;
}
}
}
......
src/aig/gia/giaAbsVta.c
......@@ -158,6 +158,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
p->nLearnedPerce = 40; // max number of learned clauses
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 10; // stop when less than this % of object is abstracted
p->nRatioMax = 0; // restart when more than this % of object is abstracted
p->fUseTermVars = 0; // use terminal variables
p->fUseRollback = 0; // use rollback to the starting number of frames
p->fVerbose = 0; // verbose flag
......
src/base/abci/abc.c
......@@ -28112,7 +28112,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, fStartVta = 0, fNewAlgo = 0;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLDETRAtrfkadnscbwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPAtrfkadnscbwvh" ) ) != EOF )
{
switch ( c )
{
......@@ -28138,17 +28138,6 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nFramesStart < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesPast = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesPast < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
......@@ -28215,6 +28204,17 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nRatioMin < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nRatioMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nRatioMax < 0 )
goto usage;
break;
case 'A':
if ( globalUtilOptind >= argc )
{
......@@ -28302,7 +28302,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &gla [-FSCLDETR num] [-A file] [-fkadnscbwvh]\n" );
Abc_Print( -2, "usage: &gla [-FSCLDETRP num] [-A file] [-fkadnscbwvh]\n" );
Abc_Print( -2, "\t fixed-time-frame gate-level proof- and cex-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
......@@ -28312,6 +28312,7 @@ usage:
Abc_Print( -2, "\t-E num : ratio percentage for learned clause removal [default = %d]\n", pPars->nLearnedPerce );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
Abc_Print( -2, "\t-P num : maximum percentage of added objects before a restart (0<=num<=100) [default = %d]\n", pPars->nRatioMax );
Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
Abc_Print( -2, "\t-f : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
Abc_Print( -2, "\t-k : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" );
......
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