mirror of https://github.com/YosysHQ/abc.git
Added command &gla_purify.
This commit is contained in:
parent
21b847a8db
commit
685faae8e2
|
|
@ -702,6 +702,11 @@ extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int
|
||||||
extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
|
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_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf );
|
||||||
extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver );
|
extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver );
|
||||||
|
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 Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
|
||||||
|
extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
|
||||||
|
extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
|
||||||
/*=== giaAbsGla.c ===========================================================*/
|
/*=== giaAbsGla.c ===========================================================*/
|
||||||
extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta );
|
extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta );
|
||||||
/*=== giaAbsVta.c ===========================================================*/
|
/*=== giaAbsVta.c ===========================================================*/
|
||||||
|
|
@ -941,11 +946,6 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
|
||||||
extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
|
extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
|
||||||
extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
|
extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
|
||||||
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
|
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
|
||||||
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 Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
|
|
||||||
extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
|
|
||||||
extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
|
|
||||||
|
|
||||||
/*=== giaCTas.c ===========================================================*/
|
/*=== giaCTas.c ===========================================================*/
|
||||||
typedef struct Tas_Man_t_ Tas_Man_t;
|
typedef struct Tas_Man_t_ Tas_Man_t;
|
||||||
|
|
|
||||||
|
|
@ -498,6 +498,216 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver )
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Converting VTA vector to GLA vector.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
|
||||||
|
{
|
||||||
|
Gia_Obj_t * pObj;
|
||||||
|
Vec_Int_t * vGla;
|
||||||
|
int nObjMask, nObjs = Gia_ManObjNum(p);
|
||||||
|
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
|
||||||
|
vGla = Vec_IntStart( nObjs );
|
||||||
|
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_IntAddToEntry( vGla, (Entry & nObjMask), 1 );
|
||||||
|
}
|
||||||
|
Vec_IntWriteEntry( vGla, 0, nFrames );
|
||||||
|
return vGla;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Converting GLA vector to VTA vector.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
|
||||||
|
{
|
||||||
|
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*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Converting GLA vector to FLA vector.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla )
|
||||||
|
{
|
||||||
|
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
|
||||||
|
return;
|
||||||
|
Gia_ObjSetTravIdCurrent(p, pObj);
|
||||||
|
Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
|
||||||
|
if ( Gia_ObjIsRo(p, pObj) )
|
||||||
|
return;
|
||||||
|
assert( Gia_ObjIsAnd(pObj) );
|
||||||
|
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
|
||||||
|
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Converting FLA vector to GLA vector.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla )
|
||||||
|
{
|
||||||
|
Vec_Int_t * vGla;
|
||||||
|
Gia_Obj_t * pObj;
|
||||||
|
int i;
|
||||||
|
// mark const0 and relevant CI objects
|
||||||
|
Gia_ManIncrementTravId( p );
|
||||||
|
Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
|
||||||
|
Gia_ManForEachPi( p, pObj, i )
|
||||||
|
Gia_ObjSetTravIdCurrent(p, pObj);
|
||||||
|
Gia_ManForEachRo( p, pObj, i )
|
||||||
|
if ( !Vec_IntEntry(vFla, i) )
|
||||||
|
Gia_ObjSetTravIdCurrent(p, pObj);
|
||||||
|
// label all objects reachable from the PO and selected flops
|
||||||
|
vGla = Vec_IntStart( Gia_ManObjNum(p) );
|
||||||
|
Vec_IntWriteEntry( vGla, 0, 1 );
|
||||||
|
Gia_ManForEachPo( p, pObj, i )
|
||||||
|
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
|
||||||
|
Gia_ManForEachRi( p, pObj, i )
|
||||||
|
if ( Vec_IntEntry(vFla, i) )
|
||||||
|
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
|
||||||
|
return vGla;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Converting GLA vector to FLA vector.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla )
|
||||||
|
{
|
||||||
|
Vec_Int_t * vFla;
|
||||||
|
Gia_Obj_t * pObj;
|
||||||
|
int i;
|
||||||
|
vFla = Vec_IntStart( Gia_ManRegNum(p) );
|
||||||
|
Gia_ManForEachRo( p, pObj, i )
|
||||||
|
if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
|
||||||
|
Vec_IntWriteEntry( vFla, i, 1 );
|
||||||
|
return vFla;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose )
|
||||||
|
{
|
||||||
|
int i, Entry, CountUpTo, CountAll, CountRem, * pCounts;
|
||||||
|
int nFrames = Vec_IntEntry( p->vGateClasses, 0 );
|
||||||
|
if ( nFrames < 2 )
|
||||||
|
{
|
||||||
|
printf( "Gate-level abstraction is missing object count information.\n" );
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
// collect info
|
||||||
|
CountAll = 0;
|
||||||
|
pCounts = ABC_CALLOC( int, nFrames + 1 );
|
||||||
|
assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) );
|
||||||
|
for ( i = 0; i < Gia_ManObjNum(p); i++ )
|
||||||
|
{
|
||||||
|
Entry = Vec_IntEntry( p->vGateClasses, i );
|
||||||
|
assert( Entry >= 0 && Entry <= nFrames );
|
||||||
|
if ( Entry == 0 )
|
||||||
|
continue;
|
||||||
|
CountAll++;
|
||||||
|
pCounts[Entry]++;
|
||||||
|
}
|
||||||
|
// print entries
|
||||||
|
CountUpTo = 0;
|
||||||
|
for ( i = 0; i <= nFrames; i++ )
|
||||||
|
printf( "%d=%d(%d) ", i, pCounts[i], CountUpTo += pCounts[i] );
|
||||||
|
printf( "\n" );
|
||||||
|
// removing entries appearing only ones
|
||||||
|
CountRem = 0;
|
||||||
|
for ( i = 0; i < Gia_ManObjNum(p); i++ )
|
||||||
|
{
|
||||||
|
if ( Vec_IntEntry( p->vGateClasses, i ) == 0 )
|
||||||
|
continue;
|
||||||
|
if ( Vec_IntEntry( p->vGateClasses, i ) <= nPurifyRatio )
|
||||||
|
{
|
||||||
|
CountRem++;
|
||||||
|
Vec_IntWriteEntry( p->vGateClasses, i, 0 );
|
||||||
|
}
|
||||||
|
}
|
||||||
|
printf( "Removed %d entries appearing less or equal than %d times (out of %d).\n", CountRem, nPurifyRatio, CountAll );
|
||||||
|
ABC_FREE( pCounts );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// END OF FILE ///
|
/// END OF FILE ///
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
||||||
|
|
@ -83,9 +83,9 @@ struct Gla_Man_t_
|
||||||
Vec_Int_t * vTemp; // temporary array
|
Vec_Int_t * vTemp; // temporary array
|
||||||
Vec_Int_t * vAddedNew; // temporary array
|
Vec_Int_t * vAddedNew; // temporary array
|
||||||
Vec_Int_t * vObjCounts; // object counters
|
Vec_Int_t * vObjCounts; // object counters
|
||||||
|
Vec_Int_t * vCoreCounts; // counts how many times each object appears in the core
|
||||||
// refinement
|
// refinement
|
||||||
Vec_Int_t * pvRefis; // vectors of each object
|
Vec_Int_t * pvRefis; // vectors of each object
|
||||||
// Vec_Int_t * vPrioSels; // selected priorities
|
|
||||||
// statistics
|
// statistics
|
||||||
clock_t timeInit;
|
clock_t timeInit;
|
||||||
clock_t timeSat;
|
clock_t timeSat;
|
||||||
|
|
@ -296,7 +296,7 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
|
||||||
assert( i >= Vec_IntSize(vPis) );
|
assert( i >= Vec_IntSize(vPis) );
|
||||||
iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
|
iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
|
||||||
assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
|
assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
|
||||||
if ( Vec_IntEntry( p->vGateClasses, iObjId ) == 1 )
|
if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
|
||||||
continue;
|
continue;
|
||||||
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
|
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
|
||||||
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
|
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
|
||||||
|
|
@ -963,7 +963,6 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
|
||||||
p->vAbs = Vec_IntAlloc( 100 );
|
p->vAbs = Vec_IntAlloc( 100 );
|
||||||
p->vTemp = Vec_IntAlloc( 100 );
|
p->vTemp = Vec_IntAlloc( 100 );
|
||||||
p->vAddedNew = Vec_IntAlloc( 100 );
|
p->vAddedNew = Vec_IntAlloc( 100 );
|
||||||
// p->vPrioSels = Vec_IntAlloc( 100 );
|
|
||||||
p->vObjCounts = Vec_IntAlloc( 100 );
|
p->vObjCounts = Vec_IntAlloc( 100 );
|
||||||
|
|
||||||
// internal data
|
// internal data
|
||||||
|
|
@ -978,6 +977,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
|
||||||
// derive new gate map
|
// derive new gate map
|
||||||
assert( pGia0->vGateClasses != 0 );
|
assert( pGia0->vGateClasses != 0 );
|
||||||
p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
|
p->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
|
||||||
|
p->vCoreCounts = Vec_IntStart( Gia_ManObjNum(p->pGia) );
|
||||||
// update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause
|
// update p->pCnf->vMapping, p->pCnf->pObj2Count, p->pCnf->pObj2Clause
|
||||||
// (here are not updating p->pCnf->pVarNums because it is not needed)
|
// (here are not updating p->pCnf->pVarNums because it is not needed)
|
||||||
vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) );
|
vMappingNew = Vec_IntStart( Gia_ManObjNum(p->pGia) );
|
||||||
|
|
@ -1129,7 +1129,6 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
|
||||||
p->vAbs = Vec_IntAlloc( 100 );
|
p->vAbs = Vec_IntAlloc( 100 );
|
||||||
p->vTemp = Vec_IntAlloc( 100 );
|
p->vTemp = Vec_IntAlloc( 100 );
|
||||||
p->vAddedNew = Vec_IntAlloc( 100 );
|
p->vAddedNew = Vec_IntAlloc( 100 );
|
||||||
// p->vPrioSels = Vec_IntAlloc( 100 );
|
|
||||||
// internal data
|
// internal data
|
||||||
pAig = Gia_ManToAigSimple( p->pGia );
|
pAig = Gia_ManToAigSimple( p->pGia );
|
||||||
p->pCnf = Cnf_DeriveOther( pAig, 1 );
|
p->pCnf = Cnf_DeriveOther( pAig, 1 );
|
||||||
|
|
@ -1228,7 +1227,7 @@ void Gla_ManStop( Gla_Man_t * p )
|
||||||
Vec_IntFreeP( &p->vObjCounts );
|
Vec_IntFreeP( &p->vObjCounts );
|
||||||
Vec_IntFreeP( &p->vCla2Obj );
|
Vec_IntFreeP( &p->vCla2Obj );
|
||||||
Vec_IntFreeP( &p->vAddedNew );
|
Vec_IntFreeP( &p->vAddedNew );
|
||||||
// Vec_IntFreeP( &p->vPrioSels );
|
Vec_IntFreeP( &p->vCoreCounts );
|
||||||
Vec_IntFreeP( &p->vTemp );
|
Vec_IntFreeP( &p->vTemp );
|
||||||
Vec_IntFreeP( &p->vAbs );
|
Vec_IntFreeP( &p->vAbs );
|
||||||
ABC_FREE( p->pvRefis );
|
ABC_FREE( p->pvRefis );
|
||||||
|
|
@ -1276,7 +1275,7 @@ int Gia_GlaAbsCount( Gla_Man_t * p, int fRo, int fAnd )
|
||||||
SeeAlso []
|
SeeAlso []
|
||||||
|
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
int Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap )
|
int Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla, int nUsageCount )
|
||||||
{
|
{
|
||||||
int Value0, Value1;
|
int Value0, Value1;
|
||||||
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
|
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
|
||||||
|
|
@ -1285,41 +1284,46 @@ int Gla_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vMap )
|
||||||
if ( Gia_ObjIsCi(pObj) )
|
if ( Gia_ObjIsCi(pObj) )
|
||||||
return 0;
|
return 0;
|
||||||
assert( Gia_ObjIsAnd(pObj) );
|
assert( Gia_ObjIsAnd(pObj) );
|
||||||
Value0 = Gla_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vMap );
|
Value0 = Gla_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vGla, nUsageCount );
|
||||||
Value1 = Gla_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vMap );
|
Value1 = Gla_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vGla, nUsageCount );
|
||||||
if ( Value0 || Value1 )
|
if ( Value0 || Value1 )
|
||||||
Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), 1 );
|
Vec_IntAddToEntry( vGla, Gia_ObjId(p, pObj), nUsageCount );
|
||||||
return Value0 || Value1;
|
return Value0 || Value1;
|
||||||
}
|
}
|
||||||
Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
|
Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
|
||||||
{
|
{
|
||||||
Vec_Int_t * vRes, * vRes2;
|
Vec_Int_t * vGla, * vGla2;
|
||||||
Gla_Obj_t * pObj, * pFanin;
|
Gla_Obj_t * pObj, * pFanin;
|
||||||
Gia_Obj_t * pGiaObj;
|
Gia_Obj_t * pGiaObj;
|
||||||
int i, k;
|
int i, k, nUsageCount;
|
||||||
vRes = Vec_IntStart( Gia_ManObjNum(p->pGia) );
|
vGla = Vec_IntStart( Gia_ManObjNum(p->pGia) );
|
||||||
Gla_ManForEachObjAbs( p, pObj, i )
|
Gla_ManForEachObjAbs( p, pObj, i )
|
||||||
{
|
{
|
||||||
Vec_IntWriteEntry( vRes, pObj->iGiaObj, 1 );
|
nUsageCount = Vec_IntEntry(p->vCoreCounts, pObj->iGiaObj);
|
||||||
|
assert( nUsageCount >= 0 );
|
||||||
pGiaObj = Gla_ManGiaObj( p, pObj );
|
pGiaObj = Gla_ManGiaObj( p, pObj );
|
||||||
if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) )
|
if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) )
|
||||||
|
{
|
||||||
|
Vec_IntWriteEntry( vGla, pObj->iGiaObj, nUsageCount );
|
||||||
continue;
|
continue;
|
||||||
|
}
|
||||||
assert( Gia_ObjIsAnd(pGiaObj) );
|
assert( Gia_ObjIsAnd(pGiaObj) );
|
||||||
Gia_ManIncrementTravId( p->pGia );
|
Gia_ManIncrementTravId( p->pGia );
|
||||||
Gla_ObjForEachFanin( p, pObj, pFanin, k )
|
Gla_ObjForEachFanin( p, pObj, pFanin, k )
|
||||||
Gia_ObjSetTravIdCurrent( p->pGia, Gla_ManGiaObj(p, pFanin) );
|
Gia_ObjSetTravIdCurrent( p->pGia, Gla_ManGiaObj(p, pFanin) );
|
||||||
Gla_ManTranslate_rec( p->pGia, pGiaObj, vRes );
|
Gla_ManTranslate_rec( p->pGia, pGiaObj, vGla, nUsageCount );
|
||||||
}
|
}
|
||||||
if ( p->pGia->vLutConfigs )
|
Vec_IntWriteEntry( vGla, 0, p->pPars->iFrame+1 );
|
||||||
|
if ( p->pGia->vLutConfigs ) // use mapping from new to old
|
||||||
{
|
{
|
||||||
vRes2 = Vec_IntStart( Gia_ManObjNum(p->pGia0) );
|
vGla2 = Vec_IntStart( Gia_ManObjNum(p->pGia0) );
|
||||||
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
|
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
|
||||||
if ( Vec_IntEntry(vRes, i) )
|
if ( Vec_IntEntry(vGla, i) )
|
||||||
Vec_IntWriteEntry( vRes2, Vec_IntEntry(p->pGia->vLutConfigs, i), 1 );
|
Vec_IntWriteEntry( vGla2, Vec_IntEntry(p->pGia->vLutConfigs, i), Vec_IntEntry(vGla, i) );
|
||||||
Vec_IntFree( vRes );
|
Vec_IntFree( vGla );
|
||||||
return vRes2;
|
return vGla2;
|
||||||
}
|
}
|
||||||
return vRes;
|
return vGla;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -1471,6 +1475,13 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
|
||||||
}
|
}
|
||||||
else assert( 0 );
|
else assert( 0 );
|
||||||
}
|
}
|
||||||
|
void Gia_GlaAddToCounters( Gla_Man_t * p, Vec_Int_t * vCore )
|
||||||
|
{
|
||||||
|
Gla_Obj_t * pGla;
|
||||||
|
int i;
|
||||||
|
Gla_ManForEachObjAbsVec( vCore, p, pGla, i )
|
||||||
|
Vec_IntAddToEntry( p->vCoreCounts, pGla->iGiaObj, 1 );
|
||||||
|
}
|
||||||
void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
|
void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
|
||||||
{
|
{
|
||||||
Gla_Obj_t * pGla;
|
Gla_Obj_t * pGla;
|
||||||
|
|
@ -1882,7 +1893,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
|
||||||
}
|
}
|
||||||
assert( Status == 1 );
|
assert( Status == 1 );
|
||||||
// valid core is obtained
|
// valid core is obtained
|
||||||
nCoreSize = Vec_IntSize(vCore);
|
nCoreSize = Vec_IntSize( vCore );
|
||||||
|
Gia_GlaAddToCounters( p, vCore );
|
||||||
if ( i == 0 )
|
if ( i == 0 )
|
||||||
Vec_IntFree( vCore );
|
Vec_IntFree( vCore );
|
||||||
else
|
else
|
||||||
|
|
|
||||||
|
|
@ -1683,7 +1683,7 @@ Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses )
|
||||||
{
|
{
|
||||||
if ( Entry == 0 )
|
if ( Entry == 0 )
|
||||||
continue;
|
continue;
|
||||||
assert( Entry == 1 );
|
assert( Entry > 0 );
|
||||||
pObj = Gia_ManObj( p, i );
|
pObj = Gia_ManObj( p, i );
|
||||||
Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) );
|
Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) );
|
||||||
if ( Gia_ObjIsAnd(pObj) )
|
if ( Gia_ObjIsAnd(pObj) )
|
||||||
|
|
|
||||||
|
|
@ -1278,159 +1278,6 @@ void Gia_ManInvertConstraints( Gia_Man_t * pAig )
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/**Function*************************************************************
|
|
||||||
|
|
||||||
Synopsis [Converting VTA vector to GLA vector.]
|
|
||||||
|
|
||||||
Description []
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta )
|
|
||||||
{
|
|
||||||
Gia_Obj_t * pObj;
|
|
||||||
Vec_Int_t * vGla;
|
|
||||||
int nObjMask, nObjs = Gia_ManObjNum(p);
|
|
||||||
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
|
|
||||||
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( vGla, (Entry & nObjMask), 1 );
|
|
||||||
}
|
|
||||||
return vGla;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
|
||||||
|
|
||||||
Synopsis [Converting GLA vector to VTA vector.]
|
|
||||||
|
|
||||||
Description []
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames )
|
|
||||||
{
|
|
||||||
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*************************************************************
|
|
||||||
|
|
||||||
Synopsis [Converting GLA vector to FLA vector.]
|
|
||||||
|
|
||||||
Description []
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla )
|
|
||||||
{
|
|
||||||
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
|
|
||||||
return;
|
|
||||||
Gia_ObjSetTravIdCurrent(p, pObj);
|
|
||||||
Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 );
|
|
||||||
if ( Gia_ObjIsRo(p, pObj) )
|
|
||||||
return;
|
|
||||||
assert( Gia_ObjIsAnd(pObj) );
|
|
||||||
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
|
|
||||||
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla );
|
|
||||||
}
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
|
||||||
|
|
||||||
Synopsis [Converting FLA vector to GLA vector.]
|
|
||||||
|
|
||||||
Description []
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla )
|
|
||||||
{
|
|
||||||
Vec_Int_t * vGla;
|
|
||||||
Gia_Obj_t * pObj;
|
|
||||||
int i;
|
|
||||||
// mark const0 and relevant CI objects
|
|
||||||
Gia_ManIncrementTravId( p );
|
|
||||||
Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
|
|
||||||
Gia_ManForEachPi( p, pObj, i )
|
|
||||||
Gia_ObjSetTravIdCurrent(p, pObj);
|
|
||||||
Gia_ManForEachRo( p, pObj, i )
|
|
||||||
if ( !Vec_IntEntry(vFla, i) )
|
|
||||||
Gia_ObjSetTravIdCurrent(p, pObj);
|
|
||||||
// label all objects reachable from the PO and selected flops
|
|
||||||
vGla = Vec_IntStart( Gia_ManObjNum(p) );
|
|
||||||
Vec_IntWriteEntry( vGla, 0, 1 );
|
|
||||||
Gia_ManForEachPo( p, pObj, i )
|
|
||||||
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
|
|
||||||
Gia_ManForEachRi( p, pObj, i )
|
|
||||||
if ( Vec_IntEntry(vFla, i) )
|
|
||||||
Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla );
|
|
||||||
return vGla;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
|
||||||
|
|
||||||
Synopsis [Converting GLA vector to FLA vector.]
|
|
||||||
|
|
||||||
Description []
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla )
|
|
||||||
{
|
|
||||||
Vec_Int_t * vFla;
|
|
||||||
Gia_Obj_t * pObj;
|
|
||||||
int i;
|
|
||||||
vFla = Vec_IntStart( Gia_ManRegNum(p) );
|
|
||||||
Gia_ManForEachRo( p, pObj, i )
|
|
||||||
if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) )
|
|
||||||
Vec_IntWriteEntry( vFla, i, 1 );
|
|
||||||
return vFla;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis [Testing the speedup due to grouping POs into batches.]
|
Synopsis [Testing the speedup due to grouping POs into batches.]
|
||||||
|
|
@ -1627,6 +1474,7 @@ void Gia_ObjComputeTruthTableTest( Gia_Man_t * p )
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// END OF FILE ///
|
/// END OF FILE ///
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
||||||
|
|
@ -347,6 +347,7 @@ static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, cha
|
||||||
//static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
//static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
static int Abc_CommandAbc9GlaRefine ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
static int Abc_CommandAbc9GlaRefine ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
|
static int Abc_CommandAbc9GlaPurify ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
//static int Abc_CommandAbc9GlaCba ( 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_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
static int Abc_CommandAbc9Gla ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
static int Abc_CommandAbc9Gla ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||||
|
|
@ -795,6 +796,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
||||||
// Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 );
|
// Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 );
|
||||||
Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 );
|
Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 );
|
||||||
Cmd_CommandAdd( pAbc, "ABC9", "&gla_refine", Abc_CommandAbc9GlaRefine, 0 );
|
Cmd_CommandAdd( pAbc, "ABC9", "&gla_refine", Abc_CommandAbc9GlaRefine, 0 );
|
||||||
|
Cmd_CommandAdd( pAbc, "ABC9", "&gla_purify", Abc_CommandAbc9GlaPurify, 0 );
|
||||||
// Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 );
|
// Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 );
|
||||||
// Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 );
|
// Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 );
|
||||||
Cmd_CommandAdd( pAbc, "ABC9", "&gla", Abc_CommandAbc9Gla, 0 );
|
Cmd_CommandAdd( pAbc, "ABC9", "&gla", Abc_CommandAbc9Gla, 0 );
|
||||||
|
|
@ -27149,6 +27151,75 @@ usage:
|
||||||
return 1;
|
return 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis []
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Abc_CommandAbc9GlaPurify( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||||
|
{
|
||||||
|
extern void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose );
|
||||||
|
int fMinCut = 0;
|
||||||
|
int nPurifyRatio = 0;
|
||||||
|
int c, fVerbose = 0;
|
||||||
|
Extra_UtilGetoptReset();
|
||||||
|
while ( ( c = Extra_UtilGetopt( argc, argv, "Rmvh" ) ) != EOF )
|
||||||
|
{
|
||||||
|
switch ( c )
|
||||||
|
{
|
||||||
|
case 'R':
|
||||||
|
if ( globalUtilOptind >= argc )
|
||||||
|
{
|
||||||
|
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
|
||||||
|
goto usage;
|
||||||
|
}
|
||||||
|
nPurifyRatio = atoi(argv[globalUtilOptind]);
|
||||||
|
globalUtilOptind++;
|
||||||
|
if ( nPurifyRatio < 0 )
|
||||||
|
goto usage;
|
||||||
|
break;
|
||||||
|
case 'm':
|
||||||
|
fMinCut ^= 1;
|
||||||
|
break;
|
||||||
|
case 'v':
|
||||||
|
fVerbose ^= 1;
|
||||||
|
break;
|
||||||
|
case 'h':
|
||||||
|
goto usage;
|
||||||
|
default:
|
||||||
|
goto usage;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if ( pAbc->pGia == NULL )
|
||||||
|
{
|
||||||
|
Abc_Print( -1, "Abc_CommandAbc9GlaPurify(): There is no AIG.\n" );
|
||||||
|
return 1;
|
||||||
|
}
|
||||||
|
if ( pAbc->pGia->vGateClasses == NULL )
|
||||||
|
{
|
||||||
|
Abc_Print( -1, "Abc_CommandAbc9GlaPurify(): There is no gate-level abstraction.\n" );
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
|
Gia_ManGlaPurify( pAbc->pGia, nPurifyRatio, fVerbose );
|
||||||
|
return 0;
|
||||||
|
|
||||||
|
usage:
|
||||||
|
Abc_Print( -2, "usage: &gla_purify [-R num] [-vh]\n" );
|
||||||
|
Abc_Print( -2, "\t purifies gate-level abstraction by removing less frequent objects\n" );
|
||||||
|
// Abc_Print( -2, "\t-R num : the percetage of rare objects to remove [default = %d]\n", nPurifyRatio );
|
||||||
|
Abc_Print( -2, "\t-R num : remove objects with usage count less or equal than this [default = %d]\n", nPurifyRatio );
|
||||||
|
// Abc_Print( -2, "\t-m : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
|
||||||
|
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*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis []
|
Synopsis []
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue