From 7d29663720b02b02ceaae5b75fb8fe05ba4aae73 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Oct 2012 18:25:41 -0700 Subject: Fixed several important problems in choice computation (command 'dch'). --- src/aig/gia/gia.h | 2 +- src/aig/gia/giaChoice.c | 362 +++----------- src/aig/gia/giaUtil.c | 91 ---- src/proof/cec/cecCorr_updated.c | 1028 --------------------------------------- src/proof/dch/dchChoice.c | 412 ++++++++-------- src/proof/dch/dchCore.c | 8 +- 6 files changed, 284 insertions(+), 1619 deletions(-) delete mode 100644 src/proof/cec/cecCorr_updated.c (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e9e714ad..0c98e94d 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -703,6 +703,7 @@ extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, i /*=== giaChoice.c ============================================================*/ extern void Gia_ManVerifyChoices( Gia_Man_t * p ); extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ); +extern int Gia_ManHasChoices( Gia_Man_t * p ); /*=== giaCsatOld.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCsat.c ============================================================*/ @@ -914,7 +915,6 @@ extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode ); extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 ); extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); -extern int Gia_ManHasChoices( Gia_Man_t * p ); extern int Gia_ManHasDangling( Gia_Man_t * p ); extern int Gia_ManMarkDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); diff --git a/src/aig/gia/giaChoice.c b/src/aig/gia/giaChoice.c index 373f9104..a1d9e325 100644 --- a/src/aig/gia/giaChoice.c +++ b/src/aig/gia/giaChoice.c @@ -51,28 +51,7 @@ void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ) // collect classes vCollected = Vec_IntAlloc( 100 ); Gia_ManForEachClass( p, iRepr ) - { Vec_IntPush( vCollected, iRepr ); -/* - // check classes - if ( !fNowIncreasing ) - { - iPrev = iRepr; - Gia_ClassForEachObj1( p, iRepr, iNode ) - { - if ( iPrev < iNode ) - { - printf( "Class %d : ", iRepr ); - Gia_ClassForEachObj( p, iRepr, iNode ) - printf( " %d", iNode ); - printf( "\n" ); - break; - } - iPrev = iNode; - } - } -*/ - } // correct each class vClass = Vec_IntAlloc( 100 ); Vec_IntForEachEntry( vCollected, iRepr, i ) @@ -83,14 +62,12 @@ void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing ) { if ( fNowIncreasing ) assert( iRepr < iNode ); -// else -// assert( iRepr > iNode ); + else + assert( iRepr > iNode ); Vec_IntPush( vClass, iNode ); } - if ( !fNowIncreasing ) - Vec_IntSort( vClass, 1 ); -// if ( iRepr == 129720 || iRepr == 129737 ) -// Vec_IntPrint( vClass ); +// if ( !fNowIncreasing ) +// Vec_IntSort( vClass, 1 ); // reverse the class iPrev = 0; iRepr = Vec_IntEntryLast( vClass ); @@ -192,9 +169,10 @@ void Gia_ManCheckReprs( Gia_Man_t * p ) printf( "GIA \"%s\": Representive verification successful.\n", Gia_ManName(p) ); } + /**Function************************************************************* - Synopsis [Find minimum level of each node using representatives.] + Synopsis [Returns 1 if AIG has choices.] Description [] @@ -203,290 +181,84 @@ void Gia_ManCheckReprs( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Gia_ManMinLevelRepr_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +int Gia_ManHasChoices( Gia_Man_t * p ) { - int levMin, levCur, objId, reprId; - // skip visited nodes - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) - return Gia_ObjLevel(p, pObj); - Gia_ObjSetTravIdCurrent(p, pObj); - // skip CI nodes - if ( Gia_ObjIsCi(pObj) ) - return Gia_ObjLevel(p, pObj); - assert( Gia_ObjIsAnd(pObj) ); - objId = Gia_ObjId(p, pObj); - if ( Gia_ObjIsNone(p, objId) ) + Gia_Obj_t * pObj; + int i, Counter1 = 0, Counter2 = 0; + int nFailNoRepr = 0; + int nFailHaveRepr = 0; + int nChoiceNodes = 0; + int nChoices = 0; + if ( p->pReprs == NULL || p->pNexts == NULL ) + return 0; + // check if there are any representatives + Gia_ManForEachObj( p, pObj, i ) { - // not part of the equivalence class - Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin0(pObj) ); - Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin1(pObj) ); - Gia_ObjSetAndLevel( p, pObj ); - return Gia_ObjLevel(p, pObj); + if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) + { +// printf( "%d ", i ); + Counter1++; + } +// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) +// Counter2++; } - // has equivalences defined - assert( Gia_ObjHasRepr(p, objId) || Gia_ObjIsHead(p, objId) ); - reprId = Gia_ObjHasRepr(p, objId) ? Gia_ObjRepr(p, objId) : objId; - // iterate through objects - levMin = ABC_INFINITY; - Gia_ClassForEachObj( p, reprId, objId ) +// printf( "\n" ); + Gia_ManForEachObj( p, pObj, i ) { - levCur = Gia_ManMinLevelRepr_rec( p, Gia_ManObj(p, objId) ); - levMin = Abc_MinInt( levMin, levCur ); +// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) +// Counter1++; + if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) + { +// printf( "%d ", i ); + Counter2++; + } } - assert( levMin < ABC_INFINITY ); - // assign minimum level to all - Gia_ClassForEachObj( p, reprId, objId ) - Gia_ObjSetLevelId( p, objId, levMin ); - return levMin; -} -int Gia_ManMinLevelRepr( Gia_Man_t * p ) -{ - Gia_Obj_t * pObj; - int i, LevelCur, LevelMax = 0; - assert( Gia_ManRegNum(p) == 0 ); - Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); - Gia_ManIncrementTravId( p ); - Gia_ManForEachAnd( p, pObj, i ) +// printf( "\n" ); + if ( Counter1 == 0 ) { - assert( !Gia_ObjIsConst(p, i) ); - LevelCur = Gia_ManMinLevelRepr_rec( p, pObj ); - LevelMax = Abc_MaxInt( LevelMax, LevelCur ); + printf( "Warning: AIG has repr data-strucure but not reprs.\n" ); + return 0; } - printf( "Max level %d\n", LevelMax ); - return LevelMax; -} - -/**Function************************************************************* - - Synopsis [Returns mapping of each old repr into new repr.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int * Gia_ManFindMinLevelMap( Gia_Man_t * p ) -{ - Gia_Obj_t * pObj; - int reprId, objId, levFan0, levFan1; - int levMin, levMinOld, levMax, reprBest; - int * pReprMap, * pMinLevels, iFanin; - int i, fChange = 1; - - Gia_ManLevelNum( p ); - pMinLevels = ABC_ALLOC( int, Gia_ManObjNum(p) ); - while ( fChange ) + printf( "%d nodes have reprs.\n", Counter1 ); + printf( "%d nodes have nexts.\n", Counter2 ); + // check if there are any internal nodes without fanout + // make sure all nodes without fanout have representatives + // make sure all nodes with fanout have no representatives + ABC_FREE( p->pRefs ); + Gia_ManCreateRefs( p ); + Gia_ManForEachAnd( p, pObj, i ) { - fChange = 0; - // clean min-levels - memset( pMinLevels, 0xFF, sizeof(int) * Gia_ManObjNum(p) ); - // for each class find min level - Gia_ManForEachClass( p, reprId ) + if ( Gia_ObjRefs(p, pObj) == 0 ) { - levMin = ABC_INFINITY; - Gia_ClassForEachObj( p, reprId, objId ) - levMin = Abc_MinInt( levMin, Gia_ObjLevelId(p, objId) ); - assert( levMin >= 0 && levMin < ABC_INFINITY ); - Gia_ClassForEachObj( p, reprId, objId ) - { - assert( pMinLevels[objId] == -1 ); - pMinLevels[objId] = levMin; - } + if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL ) + nFailNoRepr++; + else + nChoices++; } - // recompute levels - levMax = 0; - Gia_ManForEachAnd( p, pObj, i ) + else { - iFanin = Gia_ObjFaninId0(pObj, i); - if ( Gia_ObjIsNone(p, iFanin) ) - levFan0 = Gia_ObjLevelId(p, iFanin); - else if ( Gia_ObjIsConst(p, iFanin) ) - levFan0 = 0; - else - { - assert( Gia_ObjIsClass( p, iFanin ) ); - assert( pMinLevels[iFanin] >= 0 ); - levFan0 = pMinLevels[iFanin]; - } - - iFanin = Gia_ObjFaninId1(pObj, i); - if ( Gia_ObjIsNone(p, iFanin) ) - levFan1 = Gia_ObjLevelId(p, iFanin); - else if ( Gia_ObjIsConst(p, iFanin) ) - levFan1 = 0; - else - { - assert( Gia_ObjIsClass( p, iFanin ) ); - assert( pMinLevels[iFanin] >= 0 ); - levFan1 = pMinLevels[iFanin]; - } - levMinOld = Gia_ObjLevelId(p, i); - levMin = 1 + Abc_MaxInt( levFan0, levFan1 ); - Gia_ObjSetLevelId( p, i, levMin ); - assert( levMin <= levMinOld ); - if ( levMin < levMinOld ) - fChange = 1; - levMax = Abc_MaxInt( levMax, levMin ); + if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL ) + nFailHaveRepr++; + if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL ) + nChoiceNodes++; } - printf( "%d ", levMax ); - } - ABC_FREE( pMinLevels ); - printf( "\n" ); - - // create repr map - pReprMap = ABC_FALLOC( int, Gia_ManObjNum(p) ); - Gia_ManForEachAnd( p, pObj, i ) - if ( Gia_ObjIsConst(p, i) ) - pReprMap[i] = 0; - Gia_ManForEachClass( p, reprId ) - { - // find min-level repr - reprBest = -1; - levMin = ABC_INFINITY; - Gia_ClassForEachObj( p, reprId, objId ) - if ( levMin > Gia_ObjLevelId(p, objId) ) - { - levMin = Gia_ObjLevelId(p, objId); - reprBest = objId; - } - assert( reprBest > 0 ); - Gia_ClassForEachObj( p, reprId, objId ) - pReprMap[objId] = reprBest; + if ( Gia_ObjReprObj( p, i ) ) + assert( Gia_ObjRepr(p, i) < i ); } - return pReprMap; -} - - - -/**Function************************************************************* - - Synopsis [Find terminal AND nodes] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_ManDanglingAndNodes( Gia_Man_t * p ) -{ - Vec_Int_t * vTerms; - Gia_Obj_t * pObj; - int i; - Gia_ManCleanMark0( p ); - Gia_ManForEachAnd( p, pObj, i ) + if ( nChoices == 0 ) + return 0; + if ( nFailNoRepr ) { - Gia_ObjFanin0(pObj)->fMark0 = 1; - Gia_ObjFanin1(pObj)->fMark1 = 1; + printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr ); +// return 0; } - vTerms = Vec_IntAlloc( 1000 ); - Gia_ManForEachAnd( p, pObj, i ) - if ( !pObj->fMark0 ) - Vec_IntPush( vTerms, i ); - Gia_ManCleanMark0( p ); - return vTerms; -} - -/**Function************************************************************* - - Synopsis [Reconstruct AIG starting with terminals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManRebuidRepr_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprMap ) -{ - int objId, reprLit = -1; - if ( ~pObj->Value ) - return pObj->Value; - assert( Gia_ObjIsAnd(pObj) ); - objId = Gia_ObjId( p, pObj ); - if ( Gia_ObjIsClass(p, objId) ) + if ( nFailHaveRepr ) { - assert( pReprMap[objId] > 0 ); - reprLit = Gia_ManRebuidRepr_rec( pNew, p, Gia_ManObj(p, pReprMap[objId]), pReprMap ); - assert( reprLit > 1 ); + printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr ); +// return 0; } - else - assert( Gia_ObjIsNone(p, objId) ); - Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin0(pObj), pReprMap ); - Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin1(pObj), pReprMap ); - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - assert( reprLit != (int)pObj->Value ); - if ( reprLit > 1 ) - pNew->pReprs[ Abc_Lit2Var(pObj->Value) ].iRepr = Abc_Lit2Var(reprLit); - return pObj->Value; -} -Gia_Man_t * Gia_ManRebuidRepr( Gia_Man_t * p, int * pReprMap ) -{ - Vec_Int_t * vTerms; - Gia_Man_t * pNew; - Gia_Obj_t * pObj; - int i; - Gia_ManFillValue( p ); - pNew = Gia_ManStart( Gia_ManObjNum(p) ); - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachCi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); - vTerms = Gia_ManDanglingAndNodes( p ); - Gia_ManForEachObjVec( vTerms, p, pObj, i ) - Gia_ManRebuidRepr_rec( pNew, p, pObj, pReprMap ); - Vec_IntFree( vTerms ); - Gia_ManForEachCo( p, pObj, i ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Gia_ManNormalizeChoices( Aig_Man_t * pAig ) -{ - int * pReprMap; - Aig_Man_t * pNew; - Gia_Man_t * pGia, * pTemp; - // create GIA with representatives - assert( Aig_ManRegNum(pAig) == 0 ); - assert( pAig->pReprs != NULL ); - pGia = Gia_ManFromAigSimple( pAig ); - Gia_ManReprFromAigRepr2( pAig, pGia ); - // verify that representatives are correct - Gia_ManCheckReprs( pGia ); - // find min-level repr for each class - pReprMap = Gia_ManFindMinLevelMap( pGia ); - // reconstruct using correct order - pGia = Gia_ManRebuidRepr( pTemp = pGia, pReprMap ); - Gia_ManStop( pTemp ); - ABC_FREE( pReprMap ); - // create choices - - // verify that choices are correct -// Gia_ManVerifyChoices( pGia ); - // copy the result back into AIG - pNew = Gia_ManToAigSimple( pGia ); - Gia_ManReprToAigRepr( pNew, pGia ); - return pNew; -} -void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig ) -{ - Aig_Man_t * pNew = Gia_ManNormalizeChoices( pAig ); - Aig_ManStop( pNew ); +// printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices ); + return 1; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 5f443dc8..e4a4dd09 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -888,97 +888,6 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ) return ConeSize1; } -/**Function************************************************************* - - Synopsis [Returns 1 if AIG has choices.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManHasChoices( Gia_Man_t * p ) -{ - Gia_Obj_t * pObj; - int i, Counter1 = 0, Counter2 = 0; - int nFailNoRepr = 0; - int nFailHaveRepr = 0; - int nChoiceNodes = 0; - int nChoices = 0; - if ( p->pReprs == NULL || p->pNexts == NULL ) - return 0; - // check if there are any representatives - Gia_ManForEachObj( p, pObj, i ) - { - if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) - { -// printf( "%d ", i ); - Counter1++; - } -// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) -// Counter2++; - } -// printf( "\n" ); - Gia_ManForEachObj( p, pObj, i ) - { -// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) -// Counter1++; - if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) - { -// printf( "%d ", i ); - Counter2++; - } - } -// printf( "\n" ); - if ( Counter1 == 0 ) - { - printf( "Warning: AIG has repr data-strucure but not reprs.\n" ); - return 0; - } - printf( "%d nodes have reprs.\n", Counter1 ); - printf( "%d nodes have nexts.\n", Counter2 ); - // check if there are any internal nodes without fanout - // make sure all nodes without fanout have representatives - // make sure all nodes with fanout have no representatives - ABC_FREE( p->pRefs ); - Gia_ManCreateRefs( p ); - Gia_ManForEachAnd( p, pObj, i ) - { - if ( Gia_ObjRefs(p, pObj) == 0 ) - { - if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL ) - nFailNoRepr++; - else - nChoices++; - } - else - { - if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL ) - nFailHaveRepr++; - if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL ) - nChoiceNodes++; - } - if ( Gia_ObjReprObj( p, i ) ) - assert( Gia_ObjRepr(p, i) < i ); - } - if ( nChoices == 0 ) - return 0; - if ( nFailNoRepr ) - { - printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr ); -// return 0; - } - if ( nFailHaveRepr ) - { - printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr ); -// return 0; - } -// printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices ); - return 1; -} - /**Function************************************************************* Synopsis [Returns 1 if AIG has dangling nodes.] diff --git a/src/proof/cec/cecCorr_updated.c b/src/proof/cec/cecCorr_updated.c deleted file mode 100644 index 0d441629..00000000 --- a/src/proof/cec/cecCorr_updated.c +++ /dev/null @@ -1,1028 +0,0 @@ -/**CFile**************************************************************** - - FileName [cecCorr.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Combinational equivalence checking.] - - Synopsis [Latch/signal correspondence computation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: cecCorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cecInt.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Computes the real value of the literal w/o spec reduction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) -{ - if ( Gia_ObjIsAnd(pObj) ) - { - Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix ); - Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix ); - return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) ); - } - if ( f == 0 ) - { - assert( Gia_ObjIsRo(p, pObj) ); - return Gia_ObjCopyF(p, f, pObj); - } - assert( f && Gia_ObjIsRo(p, pObj) ); - pObj = Gia_ObjRoToRi( p, pObj ); - Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix ); - return Gia_ObjFanin0CopyF( p, f-1, pObj ); -} - -/**Function************************************************************* - - Synopsis [Recursively performs speculative reduction for the object.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix ) -{ - Gia_Obj_t * pRepr; - int iLitNew; - if ( ~Gia_ObjCopyF(p, f, pObj) ) - return; - if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) - { - Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix ); - iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); - Gia_ObjSetCopyF( p, f, pObj, iLitNew ); - return; - } - assert( Gia_ObjIsCand(pObj) ); - iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); - Gia_ObjSetCopyF( p, f, pObj, iLitNew ); -} - -/**Function************************************************************* - - Synopsis [Derives SRM for signal correspondence.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) -{ - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pRepr; - Vec_Int_t * vXorLits; - int f, i, iPrev, iObj, iPrevNew, iObjNew; - assert( nFrames > 0 ); - assert( Gia_ManRegNum(p) > 0 ); - assert( p->pReprs != NULL ); - p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) ); - Gia_ManSetPhase( p ); - pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); - Gia_ManHashAlloc( pNew ); - Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 ); - Gia_ManForEachRo( p, pObj, i ) - Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) ); - Gia_ManForEachRo( p, pObj, i ) - if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) - Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) ); - for ( f = 0; f < nFrames+fScorr; f++ ) - { - Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); - Gia_ManForEachPi( p, pObj, i ) - Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); - } - *pvOutputs = Vec_IntAlloc( 1000 ); - vXorLits = Vec_IntAlloc( 1000 ); - if ( fRings ) - { - Gia_ManForEachObj1( p, pObj, i ) - { - if ( Gia_ObjIsConst( p, i ) ) - { - iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); - iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ); - if ( iObjNew != 0 ) - { - Vec_IntPush( *pvOutputs, 0 ); - Vec_IntPush( *pvOutputs, i ); - Vec_IntPush( vXorLits, iObjNew ); - } - } - else if ( Gia_ObjIsHead( p, i ) ) - { - iPrev = i; - Gia_ClassForEachObj1( p, i, iObj ) - { - iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); - iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); - iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); - if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) - { - Vec_IntPush( *pvOutputs, iPrev ); - Vec_IntPush( *pvOutputs, iObj ); - Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) ); - } - iPrev = iObj; - } - iObj = i; - iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 ); - iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) ); - iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) ); - if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 ) - { - Vec_IntPush( *pvOutputs, iPrev ); - Vec_IntPush( *pvOutputs, iObj ); - Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) ); - } - } - } - } - else - { - Gia_ManForEachObj1( p, pObj, i ) - { - pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); - if ( pRepr == NULL ) - continue; - iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 ); - iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); - if ( iPrevNew != iObjNew ) - { - Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); - Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); - Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); - } - } - } - Vec_IntForEachEntry( vXorLits, iObjNew, i ) - Gia_ManAppendCo( pNew, iObjNew ); - Vec_IntFree( vXorLits ); - Gia_ManHashStop( pNew ); - ABC_FREE( p->pCopies ); -//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); - pNew = Gia_ManCleanup( pTemp = pNew ); -//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); - Gia_ManStop( pTemp ); - return pNew; -} - - -/**Function************************************************************* - - Synopsis [Derives SRM for signal correspondence.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings ) -{ - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pRepr; - Vec_Int_t * vXorLits; - int f, i, iPrevNew, iObjNew; - assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix ); - assert( Gia_ManRegNum(p) > 0 ); - assert( p->pReprs != NULL ); - p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) ); - Gia_ManSetPhase( p ); - pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); - Gia_ManHashAlloc( pNew ); - Gia_ManForEachRo( p, pObj, i ) - { - Gia_ManAppendCi(pNew); - Gia_ObjSetCopyF( p, 0, pObj, 0 ); - } - for ( f = 0; f < nFrames+nPrefix+fScorr; f++ ) - { - Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); - Gia_ManForEachPi( p, pObj, i ) - Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) ); - } - *pvOutputs = Vec_IntAlloc( 1000 ); - vXorLits = Vec_IntAlloc( 1000 ); - for ( f = nPrefix; f < nFrames+nPrefix; f++ ) - { - Gia_ManForEachObj1( p, pObj, i ) - { - pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); - if ( pRepr == NULL ) - continue; - iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix ); - iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix ); - iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); - if ( iPrevNew != iObjNew ) - { - Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) ); - Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) ); - Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) ); - } - } - } - Vec_IntForEachEntry( vXorLits, iObjNew, i ) - Gia_ManAppendCo( pNew, iObjNew ); - Vec_IntFree( vXorLits ); - Gia_ManHashStop( pNew ); - ABC_FREE( p->pCopies ); -//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) ); - pNew = Gia_ManCleanup( pTemp = pNew ); -//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) ); - Gia_ManStop( pTemp ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Initializes simulation info for lcorr/scorr counter-examples.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops, int * pInitState ) -{ - unsigned * pInfo; - int k, w, nWords; - nWords = Vec_PtrReadWordsSimInfo( vInfo ); - assert( nFlops <= Vec_PtrSize(vInfo) ); - for ( k = 0; k < nFlops; k++ ) - { - pInfo = Vec_PtrEntry( vInfo, k ); - if ( pInitState && Gia_InfoHasBit(pInitState, k) ) - { - for ( w = 0; w < nWords; w++ ) - pInfo[w] = ~0; -// pInfo[0] <<= 1; - } - else - { - for ( w = 0; w < nWords; w++ ) - pInfo[w] = 0; - } - } - for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ ) - { - pInfo = Vec_PtrEntry( vInfo, k ); - for ( w = 0; w < nWords; w++ ) - pInfo[w] = Gia_ManRandom( 0 ); - } -} - -/**Function************************************************************* - - Synopsis [Remaps simulation info from SRM to the original AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo ) -{ - Gia_Obj_t * pObj, * pRepr; - unsigned * pInfoObj, * pInfoRepr; - int i, w, nWords; - nWords = Vec_PtrReadWordsSimInfo( vInfo ); - Gia_ManForEachRo( p, pObj, i ) - { - // skip ROs without representatives - pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); - if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) ) - continue; - pInfoObj = Vec_PtrEntry( vInfo, i ); - for ( w = 0; w < nWords; w++ ) - assert( pInfoObj[w] == 0 ); - // skip ROs with constant representatives - if ( Gia_ObjIsConst0(pRepr) ) - continue; - assert( Gia_ObjIsRo(p, pRepr) ); -// printf( "%d -> %d ", i, Gia_ObjId(p, pRepr) ); - // transfer info from the representative - pInfoRepr = Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); - for ( w = 0; w < nWords; w++ ) - pInfoObj[w] = pInfoRepr[w]; - } -// printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [Collects information about remapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p ) -{ - Vec_Int_t * vPairs; - Gia_Obj_t * pObj, * pRepr; - int i; - vPairs = Vec_IntAlloc( 100 ); - Gia_ManForEachRo( p, pObj, i ) - { - // skip ROs without representatives - pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ); - if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) ) -// if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) ) - continue; - assert( Gia_ObjIsRo(p, pRepr) ); -// printf( "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) ); - // remember the pair - Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) ); - Vec_IntPush( vPairs, i ); - } - return vPairs; -} - -/**Function************************************************************* - - Synopsis [Remaps simulation info from SRM to the original AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo, int * pInitState ) -{ - unsigned * pInfoObj, * pInfoRepr; - int w, i, iObj, iRepr, nWords; - nWords = Vec_PtrReadWordsSimInfo( vInfo ); - Vec_IntForEachEntry( vPairs, iRepr, i ) - { - iObj = Vec_IntEntry( vPairs, ++i ); - pInfoObj = Vec_PtrEntry( vInfo, iObj ); - pInfoRepr = Vec_PtrEntry( vInfo, iRepr ); - for ( w = 0; w < nWords; w++ ) - { - assert( pInitState || pInfoObj[w] == 0 ); - pInfoObj[w] = pInfoRepr[w]; - } - } -} - -/**Function************************************************************* - - Synopsis [Packs one counter-examples into the array of simulation info.] - - Description [] - - SideEffects [] - - SeeAlso [] - -*************************************`**********************************/ -int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits ) -{ - unsigned * pInfo, * pPres; - int i; - for ( i = 0; i < nLits; i++ ) - { - pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - if ( Gia_InfoHasBit( pPres, iBit ) && - Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - return 0; - } - for ( i = 0; i < nLits; i++ ) - { - pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - Gia_InfoSetBit( pPres, iBit ); - if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - Gia_InfoXorBit( pInfo, iBit ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Performs bitpacking of counter-examples.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart ) -{ - Vec_Int_t * vPat; - Vec_Ptr_t * vPres; - int nWords = Vec_PtrReadWordsSimInfo(vInfo); - int nBits = 32 * nWords; - int k, nSize, iBit = 1, kMax = 0; - vPat = Vec_IntAlloc( 100 ); - vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords ); - Vec_PtrCleanSimInfo( vPres, 0, nWords ); - while ( iStart < Vec_IntSize(vCexStore) ) - { - // skip the output number - iStart++; - // get the number of items - nSize = Vec_IntEntry( vCexStore, iStart++ ); - if ( nSize <= 0 ) - continue; - // extract pattern - Vec_IntClear( vPat ); - for ( k = 0; k < nSize; k++ ) - Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) ); - // add pattern to storage - for ( k = 1; k < nBits; k++ ) - if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) ) - break; - kMax = Abc_MaxInt( kMax, k ); - if ( k == nBits-1 ) - break; - } - Vec_PtrFree( vPres ); - Vec_IntFree( vPat ); - return iStart; -} - -/**Function************************************************************* - - Synopsis [Performs bitpacking of counter-examples.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart ) -{ - unsigned * pInfo; - int nBits = 32 * Vec_PtrReadWordsSimInfo(vInfo); - int k, iLit, nLits, Out, iBit = 1; - while ( iStart < Vec_IntSize(vCexStore) ) - { - // skip the output number -// iStart++; - Out = Vec_IntEntry( vCexStore, iStart++ ); -// printf( "iBit = %d. Out = %d.\n", iBit, Out ); - // get the number of items - nLits = Vec_IntEntry( vCexStore, iStart++ ); - if ( nLits <= 0 ) - continue; - // add pattern to storage - for ( k = 0; k < nLits; k++ ) - { - iLit = Vec_IntEntry( vCexStore, iStart++ ); - pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) ); - if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) ) - Gia_InfoXorBit( pInfo, iBit ); - } - if ( ++iBit == nBits ) - break; - } -// printf( "added %d bits\n", iBit-1 ); - return iStart; -} - -/**Function************************************************************* - - Synopsis [Resimulates counter-examples derived by the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames, int * pInitState ) -{ - Vec_Int_t * vPairs; - Vec_Ptr_t * vSimInfo; - int RetValue = 0, iStart = 0; - vPairs = Gia_ManCorrCreateRemapping( pSim->pAig ); - Gia_ManSetRefs( pSim->pAig ); -// pSim->pPars->nWords = 63; - pSim->pPars->nRounds = nFrames; - vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords ); - while ( iStart < Vec_IntSize(vCexStore) ) - { - Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig), pInitState ); - iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); -// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart ); -// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo ); - Gia_ManCorrPerformRemapping( vPairs, vSimInfo, pInitState ); - RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo ); -// Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL ); - } -//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 ); - assert( iStart == Vec_IntSize(vCexStore) ); - Vec_PtrFree( vSimInfo ); - Vec_IntFree( vPairs ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Resimulates counter-examples derived by the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore ) -{ - Vec_Ptr_t * vSimInfo; - int RetValue = 0, iStart = 0; - Gia_ManSetRefs( pSim->pAig ); - pSim->pPars->nRounds = 1; - vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords ); - while ( iStart < Vec_IntSize(vCexStore) ) - { - Cec_ManStartSimInfo( vSimInfo, 0, NULL ); - iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart ); - RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo ); - } - assert( iStart == Vec_IntSize(vCexStore) ); - Vec_PtrFree( vSimInfo ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Updates equivalence classes by marking those that timed out.] - - Description [Returns 1 if all ndoes are proved.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings ) -{ - int i, status, iRepr, iObj; - int Counter = 0; - assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) ); - Vec_StrForEachEntry( vStatus, status, i ) - { - iRepr = Vec_IntEntry( vOutputs, 2*i ); - iObj = Vec_IntEntry( vOutputs, 2*i+1 ); - if ( status == 1 ) - continue; - if ( status == 0 ) - { - if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) - Counter++; -// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) -// printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj ); -// if ( Gia_ObjHasSameRepr(p, iRepr, iObj) ) -// Cec_ManSimClassRemoveOne( pSim, iObj ); - continue; - } - if ( status == -1 ) - { -// if ( !Gia_ObjFailed( p, iObj ) ) -// printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" ); -// Gia_ObjSetFailed( p, iRepr ); -// Gia_ObjSetFailed( p, iObj ); -// if ( fRings ) -// Cec_ManSimClassRemoveOne( pSim, iRepr ); - Cec_ManSimClassRemoveOne( pSim, iObj ); - continue; - } - } -// if ( Counter ) -// printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter ); - return 1; -} - - -/**Function************************************************************* - - Synopsis [Duplicates the AIG in the DFS order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) -{ - Gia_Obj_t * pRepr; - if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) ) - { - Gia_ManCorrReduce_rec( pNew, p, pRepr ); - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); - return; - } - if ( ~pObj->Value ) - return; - assert( Gia_ObjIsAnd(pObj) ); - Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); - Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) ); - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Reduces AIG using equivalence classes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p ) -{ - Gia_Man_t * pNew; - Gia_Obj_t * pObj; - int i; - Gia_ManSetPhase( p ); - pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); - Gia_ManFillValue( p ); - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachCi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); - Gia_ManHashAlloc( pNew ); - Gia_ManForEachCo( p, pObj, i ) - Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) ); - Gia_ManForEachCo( p, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManHashStop( pNew ); - Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); - return pNew; -} - - -/**Function************************************************************* - - Synopsis [Prints statistics during solving.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time ) -{ - int nLits, CounterX = 0, Counter0 = 0, Counter = 0; - int i, Entry, nProve = 0, nDispr = 0, nFail = 0; - for ( i = 1; i < Gia_ManObjNum(p); i++ ) - { - if ( Gia_ObjIsNone(p, i) ) - CounterX++; - else if ( Gia_ObjIsConst(p, i) ) - Counter0++; - else if ( Gia_ObjIsHead(p, i) ) - Counter++; - } - CounterX -= Gia_ManCoNum(p); - nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX; - if ( iIter == -1 ) - printf( "BMC : " ); - else - printf( "%3d : ", iIter ); - printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits ); - if ( vStatus ) - Vec_StrForEachEntry( vStatus, Entry, i ) - { - if ( Entry == 1 ) - nProve++; - else if ( Entry == 0 ) - nDispr++; - else if ( Entry == -1 ) - nFail++; - } - printf( "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail ); - ABC_PRT( "T", Time ); -} - -/**Function************************************************************* - - Synopsis [Computes new initial state.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames ) -{ - Gia_Obj_t * pObj, * pObjRo, * pObjRi; - unsigned * pInitState; - int i, f; - printf( "Simulating %d timeframes.\n", nFrames ); - Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark1 = 0; - for ( f = 0; f < nFrames; f++ ) - { - Gia_ManConst0(pAig)->fMark1 = 0; - Gia_ManForEachPi( pAig, pObj, i ) - pObj->fMark1 = Gia_ManRandom(0) & 1; -// pObj->fMark1 = 1; - Gia_ManForEachAnd( pAig, pObj, i ) - pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & - (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)); - Gia_ManForEachRi( pAig, pObj, i ) - pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)); - Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i ) - pObjRo->fMark1 = pObjRi->fMark1; - } - pInitState = ABC_CALLOC( unsigned, Gia_BitWordNum(Gia_ManRegNum(pAig)) ); - Gia_ManForEachRo( pAig, pObj, i ) - { - if ( pObj->fMark1 ) - Gia_InfoSetBit( pInitState, i ); -// printf( "%d", pObj->fMark1 ); - } -// printf( "\n" ); - Gia_ManCleanMark1( pAig ); - return pInitState; -} - -/**Function************************************************************* - - Synopsis [Internal procedure for register correspondence.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) -{ - int nIterMax = 100000; - int nAddFrames = 1; // additional timeframes to simulate - Vec_Str_t * vStatus; - Vec_Int_t * vOutputs; - Vec_Int_t * vCexStore; - Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; - Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; - Cec_ManSim_t * pSim; - Gia_Man_t * pSrm; - unsigned * pInitState = NULL; - int r, RetValue; - clock_t clkTotal = clock(); - clock_t clkSat = 0, clkSim = 0, clkSrm = 0; - clock_t clk2, clk = clock(); - ABC_FREE( pAig->pReprs ); - ABC_FREE( pAig->pNexts ); - if ( Gia_ManRegNum(pAig) == 0 ) - { - printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" ); - return 0; - } - Gia_ManRandom( 1 ); - // derive initial state for resimulation - if ( pPars->nPrefix ) -// pInitState = Cec_ManComputeInitState( pAig, 5+(1<<20)/Gia_ManAndNum(pAig) ); - pInitState = Cec_ManComputeInitState( pAig, 100 ); - // prepare simulation manager - Cec_ManSimSetDefaultParams( pParsSim ); - pParsSim->nWords = pPars->nWords; - pParsSim->nRounds = pPars->nRounds; - pParsSim->fVerbose = pPars->fVerbose; - pParsSim->fLatchCorr = pPars->fLatchCorr; - pParsSim->fSeqSimulate = 1; - // create equivalence classes of registers - pSim = Cec_ManSimStart( pAig, pParsSim, pInitState ); - Cec_ManSimClassesPrepare( pSim ); - Cec_ManSimClassesRefine( pSim ); - // prepare SAT solving - Cec_ManSatSetDefaultParams( pParsSat ); - pParsSat->nBTLimit = pPars->nBTLimit; - pParsSat->fVerbose = pPars->fVerbose; - if ( pPars->fVerbose ) - { - printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n", - Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), - pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat ); - Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk ); - } - // perform refinement of equivalence classes - for ( r = 0; r < nIterMax; r++ ) - { - clk = clock(); - // perform speculative reduction - clk2 = clock(); - pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); - assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) ); - clkSrm += clock() - clk2; - if ( Gia_ManCoNum(pSrm) == 0 ) - { - Vec_IntFree( vOutputs ); - Gia_ManStop( pSrm ); - break; - } -//Gia_DumpAiger( pSrm, "corrsrm", r, 2 ); - // found counter-examples to speculation - clk2 = clock(); - if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); - else - vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); - Gia_ManStop( pSrm ); - clkSat += clock() - clk2; - if ( Vec_IntSize(vCexStore) == 0 ) - { - Vec_IntFree( vCexStore ); - Vec_StrFree( vStatus ); - Vec_IntFree( vOutputs ); - break; - } - // refine classes with these counter-examples - clk2 = clock(); - RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames, pInitState ); - Vec_IntFree( vCexStore ); - clkSim += clock() - clk2; - Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk ); - Vec_StrFree( vStatus ); - Vec_IntFree( vOutputs ); -//Gia_ManEquivPrintClasses( pAig, 1, 0 ); - } - ABC_FREE( pInitState ); - // check the base case - if ( (!pPars->fLatchCorr || pPars->nFrames > 1) || pPars->nPrefix ) - { - int fChanges = 1; - while ( fChanges ) - { - clock_t clkBmc = clock(); - fChanges = 0; - pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, pPars->nPrefix, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); - if ( Gia_ManPoNum(pSrm) == 0 ) - { - Gia_ManStop( pSrm ); - Vec_IntFree( vOutputs ); - break; - } - pParsSat->nBTLimit *= 10; - if ( pPars->nPrefix ) - { - pParsSat->nBTLimit = 10000; - vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); - } - else if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); - else - vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); - // refine classes with these counter-examples - if ( Vec_IntSize(vCexStore) ) - { - clk2 = clock(); - RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames + pPars->nPrefix, NULL ); - clkSim += clock() - clk2; - Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings ); - fChanges = 1; - } - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc ); - // recycle - Vec_IntFree( vCexStore ); - Vec_StrFree( vStatus ); - Gia_ManStop( pSrm ); - Vec_IntFree( vOutputs ); - } - } - else - { - if ( pPars->fVerbose ) - Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk ); - } - // check the overflow - if ( r == nIterMax ) - printf( "The refinement was not finished. The result may be incorrect.\n" ); - Cec_ManSimStop( pSim ); - clkTotal = clock() - clkTotal; - // report the results - if ( pPars->fVerbose ) - { - ABC_PRTP( "Srm ", clkSrm, clkTotal ); - ABC_PRTP( "Sat ", clkSat, clkTotal ); - ABC_PRTP( "Sim ", clkSim, clkTotal ); - ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal ); - ABC_PRT( "TOTAL", clkTotal ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Top-level procedure for register correspondence.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) -{ - Gia_Man_t * pNew, * pTemp; - int RetValue; - RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars ); - // derive reduced AIG - if ( pPars->fMakeChoices ) - { - pNew = Gia_ManEquivToChoices( pAig, 1 ); - Gia_ManHasChoices( pNew ); - } - else - { - Gia_ManEquivImprove( pAig ); - pNew = Gia_ManCorrReduce( pAig ); - pNew = Gia_ManSeqCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 ); - } - // report the results - if ( pPars->fVerbose ) - { - printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", - Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), - 100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), - Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), - 100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) ); - } - return pNew; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c index 8fc8192f..783202e2 100644 --- a/src/proof/dch/dchChoice.c +++ b/src/proof/dch/dchChoice.c @@ -31,6 +31,36 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Counts support nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ObjCountSupp_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + int Count; + if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) + return 0; + Aig_ObjSetTravIdCurrent( p, pObj ); + if ( Aig_ObjIsCi(pObj) ) + return 1; + assert( Aig_ObjIsNode(pObj) ); + Count = Dch_ObjCountSupp_rec( p, Aig_ObjFanin0(pObj) ); + Count += Dch_ObjCountSupp_rec( p, Aig_ObjFanin1(pObj) ); + return Count; +} +int Dch_ObjCountSupp( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_ManIncrementTravId( p ); + return Dch_ObjCountSupp_rec( p, pObj ); +} + /**Function************************************************************* Synopsis [Counts the number of representatives.] @@ -56,54 +86,72 @@ int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig ) } return nReprs; } +int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ) +{ + Aig_Obj_t * pObj, * pEquiv; + int i, nEquivs = 0; + Aig_ManForEachObj( pAig, pObj, i ) + { + pEquiv = Aig_ObjEquiv( pAig, pObj ); + if ( pEquiv == NULL ) + continue; + assert( pEquiv->Id > pObj->Id ); + nEquivs++; + } + return nEquivs; +} /**Function************************************************************* - Synopsis [Counts the number of equivalences.] + Synopsis [Marks the TFI of the node.] - Description [] + Description [Returns 1 if there is a CI not marked with previous ID.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ) +int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) { - Aig_Obj_t * pObj, * pTemp, * pPrev; - int i, nEquivs = 0, Counter = 0; - Aig_ManForEachObj( pAig, pObj, i ) + int RetValue; + if ( pObj == NULL ) + return 0; + if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) + return 0; + if ( Aig_ObjIsCi(pObj) ) { - if ( !Aig_ObjIsChoice(pAig, pObj) ) - continue; - for ( pPrev = pObj, pTemp = Aig_ObjEquiv(pAig, pObj); pTemp; - pPrev = pTemp, pTemp = Aig_ObjEquiv(pAig, pTemp) ) - { - if ( pTemp->nRefs > 0 ) - { - // remove referenced node from equivalence class - assert( pAig->pEquivs[pPrev->Id] == pTemp ); - pAig->pEquivs[pPrev->Id] = pAig->pEquivs[pTemp->Id]; - pAig->pEquivs[pTemp->Id] = NULL; - // how about the need to continue iterating over the list? - // pPrev = pTemp ??? - Counter++; - } - nEquivs++; - } + RetValue = !Aig_ObjIsTravIdPrevious( p, pObj ); + Aig_ObjSetTravIdCurrent( p, pObj ); + return RetValue; } -// printf( "Removed %d classes.\n", Counter ); - - if ( Counter ) - Dch_DeriveChoiceCountEquivs( pAig ); -// if ( Counter ) -// printf( "Removed %d equiv nodes because of non-zero ref counter.\n", Counter ); - return nEquivs; + assert( Aig_ObjIsNode(pObj) ); + Aig_ObjSetTravIdCurrent( p, pObj ); + RetValue = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) ); + RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) ); +// RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) ); + return (RetValue > 0); +} +int Dch_ObjCheckSuppRed( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) +{ + // mark support of the representative node (pRepr) + Aig_ManIncrementTravId( p ); + Dch_ObjMarkTfi_rec( p, pRepr ); + // detect if the new node (pObj) depends on additional variables + Aig_ManIncrementTravId( p ); + if ( Dch_ObjMarkTfi_rec( p, pObj ) ) + return 1;//, printf( "1" ); + // detect if the representative node (pRepr) depends on additional variables + Aig_ManIncrementTravId( p ); + if ( Dch_ObjMarkTfi_rec( p, pRepr ) ) + return 1;//, printf( "2" ); + // skip the choice if this is what is happening + return 0; } /**Function************************************************************* - Synopsis [Returns representatives of fanin in approapriate polarity.] + Synopsis [Make sure reprsentative nodes do not have representatives.] Description [] @@ -112,19 +160,88 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) +void Aig_ManCheckReprs( Aig_Man_t * p ) { - Aig_Obj_t * pRepr; - if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) ) - return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) ); - return pObj; + int fPrintConst = 0; + Aig_Obj_t * pObj; + int i, fProb = 0; + int Class0 = 0, ClassCi = 0; + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjRepr(p, pObj) == NULL ) + continue; + if ( !Aig_ObjIsNode(pObj) ) + printf( "Obj %d is not an AND but it has a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)) ), fProb = 1; + else if ( Aig_ObjRepr(p, Aig_ObjRepr(p, pObj)) ) + printf( "Obj %d has repr %d with a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)), Aig_ObjId(Aig_ObjRepr(p, Aig_ObjRepr(p, pObj))) ), fProb = 1; + } + if ( !fProb ) + printf( "Representive verification successful.\n" ); + else + printf( "Representive verification FAILED.\n" ); + if ( !fPrintConst ) + return; + // count how many representatives are const0 or a CI + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjRepr(p, pObj) == Aig_ManConst1(p) ) + Class0++; + if ( Aig_ObjRepr(p, pObj) && Aig_ObjIsCi(Aig_ObjRepr(p, pObj)) ) + ClassCi++; + } + printf( "Const0 nodes = %d. ConstCI nodes = %d.\n", Class0, ClassCi ); } -static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); } -static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); } +/**Function************************************************************* + Synopsis [Verify correctness of choices.] + Description [] + + SideEffects [] + SeeAlso [] + +***********************************************************************/ +void Dch_CheckChoices( Aig_Man_t * p, int fSkipRedSupps ) +{ + Aig_Obj_t * pObj; + int i, fProb = 0; + Aig_ManCleanMarkA( p ); + Aig_ManForEachNode( p, pObj, i ) + { + if ( p->pEquivs[i] != NULL ) + { + if ( pObj->fMarkA == 1 ) + printf( "node %d participates in more than one choice class\n", i ), fProb = 1; + pObj->fMarkA = 1; + // check redundancy + if ( fSkipRedSupps && Dch_ObjCheckSuppRed( p, pObj, p->pEquivs[i]) ) + printf( "node %d and repr %d have diff supports\n", pObj->Id, p->pEquivs[i]->Id ); + // consider the next one + pObj = p->pEquivs[i]; + if ( p->pEquivs[Aig_ObjId(pObj)] == NULL ) + { + if ( pObj->fMarkA == 1 ) + printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1; + pObj->fMarkA = 1; + } + // consider the non-head ones + if ( pObj->nRefs > 0 ) + printf( "node %d belonging to choice has fanout %d\n", pObj->Id, pObj->nRefs ); + } + if ( p->pReprs && p->pReprs[i] != NULL ) + { + if ( pObj->nRefs > 0 ) + printf( "node %d has representative %d and fanout count %d\n", pObj->Id, p->pReprs[i]->Id, pObj->nRefs ), fProb = 1; + } + } + Aig_ManCleanMarkA( p ); + if ( !fProb ) + printf( "Verification of choice AIG succeeded.\n" ); + else + printf( "Verification of choice AIG FAILED.\n" ); +} /**Function************************************************************* @@ -240,104 +357,6 @@ int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose ) return fAcyclic; } -/**Function************************************************************* - - Synopsis [Removes combinational loop.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose ) -{ - Aig_Obj_t * pObj; - int i, Counter = 0, Counter2 = 0; - Aig_ManForEachObj( p, pObj, i ) - { - if ( !Aig_ObjIsTravIdCurrent(p, pObj) ) - continue; - Counter2++; - if ( Aig_ObjRepr(p, pObj) == NULL && Aig_ObjEquiv(p, pObj) != NULL ) - { - Aig_ObjSetEquiv(p, pObj, NULL); - Counter++; - } - } - if ( fVerbose ) - Abc_Print( 1, "Fixed %d choice nodes on the path with %d objects.\n", Counter, Counter2 ); -} - - -/**Function************************************************************* - - Synopsis [Verify correctness of choices.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Dch_CheckChoices( Aig_Man_t * p ) -{ - Aig_Obj_t * pObj; - int i, fProb = 0; - Aig_ManCleanMarkA( p ); - Aig_ManForEachNode( p, pObj, i ) - if ( p->pEquivs[i] != NULL ) - { - if ( pObj->fMarkA == 1 ) - printf( "node %d participates in more than one choice class\n", i ), fProb = 1; - pObj->fMarkA = 1; - // consider the last one - pObj = p->pEquivs[i]; - if ( p->pEquivs[Aig_ObjId(pObj)] == NULL ) - { - if ( pObj->fMarkA == 1 ) - printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1; - pObj->fMarkA = 1; - } - } - Aig_ManCleanMarkA( p ); - if ( !fProb ) - printf( "Verification of choice AIG succeeded.\n" ); -} - -/**Function************************************************************* - - Synopsis [Marks the TFI of the node.] - - Description [Returns 1 if there is a CI not marked with previous ID.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) -{ - int RetValue; - if ( pObj == NULL ) - return 0; - if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) - return 0; - if ( Aig_ObjIsCi(pObj) ) - { - RetValue = !Aig_ObjIsTravIdPrevious( p, pObj ); - Aig_ObjSetTravIdCurrent( p, pObj ); - return RetValue; - } - assert( Aig_ObjIsNode(pObj) ); - Aig_ObjSetTravIdCurrent( p, pObj ); - RetValue = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) ); - RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) ); -// RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) ); - return (RetValue > 0); -} /**Function************************************************************* @@ -389,6 +408,27 @@ int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) return RetValue; } +/**Function************************************************************* + + Synopsis [Returns representatives of fanin in approapriate polarity.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pRepr; + if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) ) + return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) ); + return pObj; +} +static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); } +static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); } + /**Function************************************************************* Synopsis [Derives the AIG with choices from representatives.] @@ -403,22 +443,34 @@ int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps ) { Aig_Obj_t * pRepr, * pObjNew, * pReprNew; + assert( !Aig_IsComplement(pObj) ); + // get the representative + pRepr = Aig_ObjRepr( pAigOld, pObj ); + if ( pRepr != NULL && (Aig_ObjIsConst1(pRepr) || Aig_ObjIsCi(pRepr)) ) + { + assert( pRepr->pData != NULL ); + pObj->pData = Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pObj->fPhase ^ pRepr->fPhase ); + return; + } // get the new node - assert( pObj->pData == NULL ); - pObj->pData = Aig_And( pAigNew, + pObjNew = Aig_And( pAigNew, Aig_ObjChild0CopyRepr(pAigNew, pObj), Aig_ObjChild1CopyRepr(pAigNew, pObj) ); - pRepr = Aig_ObjRepr( pAigOld, pObj ); + pObjNew = Aig_ObjGetRepr( pAigNew, pObjNew ); + assert( Aig_ObjRepr( pAigNew, pObjNew ) == NULL ); + // assign the copy + assert( pObj->pData == NULL ); + pObj->pData = pObjNew; + // skip those without reprs if ( pRepr == NULL ) return; assert( pRepr->Id < pObj->Id ); + assert( Aig_ObjIsNode(pRepr) ); // get the corresponding new nodes pObjNew = Aig_Regular((Aig_Obj_t *)pObj->pData); pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData); - if ( pObjNew == pReprNew ) - return; - // skip the earlier nodes - if ( pReprNew->Id > pObjNew->Id ) + // skip earlier nodes + if ( pReprNew->Id >= pObjNew->Id ) return; assert( pReprNew->Id < pObjNew->Id ); // set the representatives @@ -427,33 +479,16 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_ if ( pObjNew->nRefs > 0 ) return; assert( pObjNew->nRefs == 0 ); - // update new nodes of the object - if ( !Aig_ObjIsNode(pRepr) ) - return; - // skip choices with combinational loops + // skip choices that can lead to combo loops if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) ) return; // don't add choice if structural support of pObjNew and pReprNew differ - if ( fSkipRedSupps ) - { - int fSkipChoice = 0; - // mark support of the representative node (pReprNew) - Aig_ManIncrementTravId( pAigNew ); - Dch_ObjMarkTfi_rec( pAigNew, pReprNew ); - // detect if the new node (pObjNew) depends on any additional variables - Aig_ManIncrementTravId( pAigNew ); - if ( Dch_ObjMarkTfi_rec( pAigNew, pObjNew ) ) - fSkipChoice = 1;//, printf( "1" ); - // detect if the representative node (pReprNew) depends on any additional variables - Aig_ManIncrementTravId( pAigNew ); - if ( Dch_ObjMarkTfi_rec( pAigNew, pReprNew ) ) - fSkipChoice = 1;//, printf( "2" ); - // skip the choice if this is what is happening - if ( fSkipChoice ) - return; - } - // add choice - pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id]; + if ( fSkipRedSupps && Dch_ObjCheckSuppRed(pAigNew, pObjNew, pReprNew) ) + return; + // add choice to the end of the list + while ( pAigNew->pEquivs[pReprNew->Id] != NULL ) + pReprNew = pAigNew->pEquivs[pReprNew->Id]; + assert( pAigNew->pEquivs[pReprNew->Id] == NULL ); pAigNew->pEquivs[pReprNew->Id] = pObjNew; } Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps ) @@ -461,10 +496,6 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps ) Aig_Man_t * pChoices; Aig_Obj_t * pObj; int i; - // make sure reprsentative nodes do not have representatives - Aig_ManForEachNode( pAig, pObj, i ) - if ( pAig->pReprs[i] != NULL && pAig->pReprs[pAig->pReprs[i]->Id] != NULL ) - printf( "Node %d: repr %d has repr %d.\n", i, Aig_ObjId(pAig->pReprs[i]), Aig_ObjId(pAig->pReprs[pAig->pReprs[i]->Id]) ); // start recording equivalences pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) ); pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); @@ -476,45 +507,32 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps ) pObj->pData = Aig_ObjCreateCi( pChoices ); // construct choices for the internal nodes assert( pAig->pReprs != NULL ); - Aig_ManForEachNode( pAig, pObj, i ) + Aig_ManForEachNode( pAig, pObj, i ) Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, fSkipRedSupps ); Aig_ManForEachCo( pAig, pObj, i ) Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) ); - Dch_DeriveChoiceCountEquivs( pChoices ); Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) ); -//Dch_CheckChoices( pChoices ); return pChoices; } - -/**Function************************************************************* - - Synopsis [Derives the AIG with choices from representatives.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps ) { - extern int Aig_ManCheckAcyclic( Aig_Man_t * pAig, int fVerbose ); + int fCheck = 0; Aig_Man_t * pChoices, * pTemp; - int fVerbose = 0; + // verify + if ( fCheck ) + Aig_ManCheckReprs( pAig ); + // compute choices pChoices = Dch_DeriveChoiceAigInt( pAig, fSkipRedSupps ); -// pChoices = Dch_DeriveChoiceAigInt( pTemp = pChoices ); -// Aig_ManStop( pTemp ); - // there is no need for cleanup ABC_FREE( pChoices->pReprs ); - while ( !Aig_ManCheckAcyclic( pChoices, fVerbose ) ) - { - if ( fVerbose ) - Abc_Print( 1, "There is a loop!\n" ); - Aig_ManFixLoopProblem( pChoices, fVerbose ); - } + // verify + if ( fCheck ) + Dch_CheckChoices( pChoices, fSkipRedSupps ); + // find correct topo order with choices pChoices = Aig_ManDupDfs( pTemp = pChoices ); Aig_ManStop( pTemp ); + // verify + if ( fCheck ) + Dch_CheckChoices( pChoices, fSkipRedSupps ); return pChoices; } diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c index 654ed359..da103e0e 100644 --- a/src/proof/dch/dchCore.c +++ b/src/proof/dch/dchCore.c @@ -106,19 +106,13 @@ p->timeSimInit = clock() - clk; // free memory ahead of time p->timeTotal = clock() - clkTotal; Dch_ManStop( p ); - // try something different - { -// extern void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig ); -// Gia_ManNormalizeChoicesTest( pAig ); - } - // create choices ABC_FREE( pAig->pTable ); pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp ); // count the number of representatives if ( pPars->fVerbose ) Abc_Print( 1, "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", - Dch_DeriveChoiceCountReprs( pAig ), + Dch_DeriveChoiceCountReprs( pResult ), Dch_DeriveChoiceCountEquivs( pResult ), Aig_ManChoiceNum( pResult ) ); return pResult; -- cgit v1.2.3