diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 3 | ||||
-rw-r--r-- | src/aig/gia/giaAbsGla.c | 412 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 183 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 29 |
4 files changed, 390 insertions, 237 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e24ecd26..606a4540 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -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 ); diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index a9ac56b6..16c37e0e 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -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 ( !fSel0 && !fSel1 ) - { - 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 ); - } - } - else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 ) + if ( pRef->Value == 1 ) { - if ( !fSel0 ) - Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes ); +// 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 + else // select one value { - if ( !fSel1 ) - Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes ); + if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) + { +// 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, 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 ); - 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" ); + } + // check how many pseudo PIs have variables + Gla_ManForEachObjAbsVec( vPPis, p, pGla, i ) + { + 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 ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index a5c246cb..cba90721 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1664,6 +1664,83 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) /**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.] Description [] @@ -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,95 +1838,11 @@ 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.] Description [] diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 385f43d9..979bbe38 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -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************************************************************* |