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

Gate level abstraction (command &gla).

This commit is contained in:
Alan Mishchenko 2012-06-28 16:44:03 -07:00
parent 27c3ff1f9b
commit 520c436d28
4 changed files with 1074 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -625,6 +625,8 @@ extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int
extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf );
extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver );
/*=== giaAbsGla.c ===========================================================*/
extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars );
/*=== giaAbsVta.c ===========================================================*/
extern void Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
extern Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs );

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

@ -20,6 +20,9 @@
#include "gia.h"
#include "giaAig.h"
#include "src/sat/cnf/cnf.h"
#include "src/sat/bsat/satSolver2.h"
#include "src/base/main/main.h"
ABC_NAMESPACE_IMPL_START
@ -28,6 +31,63 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Gla_Obj_t_ Gla_Obj_t; // object
struct Gla_Obj_t_
{
int iGiaObj; // corresponding GIA obj
unsigned fAbs : 1; // belongs to abstraction
unsigned fCompl0 : 1; // compl bit of the first fanin
// unsigned fCompl1 : 1; // compl bit of the second fanin
unsigned fConst : 1; // object attribute
unsigned fPi : 1; // object attribute
unsigned fPo : 1; // object attribute
unsigned fRo : 1; // object attribute
unsigned fRi : 1; // object attribute
unsigned fAnd : 1; // object attribute
unsigned nFanins : 24; // fanin count
int Fanins[4]; // fanins
Vec_Int_t vFrames; // variables in each timeframe
};
typedef struct Gla_Man_t_ Gla_Man_t; // manager
struct Gla_Man_t_
{
// user data
Gia_Man_t * pGia; // AIG manager
Gia_ParVta_t* pPars; // parameters
// internal data
Gla_Obj_t * pObjs; // objects
int nObjs; // the number of objects
// other data
int nCexes; // the number of counter-examples
int nSatVars; // the number of SAT variables
Cnf_Dat_t * pCnf; // CNF derived for the nodes
sat_solver2 * pSat; // incremental SAT solver
Vec_Int_t * vCla2Obj; // mapping of clauses into GLA objs
Vec_Int_t * vTemp; // temporary array
Vec_Int_t * vAddedNew; // temporary array
// statistics
int timeSat;
int timeUnsat;
int timeCex;
int timeOther;
};
// object procedures
static inline int Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
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 ) \
for ( i = 0; i < Vec_IntSize(vVec) && ((pObj = Gla_ManObj(p, Vec_IntEntry(vVec, i))),1); i++)
// iterator through fanins of an abstracted object
#define Gla_ObjForEachFanin( p, pObj, pFanin, i ) \
for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -170,6 +230,732 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
return -1;
}
/**Function*************************************************************
Synopsis [Adds clauses for the given obj in the given frame.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gla_ManCollectFanins( Gla_Man_t * p, Gla_Obj_t * pGla, int iObj, Vec_Int_t * vFanins )
{
int i, nClauses, iFirstClause, * pLit;
nClauses = p->pCnf->pObj2Count[pGla->iGiaObj];
iFirstClause = p->pCnf->pObj2Clause[pGla->iGiaObj];
Vec_IntClear( vFanins );
for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ )
if ( lit_var(*pLit) != iObj )
Vec_IntPushUnique( vFanins, lit_var(*pLit) );
assert( Vec_IntSize( vFanins ) <= 4 );
Vec_IntSort( vFanins, 0 );
}
/**Function*************************************************************
Synopsis [Creates a new manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
{
Gla_Man_t * p;
Aig_Man_t * pAig;
Gia_Obj_t * pObj;
Gla_Obj_t * pGla;
int i, * pLits;
// start
p = ABC_CALLOC( Gla_Man_t, 1 );
p->pGia = pGia;
p->pPars = pPars;
p->vTemp = Vec_IntAlloc( 100 );
p->vAddedNew = Vec_IntAlloc( 100 );
// internal data
pAig = Gia_ManToAigSimple( p->pGia );
p->pCnf = Cnf_DeriveOther( pAig );
Aig_ManStop( pAig );
// count the number of variables
p->nObjs = 1;
Gia_ManForEachObj( p->pGia, pObj, i )
if ( p->pCnf->pObj2Count[i] >= 0 )
pObj->Value = p->nObjs++;
else
pObj->Value = ~0;
// re-express CNF using new variable IDs
pLits = p->pCnf->pClauses[0];
for ( i = 0; i < p->pCnf->nLiterals; i++ )
{
pObj = Gia_ManObj( p->pGia, lit_var(pLits[i]) );
assert( ~pObj->Value );
pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) );
}
// create objects
p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs );
Gia_ManForEachObj( p->pGia, pObj, i )
{
if ( !~pObj->Value )
continue;
pGla = Gla_ManObj( p, pObj->Value );
pGla->iGiaObj = i;
pGla->fCompl0 = Gia_ObjFaninC0(pObj);
// pGla->fCompl1 = Gia_ObjFaninC1(pObj);
pGla->fConst = Gia_ObjIsConst0(pObj);
pGla->fPi = Gia_ObjIsPi(p->pGia, pObj);
pGla->fPo = Gia_ObjIsPo(p->pGia, pObj);
pGla->fRi = Gia_ObjIsRi(p->pGia, pObj);
pGla->fRo = Gia_ObjIsRo(p->pGia, pObj);
pGla->fAnd = Gia_ObjIsAnd(pObj);
if ( Gia_ObjIsConst0(pObj) || Gia_ObjIsPi(p->pGia, pObj) )
continue;
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->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value;
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);
// other
p->vCla2Obj = Vec_IntAlloc( 1000 ); Vec_IntPush( p->vCla2Obj, -1 );
p->pSat = sat_solver2_new();
p->nSatVars = 1;
return p;
}
/**Function*************************************************************
Synopsis [Creates a new manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gla_ManStop( Gla_Man_t * p )
{
Gla_Obj_t * pGla;
for ( pGla = p->pObjs + 1; pGla < p->pObjs + p->nObjs; 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 );
ABC_FREE( p->pObjs );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Creates a new manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_GlaAbsCount( Gla_Man_t * p, int fRo, int fAnd )
{
Gla_Obj_t * pObj;
int Counter = 0;
if ( fRo )
Gla_ManForEachObjAbs( p, pObj )
Counter += (pObj->fRo && pObj->fAbs);
else if ( fAnd )
Gla_ManForEachObjAbs( p, pObj )
Counter += (pObj->fAnd && pObj->fAbs);
else
Gla_ManForEachObjAbs( p, pObj )
Counter += (pObj->fAbs);
return Counter;
}
/**Function*************************************************************
Synopsis [Derives new abstraction map.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
assert( Gia_ObjIsAnd(pObj) );
Gla_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vMap );
Gla_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vMap );
Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), 1 );
}
Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
{
Vec_Int_t * vRes;
Gla_Obj_t * pObj, * pFanin;
Gia_Obj_t * pGiaObj;
int k;
vRes = Vec_IntStart( Gia_ManObjNum(p->pGia) );
Gla_ManForEachObjAbs( p, pObj )
{
pGiaObj = Gla_ManGiaObj( p, pObj );
Vec_IntWriteEntry( vRes, pObj->iGiaObj, 1 );
if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) )
continue;
assert( Gia_ObjIsAnd(pGiaObj) );
Gia_ManIncrementTravId( p->pGia );
Gla_ObjForEachFanin( p, pObj, pFanin, k )
Gia_ObjSetTravIdCurrent( p->pGia, Gla_ManGiaObj(p, pFanin) );
Gla_ManTranslate_rec( p->pGia, Gla_ManGiaObj(p, pObj), vRes );
}
return vRes;
}
/**Function*************************************************************
Synopsis [Collect pseudo-PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p )
{
Vec_Int_t * vPPis;
Gla_Obj_t * pObj, * pFanin;
int k;
vPPis = Vec_IntAlloc( 1000 );
Gla_ManForEachObjAbs( p, pObj )
{
assert( pObj->fConst || pObj->fRo || pObj->fAnd );
Gla_ObjForEachFanin( p, pObj, pFanin, k )
if ( !pFanin->fPi && !pFanin->fAbs )
Vec_IntPush( vPPis, pObj->Fanins[k] );
}
Vec_IntUniqify( vPPis );
Vec_IntReverseOrder( vPPis );
return vPPis;
}
int Gla_ManCountPPis( Gla_Man_t * p )
{
Vec_Int_t * vPPis = Gla_ManCollectPPis( p );
int RetValue = Vec_IntSize( vPPis );
Vec_IntFree( vPPis );
return RetValue;
}
/**Function*************************************************************
Synopsis [Adds CNF for the given timeframe.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame )
{
Gla_Obj_t * pGla = Gla_ManObj( p, iObj );
int iVar = Vec_IntGetEntry( &pGla->vFrames, iFrame );
assert( !pGla->fPo && !pGla->fRi );
if ( iVar == 0 )
{
Vec_IntSetEntry( &pGla->vFrames, iFrame, (iVar = p->nSatVars++) );
// remember the change
Vec_IntPush( p->vAddedNew, iObj );
Vec_IntPush( p->vAddedNew, iFrame );
}
return iVar;
}
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 );
sat_solver2_add_const( p->pSat, iVar, 1, 0 );
// remember the clause
Vec_IntPush( p->vCla2Obj, iObj );
}
else if ( pGlaObj->fRo )
{
assert( pGlaObj->nFanins == 1 );
if ( iFrame == 0 )
{
iVar = Gla_ManGetVar( p, iObj, iFrame );
sat_solver2_add_const( p->pSat, iVar, 1, 0 );
// remember the clause
Vec_IntPush( p->vCla2Obj, iObj );
}
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
Vec_IntPush( p->vCla2Obj, iObj );
Vec_IntPush( p->vCla2Obj, iObj );
}
}
else if ( pGlaObj->fAnd )
{
int i, RetValue, nClauses, iFirstClause, * pLit;
nClauses = p->pCnf->pObj2Count[pGlaObj->iGiaObj];
iFirstClause = p->pCnf->pObj2Clause[pGlaObj->iGiaObj];
for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
{
Vec_IntClear( vLits );
for ( pLit = p->pCnf->pClauses[i]; pLit < p->pCnf->pClauses[i+1]; pLit++ )
{
iVar = Gla_ManGetVar( p, lit_var(*pLit), iFrame );
Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
}
RetValue = sat_solver2_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
assert( RetValue );
// remember the clause
Vec_IntPush( p->vCla2Obj, iObj );
}
}
else assert( 0 );
}
void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
{
Gla_Obj_t * pGla;
int i;
Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i )
{
assert( !fCheck || pGla->fAbs == 0 );
pGla->fAbs = 1;
// remember the change
Vec_IntPush( p->vAddedNew, Gla_ObjId(p, pGla) );
Vec_IntPush( p->vAddedNew, -1 );
}
}
void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f )
{
Gla_Obj_t * pObj;
Gla_ManForEachObjAbs( p, pObj )
Gla_ManAddClauses( p, Gla_ObjId(p, pObj), f, p->vTemp );
sat_solver2_simplify( p->pSat );
}
void Gia_GlaAddOneSlice( Gla_Man_t * p, int fCur, Vec_Int_t * vCore )
{
int f, i, iGlaObj;
for ( f = fCur; f >= 0; f-- )
Vec_IntForEachEntry( vCore, iGlaObj, i )
Gla_ManAddClauses( p, iGlaObj, f, p->vTemp );
sat_solver2_simplify( p->pSat );
}
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 );
}
}
}
/**Function*************************************************************
Synopsis [Finds the set of clauses involved in the UNSAT core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gla_ManGetOutLit( Gla_Man_t * p, int f )
{
Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
Gla_Obj_t * pGla = Gla_ManObj(p, pFanin->Value);
int iSat = Vec_IntEntry( &pGla->vFrames, f );
assert( iSat > 0 );
return Abc_Var2Lit( iSat, Gia_ObjFaninC0(pObj) );
}
Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_solver2 * pSat, int nConfMax, int fVerbose, int * piRetValue, int * pnConfls )
{
Vec_Int_t * vCore;
int iLit = Gla_ManGetOutLit( p, f );
int nConfPrev = pSat->stats.conflicts;
int i, Entry, RetValue, clk = clock();
if ( piRetValue )
*piRetValue = 1;
// solve the problem
RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( pnConfls )
*pnConfls = (int)pSat->stats.conflicts - nConfPrev;
if ( RetValue == l_Undef )
{
if ( piRetValue )
*piRetValue = -1;
return NULL;
}
if ( RetValue == l_True )
{
if ( piRetValue )
*piRetValue = 0;
return NULL;
}
if ( fVerbose )
{
// Abc_Print( 1, "%6d", (int)pSat->stats.conflicts - nConfPrev );
// Abc_Print( 1, "UNSAT after %7d conflicts. ", pSat->stats.conflicts );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
assert( RetValue == l_False );
// derive the UNSAT core
clk = clock();
vCore = (Vec_Int_t *)Sat_ProofCore( pSat );
if ( fVerbose )
{
// Abc_Print( 1, "Core is %8d clauses (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nclauses(pSat) );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
// remap core into original objects
Vec_IntForEachEntry( vCore, Entry, i )
Vec_IntWriteEntry( vCore, i, Vec_IntEntry(p->vCla2Obj, Entry) );
Vec_IntUniqify( vCore );
Vec_IntReverseOrder( vCore );
if ( fVerbose )
{
// Abc_Print( 1, "Core is %8d vars (out of %8d). ", Vec_IntSize(vCore), sat_solver2_nvars(pSat) );
// Abc_PrintTime( 1, "Time", clock() - clk );
}
return vCore;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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, "%6d", Gia_GlaAbsCount(p, 0, 0) );
Abc_Print( 1, "%5d", Gla_ManCountPPis(p) );
Abc_Print( 1, "%5d", Gia_GlaAbsCount(p, 1, 0) );
Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 1) );
Abc_Print( 1, "%8d", nConfls );
if ( nCexes == 0 )
Abc_Print( 1, "%5c", '-' );
else
Abc_Print( 1, "%5d", nCexes );
Abc_Print( 1, " %6d", nCoreSize > 0 ? nCoreSize : 0 );
Abc_Print( 1, " %9d", sat_solver2_nvars(p->pSat) );
Abc_Print( 1, "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
Abc_Print( 1, "%s", nCoreSize > 0 ? "\n" : "\r" );
fflush( stdout );
}
void Gla_ManReportMemory( Gla_Man_t * p )
{
Gla_Obj_t * pGla;
double memTot = 0;
double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
double memSat = sat_solver2_memory( p->pSat );
double memPro = sat_solver2_memory_proof( p->pSat );
double memMap = p->nObjs * sizeof(Gla_Obj_t);
double memOth = sizeof(Gla_Man_t);
for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ )
memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int);
memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int);
memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
memOth += Vec_IntCap(p->vTemp) * sizeof(int);
memTot = memAig + memSat + memPro + memMap + 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: Other", memOth, memTot );
ABC_PRMP( "Memory: TOTAL", memTot, memTot );
}
/**Function*************************************************************
Synopsis [Send abstracted model or send cancel.]
Description [Counter-example will be sent automatically when &vta terminates.]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
{
char * pFileName = p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig";
Gia_Man_t * pAbs;
if ( fVerbose )
Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
// if ( !Abc_FrameIsBridgeMode() )
// return;
// create gate classes
Vec_IntFreeP( &p->pGia->vGateClasses );
p->pGia->vGateClasses = Gla_ManTranslate( p );
// create abstrated model
pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
Vec_IntFreeP( &p->pGia->vGateClasses );
// send it out
Gia_WriteAiger( pAbs, pFileName, 0, 0 );
Gia_ManStop( pAbs );
}
/**Function*************************************************************
Synopsis [Performs gate-level abstraction]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
Gla_Man_t * p;
Vec_Int_t * vCore, * vPPis;
Abc_Cex_t * pCex = NULL;
int i, f, nConfls, Status, nCoreSize, RetValue = -1;
int clk = clock(), clk2;
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
// start the manager
p = Gla_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 );
// perform initial abstraction
if ( p->pPars->fVerbose )
{
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" );
}
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 );
// nClaOld = Vec_IntSize( p->vCla2Obj );
// iterate as long as there are counter-examples
for ( i = 0; ; i++ )
{
clk2 = clock();
vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
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 );
pCex = NULL;
vPPis = Gla_ManCollectPPis( p );
Gia_GlaAddToAbs( p, vPPis, 1 );
Gia_GlaAddOneSlice( p, f, vPPis );
Vec_IntFree( vPPis );
p->timeCex += clock() - clk2;
if ( pCex != NULL )
{
RetValue = 0;
goto finish;
}
// print the result (do not count it towards change)
if ( p->pPars->fVerbose )
Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
}
assert( Status == 1 );
// valid core is obtained
nCoreSize = Vec_IntSize(vCore);
if ( i == 0 )
Vec_IntFree( vCore );
else
{
// update the SAT solver
sat_solver2_rollback( p->pSat );
// update storage
Gla_ManRollBack( p );
Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 );
// load this timeframe
Gia_GlaAddToAbs( p, vCore, 0 );
Gia_GlaAddOneSlice( p, f, vCore );
Vec_IntFree( vCore );
// run SAT solver
clk2 = clock();
vCore = Gla_ManUnsatCore( p, f, p->vCla2Obj, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status, &nConfls );
p->timeUnsat += clock() - clk2;
assert( (vCore != NULL) == (Status == 1) );
Vec_IntFree( vCore );
if ( Status == -1 ) // resource limit is reached
break;
if ( Status == 0 )
{
// Vta_ManSatVerify( p );
// make sure, there was no initial abstraction (otherwise, it was invalid)
assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
// pCex = Vga_ManDeriveCex( p );
RetValue = 0;
break;
}
}
// print the result
if ( p->pPars->fVerbose )
Gla_ManAbsPrintFrame( p, nCoreSize, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
// dump the model
if ( p->pPars->fDumpVabs && (f & 1) )
{
Abc_FrameSetCex( NULL );
Abc_FrameSetNFrames( f+1 );
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "write_status gla.status" );
Gia_GlaDumpAbsracted( p, pPars->fVerbose );
}
// check if the number of objects is below limit
if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
{
Status = -1;
break;
}
}
finish:
// analize the results
if ( pCex == NULL )
{
if ( pAig->vGateClasses != NULL )
Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
Vec_IntFreeP( &pAig->vGateClasses );
pAig->vGateClasses = Gla_ManTranslate( p );
if ( Status == -1 )
{
if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit )
Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 )
Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f );
else
Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f );
}
else
Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f );
}
else
{
ABC_FREE( p->pGia->pCexSeq );
p->pGia->pCexSeq = pCex;
if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" );
Abc_Print( 1, "Counter-example detected in frame %d. ", f );
p->pPars->iFrame = pCex->iFrame - 1;
}
Abc_PrintTime( 1, "Time", clock() - clk );
p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
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;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

99
src/aig/saig/saigBmc3.c
View File

@ -57,6 +57,7 @@ struct Gia_ManBmc_t_
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define SAIG_TER_NON 0
#define SAIG_TER_ZER 1
#define SAIG_TER_ONE 2
#define SAIG_TER_UND 3
@ -91,6 +92,13 @@ static inline void Saig_ManBmcSimInfoSet( unsigned * pInfo, Aig_Obj_t * pObj, in
pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
}
static inline int Saig_ManBmcSimInfoClear( unsigned * pInfo, Aig_Obj_t * pObj )
{
int Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
return Value;
}
/**Function*************************************************************
Synopsis [Returns the number of LIs with binary ternary info.]
@ -218,6 +226,97 @@ void Saig_ManBmcTerSimTest( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Count the number of non-ternary per frame.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManBmcCountNonternary_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vInfos, unsigned * pInfo, int f, int * pCounter )
{
int Value = Saig_ManBmcSimInfoClear( pInfo, pObj );
if ( Value == SAIG_TER_NON )
return 0;
assert( f >= 0 );
pCounter[f] += (Value == SAIG_TER_UND);
if ( Saig_ObjIsPi(p, pObj) || (f == 0 && Saig_ObjIsLo(p, pObj)) || Aig_ObjIsConst1(pObj) )
return 0;
if ( Saig_ObjIsLi(p, pObj) )
return Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
if ( Saig_ObjIsLo(p, pObj) )
return Saig_ManBmcCountNonternary_rec( p, Saig_ObjLoToLi(p, pObj), vInfos, (unsigned *)Vec_PtrEntry(vInfos, f-1), f-1, pCounter );
assert( Aig_ObjIsNode(pObj) );
Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin1(pObj), vInfos, pInfo, f, pCounter );
return 0;
}
void Saig_ManBmcCountNonternary( Aig_Man_t * p, Vec_Ptr_t * vInfos, int iFrame )
{
int i, * pCounters = ABC_CALLOC( int, iFrame + 1 );
unsigned * pInfo = (unsigned *)Vec_PtrEntry(vInfos, iFrame);
assert( Saig_ManBmcSimInfoGet( pInfo, Aig_ManCo(p, 0) ) == SAIG_TER_UND );
Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(Aig_ManCo(p, 0)), vInfos, pInfo, iFrame, pCounters );
for ( i = 0; i <= iFrame; i++ )
printf( "%d=%d ", i, pCounters[i] );
printf( "\n" );
ABC_FREE( pCounters );
}
/**Function*************************************************************
Synopsis [Returns the number of POs with binary ternary info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManBmcTerSimCount01Po( Aig_Man_t * p, unsigned * pInfo )
{
Aig_Obj_t * pObj;
int i, Counter = 0;
Saig_ManForEachPo( p, pObj, i )
Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
return Counter;
}
Vec_Ptr_t * Saig_ManBmcTerSimPo( Aig_Man_t * p )
{
Vec_Ptr_t * vInfos;
unsigned * pInfo = NULL;
int i, nPoBin;
vInfos = Vec_PtrAlloc( 100 );
for ( i = 0; ; i++ )
{
if ( i % 100 == 0 )
printf( "Frame %5d\n", i );
pInfo = Saig_ManBmcTerSimOne( p, pInfo );
Vec_PtrPush( vInfos, pInfo );
nPoBin = Saig_ManBmcTerSimCount01Po( p, pInfo );
if ( nPoBin < Saig_ManPoNum(p) )
break;
}
printf( "Detected terminary PO in frame %d.\n", i );
Saig_ManBmcCountNonternary( p, vInfos, i );
return vInfos;
}
void Saig_ManBmcTerSimTestPo( Aig_Man_t * p )
{
Vec_Ptr_t * vInfos;
vInfos = Saig_ManBmcTerSimPo( p );
Vec_PtrFreeFree( vInfos );
}
/**Function*************************************************************
Synopsis [Collects internal nodes in the DFS order.]

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

@ -349,6 +349,7 @@ static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9GlaRefine ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
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_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -793,6 +794,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&gla_refine", Abc_CommandAbc9GlaRefine, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 );
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", "&reparam", Abc_CommandAbc9Reparam, 0 );
@ -9211,20 +9213,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig );
extern Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap );
extern void Abc2_NtkTestGia( char * pFileName, int fVerbose );
extern void Saig_ManBmcTerSimTestPo( Aig_Man_t * p );
if ( pNtk )
{
/*
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
if ( fNewAlgo )
Saig_IsoDetectFast( pAig );
else
{
Aig_Man_t * pRes = Iso_ManTest( pAig, fVerbose );
Aig_ManStopP( &pRes );
}
Saig_ManBmcTerSimTestPo( pAig );
Aig_ManStop( pAig );
*/
/*
extern Abc_Ntk_t * Abc_NtkShareXor( Abc_Ntk_t * pNtk );
Abc_Ntk_t * pNtkRes = Abc_NtkShareXor( pNtk );
@ -27359,6 +27356,186 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParVta_t Pars, * pPars = &Pars;
int c;
Gia_VtaSetDefaultParams( pPars );
pPars->nLearntMax = 100000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesMax < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
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 )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nConfLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfLimit < 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;
}
pPars->nLearntMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nLearntMax < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTimeOut < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
pPars->nRatioMin = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nRatioMin < 0 )
goto usage;
break;
case 'A':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-A\" should be followed by a file name.\n" );
goto usage;
}
pPars->pFileVabs = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 't':
pPars->fUseTermVars ^= 1;
break;
case 'r':
pPars->fUseRollback ^= 1;
break;
case 'd':
pPars->fDumpVabs ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "There is no AIG.\n" );
return 0;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
if ( Gia_ManPoNum(pAbc->pGia) > 1 )
{
Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
return 0;
}
if ( pPars->nFramesMax < 0 )
{
Abc_Print( 1, "The number of starting frames should be a positive integer.\n" );
return 0;
}
if ( pPars->nFramesMax && pPars->nFramesStart > pPars->nFramesMax )
{
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 );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-dvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with proof-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-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");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -27486,7 +27663,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
Abc_Print( -1, "There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )