From e3f88c81c62cb771faba13cbe58a7488af0087bd Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 19 Feb 2011 16:47:05 -0800 Subject: Changes to support sequential verification with reduction without speculation. --- src/aig/cec/cecSeq.c | 2 +- src/aig/gia/gia.h | 2 +- src/aig/gia/giaEquiv.c | 79 ++++++++++++++++++---- src/aig/ivy/ivyFraig.c | 176 ++++++++++++++++++++++++++++++++++++++++++++++++- 4 files changed, 243 insertions(+), 16 deletions(-) (limited to 'src/aig') diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index c255d50e..269c42c0 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -393,7 +393,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) // write equivalence classes Gia_WriteAiger( pAig, "gore.aig", 0, 0 ); // reduce the model - pReduce = Gia_ManSpecReduce( pAig, 0, 0, 0 ); + pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0 ); if ( pReduce ) { pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); 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 ) @@ -1125,6 +1126,62 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ) nRemovedClas, nTotalClas, nRemovedLits, nTotalLits ); } +/**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.] @@ -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 ); diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index 7310d4cb..87209ca3 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -200,6 +200,7 @@ static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int static int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p ); static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 ); +static int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit ); static ABC_INT64_T s_nBTLimitGlobal = 0; static ABC_INT64_T s_nInsLimitGlobal = 0; @@ -593,10 +594,10 @@ Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParam } assert( k == Ivy_ManObjNum(pManAig) ); // allocate storage for sim pattern - p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) ); - p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords ); + p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) ); + p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords ); p->pPatScores = ABC_ALLOC( int, 32 * p->nSimWords ); - p->vPiVars = Vec_PtrAlloc( 100 ); + p->vPiVars = Vec_PtrAlloc( 100 ); // set random number generator srand( 0xABCABC ); return p; @@ -1992,6 +1993,7 @@ p->nClassesEnd = p->lClasses.nItems; if ( Ivy_ObjFaninVec(pObj) ) Vec_PtrFree( Ivy_ObjFaninVec(pObj) ); pObj->pNextFan0 = pObj->pNextFan1 = NULL; + pObj->pEquiv = NULL; } // remove dangling nodes Ivy_ManCleanup( p->pManFraig ); @@ -2154,6 +2156,14 @@ p->timeSatSat += clock() - clk; else // if ( RetValue1 == l_Undef ) { p->timeSatFail += clock() - clk; +/* + if ( nBTLimit > 1000 ) + { + RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit ); + if ( RetValue != -1 ) + return RetValue; + } +*/ // mark the node as the failed node if ( pOld != p->pManFraig->pConst1 ) pOld->fFailTfo = 1; @@ -2197,6 +2207,14 @@ p->timeSatSat += clock() - clk; else // if ( RetValue1 == l_Undef ) { p->timeSatFail += clock() - clk; +/* + if ( nBTLimit > 1000 ) + { + RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit ); + if ( RetValue != -1 ) + return RetValue; + } +*/ // mark the node as the failed node pOld->fFailTfo = 1; pNew->fFailTfo = 1; @@ -2286,6 +2304,14 @@ p->timeSatSat += clock() - clk; else // if ( RetValue1 == l_Undef ) { p->timeSatFail += clock() - clk; +/* + if ( p->pParams->nBTLimitMiter > 1000 ) + { + RetValue = Ivy_FraigCheckCone( p, p->pManFraig, p->pManFraig->pConst1, pNew, p->pParams->nBTLimitMiter ); + if ( RetValue != -1 ) + return RetValue; + } +*/ // mark the node as the failed node pNew->fFailTfo = 1; p->nSatFailsReal++; @@ -2773,6 +2799,150 @@ int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 ) return RetValue; } +ABC_NAMESPACE_IMPL_END + +#include "aig.h" + +ABC_NAMESPACE_IMPL_START + + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigExtractCone_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) +{ + if ( pNode->fMarkB ) + return; + pNode->fMarkB = 1; + if ( Ivy_ObjIsPi(pNode) ) + { + Vec_IntPush( vLeaves, pNode->Id ); + return; + } + assert( Ivy_ObjIsAnd(pNode) ); + Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin0(pNode), vLeaves, vNodes ); + Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin1(pNode), vLeaves, vNodes ); + Vec_IntPush( vNodes, pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Checks equivalence using BDDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ivy_FraigExtractCone( Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, Vec_Int_t * vLeaves ) +{ + Aig_Man_t * pMan; + Aig_Obj_t * pMiter; + Vec_Int_t * vNodes; + Ivy_Obj_t * pObjIvy; + int i; + // collect nodes + vNodes = Vec_IntAlloc( 100 ); + Ivy_ManConst1(p)->fMarkB = 1; + Ivy_FraigExtractCone_rec( p, pObj1, vLeaves, vNodes ); + Ivy_FraigExtractCone_rec( p, pObj2, vLeaves, vNodes ); + Ivy_ManConst1(p)->fMarkB = 0; + // create new manager + pMan = Aig_ManStart( 1000 ); + Ivy_ManConst1(p)->pEquiv = (Ivy_Obj_t *)Aig_ManConst1(pMan); + Ivy_ManForEachNodeVec( p, vLeaves, pObjIvy, i ) + { + pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_ObjCreatePi( pMan ); + pObjIvy->fMarkB = 0; + } + // duplicate internal nodes + Ivy_ManForEachNodeVec( p, vNodes, pObjIvy, i ) + { + + pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pObjIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pObjIvy) ); + pObjIvy->fMarkB = 0; + + pMiter = (Aig_Obj_t *)pObjIvy->pEquiv; + assert( pMiter->fPhase == pObjIvy->fPhase ); + } + // create the PO + pMiter = Aig_Exor( pMan, (Aig_Obj_t *)pObj1->pEquiv, (Aig_Obj_t *)pObj2->pEquiv ); + pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); + +/* +printf( "Polarity = %d\n", pMiter->fPhase ); + if ( Ivy_ObjIsConst1(pObj1) || Ivy_ObjIsConst1(pObj2) ) + { + pMiter = Aig_NotCond( pMiter, 1 ); +printf( "***************\n" ); + } +*/ + pMiter = Aig_ObjCreatePo( pMan, pMiter ); +//printf( "Polarity = %d\n", pMiter->fPhase ); + Aig_ManCleanup( pMan ); + Vec_IntFree( vNodes ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Checks equivalence using BDDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit ) +{ + extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); + Vec_Int_t * vLeaves; + Aig_Man_t * pMan; + Aig_Obj_t * pObj; + int i, RetValue; + vLeaves = Vec_IntAlloc( 100 ); + pMan = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves ); + RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 1 ); + if ( RetValue == 0 ) + { + int Counter = 0; + memset( pGlo->pPatWords, 0, sizeof(unsigned) * pGlo->nPatWords ); + Aig_ManForEachPi( pMan, pObj, i ) + if ( ((int *)pMan->pData)[i] ) + { + int iObjIvy = Vec_IntEntry( vLeaves, i ); + assert( iObjIvy > 0 && iObjIvy <= Ivy_ManPiNum(p) ); + Ivy_InfoSetBit( pGlo->pPatWords, iObjIvy-1 ); +//printf( "%d ", iObjIvy ); +Counter++; + } + assert( Counter > 0 ); + } + Vec_IntFree( vLeaves ); + if ( RetValue == 1 ) + printf( "UNSAT\n" ); + else if ( RetValue == 0 ) + printf( "SAT\n" ); + else if ( RetValue == -1 ) + printf( "UNDEC\n" ); + +// p->pModel = (int *)pMan->pData, pMan2->pData = NULL; + Aig_ManStop( pMan ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3