diff options
Diffstat (limited to 'src/proof/cec/cecSeq.c')
-rw-r--r-- | src/proof/cec/cecSeq.c | 448 |
1 files changed, 448 insertions, 0 deletions
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c new file mode 100644 index 00000000..21ed8656 --- /dev/null +++ b/src/proof/cec/cecSeq.c @@ -0,0 +1,448 @@ +/**CFile**************************************************************** + + FileName [cecSeq.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinational equivalence checking.] + + Synopsis [Refinement of sequential equivalence classes.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cecInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Sets register values from the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex ) +{ + unsigned * pInfo; + int k, i, w, nWords; + assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) ); + assert( pCex->nBits - pCex->nRegs + Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) ); + nWords = Vec_PtrReadWordsSimInfo( vInfo ); +/* + // user register values + assert( pCex->nRegs == Gia_ManRegNum(pAig) ); + for ( k = 0; k < pCex->nRegs; k++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Abc_InfoHasBit( pCex->pData, k )? ~0 : 0; + } +*/ + // print warning about register values + for ( k = 0; k < pCex->nRegs; k++ ) + if ( Abc_InfoHasBit( pCex->pData, k ) ) + break; + if ( k < pCex->nRegs ) + Abc_Print( 0, "The CEX has flop values different from 0, but they are currently not used by \"resim\".\n" ); + + // assign zero register values + for ( k = 0; k < Gia_ManRegNum(pAig); k++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = 0; + } + for ( i = pCex->nRegs; i < pCex->nBits; i++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k++ ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Gia_ManRandom(0); + // set simulation pattern and make sure it is second (first will be erased during simulation) + pInfo[0] = (pInfo[0] << 1) | Abc_InfoHasBit( pCex->pData, i ); + pInfo[0] <<= 1; + } + for ( ; k < Vec_PtrSize(vInfo); k++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Gia_ManRandom(0); + } +} + +/**Function************************************************************* + + Synopsis [Sets register values from the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex ) +{ + unsigned * pInfo; + int k, w, nWords; + nWords = Vec_PtrReadWordsSimInfo( vInfo ); + assert( pCex == NULL || Gia_ManRegNum(pAig) == pCex->nRegs ); + assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) ); + for ( k = 0; k < Gia_ManRegNum(pAig); k++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = (pCex && Abc_InfoHasBit(pCex->pData, k))? ~0 : 0; + } + + for ( ; k < Vec_PtrSize(vInfo); k++ ) + { + pInfo = (unsigned *)Vec_PtrEntry( vInfo, k ); + for ( w = 0; w < nWords; w++ ) + pInfo[w] = Gia_ManRandom( 0 ); + } +} + +/**Function************************************************************* + + Synopsis [Resimulates the classes using sequential simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo ) +{ + unsigned * pInfo0, * pInfo1; + int f, i, k, w; +// assert( Gia_ManRegNum(p->pAig) > 0 ); + assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames ); + for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ ) + { + pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k ); + pInfo1 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k ); + for ( w = 0; w < p->nWords; w++ ) + pInfo1[w] = pInfo0[w]; + } + for ( f = 0; f < p->pPars->nFrames; f++ ) + { + for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ ) + { + pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k++ ); + pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i ); + for ( w = 0; w < p->nWords; w++ ) + pInfo1[w] = pInfo0[w]; + } + for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) + { + pInfo0 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i ); + pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i ); + for ( w = 0; w < p->nWords; w++ ) + pInfo1[w] = pInfo0[w]; + } + if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) ) + return 1; + } + assert( k == Vec_PtrSize(vInfo) ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Resimulates information to refine equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter ) +{ + Cec_ParSim_t ParsSim, * pParsSim = &ParsSim; + Cec_ManSim_t * pSim; + int RetValue, clkTotal = clock(); + assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 ); + Cec_ManSimSetDefaultParams( pParsSim ); + pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig); + pParsSim->nWords = Vec_PtrReadWordsSimInfo( vSimInfo ); + pParsSim->fCheckMiter = fCheckMiter; + Gia_ManSetRefs( pAig ); + pSim = Cec_ManSimStart( pAig, pParsSim ); + if ( pBestState ) + pSim->pBestState = pBestState; + RetValue = Cec_ManSeqResimulate( pSim, vSimInfo ); + pSim->pBestState = NULL; + Cec_ManSimStop( pSim ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Resimuates one counter-example to refine equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex_t * pCex ) +{ + Vec_Ptr_t * vSimInfo; + int RetValue, clkTotal = clock(); + if ( pCex == NULL ) + { + Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" ); + return -1; + } + if ( pAig->pReprs == NULL ) + { + Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" ); + return -1; + } + if ( Gia_ManRegNum(pAig) == 0 ) + { + Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" ); + return -1; + } +// if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis ) + if ( Gia_ManPiNum(pAig) != pCex->nPis ) + { + Abc_Print( 1, "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" ); + return -1; + } + if ( pPars->fVerbose ) + Abc_Print( 1, "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 ); + Gia_ManRandom( 1 ); + vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + + Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 ); + Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex ); + if ( pPars->fVerbose ) + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL, pPars->fCheckMiter ); + if ( pPars->fVerbose ) + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + Vec_PtrFree( vSimInfo ); + if ( pPars->fVerbose ) + ABC_PRT( "Time", clock() - clkTotal ); +// if ( RetValue && pPars->fCheckMiter ) +// Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [Returns the number of POs that are not const0 cands.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig ) +{ + Gia_Obj_t * pObj; + int i, Counter = 0; + if ( pAig->pReprs == NULL ) + return -1; + Gia_ManForEachPo( pAig, pObj, i ) + if ( !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, pObj) ) ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns the number of POs that are not const0 cands.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig ) +{ + Gia_Obj_t * pObj; + int i, RetValue = 0; + if ( pAig->pReprs == NULL ) + return 0; + // label internal nodes driving POs + Gia_ManForEachPo( pAig, pObj, i ) + Gia_ObjFanin0(pObj)->fMark0 = 1; + // check if there are non-labled equivs + Gia_ManForEachObj( pAig, pObj, i ) + if ( Gia_ObjIsCand(pObj) && !pObj->fMark0 && Gia_ObjRepr(pAig, i) != GIA_VOID ) + { + RetValue = 1; + break; + } + // clean internal nodes driving POs + Gia_ManForEachPo( pAig, pObj, i ) + Gia_ObjFanin0(pObj)->fMark0 = 0; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Performs semiformal refinement of equivalence classes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars ) +{ + int nAddFrames = 16; // additional timeframes to simulate + int nCountNoRef = 0; + int nFramesReal; + Cec_ParSat_t ParsSat, * pParsSat = &ParsSat; + Vec_Ptr_t * vSimInfo; + Vec_Str_t * vStatus; + Abc_Cex_t * pState; + Gia_Man_t * pSrm, * pReduce, * pAux; + int r, nPats, RetValue = 0; + if ( pAig->pReprs == NULL ) + { + Abc_Print( 1, "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" ); + return -1; + } + if ( Gia_ManRegNum(pAig) == 0 ) + { + Abc_Print( 1, "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" ); + return -1; + } + Gia_ManRandom( 1 ); + // prepare starting pattern + pState = Abc_CexAlloc( Gia_ManRegNum(pAig), 0, 0 ); + pState->iFrame = -1; + pState->iPo = -1; + // prepare SAT solving + Cec_ManSatSetDefaultParams( pParsSat ); + pParsSat->nBTLimit = pPars->nBTLimit; + pParsSat->fVerbose = pPars->fVerbose; + if ( pParsSat->fVerbose ) + { + Abc_Print( 1, "Starting: " ); + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + } + // perform the given number of BMC rounds + Gia_ManCleanMark0( pAig ); + for ( r = 0; r < pPars->nRounds; r++ ) + { + if ( !Cec_ManCheckNonTrivialCands(pAig) ) + { + Abc_Print( 1, "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" ); + break; + } +// Abc_CexPrint( pState ); + // derive speculatively reduced model +// pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut ); + pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs ); + if ( pSrm == NULL ) + { + Abc_Print( 1, "Quitting refinement because miter could not be unrolled.\n" ); + break; + } + assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * nFramesReal) ); + if ( pPars->fVerbose ) + Abc_Print( 1, "Unrolled for %d frames.\n", nFramesReal ); + // allocate room for simulation info + vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + + Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords ); + Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState ); + // fill in simulation info with counter-examples + vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats ); + Vec_StrFree( vStatus ); + Gia_ManStop( pSrm ); + // resimulate and refine the classes + RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState, pPars->fCheckMiter ); + Vec_PtrFree( vSimInfo ); + assert( pState->iPo >= 0 ); // hit counter + pState->iPo = -1; + if ( pPars->fVerbose ) + { + Abc_Print( 1, "BMC = %3d ", nPats ); + Gia_ManEquivPrintClasses( pAig, 0, 0 ); + } + + // write equivalence classes + Gia_WriteAiger( pAig, "gore.aig", 0, 0 ); + // reduce the model + pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 ); + if ( pReduce ) + { + pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 ); + Gia_ManStop( pAux ); + Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 ); +// Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" ); +// Gia_ManPrintStatsShort( pReduce ); + Gia_ManStop( pReduce ); + } + + if ( RetValue ) + { + Abc_Print( 1, "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" ); + break; + } + // decide when to stop + if ( nPats > 0 ) + nCountNoRef = 0; + else if ( ++nCountNoRef == pPars->nNonRefines ) + break; + } + ABC_FREE( pState ); + if ( pPars->fCheckMiter ) + { + int nNonConsts = Cec_ManCountNonConstOutputs( pAig ); + if ( nNonConsts ) + Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts ); + } + return RetValue; +} + +//&r s13207.aig; &ps; ≡ &ps; &semi -R 2 -vm +//&r bug/50/temp.aig; &ps; &equiv -smv; &semi -v +//r mentor/1_05c.blif; st; &get; &ps; &equiv -smv; &semi -mv +//&r bug/50/hdl1.aig; &ps; &equiv -smv; &semi -mv; &srm; &r gsrm.aig; &ps + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |