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

Other improvements to &vta and &gla.

This commit is contained in:
Alan Mishchenko 2012-07-05 13:09:41 -07:00
parent ce6e6551c3
commit 3c43fbba1a
5 changed files with 257 additions and 188 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/gia/gia.h
View File

@ -213,6 +213,7 @@ struct Gia_ParVta_t_
int fUseTermVars; // use terminal variables
int fUseRollback; // use rollback to the starting number of frames
int fPropFanout; // propagate fanout implications
int fAddLayer; // refinement strategy by adding layers
int fDumpVabs; // dumps the abstracted model
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
@ -704,7 +705,8 @@ extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars,
extern void Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
extern Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs );
extern Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames );
extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs );
extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
extern int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );

44
src/aig/gia/giaAbsGla.c
View File

@ -445,7 +445,7 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
***********************************************************************/
void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
{
int i, Id = Gia_ObjId(p->pGia, pObj);
int i;//, Id = Gia_ObjId(p->pGia, pObj);
Rfn_Obj_t * pRef0, * pRef1, * pRef = Gla_ObjRef( p, pObj, f );
Gia_Obj_t * pFanout;
int k;
@ -506,7 +506,7 @@ void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec
***********************************************************************/
void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
{
int i, Id = Gia_ObjId(p->pGia, pObj);
int i;//, Id = Gia_ObjId(p->pGia, pObj);
Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f );
assert( (int)pRef->Sign == Sign );
if ( pRef->fVisit )
@ -1100,6 +1100,8 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
// other
p->vCla2Obj = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Obj, -1 );
p->pSat = sat_solver2_new();
// p->pSat->fVerbose = p->pPars->fVerbose;
sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
p->nSatVars = 1;
return p;
}
@ -1214,7 +1216,7 @@ void Gla_ManStop( Gla_Man_t * p )
Gla_Obj_t * pGla;
int i;
// if ( p->pPars->fVerbose )
Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Confs = %d. Cexes = %d. ObjAdded = %d\n",
Abc_Print( 1, "SAT solver: Vars = %d Clauses = %d Confs = %d Cexes = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
ABC_FREE( p->pvRefis[i].pArray );
@ -1754,8 +1756,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
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
if ( p->pPars->nTimeOut )
sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
@ -1763,21 +1763,23 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "Running gate-level abstraction (GLA) 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 SatVar Core Time\n" );
Abc_Print( 1, "FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%.\n",
pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex SatVar Core Time\n" );
}
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
int nConflsBeg = sat_solver2_nconflicts(p->pSat);
p->pPars->iFrame = f;
// load timeframe
Gia_GlaAddTimeFrame( p, f );
// create bookmark to be used for rollback
// sat_solver2_reducedb( p->pSat );
sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew );
p->nAbsOld = Vec_IntSize( p->vAbs );
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
{
@ -1805,17 +1807,20 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
p->nCexes++;
// perform the refinement
clk2 = clock();
vPPis = Gla_ManRefinement( p );
if ( vPPis == NULL )
if ( pPars->fAddLayer )
{
pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
break;
vPPis = Gla_ManCollectPPis( p, NULL );
// Gla_ManExplorePPis( p, vPPis );
}
else
{
vPPis = Gla_ManRefinement( p );
if ( vPPis == NULL )
{
pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
break;
}
}
// vPPis = Gla_ManCollectPPis( p, NULL );
// Gla_ManExplorePPis( p, vPPis );
Gia_GlaAddToAbs( p, vPPis, 1 );
Gia_GlaAddOneSlice( p, f, vPPis );
Vec_IntFree( vPPis );
@ -1905,7 +1910,10 @@ finish:
Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
}
else
{
p->pPars->iFrame++;
Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
}
}
else
{

270
src/aig/gia/giaAbsVta.c
View File

@ -61,6 +61,7 @@ struct Vta_Man_t_
Vec_Ptr_t * vFrames; // start abstraction for each frame
int nWords; // the number of words in the record
int nCexes; // the number of CEXes
int nObjAdded; // objects added to the abstraction
Vec_Int_t * vSeens; // seen objects
Vec_Bit_t * vSeenGla; // seen objects in all frames
int nSeenGla; // seen objects in all frames
@ -149,10 +150,10 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
{
memset( p, 0, sizeof(Gia_ParVta_t) );
p->nFramesMax = 0; // maximum frames
p->nFramesStart = 5; // starting frame
p->nFramesStart = 0; // starting frame
p->nFramesPast = 4; // overlap frames
p->nConfLimit = 0; // conflict limit
p->nLearntMax = 15000; // max number of learned clauses
p->nLearntMax = 1000; // max number of learned clauses
p->nTimeOut = 0; // timeout in seconds
p->nRatioMin = 10; // stop when less than this % of object is abstracted
p->fUseTermVars = 1; // use terminal variables
@ -236,31 +237,31 @@ Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames )
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
{
Gia_Obj_t * pObj;
Vec_Int_t * vPresent;
Vec_Int_t * vGla;
int nObjMask, nObjs = Gia_ManObjNum(p);
int i, Entry, nFrames = Vec_IntEntry( vAbs, 0 );
assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
int i, Entry, nFrames = Vec_IntEntry( vVta, 0 );
assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
// get the bitmask
nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
assert( nObjs <= nObjMask );
// go through objects
vPresent = Vec_IntStart( nObjs );
Vec_IntWriteEntry( vPresent, 0, 1 );
Vec_IntForEachEntryStart( vAbs, Entry, i, nFrames+2 )
vGla = Vec_IntStart( nObjs );
Vec_IntWriteEntry( vGla, 0, 1 );
Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 )
{
pObj = Gia_ManObj( p, (Entry & nObjMask) );
assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
Vec_IntWriteEntry( vPresent, (Entry & nObjMask), 1 );
Vec_IntWriteEntry( vGla, (Entry & nObjMask), 1 );
}
return vPresent;
return vGla;
}
/**Function*************************************************************
Synopsis [Detects how many frames are completed.]
Synopsis [Converting GLA vector to VTA vector.]
Description []
@ -269,26 +270,31 @@ Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
SeeAlso []
***********************************************************************/
static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords )
Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
{
unsigned * pTotal, * pThis;
int i, w, nObjs = Vec_IntSize(p) / nWords;
assert( Vec_IntSize(p) % nWords == 0 );
pTotal = ABC_CALLOC( unsigned, nWords );
for ( i = 0; i < nObjs; i++ )
{
pThis = (unsigned *)Vec_IntEntryP( p, nWords * i );
for ( w = 0; w < nWords; w++ )
pTotal[w] |= pThis[i];
}
for ( i = nWords * 32 - 1; i >= 0; i-- )
if ( Abc_InfoHasBit(pTotal, i) )
{
ABC_FREE( pTotal );
return i+1;
}
ABC_FREE( pTotal );
return -1;
Vec_Int_t * vVta;
int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p);
int i, k, j, Entry, Counter, nGlaSize;
//. get the GLA size
nGlaSize = Vec_IntSum(vGla);
// get the bitmask
nObjBits = Abc_Base2Log(nObjs);
nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
assert( nObjs <= nObjMask );
// go through objects
vVta = Vec_IntAlloc( 1000 );
Vec_IntPush( vVta, nFrames );
Counter = nFrames + 2;
for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize )
Vec_IntPush( vVta, Counter );
for ( i = 0; i < nFrames; i++ )
for ( k = 0; k <= i; k++ )
Vec_IntForEachEntry( vGla, Entry, j )
if ( Entry )
Vec_IntPush( vVta, (k << nObjBits) | j );
Counter = Vec_IntEntry(vVta, nFrames+1);
assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) );
return vVta;
}
/**Function*************************************************************
@ -949,25 +955,28 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
assert( 0 );
}
// mark those currently included
Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
if ( p->pPars->fAddLayer )
{
assert( pThis->fVisit == 0 );
pThis->fVisit = 1;
// mark those currently included
Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
{
assert( pThis->fVisit == 0 );
pThis->fVisit = 1;
}
// add used terms, which have close relationship
Counter = Vec_IntSize(vTermsToAdd);
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
{
if ( pThis->fVisit )
continue;
// Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
// if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
}
// remove those currenty included
Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
pThis->fVisit = 0;
}
// add used terms, which have close relationship
Counter = Vec_IntSize(vTermsToAdd);
Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
{
if ( pThis->fVisit )
continue;
// Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
// if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
}
// remove those currenty included
Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
pThis->fVisit = 0;
// printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) );
//Vec_IntReverseOrder( vTermsToAdd );
//Vec_IntSort( vTermsToAdd, 1 );
@ -1054,6 +1063,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
sat_solver2_simplify( p->pSat );
}
p->nObjAdded += Vec_IntSize(vTermsToAdd);
Vec_IntFree( vTermsToAdd );
return pCex;
}
@ -1091,28 +1101,15 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vSeenGla = Vec_BitStart( Gia_ManObjNum(pGia) );
p->nSeenGla = 1;
p->nSeenAll = 1;
// start the abstraction
if ( pGia->vObjClasses == NULL )
p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart );
else
{
p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
// update parameters
if ( pPars->nFramesStart != Vec_PtrSize(p->vFrames) )
{
Abc_Print( 1, "Starting frame count is changed to match the abstraction (from %d to %d).\n", pPars->nFramesStart, Vec_PtrSize(p->vFrames) );
pPars->nFramesStart = Vec_PtrSize(p->vFrames);
}
if ( pPars->nFramesMax && pPars->nFramesMax < pPars->nFramesStart )
{
Abc_Print( 1, "Maximum frame count is changed to match the starting frames (from %d to %d).\n", pPars->nFramesMax, pPars->nFramesStart );
pPars->nFramesMax = Abc_MaxInt( pPars->nFramesMax, pPars->nFramesStart );
}
}
// other data
p->vCla2Var = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Var, -1 );
p->vCores = Vec_PtrAlloc( 100 );
p->pSat = sat_solver2_new();
// p->pSat->fVerbose = p->pPars->fVerbose;
sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
// start the abstraction
assert( pGia->vObjClasses != NULL );
p->vFrames = Gia_VtaAbsToFrames( pGia->vObjClasses );
p->vAddedNew = Vec_IntAlloc( 1000 );
return p;
}
@ -1131,9 +1128,8 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
void Vga_ManStop( Vta_Man_t * p )
{
// if ( p->pPars->fVerbose )
Abc_Print( 1, "SAT solver: Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes );
Abc_Print( 1, "SAT solver: Vars = %d Clauses = %d Confs = %d Cexes = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
Vec_BitFreeP( &p->vSeenGla );
@ -1624,8 +1620,6 @@ int Gia_VtaPerformInt( 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->vObjClasses == NULL )
{
@ -1635,11 +1629,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Vec_IntPush( pAig->vObjClasses, 4 );
Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
}
*/
// start the manager
p = Vga_ManStart( pAig, pPars );
p->pSat->fVerbose = p->pPars->fVerbose;
sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
// set runtime limit
if ( p->pPars->nTimeOut )
sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
@ -1647,11 +1638,11 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
Abc_Print( 1, "FrameStart = %d FramePast = %d FrameMax = %d Conf = %d Timeout = %d. RatioMin = %d %%.\n",
p->pPars->nFramesStart, p->pPars->nFramesPast, p->pPars->nFramesMax,
p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "FramePast = %d FrameMax = %d ConfMax = %d LearnMax = %d Timeout = %d RatioMin = %d %%\n",
pPars->nFramesPast, pPars->nFramesMax, pPars->nConfLimit, pPars->nLearntMax, pPars->nTimeOut, pPars->nRatioMin );
Abc_Print( 1, "Frame %% Abs %% Confl Cex SatVar Core F0 F1 F2 ...\n" );
}
assert( Vec_PtrSize(p->vFrames) > 0 );
for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
int nConflsBeg = sat_solver2_nconflicts(p->pSat);
@ -1659,72 +1650,72 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// realloc storage for abstraction marks
if ( f == p->nWords * 32 )
p->nWords = Vec_IntDoubleWidth( p->vSeens, p->nWords );
// check this timeframe
if ( f < p->pPars->nFramesStart )
{
Vga_ManAddClausesOne( p, 0, f );
// create bookmark to be used for rollback
nObjOld = p->nObjs;
sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew );
// load new timeframe
Vga_ManAddClausesOne( p, 0, f );
if ( f < Vec_PtrSize(p->vFrames) )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
}
else
{
// create bookmark to be used for rollback
nObjOld = p->nObjs;
// sat_solver2_reducedb( p->pSat );
sat_solver2_bookmark( p->pSat );
Vec_IntClear( p->vAddedNew );
// load the time frame
for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, p->pPars->nFramesStart); i++ )
for ( i = 1; i <= Abc_MinInt(p->pPars->nFramesPast, f); i++ )
Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
{
clk2 = clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
{
Vga_ManRollBack( p, nObjOld );
goto finish;
}
// check timeout
if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
{
Vga_ManRollBack( p, nObjOld );
goto finish;
}
if ( vCore != NULL )
{
p->timeUnsat += clock() - clk2;
break;
}
p->timeSat += clock() - clk2;
assert( Status == 0 );
p->nCexes++;
// perform the refinement
clk2 = clock();
pCex = Vta_ManRefineAbstraction( p, f );
p->timeCex += clock() - clk2;
if ( pCex != NULL )
{
RetValue = 0;
goto finish;
}
// print the result (do not count it towards change)
Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose );
}
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
{
clk2 = clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
{
Vga_ManRollBack( p, nObjOld );
goto finish;
}
assert( Status == 1 );
// valid core is obtained
Vta_ManUnsatCoreRemap( p, vCore );
Vec_IntSort( vCore, 1 );
// update the SAT solver
sat_solver2_rollback( p->pSat );
// update storage
Vga_ManRollBack( p, nObjOld );
Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
// load this timeframe
Vga_ManLoadSlice( p, vCore, 0 );
Vec_IntFree( vCore );
}
// check timeout
if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
{
Vga_ManRollBack( p, nObjOld );
goto finish;
}
if ( vCore != NULL )
{
p->timeUnsat += clock() - clk2;
break;
}
p->timeSat += clock() - clk2;
assert( Status == 0 );
p->nCexes++;
// perform the refinement
clk2 = clock();
pCex = Vta_ManRefineAbstraction( p, f );
p->timeCex += clock() - clk2;
if ( pCex != NULL )
{
RetValue = 0;
goto finish;
}
// print the result (do not count it towards change)
Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose );
}
assert( Status == 1 );
// valid core is obtained
Vta_ManUnsatCoreRemap( p, vCore );
Vec_IntSort( vCore, 1 );
// update the SAT solver
sat_solver2_rollback( p->pSat );
// update storage
Vga_ManRollBack( p, nObjOld );
Vec_IntShrink( p->vCla2Var, (int)p->pSat->stats.clauses+1 );
// load this timeframe
Vga_ManLoadSlice( p, vCore, 0 );
Vec_IntFree( vCore );
// run SAT solver
clk2 = clock();
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
@ -1808,7 +1799,10 @@ finish:
Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
}
else
{
p->pPars->iFrame++;
Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
}
}
}
else

7
src/aig/gia/giaMan.c
View File

@ -202,6 +202,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
void Gia_ManPrintGateClasses( Gia_Man_t * p )
{
Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
int nTotal;
if ( p->vGateClasses == NULL )
return;
if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
@ -211,10 +212,12 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p )
}
// create additional arrays
Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%)\n",
nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes);
printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%) Obj = %d (%.2f %%)\n",
Vec_IntSize(vPis), Vec_IntSize(vPPis),
Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1),
Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1) );
Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1),
nTotal, 100.0*nTotal /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );

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

@ -352,6 +352,7 @@ static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Gla ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Vta ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Vta2Gla ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Gla2Vta ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BackReach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -797,6 +798,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&gla", Abc_CommandAbc9Gla, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&vta", Abc_CommandAbc9Vta, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&vta_gla", Abc_CommandAbc9Vta2Gla, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_vta", Abc_CommandAbc9Gla2Vta, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&back_reach", Abc_CommandAbc9BackReach, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 );
@ -27384,10 +27386,8 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ParVta_t Pars, * pPars = &Pars;
int c, fStartVta = 0;
Gia_VtaSetDefaultParams( pPars );
pPars->nFramesStart = 30;
pPars->nLearntMax = 100000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfdavh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfkadvh" ) ) != EOF )
{
switch ( c )
{
@ -27486,11 +27486,14 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
pPars->fPropFanout ^= 1;
break;
case 'd':
pPars->fDumpVabs ^= 1;
case 'k':
fStartVta ^= 1;
break;
case 'a':
fStartVta ^= 1;
pPars->fAddLayer ^= 1;
break;
case 'd':
pPars->fDumpVabs ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
@ -27526,32 +27529,25 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;
}
if ( pPars->nFramesStart < 1 )
{
Abc_Print( 1, "The starting frame should be 1 or larger.\n" );
return 0;
}
pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fdavh]\n" );
Abc_Print( -2, "\t performs gate-level abstraction of a sequential miter\n" );
Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fkadvh]\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 );
// Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-L num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearntMax );
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-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
// Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
// Abc_Print( -2, "\t-r : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
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" );
Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
Abc_Print( -2, "\t-a : toggle using VTA to kick start GLA [default = %s]\n", fStartVta? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@ -27574,7 +27570,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtradvh" ) ) != EOF )
{
switch ( c )
{
@ -27670,6 +27666,9 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
pPars->fUseRollback ^= 1;
break;
case 'a':
pPars->fAddLayer ^= 1;
break;
case 'd':
pPars->fDumpVabs ^= 1;
break;
@ -27707,21 +27706,14 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
return 0;
}
if ( pPars->nFramesStart < 1 )
{
Abc_Print( 1, "The starting frame should be 1 or larger.\n" );
return 0;
}
// if ( argc == globalUtilOptind + 1 )
// pPars->pFileVabs = argv[globalUtilOptind];
pAbc->Status = Gia_VtaPerform( pAbc->pGia, pPars );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-A file] [-trdvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
Abc_Print( -2, "usage: &vta [-FSPCLTR num] [-A file] [-tradvh]\n" );
Abc_Print( -2, "\t variable-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 );
Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
@ -27732,6 +27724,7 @@ usage:
Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"vabs.aig\"]\n" );
Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
Abc_Print( -2, "\t-a : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -27773,7 +27766,7 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia->vObjClasses == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction defines.\n" );
Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction is defined.\n" );
return 1;
}
Vec_IntFreeP( &pAbc->pGia->vGateClasses );
@ -27783,12 +27776,81 @@ int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: &vta_gla [-vh]\n" );
Abc_Print( -2, "\t maps variable- into fixed-time-frame abstraction\n" );
Abc_Print( -2, "\t maps variable- into fixed-time-frame gate-level abstraction\n" );
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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Gla2Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c, fVerbose = 0;
int nFrames = pAbc->nFrames;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no AIG.\n" );
return 1;
}
if ( pAbc->pGia->vGateClasses == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): There is no gate-level abstraction is defined.\n" );
return 1;
}
if ( pAbc->nFrames < 1 )
{
Abc_Print( -1, "Abc_CommandAbc9Gla2Vta(): The number of timeframes (%d) should be a positive integer.\n", nFrames );
return 1;
}
Vec_IntFreeP( &pAbc->pGia->vObjClasses );
pAbc->pGia->vObjClasses = Gia_VtaConvertFromGla( pAbc->pGia, pAbc->pGia->vGateClasses, nFrames );
Vec_IntFreeP( &pAbc->pGia->vGateClasses );
return 0;
usage:
Abc_Print( -2, "usage: &gla_vta [-F num] [-vh]\n" );
Abc_Print( -2, "\t maps fixed- into variable-time-frame gate-level abstraction\n" );
Abc_Print( -2, "\t-F num : timeframes in the resulting variable-time-frame abstraction [default = %d]\n", nFrames );
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;
}
/**Function*************************************************************
Synopsis []