From 28e065b0aebc08990ca8208b4982edafe66fb0fd Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 22 May 2013 11:02:56 -0700 Subject: Counter-example depth minimization. --- src/aig/gia/gia.h | 5 ++- src/aig/gia/giaDup.c | 93 +++++++++++++++++++++++++++++++++++++++++++++++++--- src/aig/gia/giaMan.c | 6 +++- 3 files changed, 98 insertions(+), 6 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 12d255a4..c890b165 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -343,6 +343,7 @@ static inline int Gia_ManObjIsConst0( Gia_Man_t * p, Gia_Obj_t * pObj){ static inline int Gia_Obj2Lit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit(Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj)); } static inline Gia_Obj_t * Gia_Lit2Obj( Gia_Man_t * p, int iLit ) { return Gia_NotCond(Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); } +static inline int Gia_ManCiLit( Gia_Man_t * p, int CiId ) { return Gia_Obj2Lit( p, Gia_ManCi(p, CiId) ); } static inline int Gia_ManIdToCioId( Gia_Man_t * p, int Id ) { return Gia_ObjCioId( Gia_ManObj(p, Id) ); } static inline int Gia_ManCiIdToId( Gia_Man_t * p, int CiId ) { return Gia_ObjId( p, Gia_ManCi(p, CiId) ); } @@ -897,13 +898,15 @@ extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop ); extern Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres ); extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis ); extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ); -extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, int nFrames ); +extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm ); extern void Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo ); extern void Gia_ManDupAppendShare( Gia_Man_t * p, Gia_Man_t * pTwo ); extern Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ); +extern Gia_Man_t * Gia_ManDupAppendCones( Gia_Man_t * p, Gia_Man_t ** ppCones, int nCones, int fOnlyRegs ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 2c7fd59b..d533dc1f 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -383,6 +383,36 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + assert( Gia_ManRegNum(p) == 0 ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = (i < Gia_ManCiNum(p) - nLastPis) ? ~0 : Gia_ManAppendCi(pNew); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + return pNew; +} + /**Function************************************************************* Synopsis [Duplicates AIG while complementing the flops.] @@ -438,16 +468,17 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ) SeeAlso [] ***********************************************************************/ -void Gia_ManCycle( Gia_Man_t * p, int nFrames ) +void Gia_ManCycle( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames ) { Gia_Obj_t * pObj, * pObjRi, * pObjRo; int i, k; Gia_ManRandom( 1 ); + assert( pCex == NULL || nFrames <= pCex->iFrame ); // iterate for the given number of frames for ( i = 0; i < nFrames; i++ ) { Gia_ManForEachPi( p, pObj, k ) - pObj->fMark0 = (1 & Gia_ManRandom(0)); + pObj->fMark0 = pCex ? Abc_InfoHasBit(pCex->pData, pCex->nRegs+i*pCex->nPis+k) : (1 & Gia_ManRandom(0)); Gia_ManForEachAnd( p, pObj, k ) pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); @@ -457,14 +488,14 @@ void Gia_ManCycle( Gia_Man_t * p, int nFrames ) pObjRo->fMark0 = pObjRi->fMark0; } } -Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * p, int nFrames ) +Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames ) { Gia_Man_t * pNew; Vec_Bit_t * vInits; Gia_Obj_t * pObj; int i; Gia_ManCleanMark0(p); - Gia_ManCycle( p, nFrames ); + Gia_ManCycle( p, pCex, nFrames ); vInits = Vec_BitAlloc( Gia_ManRegNum(p) ); Gia_ManForEachRo( p, pObj, i ) Vec_BitPush( vInits, pObj->fMark0 ); @@ -649,6 +680,60 @@ Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ) return pNew; } +/**Function************************************************************* + + Synopsis [Appends logic cones as additional property outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAppendCones( Gia_Man_t * p, Gia_Man_t ** ppCones, int nCones, int fOnlyRegs ) +{ + Gia_Man_t * pNew, * pOne; + Gia_Obj_t * pObj; + int i, k; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + for ( k = 0; k < nCones; k++ ) + { + pOne = ppCones[k]; + assert( Gia_ManPoNum(pOne) == 1 ); + assert( Gia_ManRegNum(pOne) == 0 ); + if ( fOnlyRegs ) + assert( Gia_ManPiNum(pOne) == Gia_ManRegNum(p) ); + else + assert( Gia_ManPiNum(pOne) == Gia_ManCiNum(p) ); + Gia_ManConst0(pOne)->Value = 0; + Gia_ManForEachPi( pOne, pObj, i ) + pObj->Value = Gia_ManCiLit( pNew, fOnlyRegs ? Gia_ManPiNum(p) + i : i ); + Gia_ManForEachAnd( pOne, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( pOne, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + pNew = Gia_ManCleanup( pOne = pNew ); + Gia_ManStop( pOne ); + return pNew; +} + + /**Function************************************************************* Synopsis [Duplicates while adding self-loops to the registers.] diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 8670993d..5738595b 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -245,11 +245,15 @@ void Gia_ManPrintTents( Gia_Man_t * p ) printf( "Tents: " ); for ( t = 1; nSizePrev < Vec_IntSize(vObjs); t++ ) { + int nPis = 0; nSizeCurr = Vec_IntSize(vObjs); Vec_IntForEachEntryStartStop( vObjs, iObjId, i, nSizePrev, nSizeCurr ) + { + nPis += Gia_ObjIsPi(p, Gia_ManObj(p, iObjId)); if ( Gia_ObjIsRo(p, Gia_ManObj(p, iObjId)) ) Gia_ManPrintTents_rec( p, Gia_ObjRoToRi(p, Gia_ManObj(p, iObjId)), vObjs ); - printf( "%d=%d ", t, nSizeCurr - nSizePrev ); + } + printf( "%d=%d(%d) ", t, nSizeCurr - nSizePrev, nPis ); nSizePrev = nSizeCurr; } printf( " Unused=%d\n", Gia_ManObjNum(p) - Vec_IntSize(vObjs) ); -- cgit v1.2.3