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

Performance improvement in &gla_refine.

This commit is contained in:
Alan Mishchenko 2012-07-03 11:17:04 -07:00
parent 3bd0420bd9
commit 32217230b0
5 changed files with 391 additions and 238 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -752,8 +752,7 @@ extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
extern Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses );
extern void Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis );
extern void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes );
extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
/*=== giaEnable.c ==========================================================*/
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );

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

@ -36,7 +36,8 @@ struct Rfn_Obj_t_
unsigned Value : 1; // value
unsigned fVisit : 1; // visited
unsigned fPPi : 1; // PPI
unsigned Prio : 28; // priority
unsigned Prio : 18; // priority
unsigned Sign : 10; // priority
};
typedef struct Gla_Obj_t_ Gla_Obj_t; // abstraction object
@ -117,6 +118,10 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { *
#define Gla_ObjForEachFanin( p, pObj, pFanin, i ) \
for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ )
// some lessons learned from debugging mismatches between GIA and mapped CNF
// - inputs/output of AND-node maybe PPIs (have SAT vars), but the node is not included in the abstraction
// - some logic node can be a PPI of one LUT and an internal node of another LUT
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -132,7 +137,7 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { *
SeeAlso []
***********************************************************************/
Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Gia_Man_t * pAbs, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
{
Abc_Cex_t * pCex;
int i, f, iPiNum;
@ -181,11 +186,14 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
{
extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
int fAddOneLayer = 1;
Abc_Cex_t * pCexNew = NULL;
Gia_Man_t * pAbs;
Aig_Man_t * pAig;
Abc_Cex_t * pCare;
Vec_Int_t * vPis, * vPPis;
int f, i, iObjId, nOnes = 0, Counter = 0;
int f, i, iObjId, clk = clock();
int nOnes = 0, Counter = 0;
if ( p->vGateClasses == NULL )
{
printf( "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
@ -210,49 +218,110 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
// else
// printf( "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
// get inputs
Gia_GlaCollectInputs( p, p->vGateClasses, &vPis, &vPPis );
Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
// minimize the CEX
pAig = Gia_ManToAigSimple( pAbs );
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
Aig_ManStop( pAig );
if ( pCare == NULL )
printf( "Counter-example minimization has failed.\n" );
// add new objects to the map
iObjId = -1;
for ( f = 0; f <= pCare->iFrame; f++ )
for ( i = 0; i < pCare->nPis; i++ )
if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
// add missing logic
if ( fAddOneLayer )
{
Gia_Obj_t * pObj;
// check if this is a real counter-example
Gia_ObjTerSimSet0( Gia_ManConst0(pAbs) );
for ( f = 0; f <= pCex->iFrame; f++ )
{
Gia_ManForEachPi( pAbs, pObj, i )
{
if ( i >= Vec_IntSize(vPis) ) // PPIs
Gia_ObjTerSimSetX( pObj );
else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
Gia_ObjTerSimSet1( pObj );
else
Gia_ObjTerSimSet0( pObj );
}
Gia_ManForEachRo( pAbs, pObj, i )
{
if ( f == 0 )
Gia_ObjTerSimSet0( pObj );
else
Gia_ObjTerSimRo( pAbs, pObj );
}
Gia_ManForEachAnd( pAbs, pObj, i )
Gia_ObjTerSimAnd( pObj );
Gia_ManForEachCo( pAbs, pObj, i )
Gia_ObjTerSimCo( pObj );
}
pObj = Gia_ManPo( pAbs, 0 );
if ( Gia_ObjTerSimGet1(pObj) )
{
pCexNew = Gia_ManCexRemap( p, pCex, vPis );
printf( "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
}
else
printf( "CEX is not real.\n" );
Gia_ManForEachObj( pAbs, pObj, i )
Gia_ObjTerSimSetC( pObj );
if ( pCexNew == NULL )
{
// grow one layer
Vec_IntForEachEntry( vPPis, iObjId, i )
{
nOnes++;
assert( i >= Vec_IntSize(vPis) );
iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
if ( Vec_IntEntry( p->vGateClasses, iObjId ) == 1 )
continue;
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
// printf( "Adding object %d.\n", iObjId );
// Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
Counter++;
}
Abc_CexFree( pCare );
if ( fVerbose )
printf( "Essential bits = %d. Additional objects = %d.\n", nOnes, Counter );
// consider the case of SAT
if ( iObjId == -1 )
if ( fVerbose )
{
printf( "Additional objects = %d. ", Vec_IntSize(vPPis) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
}
}
else
{
ABC_FREE( p->pCexSeq );
p->pCexSeq = Gia_ManCexRemap( p, pAbs, pCex, vPis );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Gia_ManStop( pAbs );
return 0;
// minimize the CEX
pAig = Gia_ManToAigSimple( pAbs );
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
Aig_ManStop( pAig );
if ( pCare == NULL )
printf( "Counter-example minimization has failed.\n" );
// add new objects to the map
iObjId = -1;
for ( f = 0; f <= pCare->iFrame; f++ )
for ( i = 0; i < pCare->nPis; i++ )
if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
{
nOnes++;
assert( i >= Vec_IntSize(vPis) );
iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
if ( Vec_IntEntry( p->vGateClasses, iObjId ) == 1 )
continue;
assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
// printf( "Adding object %d.\n", iObjId );
// Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
Counter++;
}
Abc_CexFree( pCare );
if ( fVerbose )
{
printf( "Essential bits = %d. Additional objects = %d. ", nOnes, Counter );
Abc_PrintTime( 1, "Time", clock() - clk );
}
// consider the case of SAT
if ( iObjId == -1 )
{
pCexNew = Gia_ManCexRemap( p, pCex, vPis );
printf( "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
}
}
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Gia_ManStop( pAbs );
if ( pCexNew )
{
ABC_FREE( p->pCexSeq );
p->pCexSeq = pCexNew;
return 0;
}
// extract abstraction to include min-cut
if ( fMinCut )
Nwk_ManDeriveMinCut( p, fVerbose );
@ -294,7 +363,7 @@ Abc_Cex_t * Gla_ManDeriveCex( Gla_Man_t * p, Vec_Int_t * vPis )
/**Function*************************************************************
Synopsis [Collects internal objects in a topo order.]
Synopsis [Collects GIA abstraction objects.]
Description []
@ -303,21 +372,66 @@ Abc_Cex_t * Gla_ManDeriveCex( Gla_Man_t * p, Vec_Int_t * vPis )
SeeAlso []
***********************************************************************/
void Gla_ManRefCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRoAnds, Vec_Int_t * vCos )
int Gla_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pGiaObj, Vec_Int_t * vRoAnds )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
if ( Gia_ObjIsRo(p, pObj) )
int Value0, Value1;
if ( Gia_ObjIsTravIdCurrent(p, pGiaObj) )
return 1;
Gia_ObjSetTravIdCurrent(p, pGiaObj);
if ( Gia_ObjIsCi(pGiaObj) )
return 0;
assert( Gia_ObjIsAnd(pGiaObj) );
Value0 = Gla_ManCollectInternal_rec( p, Gia_ObjFanin0(pGiaObj), vRoAnds );
Value1 = Gla_ManCollectInternal_rec( p, Gia_ObjFanin1(pGiaObj), vRoAnds );
if ( Value0 || Value1 )
{
Vec_IntPush( vRoAnds, Gia_ObjId(p, pObj) );
Vec_IntPush( vCos, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
return;
assert( Gia_ObjIsAnd(pGiaObj) );
Vec_IntPush( vRoAnds, Gia_ObjId(p, pGiaObj) );
}
assert( Gia_ObjIsAnd(pObj) );
Gla_ManRefCollect_rec( p, Gia_ObjFanin0(pObj), vRoAnds, vCos );
Gla_ManRefCollect_rec( p, Gia_ObjFanin1(pObj), vRoAnds, vCos );
Vec_IntPush( vRoAnds, Gia_ObjId(p, pObj) );
return Value0 || Value1;
}
void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vCos, Vec_Int_t * vRoAnds )
{
Gla_Obj_t * pObj, * pFanin;
Gia_Obj_t * pGiaObj;
int i, k;
// collect COs
Vec_IntPush( vCos, Gia_ObjId(p->pGia, Gia_ManPo(p->pGia, 0)) );
// collect fanins of abstracted objects
Gla_ManForEachObjAbs( p, pObj, i )
{
assert( pObj->fConst || pObj->fRo || pObj->fAnd );
if ( pObj->fRo )
{
pGiaObj = Gia_ObjRoToRi( p->pGia, Gia_ManObj(p->pGia, pObj->iGiaObj) );
Vec_IntPush( vCos, Gia_ObjId(p->pGia, pGiaObj) );
}
Gla_ObjForEachFanin( p, pObj, pFanin, k )
if ( !pFanin->fAbs )
Vec_IntPush( (pFanin->fPi ? vPis : vPPis), pFanin->iGiaObj );
}
Vec_IntUniqify( vPis );
Vec_IntUniqify( vPPis );
// mark const/PIs/PPIs
Gia_ManIncrementTravId( p->pGia );
Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pGiaObj, i )
Gia_ObjSetTravIdCurrent( p->pGia, pGiaObj );
Gia_ManForEachObjVec( vPPis, p->pGia, pGiaObj, i )
Gia_ObjSetTravIdCurrent( p->pGia, pGiaObj );
// mark and add ROs first
Gia_ManForEachObjVec( vCos, p->pGia, pGiaObj, i )
{
if ( i == 0 ) continue;
pGiaObj = Gia_ObjRiToRo( p->pGia, pGiaObj );
Gia_ObjSetTravIdCurrent( p->pGia, pGiaObj );
Vec_IntPush( vRoAnds, Gia_ObjId(p->pGia, pGiaObj) );
}
// collect nodes between PIs/PPIs/ROs and COs
Gia_ManForEachObjVec( vCos, p->pGia, pGiaObj, i )
Gla_ManCollectInternal_rec( p->pGia, Gia_ObjFanin0(pGiaObj), vRoAnds );
}
/**Function*************************************************************
@ -331,14 +445,16 @@ void Gla_ManRefCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRoAnds
SeeAlso []
***********************************************************************/
void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vRes )
void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vRes, int Sign )
{
Rfn_Obj_t * pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );
assert( (int)pRef->Sign == Sign );
if ( pRef->fVisit )
return;
pRef->fVisit = 1;
if ( pRef->fPPi )
{
assert( (int)pRef->Prio > 0 );
assert( (int)pRef->Prio < Vec_IntSize(p->vPrioSels) );
if ( Vec_IntEntry( p->vPrioSels, pRef->Prio ) == 0 ) // not selected yet
{
@ -352,43 +468,48 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( f > 0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vRes );
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vRes, Sign );
return;
}
assert( Gia_ObjIsAnd(pObj) );
if ( pRef->Value == 1 )
{
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes );
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes );
}
else // select one value
if ( Gia_ObjIsAnd(pObj) )
{
Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
int fSel0 = Vec_IntEntry( p->vPrioSels, pRef0->Prio );
int fSel1 = Vec_IntEntry( p->vPrioSels, pRef1->Prio );
if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
if ( pRef->Value == 1 )
{
if ( !fSel0 && !fSel1 )
// if ( !fSel0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
// if ( !fSel1 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
}
else // select one value
{
if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
{
if ( pRef0->Prio <= pRef1->Prio ) // choice
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes );
else
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes );
// if ( !fSel0 && !fSel1 )
{
if ( pRef0->Prio <= pRef1->Prio ) // choice
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
else
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
}
}
}
else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
{
if ( !fSel0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes );
}
else
{
if ( !fSel1 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes );
else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
{
// if ( !fSel0 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
}
else if ( (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
{
// if ( !fSel1 )
Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
}
else assert( 0 );
}
}
else assert( 0 );
}
/**Function*************************************************************
@ -404,38 +525,40 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
***********************************************************************/
Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
{
int fVerify = 0;
Vec_Int_t * vPis, * vPPis, * vRoAnds, * vCos, * vRes = NULL;
int fVerify = 1;
static int Sign = 0;
Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vRes = NULL;
Rfn_Obj_t * pRef, * pRef0, * pRef1;
Gia_Obj_t * pObj;
Gla_Obj_t * pGla;
// Gla_Obj_t * pGla;
int i, f;
Sign++;
// compute PIs and pseudo-PIs
vPis = Vec_IntAlloc( 100 );
vPPis = Gla_ManCollectPPis( p, vPis );
// remap into GIA
vCos = Vec_IntAlloc( 1000 );
vPis = Vec_IntAlloc( 1000 );
vPPis = Vec_IntAlloc( 1000 );
vRoAnds = Vec_IntAlloc( 1000 );
Gla_ManCollect( p, vPis, vPPis, vCos, vRoAnds );
/*
// check how many pseudo PIs have variables
Gla_ManForEachObjAbsVec( vPis, p, pGla, i )
Vec_IntWriteEntry( vPis, i, pGla->iGiaObj );
{
printf( " %5d : ", Gla_ObjId(p, pGla) );
for ( f = 0; f <= p->pPars->iFrame; f++ )
printf( "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) );
printf( "\n" );
}
// check how many pseudo PIs have variables
Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
Vec_IntWriteEntry( vPPis, i, pGla->iGiaObj );
// prepare boundary objects
Gia_ManIncrementTravId( p->pGia );
Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
Gia_ObjSetTravIdCurrent( p->pGia, pObj );
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
Gia_ObjSetTravIdCurrent( p->pGia, pObj );
// collect internal objects
vCos = Vec_IntAlloc( 1000 );
vRoAnds = Vec_IntAlloc( 1000 );
Vec_IntPush( vCos, Gia_ObjId(p->pGia, Gia_ManPo(p->pGia, 0)) );
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
Gla_ManRefCollect_rec( p->pGia, Gia_ObjFanin0(pObj), vRoAnds, vCos );
{
printf( "%5d : ", Gla_ObjId(p, pGla) );
for ( f = 0; f <= p->pPars->iFrame; f++ )
printf( "%d", Gla_ManCheckVar(p, Gla_ObjId(p, pGla), f) );
printf( "\n" );
}
*/
// propagate values
for ( f = 0; f <= p->pPars->iFrame; f++ )
{
@ -443,25 +566,43 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef = Gla_ObjRef( p, 0, f ); Gla_ObjClearRef( pRef );
pRef->Value = 0;
pRef->Prio = 0;
pRef->Sign = Sign;
// primary input
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
{
assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
pRef->Prio = 0;
pRef->Sign = Sign;
assert( pRef->fVisit == 0 );
}
// primary input
Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
{
int ObjId = Gia_ObjId(p->pGia, pObj);
if ( 1308 == Gia_ObjId(p->pGia, pObj) )
{
int s = 0;
}
assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
pRef->Prio = i+1;
pRef->fPPi = 1;
pRef->Sign = Sign;
assert( pRef->fVisit == 0 );
}
// internal nodes
Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
{
if ( 1598 == Gia_ObjId(p->pGia, pObj) )
{
int s = 0;
}
assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f ); Gla_ObjClearRef( pRef );
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
@ -469,12 +610,21 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
{
pRef->Value = 0;
pRef->Prio = 0;
pRef->Sign = Sign;
}
else
{
pRef0 = Gla_ObjRef( p, Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj)), f-1 );
pRef->Value = pRef0->Value;
pRef->Prio = pRef0->Prio;
pRef->Sign = Sign;
if ( (int)pRef->Value != Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
{
Gla_Obj_t * pGla = Gla_ManObj(p, p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj))]);
int s = 0;
}
}
continue;
}
@ -482,8 +632,54 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj));
// if ( p->pCnf->pObj2Count[Gia_ObjId(p->pGia, pObj)] >= 0 )
// assert( (int)pRef->Value == Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) );
if ( p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] != ~0 && Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) )
{
Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj);
Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj);
int iff = Gia_ObjId(p->pGia, pFan1);
// assert( (int)pRef->Value == Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) );
if ( (int)pRef->Value != Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
{
Gia_Obj_t * pFanin0 = Gia_ObjFanin0(pObj);
Gia_Obj_t * pFanin1 = Gia_ObjFanin1(pObj);
int id = Gia_ObjId(p->pGia, pObj);
int v = p->pObj2Obj[Gia_ObjId(p->pGia, pObj)];
int v1 = p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjFanin0(pObj))];
int v2 = p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjFanin1(pObj))];
int c = Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f);
// int c1 = Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjFanin0(pObj))], f);
// int c2 = Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, Gia_ObjFanin1(pObj))], f);
int Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj) , f );
// int Value1 = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, Gia_ObjFanin0(pObj)), f );
// int Value2 = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, Gia_ObjFanin1(pObj)), f );
Gla_Obj_t * pGla= Gla_ManObj( p, v );
Gla_Obj_t * pFanin;
int j;
Gla_ObjForEachFanin( p, pGla, pFanin, j )
{
Rfn_Obj_t * pRef3 = Gla_ObjRef( p, pFanin->iGiaObj, f );
int c = Gla_ManCheckVar(p, p->pObj2Obj[pFanin->iGiaObj], f);
Gia_ObjPrint( p->pGia, Gia_ManObj(p->pGia, pFanin->iGiaObj) );
if ( (int)pRef3->Value != Gla_ObjSatValue( p, pFanin->iGiaObj, f ) )
{
int s = 0;
}
}
printf( "Object has value mismatch " );
Gia_ObjPrint( p->pGia, pObj );
}
}
if ( pRef->Value == 1 )
pRef->Prio = Abc_MaxInt( pRef0->Prio, pRef1->Prio );
else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
@ -492,6 +688,8 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef->Prio = pRef0->Prio;
else
pRef->Prio = pRef1->Prio;
assert( pRef->fVisit == 0 );
pRef->Sign = Sign;
}
// output nodes
Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
@ -500,6 +698,8 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj));
pRef->Prio = pRef0->Prio;
assert( pRef->fVisit == 0 );
pRef->Sign = Sign;
}
}
// make sure the output value is 1
@ -521,7 +721,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
// select objects
vRes = Vec_IntAlloc( 100 );
Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vRes );
Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vRes, Sign );
if ( fVerify )
{
@ -560,7 +760,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
}
pObj = Gia_ManPo( p->pGia, 0 );
if ( !Gia_ObjTerSimGet1(pObj) )
printf( "Refinement verification has failed!!!" );
printf( "Refinement verification has failed!!!\n" );
// clear
Gia_ObjTerSimSetC( Gia_ManConst0(p->pGia) );
Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
@ -1081,6 +1281,10 @@ 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 ( 4786 == iObj && iFrame == 2 )
{
int s = 0;
}
if ( pGlaObj->fConst )
{
iVar = Gla_ManGetVar( p, iObj, iFrame );

183
src/aig/gia/giaDup.c
View File

@ -1662,6 +1662,83 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
return pNew;
}
/**Function*************************************************************
Synopsis [Returns the array of neighbors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned;
Gia_Obj_t * pObj;
int i, Entry;
vAssigned = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( vGateClasses, Entry, i )
{
if ( Entry == 0 )
continue;
assert( Entry == 1 );
pObj = Gia_ManObj( p, i );
Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, pObj) );
Vec_IntPush( vAssigned, Gia_ObjFaninId1p(p, pObj) );
}
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)) );
else assert( Gia_ObjIsConst0(pObj) );
}
Vec_IntUniqify( vAssigned );
return vAssigned;
}
/**Function*************************************************************
Synopsis [Collects PIs and PPIs of the abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes )
{
Vec_Int_t * vAssigned;
Gia_Obj_t * pObj;
int i;
assert( Gia_ManPoNum(p) == 1 );
assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
// create included objects and their fanins
vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
// create additional arrays
if ( pvPis ) *pvPis = Vec_IntAlloc( 100 );
if ( pvPPis ) *pvPPis = Vec_IntAlloc( 100 );
if ( pvFlops ) *pvFlops = Vec_IntAlloc( 100 );
if ( pvNodes ) *pvNodes = Vec_IntAlloc( 1000 );
Gia_ManForEachObjVec( vAssigned, p, pObj, i )
{
if ( Gia_ObjIsPi(p, pObj) )
{ if ( pvPis ) Vec_IntPush( *pvPis, Gia_ObjId(p,pObj) ); }
else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
{ if ( pvPPis ) Vec_IntPush( *pvPPis, Gia_ObjId(p,pObj) ); }
else if ( Gia_ObjIsRo(p, pObj) )
{ if ( pvFlops ) Vec_IntPush( *pvFlops, Gia_ObjId(p,pObj) ); }
else if ( Gia_ObjIsAnd(pObj) )
{ if ( pvNodes ) Vec_IntPush( *pvNodes, Gia_ObjId(p,pObj) ); }
else assert( Gia_ObjIsConst0(pObj) );
}
Vec_IntFree( vAssigned );
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
@ -1697,33 +1774,15 @@ void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
***********************************************************************/
Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pCopy;
int i;//, nFlops = 0;
assert( Gia_ManPoNum(p) == 1 );
assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
// create included objects and their fanins
vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
// create additional arrays
vPis = Vec_IntAlloc( 1000 );
vPPis = Vec_IntAlloc( 1000 );
vFlops = Vec_IntAlloc( 1000 );
vNodes = Vec_IntAlloc( 1000 );
Gia_ManForEachObjVec( vAssigned, p, pObj, i )
{
if ( Gia_ObjIsPi(p, pObj) )
Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
else if ( Gia_ObjIsAnd(pObj) )
Vec_IntPush( vNodes, Gia_ObjId(p,pObj) );
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vFlops, Gia_ObjId(p,pObj) );
else assert( Gia_ObjIsConst0(pObj) );
}
Gia_ManGlaCollect( p, vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
// start the new manager
pNew = Gia_ManStart( 5000 );
@ -1779,93 +1838,9 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );
Vec_IntFree( vNodes );
Vec_IntFree( vAssigned );
return pNew;
}
/**Function*************************************************************
Synopsis [Collects PIs and PPIs of the abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis )
{
Vec_Int_t * vAssigned, * vPis, * vPPis;
Gia_Obj_t * pObj;
int i;
assert( Gia_ManPoNum(p) == 1 );
assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
// create included objects and their fanins
vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
// create additional arrays
vPis = Vec_IntAlloc( 1000 );
vPPis = Vec_IntAlloc( 1000 );
Gia_ManForEachObjVec( vAssigned, p, pObj, i )
{
if ( Gia_ObjIsPi(p, pObj) )
Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
else if ( Gia_ObjIsAnd(pObj) )
{}
else if ( Gia_ObjIsRo(p, pObj) )
{}
else assert( Gia_ObjIsConst0(pObj) );
}
Vec_IntFree( vAssigned );
if ( pvPis )
*pvPis = vPis;
else
Vec_IntFree( vPis );
if ( pvPPis )
*pvPPis = vPPis;
else
Vec_IntFree( vPPis );
}
/**Function*************************************************************
Synopsis [Returns the array of neighbors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned;
Gia_Obj_t * pObj;
int i, Entry;
vAssigned = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( vGateClasses, Entry, i )
{
if ( Entry == 0 )
continue;
assert( Entry == 1 );
pObj = Gia_ManObj( p, i );
Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, pObj) );
Vec_IntPush( vAssigned, Gia_ObjFaninId1p(p, pObj) );
}
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)) );
else assert( Gia_ObjIsConst0(pObj) );
}
Vec_IntUniqify( vAssigned );
return vAssigned;
}
/**Function*************************************************************
Synopsis [Copy an AIG structure related to the selected POs.]

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

@ -200,10 +200,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
***********************************************************************/
void Gia_ManPrintGateClasses( Gia_Man_t * p )
{
Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
Gia_Obj_t * pObj;
int i;
Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes;
if ( p->vGateClasses == NULL )
return;
if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
@ -211,38 +208,16 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p )
printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" );
return;
}
// create included objects and their fanins
vAssigned = Gia_GlaCollectAssigned( p, p->vGateClasses );
// create additional arrays
vPis = Vec_IntAlloc( 1000 );
vPPis = Vec_IntAlloc( 1000 );
vFlops = Vec_IntAlloc( 1000 );
vNodes = Vec_IntAlloc( 1000 );
Gia_ManForEachObjVec( vAssigned, p, pObj, i )
{
if ( Gia_ObjIsPi(p, pObj) )
Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
else if ( !Vec_IntEntry(p->vGateClasses, Gia_ObjId(p,pObj)) )
Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
else if ( Gia_ObjIsAnd(pObj) )
Vec_IntPush( vNodes, Gia_ObjId(p,pObj) );
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vFlops, Gia_ObjId(p,pObj) );
else assert( Gia_ObjIsConst0(pObj) );
}
Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes );
printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%)\n",
Vec_IntSize(vPis), Vec_IntSize(vPPis),
Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1),
Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1) );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );
Vec_IntFree( vNodes );
Vec_IntFree( vAssigned );
}
/**Function*************************************************************

2
src/opt/nwk/nwkAig.c
View File

@ -219,7 +219,7 @@ void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose )
Gia_Obj_t * pObj;
int i, iObjId;
// get inputs
Gia_GlaCollectInputs( p, p->vGateClasses, NULL, &vPPis );
Gia_ManGlaCollect( p, p->vGateClasses, NULL, &vPPis, NULL, NULL );
// collect nodes rechable from PPIs
vNodes = Vec_IntAlloc( 100 );
vLeaves = Vec_IntAlloc( 100 );