| /**CFile**************************************************************** | |
| FileName [cecCec.c] | |
| SystemName [ABC: Logic synthesis and verification system.] | |
| PackageName [Combinational equivalence checking.] | |
| Synopsis [Integrated combinatinal equivalence checker.] | |
| Author [Alan Mishchenko] | |
| Affiliation [UC Berkeley] | |
| Date [Ver. 1.0. Started - June 20, 2005.] | |
| Revision [$Id: cecCec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] | |
| ***********************************************************************/ | |
| #include "cecInt.h" | |
| #include "proof/fra/fra.h" | |
| #include "aig/gia/giaAig.h" | |
| #include "misc/extra/extra.h" | |
| #include "sat/cnf/cnf.h" | |
| ABC_NAMESPACE_IMPL_START | |
| //////////////////////////////////////////////////////////////////////// | |
| /// DECLARATIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| //////////////////////////////////////////////////////////////////////// | |
| /// FUNCTION DEFINITIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| /**Function************************************************************* | |
| Synopsis [Saves the input pattern with the given number.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues ) | |
| { | |
| int i; | |
| assert( p->pCexComb == NULL ); | |
| p->pCexComb = Abc_CexAlloc( 0, Gia_ManCiNum(p), 1 ); | |
| p->pCexComb->iPo = iOut; | |
| for ( i = 0; i < Gia_ManCiNum(p); i++ ) | |
| if ( pValues && pValues[i] ) | |
| Abc_InfoSetBit( p->pCexComb->pData, i ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Interface to the old CEC engine] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime clkTotal, int fSilent ) | |
| { | |
| // extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ); | |
| extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs ); | |
| Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter ); | |
| Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 ); | |
| int RetValue, iOut, nOuts; | |
| if ( piOutFail ) | |
| *piOutFail = -1; | |
| Gia_ManStop( pTemp ); | |
| // run CEC on this miter | |
| RetValue = Fra_FraigCec( &pMiterCec, 10000000, fVerbose ); | |
| // report the miter | |
| if ( RetValue == 1 ) | |
| { | |
| if ( !fSilent ) | |
| { | |
| Abc_Print( 1, "Networks are equivalent. " ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); | |
| } | |
| } | |
| else if ( RetValue == 0 ) | |
| { | |
| if ( !fSilent ) | |
| { | |
| Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); | |
| } | |
| if ( pMiterCec->pData == NULL ) | |
| Abc_Print( 1, "Counter-example is not available.\n" ); | |
| else | |
| { | |
| iOut = Ssw_SecCexResimulate( pMiterCec, (int *)pMiterCec->pData, &nOuts ); | |
| if ( iOut == -1 ) | |
| Abc_Print( 1, "Counter-example verification has failed.\n" ); | |
| else | |
| { | |
| if ( !fSilent ) | |
| { | |
| Abc_Print( 1, "Primary output %d has failed", iOut ); | |
| if ( nOuts-1 >= 0 ) | |
| Abc_Print( 1, ", along with other %d incorrect outputs", nOuts-1 ); | |
| Abc_Print( 1, ".\n" ); | |
| } | |
| if ( piOutFail ) | |
| *piOutFail = iOut; | |
| } | |
| Cec_ManTransformPattern( pMiter, iOut, (int *)pMiterCec->pData ); | |
| } | |
| } | |
| else if ( !fSilent ) | |
| { | |
| Abc_Print( 1, "Networks are UNDECIDED. " ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); | |
| } | |
| fflush( stdout ); | |
| Aig_ManStop( pMiterCec ); | |
| return RetValue; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) | |
| { | |
| Gia_Obj_t * pObj1, * pObj2; | |
| Gia_Obj_t * pDri1, * pDri2; | |
| int i; | |
| abctime clk = Abc_Clock(); | |
| Gia_ManSetPhase( p ); | |
| Gia_ManForEachPo( p, pObj1, i ) | |
| { | |
| pObj2 = Gia_ManPo( p, ++i ); | |
| // check if they different on all-0 pattern | |
| // (for example, when they have the same driver but complemented) | |
| if ( Gia_ObjPhase(pObj1) != Gia_ObjPhase(pObj2) ) | |
| { | |
| if ( !pPars->fSilent ) | |
| { | |
| Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (different phase). ", i/2 ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); | |
| } | |
| pPars->iOutFail = i/2; | |
| Cec_ManTransformPattern( p, i/2, NULL ); | |
| return 0; | |
| } | |
| // get the drivers | |
| pDri1 = Gia_ObjFanin0(pObj1); | |
| pDri2 = Gia_ObjFanin0(pObj2); | |
| // drivers are different PIs | |
| if ( Gia_ObjIsPi(p, pDri1) && Gia_ObjIsPi(p, pDri2) && pDri1 != pDri2 ) | |
| { | |
| if ( !pPars->fSilent ) | |
| { | |
| Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (different PIs). ", i/2 ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); | |
| } | |
| pPars->iOutFail = i/2; | |
| Cec_ManTransformPattern( p, i/2, NULL ); | |
| // if their compl attributes are the same - one should be complemented | |
| assert( Gia_ObjFaninC0(pObj1) == Gia_ObjFaninC0(pObj2) ); | |
| Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri1) ); | |
| return 0; | |
| } | |
| // one of the drivers is a PI; another is a constant 0 | |
| if ( (Gia_ObjIsPi(p, pDri1) && Gia_ObjIsConst0(pDri2)) || | |
| (Gia_ObjIsPi(p, pDri2) && Gia_ObjIsConst0(pDri1)) ) | |
| { | |
| if ( !pPars->fSilent ) | |
| { | |
| Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d trivially differs (PI vs. constant). ", i/2 ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); | |
| } | |
| pPars->iOutFail = i/2; | |
| Cec_ManTransformPattern( p, i/2, NULL ); | |
| // the compl attributes are the same - the PI should be complemented | |
| assert( Gia_ObjFaninC0(pObj1) == Gia_ObjFaninC0(pObj2) ); | |
| if ( Gia_ObjIsPi(p, pDri1) ) | |
| Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri1) ); | |
| else | |
| Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri2) ); | |
| return 0; | |
| } | |
| } | |
| if ( Gia_ManAndNum(p) == 0 ) | |
| { | |
| if ( !pPars->fSilent ) | |
| { | |
| Abc_Print( 1, "Networks are equivalent. " ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); | |
| } | |
| return 1; | |
| } | |
| return -1; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Performs naive checking.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManVerifyNaive( Gia_Man_t * p, Cec_ParCec_t * pPars ) | |
| { | |
| Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 ); | |
| sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); | |
| Gia_Obj_t * pObj0, * pObj1; | |
| abctime clkStart = Abc_Clock(); | |
| int nPairs = Gia_ManPoNum(p)/2; | |
| int nUnsats = 0, nSats = 0, nUndecs = 0, nTrivs = 0; | |
| int i, iVar0, iVar1, pLits[2], status, RetValue; | |
| ProgressBar * pProgress = Extra_ProgressBarStart( stdout, nPairs ); | |
| assert( Gia_ManPoNum(p) % 2 == 0 ); | |
| for ( i = 0; i < nPairs; i++ ) | |
| { | |
| if ( (i & 0xFF) == 0 ) | |
| Extra_ProgressBarUpdate( pProgress, i, NULL ); | |
| pObj0 = Gia_ManPo(p, 2*i); | |
| pObj1 = Gia_ManPo(p, 2*i+1); | |
| if ( Gia_ObjChild0(pObj0) == Gia_ObjChild0(pObj1) ) | |
| { | |
| nUnsats++; | |
| nTrivs++; | |
| continue; | |
| } | |
| if ( pPars->TimeLimit && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->TimeLimit ) | |
| { | |
| printf( "Timeout (%d sec) is reached.\n", pPars->TimeLimit ); | |
| nUndecs = nPairs - nUnsats - nSats; | |
| break; | |
| } | |
| iVar0 = pCnf->pVarNums[ Gia_ObjId(p, pObj0) ]; | |
| iVar1 = pCnf->pVarNums[ Gia_ObjId(p, pObj1) ]; | |
| assert( iVar0 >= 0 && iVar1 >= 0 ); | |
| pLits[0] = Abc_Var2Lit( iVar0, 0 ); | |
| pLits[1] = Abc_Var2Lit( iVar1, 0 ); | |
| // check direct | |
| pLits[0] = lit_neg(pLits[0]); | |
| status = sat_solver_solve( pSat, pLits, pLits + 2, pPars->nBTLimit, 0, 0, 0 ); | |
| if ( status == l_False ) | |
| { | |
| pLits[0] = lit_neg( pLits[0] ); | |
| pLits[1] = lit_neg( pLits[1] ); | |
| RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 ); | |
| assert( RetValue ); | |
| } | |
| else if ( status == l_True ) | |
| { | |
| printf( "Output %d is SAT.\n", i ); | |
| nSats++; | |
| continue; | |
| } | |
| else | |
| { | |
| nUndecs++; | |
| continue; | |
| } | |
| // check inverse | |
| status = sat_solver_solve( pSat, pLits, pLits + 2, pPars->nBTLimit, 0, 0, 0 ); | |
| if ( status == l_False ) | |
| { | |
| pLits[0] = lit_neg( pLits[0] ); | |
| pLits[1] = lit_neg( pLits[1] ); | |
| RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 ); | |
| assert( RetValue ); | |
| } | |
| else if ( status == l_True ) | |
| { | |
| printf( "Output %d is SAT.\n", i ); | |
| nSats++; | |
| continue; | |
| } | |
| else | |
| { | |
| nUndecs++; | |
| continue; | |
| } | |
| nUnsats++; | |
| } | |
| Extra_ProgressBarStop( pProgress ); | |
| printf( "UNSAT = %6d. SAT = %6d. UNDEC = %6d. Trivial = %6d. ", nUnsats, nSats, nUndecs, nTrivs ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); | |
| Cnf_DataFree( pCnf ); | |
| sat_solver_delete( pSat ); | |
| if ( nSats ) | |
| return 0; | |
| if ( nUndecs ) | |
| return -1; | |
| return 1; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [New CEC engine.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) | |
| { | |
| int fDumpUndecided = 0; | |
| Cec_ParFra_t ParsFra, * pParsFra = &ParsFra; | |
| Gia_Man_t * p, * pNew; | |
| int RetValue; | |
| abctime clk = Abc_Clock(); | |
| abctime clkTotal = Abc_Clock(); | |
| // consider special cases: | |
| // 1) (SAT) a pair of POs have different value under all-0 pattern | |
| // 2) (SAT) a pair of POs has different PI/Const drivers | |
| // 3) (UNSAT) 1-2 do not hold and there is no nodes | |
| RetValue = Cec_ManHandleSpecialCases( pInit, pPars ); | |
| if ( RetValue == 0 || RetValue == 1 ) | |
| return RetValue; | |
| // preprocess | |
| p = Gia_ManDup( pInit ); | |
| Gia_ManEquivFixOutputPairs( p ); | |
| p = Gia_ManCleanup( pNew = p ); | |
| Gia_ManStop( pNew ); | |
| if ( pPars->fNaive ) | |
| { | |
| RetValue = Cec_ManVerifyNaive( p, pPars ); | |
| Gia_ManStop( p ); | |
| return RetValue; | |
| } | |
| // sweep for equivalences | |
| Cec_ManFraSetDefaultParams( pParsFra ); | |
| pParsFra->nItersMax = 1000; | |
| pParsFra->nBTLimit = pPars->nBTLimit; | |
| pParsFra->TimeLimit = pPars->TimeLimit; | |
| pParsFra->fVerbose = pPars->fVerbose; | |
| pParsFra->fCheckMiter = 1; | |
| pParsFra->fDualOut = 1; | |
| pNew = Cec_ManSatSweeping( p, pParsFra, pPars->fSilent ); | |
| pPars->iOutFail = pParsFra->iOutFail; | |
| // update | |
| pInit->pCexComb = p->pCexComb; p->pCexComb = NULL; | |
| Gia_ManStop( p ); | |
| p = pInit; | |
| // continue | |
| if ( pNew == NULL ) | |
| { | |
| if ( p->pCexComb != NULL ) | |
| { | |
| if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) ) | |
| Abc_Print( 1, "Counter-example simulation has failed.\n" ); | |
| if ( !pPars->fSilent ) | |
| { | |
| Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); | |
| } | |
| return 0; | |
| } | |
| p = Gia_ManDup( pInit ); | |
| Gia_ManEquivFixOutputPairs( p ); | |
| p = Gia_ManCleanup( pNew = p ); | |
| Gia_ManStop( pNew ); | |
| pNew = p; | |
| } | |
| if ( pPars->fVerbose ) | |
| { | |
| Abc_Print( 1, "Networks are UNDECIDED after the new CEC engine. " ); | |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); | |
| } | |
| if ( fDumpUndecided ) | |
| { | |
| ABC_FREE( pNew->pReprs ); | |
| ABC_FREE( pNew->pNexts ); | |
| Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 ); | |
| Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" ); | |
| } | |
| if ( pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit ) | |
| { | |
| Gia_ManStop( pNew ); | |
| return -1; | |
| } | |
| // call other solver | |
| if ( pPars->fVerbose ) | |
| Abc_Print( 1, "Calling the old CEC engine.\n" ); | |
| fflush( stdout ); | |
| RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail, clkTotal, pPars->fSilent ); | |
| p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL; | |
| if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) ) | |
| Abc_Print( 1, "Counter-example simulation has failed.\n" ); | |
| Gia_ManStop( pNew ); | |
| return RetValue; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Simple SAT run to check equivalence.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManVerifySimple( Gia_Man_t * p ) | |
| { | |
| Cec_ParCec_t ParsCec, * pPars = &ParsCec; | |
| Cec_ManCecSetDefaultParams( pPars ); | |
| pPars->fSilent = 1; | |
| assert( Gia_ManCoNum(p) == 2 ); | |
| assert( Gia_ManRegNum(p) == 0 ); | |
| return Cec_ManVerify( p, pPars ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [New CEC engine applied to two circuits.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose ) | |
| { | |
| Cec_ParCec_t ParsCec, * pPars = &ParsCec; | |
| Gia_Man_t * pMiter; | |
| int RetValue; | |
| Cec_ManCecSetDefaultParams( pPars ); | |
| pPars->fVerbose = fVerbose; | |
| pMiter = Gia_ManMiter( p0, p1, 0, 1, 0, 0, pPars->fVerbose ); | |
| if ( pMiter == NULL ) | |
| return -1; | |
| RetValue = Cec_ManVerify( pMiter, pPars ); | |
| p0->pCexComb = pMiter->pCexComb; pMiter->pCexComb = NULL; | |
| Gia_ManStop( pMiter ); | |
| return RetValue; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [New CEC engine applied to two circuits.] | |
| Description [Returns 1 if equivalent, 0 if counter-example, -1 if undecided. | |
| Counter-example is returned in the first manager as pAig0->pSeqModel. | |
| The format is given in Abc_Cex_t (file "abc\src\aig\gia\gia.h").] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose ) | |
| { | |
| Gia_Man_t * p0, * p1, * pTemp; | |
| int RetValue; | |
| p0 = Gia_ManFromAig( pAig0 ); | |
| p0 = Gia_ManCleanup( pTemp = p0 ); | |
| Gia_ManStop( pTemp ); | |
| p1 = Gia_ManFromAig( pAig1 ); | |
| p1 = Gia_ManCleanup( pTemp = p1 ); | |
| Gia_ManStop( pTemp ); | |
| RetValue = Cec_ManVerifyTwo( p0, p1, fVerbose ); | |
| pAig0->pSeqModel = p0->pCexComb; p0->pCexComb = NULL; | |
| Gia_ManStop( p0 ); | |
| Gia_ManStop( p1 ); | |
| return RetValue; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Implementation of new signal correspodence.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ) | |
| { | |
| Gia_Man_t * pGia; | |
| Cec_ParCor_t CorPars, * pCorPars = &CorPars; | |
| Cec_ManCorSetDefaultParams( pCorPars ); | |
| pCorPars->fLatchCorr = 1; | |
| pCorPars->fUseCSat = fUseCSat; | |
| pCorPars->nBTLimit = nConfs; | |
| pGia = Gia_ManFromAigSimple( pAig ); | |
| Cec_ManLSCorrespondenceClasses( pGia, pCorPars ); | |
| Gia_ManReprToAigRepr( pAig, pGia ); | |
| Gia_ManStop( pGia ); | |
| return Aig_ManDupSimple( pAig ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Implementation of new signal correspodence.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat ) | |
| { | |
| Gia_Man_t * pGia; | |
| Cec_ParCor_t CorPars, * pCorPars = &CorPars; | |
| Cec_ManCorSetDefaultParams( pCorPars ); | |
| pCorPars->fUseCSat = fUseCSat; | |
| pCorPars->nBTLimit = nConfs; | |
| pGia = Gia_ManFromAigSimple( pAig ); | |
| Cec_ManLSCorrespondenceClasses( pGia, pCorPars ); | |
| Gia_ManReprToAigRepr( pAig, pGia ); | |
| Gia_ManStop( pGia ); | |
| return Aig_ManDupSimple( pAig ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Implementation of fraiging.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose ) | |
| { | |
| Gia_Man_t * pGia; | |
| Cec_ParFra_t FraPars, * pFraPars = &FraPars; | |
| Cec_ManFraSetDefaultParams( pFraPars ); | |
| pFraPars->fSatSweeping = 1; | |
| pFraPars->nBTLimit = nConfs; | |
| pFraPars->nItersMax = 20; | |
| pFraPars->fVerbose = fVerbose; | |
| pGia = Gia_ManFromAigSimple( pAig ); | |
| Cec_ManSatSweeping( pGia, pFraPars, 0 ); | |
| Gia_ManReprToAigRepr( pAig, pGia ); | |
| Gia_ManStop( pGia ); | |
| return Aig_ManDupSimple( pAig ); | |
| } | |
| //////////////////////////////////////////////////////////////////////// | |
| /// END OF FILE /// | |
| //////////////////////////////////////////////////////////////////////// | |
| ABC_NAMESPACE_IMPL_END | |