Home
last modified time | relevance | path

Searched refs:pCexState (Results 1 – 2 of 2) sorted by relevance

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/
H A DbmcCexTools.c556 assert( pCexState->nRegs == 0 ); in Bmc_CexCareBits()
559 pNew->iFrame = pCexState->iFrame; in Bmc_CexCareBits()
560 pNew->iPo = pCexState->iPo; in Bmc_CexCareBits()
569 iBit = pCexState->nPis * i; in Bmc_CexCareBits()
597 if ( i == pCexState->iFrame ) in Bmc_CexCareBits()
649 assert( pCexState->nRegs == 0 ); in Bmc_CexEssentialBitOne()
656 pNew->iPo = pCexState->iPo; in Bmc_CexEssentialBitOne()
662 for ( i = iBit / pCexState->nPis; i <= pCexState->iFrame; i++ ) in Bmc_CexEssentialBitOne()
666 pObj->fMark0 = Abc_InfoHasBit( pCexState->pData, i * pCexState->nPis + k ); in Bmc_CexEssentialBitOne()
689 if ( i < pCexState->iFrame ) in Bmc_CexEssentialBitOne()
[all …]
H A DbmcCexDepth.c31 extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc…