Skip to content

A
abc
Commit 46772882 by Alan Mishchenko
Options

Scalable gate-level abstraction.

parent 7e486af8
Showing with 319 additions and 211 deletions
src/aig/gia/giaAbsGla2.c
......@@ -26,12 +26,14 @@
ABC_NAMESPACE_IMPL_START
#if 0
//#if 0
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define GA2_BIG_NUM 0x3FFFFFFF
typedef struct Ga2_Man_t_ Ga2_Man_t; // manager
struct Ga2_Man_t_
{
......@@ -39,17 +41,18 @@ struct Ga2_Man_t_
Gia_Man_t * pGia; // working AIG manager
Gia_ParVta_t * pPars; // parameters
// markings
Vec_Int_t * vMapping; // for each object: leaf count, leaves, truth table
int nMarked; // total number of marked nodes and flops
// data storage
Vec_Int_t * vId2Data; // mapping of object ID into its data for each object
Vec_Ptr_t * vDatas; // for each object: leaves, CNF0, CNF1
// abstraction
Vec_Int_t * vAbs; // array of abstracted objects
int nAbsStart; // marker of the abstracted objects
Vec_Int_t * vValues; // array of objects with SAT numbers assigned
int LimAbs; // limit value for starting abstraction objects
int LimPpi; // limit value for starting PPI objects
// refinement
Rnm_Man_t * pRnm; // refinement manager
// SAT solver and variables
Vec_Ptr_t * vId2Lit; // mapping of object ID into SAT literal for each timeframe
Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal
sat_solver2 * pSat; // incremental SAT solver
int nSatVars; // the number of SAT variables
// temporaries
......@@ -68,34 +71,40 @@ struct Ga2_Man_t_
clock_t timeOther;
};
static inline int Ga2_ObjOffset( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(pObj->Value); return Vec_IntEntry(p->vMapping, Gia_ObjId(p->pGia, pObj)); }
static inline int Ga2_ObjLeaveNum( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); }
static inline int * Ga2_ObjLeavePtr( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); }
static inline unsigned Ga2_ObjTruth( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); }
static inline int Ga2_ObjRefNum( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); }
static inline Vec_Int_t * Ga2_ObjLeaves( Ga2_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t vVec; vVec.nSize = Ga2_ObjLeaveNum(p, pObj), vVec.pArray = Ga2_ObjLeavePtr(p, pObj); return &vVec; }
static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(pObj->Value); return Vec_PtrEntry(p->vDatas, (pObj->Value << 1) ); }
static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(pObj->Value); return Vec_PtrEntry(p->vDatas, (pObj->Value << 1)+1); }
static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert( pObj->Value ); return (int)pObj->Value < p->LimAbs; }
static inline int Ga2_ObjIsPPI( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert( pObj->Value ); return (int)pObj->Value >= p->LimAbs && (int)pObj->Value < p->LimPpi; }
static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f ) { return (Vec_Int_t *)Vec_PtrEntry( p->vId2Lit, f ); }
// returns literal of this object, or -1 if SAT variable of the object is not assigned
static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{
Vec_Int_t * vMap;
assert( pObj->fPhase );
if ( pObj->Value == 0 )
return -1;
vMap = (Vec_Int_t *)Vec_PtrEntry(p->vMaps, f);
if ( pObj->Value >= Vec_IntSize(vMap) )
return -1;
return Vec_IntEntry( vMap, pObj->Value );
assert( pObj->Value && pObj->Value < Vec_IntSize(p->vValues) );
if ( f == Vec_PtrSize(p->vId2Lit) )
Vec_PtrPush( p->vId2Lit, Vec_IntStartFull(Vec_IntSize(p->vValues)) );
assert( f < Vec_PtrSize(p->vId2Lit) );
return Vec_IntEntry( Ga2_MapFrameMap(p, f), pObj->Value );
}
// inserts literal of this object
static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit )
{
Vec_Int_t * vMap;
assert( Lit > 1 );
assert( pObj->fPhase );
assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
if ( pObj->Value == 0 )
{
pObj->Value = Vec_IntSize(p->vAbs);
Vec_IntEntry( p->vAbs, Gia_ObjId(p, pObj) );
}
vMap = (Vec_Int_t *)Vec_PtrEntry(p->vMaps, f);
Vec_IntSetEntry( vMap, pObj->Value, Lit );
Vec_IntSetEntry( Ga2_MapFrameMap(p, f), pObj->Value, Lit );
}
// returns
// returns or inserts-and-returns literal of this object
static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{
int Lit = Ga2_ObjFindLit( p, pObj, f );
......@@ -108,12 +117,54 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
return Lit;
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes truth table for the marked node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Ga2_ObjComputeTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst )
{
unsigned Val0, Val1;
if ( pObj->fPhase && !fFirst )
return pObj->Value;
assert( Gia_ObjIsAnd(pObj) );
Val0 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin0(pObj), 0 );
Val1 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin1(pObj), 0 );
return (Gia_ObjFaninC0(pObj) ? ~Val0 : Val0) & (Gia_ObjFaninC1(pObj) ? ~Val1 : Val1);
}
unsigned Ga2_ManComputeTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
{
static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
unsigned Res, Values[5];
Gia_Obj_t * pObj;
int i;
// assign elementary truth tables
Gia_ManForEachObjVec( vLeaves, p, pObj, i )
{
assert( pObj->fPhase );
Values[i] = pObj->Value;
pObj->Value = uTruth5[i];
}
Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
// return values
Gia_ManForEachObjVec( vLeaves, p, pObj, i )
pObj->Value = Values[i];
return Res;
}
/**Function*************************************************************
Synopsis [Returns AIG marked for CNF generation.]
Description [The marking satisfies the following requirements:
......@@ -191,12 +242,14 @@ void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLea
Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin0(pObj), vLeaves, 0 );
Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin1(pObj), vLeaves, 0 );
}
int Ga2_ManMarkup( Gia_Man_t * p, int N )
int Ga2_ManMarkup( Gia_Man_t * p, int N, Vec_Int_t ** pvMap )
{
static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
clock_t clk = clock();
Vec_Int_t * vMap;
Vec_Int_t * vLeaves;
Gia_Obj_t * pObj;
int i, CountMarks;
int i, k, Leaf, CountMarks;
// label nodes with multiple fanouts and inputs MUXes
Gia_ManForEachObj( p, pObj, i )
{
......@@ -221,7 +274,6 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N )
Gia_ObjFanin0(pObj)->fPhase = 1;
else
pObj->fPhase = 1;
pObj->Value = 0;
}
// add marks when needed
vLeaves = Vec_IntAlloc( 100 );
......@@ -236,21 +288,54 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N )
}
// verify that the tree is split correctly
CountMarks = 0;
vMap = Vec_IntStart( Gia_ManObjNum(p) );
Gia_ManForEachAnd( p, pObj, i )
{
if ( !pObj->fPhase )
continue;
Vec_IntClear( vLeaves );
Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
assert( Vec_IntSize(vLeaves) <= N );
// printf( "%d ", Vec_IntSize(vLeaves) );
assert( Vec_IntSize(vLeaves) <= N );
// create map
Vec_IntWriteEntry( vMap, i, Vec_IntSize(vMap) );
Vec_IntPush( vMap, Vec_IntSize(vLeaves) );
Vec_IntForEachEntry( vLeaves, Leaf, k )
{
Vec_IntPush( vMap, Leaf );
Gia_ManObj(p, Leaf)->Value = uTruth5[k];
}
Vec_IntPush( vMap, (int)Ga2_ObjComputeTruth_rec( p, pObj, 1 ) );
Vec_IntPush( vMap, -1 ); // placeholder for ref counter
CountMarks++;
}
*pvMap = vMap;
// printf( "Internal nodes = %d. ", CountMarks );
Abc_PrintTime( 1, "Time", clock() - clk );
Vec_IntFree( vLeaves );
return CountMarks;
}
void Ga2_ManComputeTest( Gia_Man_t * p )
{
clock_t clk;
Vec_Int_t * vLeaves, * vMap;
Gia_Obj_t * pObj;
int i;
Ga2_ManMarkup( p, 5, &vMap );
clk = clock();
vLeaves = Vec_IntAlloc( 100 );
Gia_ManForEachAnd( p, pObj, i )
{
if ( !pObj->fPhase )
continue;
Vec_IntClear( vLeaves );
Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
Ga2_ManComputeTruth( p, pObj, vLeaves );
}
Vec_IntFree( vLeaves );
Vec_IntFree( vMap );
Abc_PrintTime( 1, "Time", clock() - clk );
}
/**Function*************************************************************
......@@ -272,17 +357,14 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->pGia = pGia;
p->pPars = pPars;
// markings
p->nMarked = Gia_ManRegNum(p->pGia) + Ga2_ManMarkup( pGia, 5 );
// data storage
p->vId2Data = Vec_IntStart( Gia_ManObjNum(pGia) );
p->nMarked = Gia_ManRegNum(p->pGia) + Ga2_ManMarkup( pGia, 5, &p->vMapping );
p->vDatas = Vec_PtrAlloc( 1000 );
Vec_PtrPush( p->vDatas, Vec_IntAlloc(0) );
Vec_PtrPush( p->vDatas, Vec_IntAlloc(0) );
Vec_PtrPush( p->vDatas, Vec_IntAlloc(0) );
// abstraction
p->nAbsStart= 1;
p->vAbs = Vec_IntAlloc( 1000 );
Vec_IntPush( p->vAbs, -1 );
p->vValues = Vec_IntAlloc( 1000 );
Vec_IntPush( p->vValues, -1 );
// refinement
p->pRnm = Rnm_ManStart( pGia );
// SAT solver and variables
......@@ -292,6 +374,8 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
p->vLits = Vec_IntAlloc( 100 );
p->vIsopMem = Vec_IntAlloc( 100 );
Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
// prepare
Gia_ManCleanValue( pGia );
return p;
}
......@@ -308,13 +392,13 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
***********************************************************************/
void Ga2_ManStop( Ga2_Man_t * p )
{
int i;
// if ( p->pPars->fVerbose )
Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n",
sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
Vec_IntFree( p->vId2Data );
Vec_IntFree( p->vMapping );
Vec_VecFree( (Vec_Vec_t *)p->vDatas );
Vec_IntFree( p->vAbs );
Vec_IntFree( p->vValues );
Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
Vec_IntFree( p->vCnf );
Vec_IntFree( p->vLits );
......@@ -330,68 +414,6 @@ void Ga2_ManStop( Ga2_Man_t * p )
/**Function*************************************************************
Synopsis [Computes truth table for the marked node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Ga2_ObjComputeTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst )
{
unsigned Val0, Val1;
if ( pObj->fPhase && !fFirst )
return pObj->Value;
assert( Gia_ObjIsAnd(pObj) );
Val0 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin0(pObj), 0 );
Val1 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin1(pObj), 0 );
return (Gia_ObjFaninC0(pObj) ? ~Val0 : Val0) & (Gia_ObjFaninC1(pObj) ? ~Val1 : Val1);
}
unsigned Ga2_ManComputeTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
{
static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
unsigned Res, Values[5];
Gia_Obj_t * pObj;
int i;
// compute leaves
Vec_IntClear( vLeaves );
Ga2_ManCollectLeaves_rec( p, pRoot, vLeaves, 1 );
// assign elementary truth tables
Gia_ManForEachObjVec( vLeaves, p, pObj, i )
{
assert( pObj->fPhase );
Values[i] = pObj->Value;
pObj->Value = uTruth5[i];
}
Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
// return values
Gia_ManForEachObjVec( vLeaves, p, pObj, i )
pObj->Value = Values[i];
return Res;
}
void Ga2_ManComputeTest( Gia_Man_t * p )
{
clock_t clk;
Vec_Int_t * vLeaves;
Gia_Obj_t * pObj;
int i;
Ga2_ManMarkup( p, 5 );
clk = clock();
vLeaves = Vec_IntAlloc( 100 );
Gia_ManForEachAnd( p, pObj, i )
{
if ( !pObj->fPhase )
continue;
Ga2_ManComputeTruth( p, pObj, vLeaves );
}
Vec_IntFree( vLeaves );
Abc_PrintTime( 1, "Time", clock() - clk );
}
/**Function*************************************************************
Synopsis [Computes and minimizes the truth table.]
Description [Array of input literals may contain 0 (const0), 1 (const1)
......@@ -475,7 +497,7 @@ unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t
SeeAlso []
***********************************************************************/
void Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCnf, Vec_Int_t * vCover )
Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover )
{
extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
int RetValue;
......@@ -484,8 +506,7 @@ void Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCnf, Vec_Int_t
RetValue = Kit_TruthIsop( &uTruth, nVars, vCover, 0 );
assert( RetValue == 0 );
// check the case of constant cover
Vec_IntClear( vCnf );
Vec_IntAppend( vCnf, vCover );
return Vec_IntDup( vCover );
}
......@@ -587,72 +608,87 @@ static inline void Ga2_ManCnfAddStatic( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_In
SeeAlso []
***********************************************************************/
void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj )
void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
{
Vec_Int_t * vLeaves, * vCnf0, * vCnf1;
unsigned uTruth;
// create new data entry
assert( Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) ) == 0 );
Vec_IntWriteEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj), Vec_IntSize(p->vDatas) );
Vec_IntPush( p->vDatas, (vLeaves = Vec_IntAlloc(5)) );
Vec_IntPush( p->vDatas, (vCnf0 = Vec_IntAlloc(8)) );
Vec_IntPush( p->vDatas, (vCnf1 = Vec_IntAlloc(8)) );
// derive leaves
Ga2_ManCollectLeaves_rec( p->pGia, pObj, vLeaves, 1 );
assert( Vec_IntSize(vLeaves) < 6 );
// compute truth table
uTruth = Ga2_ManComputeTruth( p->pGia, pObj, vLeaves );
// prepare CNF
Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf0, p->vIsopMem );
uTruth = (~uTruth) & Abc_InfoMask( (1 << Vec_IntSize(vLeaves)) );
Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf1, p->vIsopMem );
}
static inline Vec_Int_t * Ga2_ManNodeLeaves( Ga2_Man_t * p, Gia_Obj_t * pObj )
{
if ( Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) ) == 0 )
Ga2_ManSetupNode( p, pObj );
return (Vec_Int_t *)Vec_PtrEntry( p->vDatas, Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) ) );
}
static inline Vec_Int_t * Ga2_ManNodeCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj )
{
int Num = Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) );
assert( Num > 0 );
return (Vec_Int_t *)Vec_PtrEntry( p->vDatas, Num + 1 );
}
static inline Vec_Int_t * Ga2_ManNodeCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj )
{
int Num = Vec_IntEntry( p->vId2Data, Gia_ObjId(p->pGia, pObj) );
assert( Num > 0 );
return (Vec_Int_t *)Vec_PtrEntry( p->vDatas, Num + 2 );
int nLeaves;
assert( pObj->fPhase );
assert( Vec_PtrSize(p->vDatas) == 2 * Vec_IntSize(p->vValues) );
// assign value to the node
if ( pObj->Value == 0 )
{
pObj->Value = Vec_IntSize(p->vValues);
Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) );
Vec_PtrPush( p->vDatas, NULL );
Vec_PtrPush( p->vDatas, NULL );
}
assert( Ga2_ObjCnf0(p, pObj) == NULL );
if ( !fAbs )
return;
// compute parameters
nLeaves = Ga2_ObjLeaveNum(p, pObj);
uTruth = Ga2_ObjTruth( p, pObj );
// create CNF for pos/neg phases
Vec_PtrWriteEntry( p->vDatas, 2 * pObj->Value, Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) );
uTruth = (~uTruth) & Abc_InfoMask( (1 << nLeaves) );
Vec_PtrWriteEntry( p->vDatas, 2 * pObj->Value + 1, Ga2_ManCnfCompute(uTruth, nLeaves, p->vIsopMem) );
}
void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
{
Gia_Obj_t * pObj;
int i;
Vec_Int_t * vLeaves, * vMap;
Gia_Obj_t * pObj, * pFanin;
int i, k;
// add abstraction objects
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
{
assert( pObj->fMark0 == 0 );
pObj->fMark0 = 1;
Ga2_ManSetupNode( p, pObj );
Ga2_ManSetupNode( p, pObj, 1 );
Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) );
}
// add PPI objects
Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
{
vLeaves = Ga2_ObjLeaves( p, pObj );
Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k, )
Ga2_ManSetupNode( p, pObj, 0 );
}
// clean mapping into timeframes
Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
Vec_IntFillExtra( vMap, Vec_IntSize(p->vValues), -1 );
}
void Ga2_ManRemoveFromAbs( Ga2_Man_t * p )
void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues )
{
Vec_Int_t * vMap;
Gia_Obj_t * pObj;
int i, k;
int i;
assert( nAbs >= 0 );
assert( nValues > 0 );
// shrink abstraction
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
{
if ( i < p->nAbs )
assert( Ga2_ObjCnf0(p, pObj) != NULL );
assert( Ga2_ObjCnf1(p, pObj) != NULL );
if ( i < nAbs )
continue;
Vec_IntFree( Ga2_ObjCnf0(p, pObj) );
Vec_IntFree( Ga2_ObjCnf1(p, pObj) );
Vec_PtrWriteEntry( p->vDatas, 2 * pObj->Value, NULL );
Vec_PtrWriteEntry( p->vDatas, 2 * pObj->Value + 1, NULL );
}
Vec_IntShrink( p->vAbs, nAbs );
// shrink values
Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
{
assert( pObj->Value );
if ( i < nValues )
continue;
assert( pObj->fMark0 == 1 );
pObj->fMark0 = 0;
pObj->Value = 0;
}
Vec_IntShrink( p->vAbs, p->nAbs );
Vec_IntShrink( p->vValues, nValues );
// clean mapping into timeframes
Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
Vec_IntShrink( vMap, nValues );
}
......@@ -667,52 +703,66 @@ void Ga2_ManRemoveFromAbs( Ga2_Man_t * p )
SeeAlso []
***********************************************************************/
void Ga2_ManRestart( Ga2_Man_t * p )
void Ga2_ManAbsTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vClasses, int fFirst )
{
if ( pObj->fPhase && !fFirst )
return;
assert( Gia_ObjIsAnd(pObj) );
Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin0(pObj), vClasses, 0 );
Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin1(pObj), vClasses, 0 );
Vec_IntWriteEntry( vClasses, Gia_ObjId(p, pObj), 1 );
}
Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p )
{
Vec_Int_t * vGateClasses;
Gia_Obj_t * pObj;
int i;
vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
return vGateClasses;
}
Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p )
{
Vec_Int_t * vToAdd;
Gia_Obj_t * pObj;
int i, Lit;
int i;
vToAdd = Vec_IntAlloc( 1000 );
Gia_ManForEachObj( p, pObj, i )
if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) )
Vec_IntPush( vToAdd, i );
return vToAdd;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ga2_ManRestart( Ga2_Man_t * p )
{
Vec_Int_t * vToAdd;
assert( p->pGia != NULL );
assert( p->pGia->vGateClasses != NULL );
assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set
// clear mappings from objects
Gia_ManCleanValue( p->pGia );
for ( i = 1; i < p->nObjs; i++ )
{
Vec_IntShrink( &p->pvLeaves[i], 0 );
Vec_IntShrink( &p->pvCnfs0[i], 0 );
Vec_IntShrink( &p->pvCnfs1[i], 0 );
}
// clear abstraction
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
{
assert( pObj->fMark0 );
pObj->fMark0 = 0;
}
// clear mapping into timeframes
Vec_VecFreeP( (Vec_Vec_t **)&p->vMaps );
p->vMaps = Vec_PtrAlloc( 1000 );
Vec_PtrPush( p->vMaps, Vec_IntAlloc(0) );
Ga2_ManShrinkAbs( p, 0, 1 );
// clear SAT variable numbers (begin with 1)
if ( p->pSat ) sat_solver2_delete( p->pSat );
p->pSat = sat_solver2_new();
p->nSatVars = 1;
// create constant literals
Lit = toLitCond( 1, 1 );
sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 );
// start abstraction
p->nObjs = 1;
Vec_IntClear( p->vAbs );
Gia_ManForEachObj( p->pGia, pObj, i )
{
if ( pObj->fPhase && Vec_IntEntry(p->pGia->vGateClasses, i) )
{
assert( pObj->fMark0 == 0 );
pObj->fMark0 = 1;
Vec_IntPush( p->vAbs, i );
Ga2_ManSetupNode( p, pObj );
}
}
p->nAbs = Vec_IntSize( p->vAbs );
vToAdd = Ga2_ManAbsDerive( p->pGia );
Ga2_ManAddToAbs( p, vToAdd );
Vec_IntFree( vToAdd );
p->LimAbs = Vec_IntSize(p->vAbs) + 1;
p->LimPpi = Vec_IntSize(p->vValues);
// set runtime limit
if ( p->pPars->nTimeOut )
sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart );
......@@ -720,7 +770,7 @@ void Ga2_ManRestart( Ga2_Man_t * p )
/**Function*************************************************************
Synopsis []
Synopsis [Unrolls one timeframe.]
Description []
......@@ -729,24 +779,73 @@ void Ga2_ManRestart( Ga2_Man_t * p )
SeeAlso []
***********************************************************************/
void Ga2_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vClasses, int fFirst )
{
if ( pObj->fPhase && !fFirst )
return;
assert( Gia_ObjIsAnd(pObj) );
Ga2_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vClasses, 0 );
Ga2_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vClasses, 0 );
Vec_IntWriteEntry( vClasses, Gia_ObjId(p, pObj), 1 );
}
Vec_Int_t * Ga2_ManTranslate( Ga2_Man_t * p )
int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{
Vec_Int_t * vGateClasses;
Gia_Obj_t * pObj;
int i;
vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
Ga2_ManTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
return vGateClasses;
Vec_Int_t * vLeaves;
Gia_Obj_t * pLeaf;
unsigned uTruth;
int nLeaves, * pLeaves;
int i, Lit, pLits[5];
if ( Gia_ObjIsCo(pObj) )
return Abc_LitNotCond( Ga2_ManUnroll_rec(p, Gia_ObjFanin0(pObj), f), Gia_ObjFaninC0(pObj) );
if ( Gia_ObjIsConst0(pObj) || (f==0 && Gia_ObjIsRo(p->pGia, pObj)) )
return 0;
Lit = Ga2_ObjFindLit( p, pObj, f );
if ( Lit >= 0 )
return Lit;
if ( Gia_ObjIsPi(p->pGia, pObj) )
return Ga2_ObjFindOrAddLit( p, pObj, f );
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
assert( f > 0 );
Lit = Ga2_ManUnroll_rec( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 );
Ga2_ObjAddLit( p, pObj, f, Lit );
return Lit;
}
// collect fanin literals
nLeaves = Ga2_ObjLeaveNum( p, pObj );
pLeaves = Ga2_ObjLeavePtr( p, pObj );
for ( i = 0; i < nLeaves; i++ )
{
pLeaf = Gia_ManObj( p->pGia, pLeaves[i] );
if ( Ga2_ObjIsAbs(p, pLeaf) ) // belongs to original abstraction
pLits[i] = Ga2_ManUnroll_rec( p, pObj, f );
else if ( Ga2_ObjIsPPI(p, pLeaf) ) // belongs to original PPIs
pLits[i] = GA2_BIG_NUM + i;
else
assert( 0 );
}
// collect literals
Vec_IntClear( p->vLits );
for ( i = 0; i < nLeaves; i++ )
Vec_IntPush( p->vLits, pLits[i] );
// minimize truth table
vLeaves = Ga2_ObjLeaves( p, pObj );
uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits );
if ( uTruth == 0 || uTruth == ~0 )
Ga2_ObjAddLit( p, pObj, f, uTruth == 0 ? 3 : 2 ); // const 0 / 1
else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 ) // buffer / inverter
{
Lit = Vec_IntEntry( p->vLits, 0 );
pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) );
Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
Ga2_ObjAddLit( p, pObj, f, Abc_LitNotCond(Lit, uTruth == 0x55555555) );
}
else
{
// replace numbers of literals by actual literals
Vec_IntForEachEntry( p->vLits, Lit, i )
{
pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) );
Lit = Ga2_ObjFindOrAddLit(p, pLeaf, f);
Vec_IntWriteEntry( p->vLits, i, Lit );
}
// add CNF
Lit = Ga2_ObjFindOrAddLit(p, pObj, f);
Ga2_ManCnfAddDynamic( p, uTruth, Vec_IntArray(p->vLits), Lit, 0 );
Ga2_ObjAddLit( p, pObj, f, Lit );
}
return Lit;
}
/**Function*************************************************************
......@@ -760,7 +859,8 @@ Vec_Int_t * Ga2_ManTranslate( Ga2_Man_t * p )
SeeAlso []
***********************************************************************/
void Ga2_ManUnroll( Ga2_Man_t * p, int f )
/*
void Ga2_ManUnroll2( Ga2_Man_t * p, int f )
{
Gia_Obj_t * pObj, * pObjRi, * pLeaf;
Vec_Int_t * vLeaves;
......@@ -785,8 +885,8 @@ void Ga2_ManUnroll( Ga2_Man_t * p, int f )
}
assert( Gia_ObjIsAnd(pObj) );
assert( pObj->Value > 0 );
vLeaves = &p->pvLeaves[pObj->Value];
// for nodes recently added to abstration, add CNF without const propagation
vLeaves = Ga2_ObjLeaves(p, pObj);
// for nodes recently added to abstraction, add CNF without const propagation
fFullTable = 1;
if ( i < p->nAbs )
{
......@@ -864,7 +964,7 @@ void Ga2_ManUnroll( Ga2_Man_t * p, int f )
Ga2_ObjAddLit( p, pObjRi, f, Lit );
}
}
*/
/**Function*************************************************************
......@@ -1000,7 +1100,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Ga2_Man_t * p;
Vec_Int_t * vCore, * vPPis;
clock_t clk = clock();
int i, c, f, Lit, Status, RetValue = -1;;
int i, c, f, Lit, nAbs, nValues, Status, RetValue = -1;;
// start the manager
p = Ga2_ManStart( pAig, pPars );
// check trivial case
......@@ -1042,16 +1142,19 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
// create new SAT solver
Ga2_ManRestart( p );
// remember current limits
nAbs = Vec_IntSize(p->vAbs);
nValues = Vec_IntSize(p->vValues);
// unroll the circuit
for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
{
// add one more time-frame
Ga2_ManUnroll( p, f );
p->pPars->iFrame = f;
// get the output literal
Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f );
// check for counter-examples
for ( c = 0; ; c++ )
{
// perform SAT solving
Lit = Ga2_ObjFindOrAddLit( p, Gia_ManPo(p->pGia, 0), f );
Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( Status == l_True ) // perform refinement
{
......@@ -1060,6 +1163,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
goto finish;
Ga2_ManAddToAbs( p, vPPis );
Vec_IntFree( vPPis );
// verify
if ( Vec_IntCheckUnique(p->vAbs) )
printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) );
continue;
......@@ -1071,9 +1175,13 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
assert( RetValue == l_False );
// derive UNSAT core
vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
Ga2_ManRemoveFromAbs( p );
Ga2_ManShrinkAbs( p, nAbs, nValues );
Ga2_ManAddToAbs( p, vCore );
Vec_IntFree( vCore );
// remember current limits
nAbs = Vec_IntSize(p->vAbs);
nValues = Vec_IntSize(p->vValues);
// verify
if ( Vec_IntCheckUnique(p->vAbs) )
printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) );
break;
......@@ -1081,7 +1189,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
if ( c > 0 )
{
Vec_IntFreeP( &pAig->vGateClasses );
pAig->vGateClasses = Ga2_ManTranslate( p );
pAig->vGateClasses = Ga2_ManAbsTranslate( p );
break; // temporary
}
}
......@@ -1099,7 +1207,7 @@ finish:
if ( pAig->vGateClasses != NULL )
Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );
Vec_IntFreeP( &pAig->vGateClasses );
pAig->vGateClasses = Ga2_ManTranslate( p );
pAig->vGateClasses = Ga2_ManAbsTranslate( p );
if ( Status == l_Undef )
{
if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
......@@ -1143,7 +1251,7 @@ finish:
return RetValue;
}
#endif
//#endif
////////////////////////////////////////////////////////////////////////
......
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