Skip to content

A
abc
Commit 051cc64e by Alan Mishchenko
Options

Gate level abstraction (command &gla).

parent 311486d9
Showing with 102 additions and 42 deletions
abc.rc
......@@ -119,6 +119,7 @@ alias share "st; multi -m; fx; resyn2"
alias addinit "read_init; undc; strash; zero"
alias blif2aig "undc; strash; zero"
alias v2p "&vta_gla; &ps; &gla_derive; &put; w 1.aig; pdr -v"
alias g2p "&ps; &gla_derive; &put; w 2.aig; pdr -v"
# resubstitution scripts for the IWLS paper
alias src_rw "st; rw -l; rwz -l; rwz -l"
......
src/aig/gia/giaAbsGla.c
......@@ -56,8 +56,10 @@ struct Gla_Man_t_
Gia_Man_t * pGia; // AIG manager
Gia_ParVta_t* pPars; // parameters
// internal data
Vec_Int_t * vAbs; // abstracted objects
Gla_Obj_t * pObjs; // objects
int nObjs; // the number of objects
int nAbsOld; // previous abstraction
// other data
int nCexes; // the number of counter-examples
int nSatVars; // the number of SAT variables
......@@ -67,6 +69,7 @@ struct Gla_Man_t_
Vec_Int_t * vTemp; // temporary array
Vec_Int_t * vAddedNew; // temporary array
// statistics
int timeInit;
int timeSat;
int timeUnsat;
int timeCex;
......@@ -79,9 +82,11 @@ static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { ass
static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj ); }
// iterator through abstracted objects
#define Gla_ManForEachObjAbs( p, pObj ) \
for ( pObj = p->pObjs + 1; pObj < p->pObjs + p->nObjs; pObj++ ) if ( !pObj->fAbs ) {} else
#define Gla_ManForEachObjAbsVec( vVec, p, pObj, i ) \
#define Gla_ManForEachObj( p, pObj ) \
for ( pObj = p->pObjs + 1; pObj < p->pObjs + p->nObjs; pObj++ )
#define Gla_ManForEachObjAbs( p, pObj, i ) \
for ( i = 0; i < Vec_IntSize(p->vAbs) && ((pObj = Gla_ManObj(p, Vec_IntEntry(p->vAbs, i))),1); i++)
#define Gla_ManForEachObjAbsVec( vVec, p, pObj, i ) \
for ( i = 0; i < Vec_IntSize(vVec) && ((pObj = Gla_ManObj(p, Vec_IntEntry(vVec, i))),1); i++)
// iterator through fanins of an abstracted object
......@@ -283,6 +288,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p = ABC_CALLOC( Gla_Man_t, 1 );
p->pGia = pGia;
p->pPars = pPars;
p->vAbs = Vec_IntAlloc( 100 );
p->vTemp = Vec_IntAlloc( 100 );
p->vAddedNew = Vec_IntAlloc( 100 );
// internal data
......@@ -325,20 +331,24 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) )
{
Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp );
pGla->fConst = Gia_ObjIsConst0(pObj);
pGla->nFanins = Vec_IntSize( p->vTemp );
memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) );
continue;
}
assert( Gia_ObjIsRo(p->pGia, pObj) );
pGla->nFanins = 1;
pGla->nFanins = 1;
pGla->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value;
pGla->fCompl0 = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) );
pGla->fCompl0 = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) );
}
// abstraction
assert( pGia->vGateClasses != NULL );
for ( pGla = p->pObjs + 1; pGla < p->pObjs + p->nObjs; pGla++ )
pGla->fAbs = (Vec_IntEntry( pGia->vGateClasses, pGla->iGiaObj ) == 1);
Gla_ManForEachObj( p, pGla )
{
if ( Vec_IntEntry( pGia->vGateClasses, pGla->iGiaObj ) == 0 )
continue;
pGla->fAbs = 1;
Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
}
// other
p->vCla2Obj = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Obj, -1 );
p->pSat = sat_solver2_new();
......@@ -360,13 +370,14 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
void Gla_ManStop( Gla_Man_t * p )
{
Gla_Obj_t * pGla;
for ( pGla = p->pObjs + 1; pGla < p->pObjs + p->nObjs; pGla++ )
Gla_ManForEachObj( p, pGla )
ABC_FREE( pGla->vFrames.pArray );
Cnf_DataFree( p->pCnf );
sat_solver2_delete( p->pSat );
Vec_IntFree( p->vCla2Obj );
Vec_IntFree( p->vAddedNew );
Vec_IntFree( p->vTemp );
Vec_IntFree( p->vAbs );
ABC_FREE( p->pObjs );
ABC_FREE( p );
}
......@@ -385,15 +396,15 @@ void Gla_ManStop( Gla_Man_t * p )
int Gia_GlaAbsCount( Gla_Man_t * p, int fRo, int fAnd )
{
Gla_Obj_t * pObj;
int Counter = 0;
int i, Counter = 0;
if ( fRo )
Gla_ManForEachObjAbs( p, pObj )
Gla_ManForEachObjAbs( p, pObj, i )
Counter += (pObj->fRo && pObj->fAbs);
else if ( fAnd )
Gla_ManForEachObjAbs( p, pObj )
Gla_ManForEachObjAbs( p, pObj, i )
Counter += (pObj->fAnd && pObj->fAbs);
else
Gla_ManForEachObjAbs( p, pObj )
Gla_ManForEachObjAbs( p, pObj, i )
Counter += (pObj->fAbs);
return Counter;
}
......@@ -430,9 +441,9 @@ Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
Vec_Int_t * vRes;
Gla_Obj_t * pObj, * pFanin;
Gia_Obj_t * pGiaObj;
int k;
int i, k;
vRes = Vec_IntStart( Gia_ManObjNum(p->pGia) );
Gla_ManForEachObjAbs( p, pObj )
Gla_ManForEachObjAbs( p, pObj, i )
{
Vec_IntWriteEntry( vRes, pObj->iGiaObj, 1 );
pGiaObj = Gla_ManGiaObj( p, pObj );
......@@ -463,9 +474,9 @@ Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p )
{
Vec_Int_t * vPPis;
Gla_Obj_t * pObj, * pFanin;
int k;
int i, k;
vPPis = Vec_IntAlloc( 1000 );
Gla_ManForEachObjAbs( p, pObj )
Gla_ManForEachObjAbs( p, pObj, i )
{
assert( pObj->fConst || pObj->fRo || pObj->fAnd );
Gla_ObjForEachFanin( p, pObj, pFanin, k )
......@@ -484,6 +495,35 @@ int Gla_ManCountPPis( Gla_Man_t * p )
return RetValue;
}
void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
{
static int Round = 0;
Gla_Obj_t * pObj, * pFanin;
int i, j, k, Count;
if ( (Round++ % 3) == 0 )
return;
// printf( "\n" );
j = 0;
Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
{
assert( pObj->fAbs == 0 );
// printf( "%6d ", Gla_ObjId(p, pObj) );
// printf( "Fanins=%d ", pObj->nFanins );
// Gla_ObjForEachFanin( p, pObj, pFanin, k )
// printf( "%d", pFanin->fAbs );
// printf( "\n" );
Count = 0;
Gla_ObjForEachFanin( p, pObj, pFanin, k )
Count += pFanin->fAbs;
if ( Count == 0 )
continue;
Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) );
}
// printf( "\n%d -> %d\n", Vec_IntSize(vPPis), j );
Vec_IntShrink( vPPis, j );
}
/**Function*************************************************************
......@@ -514,10 +554,6 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
{
Gla_Obj_t * pGlaObj = Gla_ManObj( p, iObj );
int iVar, iVar1, iVar2;
if ( iObj == 4753 )
{
int s = 0;
}
if ( pGlaObj->fConst )
{
iVar = Gla_ManGetVar( p, iObj, iFrame );
......@@ -538,9 +574,6 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
else
{
iVar1 = Gla_ManGetVar( p, iObj, iFrame );
// pGlaObj = Gla_ManObj( p, pGlaObj->Fanins[0] );
// assert( pGlaObj->fRo && pGlaObj->nFanins == 1 );
// assert( Vec_IntSize(&pGlaObj->vFrames) == 0 );
iVar2 = Gla_ManGetVar( p, pGlaObj->Fanins[0], iFrame-1 );
sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0 );
// remember the clause
......@@ -576,16 +609,17 @@ void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i )
{
assert( !fCheck || pGla->fAbs == 0 );
if ( pGla->fAbs )
continue;
pGla->fAbs = 1;
// remember the change
Vec_IntPush( p->vAddedNew, Gla_ObjId(p, pGla) );
Vec_IntPush( p->vAddedNew, -1 );
Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
}
}
void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f )
{
Gla_Obj_t * pObj;
Gla_ManForEachObjAbs( p, pObj )
int i;
Gla_ManForEachObjAbs( p, pObj, i )
Gla_ManAddClauses( p, Gla_ObjId(p, pObj), f, p->vTemp );
sat_solver2_simplify( p->pSat );
}
......@@ -602,17 +636,15 @@ void Gla_ManRollBack( Gla_Man_t * p )
int i, iObj, iFrame;
Vec_IntForEachEntryDouble( p->vAddedNew, iObj, iFrame, i )
{
if ( iFrame == -1 )
{
assert( Gla_ManObj(p, iObj)->fAbs == 1 );
Gla_ManObj(p, iObj)->fAbs = 0;
}
else
{
assert( Vec_IntEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame ) > 0 );
Vec_IntWriteEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame, 0 );
}
assert( Vec_IntEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame ) > 0 );
Vec_IntWriteEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame, 0 );
}
Vec_IntForEachEntryStart( p->vAbs, iObj, i, p->nAbsOld )
{
assert( Gla_ManObj( p, iObj )->fAbs == 1 );
Gla_ManObj( p, iObj )->fAbs = 0;
}
Vec_IntShrink( p->vAbs, p->nAbsOld );
}
......@@ -708,6 +740,7 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_so
void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, int Time )
{
Abc_Print( 1, "%3d :", nFrames-1 );
Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Gia_GlaAbsCount(p, 0, 0) / (p->nObjs - Gia_ManPoNum(p->pGia) + Gia_ManCoNum(p->pGia) + 1)) );
Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) );
Abc_Print( 1, "%5d", Gla_ManCountPPis(p) );
Abc_Print( 1, "%5d", Gia_GlaAbsCount(p, 1, 0) );
......@@ -737,6 +770,7 @@ void Gla_ManReportMemory( Gla_Man_t * p )
memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int);
memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
memOth += Vec_IntCap(p->vTemp) * sizeof(int);
memOth += Vec_IntCap(p->vAbs) * sizeof(int);
memTot = memAig + memSat + memPro + memMap + memOth;
ABC_PRMP( "Memory: AIG ", memAig, memTot );
ABC_PRMP( "Memory: SAT ", memSat, memTot );
......@@ -791,6 +825,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
***********************************************************************/
int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
Gla_Man_t * p;
Vec_Int_t * vCore, * vPPis;
Abc_Cex_t * pCex = NULL;
......@@ -799,8 +834,30 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
// compute intial abstraction
if ( pAig->vGateClasses == NULL )
{
int nFramesMaxOld = pPars->nFramesMax;
int nFramesStartOld = pPars->nFramesStart;
int nTimeOutOld = pPars->nTimeOut;
pPars->nFramesMax = pPars->nFramesStart;
pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
pPars->nTimeOut = 10;
RetValue = Gia_VtaPerformInt( pAig, pPars );
pPars->nFramesMax = nFramesMaxOld;
pPars->nFramesStart = nFramesStartOld;
pPars->nTimeOut = nTimeOutOld;
// create gate classes
Vec_IntFreeP( &pAig->vGateClasses );
pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
Vec_IntFreeP( &pAig->vObjClasses );
}
if ( RetValue == 0 )
return RetValue;
// start the manager
clk = clock();
p = Gla_ManStart( pAig, pPars );
p->timeInit = clock() - clk;
p->pSat->fVerbose = p->pPars->fVerbose;
sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
// set runtime limit
......@@ -812,7 +869,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
Abc_Print( 1, "FrameStart = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n",
p->pPars->nFramesStart, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "Frame Abs PPI FF AND Confl Cex Core SatVar Time\n" );
Abc_Print( 1, "Frame %% Abs PPI FF AND Confl Cex Core SatVar Time\n" );
}
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
......@@ -824,6 +881,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// sat_solver2_reducedb( p->pSat );
sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew );
p->nAbsOld = Vec_IntSize( p->vAbs );
// nClaOld = Vec_IntSize( p->vCla2Obj );
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
......@@ -847,6 +905,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
pCex = NULL;
vPPis = Gla_ManCollectPPis( p );
Gla_ManExplorePPis( p, vPPis );
Gia_GlaAddToAbs( p, vPPis, 1 );
Gia_GlaAddOneSlice( p, f, vPPis );
Vec_IntFree( vPPis );
......@@ -947,15 +1006,14 @@ finish:
p->pPars->iFrame = pCex->iFrame - 1;
}
Abc_PrintTime( 1, "Time", clock() - clk );
p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
ABC_PRTP( "Runtime: Initializing", p->timeInit, clock() - clk );
ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk );
ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk );
ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk );
ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk );
ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk );
Gla_ManReportMemory( p );
Gla_ManStop( p );
fflush( stdout );
return RetValue;
......
src/base/abci/abc.c
......@@ -27372,6 +27372,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ParVta_t Pars, * pPars = &Pars;
int c;
Gia_VtaSetDefaultParams( pPars );
pPars->nFramesStart = 20;
pPars->nLearntMax = 100000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )
......
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