diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-19 16:47:05 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-19 16:47:05 -0800 |
commit | e3f88c81c62cb771faba13cbe58a7488af0087bd (patch) | |
tree | ff1149e8ef349c5bb9232bbc817f9cb45c980e96 /src/aig/gia | |
parent | 2619edf8c0347b78549c28083dd0565ed2589425 (diff) | |
download | abc-e3f88c81c62cb771faba13cbe58a7488af0087bd.tar.gz abc-e3f88c81c62cb771faba13cbe58a7488af0087bd.tar.bz2 abc-e3f88c81c62cb771faba13cbe58a7488af0087bd.zip |
Changes to support sequential verification with reduction without speculation.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 79 |
2 files changed, 69 insertions, 12 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index b2f039a7..c4d41459 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -659,7 +659,7 @@ extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ); extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ); extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); -extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fVerbose ); +extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut ); extern Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ); diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 581383ea..170830ee 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -748,7 +748,7 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut ) +static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate ) { Gia_Obj_t * pRepr; unsigned iLitNew; @@ -761,7 +761,8 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) ); - pObj->Value = iLitNew; + if ( fSpeculate ) + pObj->Value = iLitNew; } /**Function************************************************************* @@ -798,15 +799,15 @@ int Gia_ManHasNoEquivs( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut ) +void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate ) { if ( ~pObj->Value ) return; assert( Gia_ObjIsAnd(pObj) ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut ); - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut ); + Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate ); } /**Function************************************************************* @@ -820,7 +821,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fVerbose ) +Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fVerbose ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; @@ -862,9 +863,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); Gia_ManForEachRo( p, pObj, i ) - Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut ); + Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut ); + Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate ); if ( !fSynthesis ) { Gia_ManForEachPo( p, pObj, i ) @@ -1127,6 +1128,62 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ) /**Function************************************************************* + Synopsis [Marks proved equivalences.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fVerbose ) +{ + Gia_Man_t * pMiter; + Gia_Obj_t * pObj; + int i, nLits = 0; + int nLitsAll, Counter = 0; + nLitsAll = Gia_ManEquivCountLitsAll( p ); + if ( nLitsAll == 0 ) + { + printf( "Gia_ManEquivMark(): Current AIG does not have equivalences.\n" ); + return; + } + // read AIGER file + pMiter = Gia_ReadAiger( pFileName, 0 ); + if ( pMiter == NULL ) + { + printf( "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName ); + return; + } + if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll ) + { + printf( "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n", + Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll ); + Gia_ManStop( pMiter ); + return; + } + // mark corresponding POs as solved + nLits = 0; + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + { + if ( Gia_ObjRepr(p, i) == GIA_VOID ) + continue; + pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + nLits++ ); + if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven + { + Gia_ObjSetProved(p, i); + Counter++; + } + } + if ( fVerbose ) + printf( "Set %d equivalences as proved.\n", Counter ); + assert( nLits == nLitsAll ); + Gia_ManStop( pMiter ); +} + +/**Function************************************************************* + Synopsis [Transforms equiv classes by setting a good representative.] Description [] @@ -1534,7 +1591,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" ); break; } - pSrm = Gia_ManSpecReduce( pGia, 0, 0, 0 ); + pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 ); // bmc2 -F 100 -C 25000 { Abc_Cex_t * pCex; @@ -1571,7 +1628,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f // write equivalence classes Gia_WriteAiger( pGia, "gore.aig", 0, 0 ); // reduce the model - pReduce = Gia_ManSpecReduce( pGia, 0, 0, 0 ); + pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 ); if ( pReduce ) { pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); |