diff options
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bmc/bmcCexDepth.c | 421 | ||||
-rw-r--r-- | src/sat/bmc/module.make | 1 |
2 files changed, 422 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c new file mode 100644 index 00000000..b28a7ba7 --- /dev/null +++ b/src/sat/bmc/bmcCexDepth.c @@ -0,0 +1,421 @@ +/**CFile**************************************************************** + + FileName [bmcCexDepth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [CEX depth minimization.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcCexDepth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose ); +extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose ); +extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Existentially quantified given variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + assert( iVar >= 0 && iVar < Gia_ManPiNum(p) ); + assert( Gia_ManPoNum(p) == 1 ); + assert( Gia_ManRegNum(p) == 0 ); + Gia_ManFillValue( p ); + // find the cofactoring variable + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + // compute negative cofactor + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + // compute the positive cofactor + Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // create OR gate + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, pObj->Value, Gia_ObjFanin0Copy(pObj)) ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Performs targe enlargement of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Bmc_CexTargetEnlarge( Gia_Man_t * p, int nFrames ) +{ + Gia_Man_t * pNew, * pOne; + Gia_Obj_t * pObj, * pObjRo; + int i, k; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + for ( k = 0; k < nFrames; k++ ) + Gia_ManForEachPi( p, pObj, i ) + Gia_ManAppendCi( pNew ); + Gia_ManForEachRo( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + for ( k = 0; k < nFrames; k++ ) + { + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManCiLit( pNew, (nFrames - 1 - k) * Gia_ManPiNum(p) + i ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachRiRo( p, pObj, pObjRo, i ) + pObjRo->Value = pObj->Value; + } + pObj = Gia_ManPo( p, 0 ); + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pOne = pNew ); + Gia_ManStop( pOne ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Create target with quantified inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames ) +{ + Gia_Man_t * pNew, * pTemp; + int i, Limit = nFrames * Gia_ManPiNum(p); + pNew = Bmc_CexTargetEnlarge( p, nFrames ); + for ( i = 0; i < Limit; i++ ) + { + printf( "%3d : ", i ); + if ( i % Gia_ManPiNum(p) == 0 ) + Gia_ManPrintStats( pNew, 0, 0, 0 ); + pNew = Gia_ManDupExist( pTemp = pNew, i ); + Gia_ManStop( pTemp ); + } + Gia_ManPrintStats( pNew, 0, 0, 0 ); + pNew = Gia_ManDupLastPis( pTemp = pNew, Gia_ManRegNum(p) ); + Gia_ManStop( pTemp ); + Gia_ManPrintStats( pNew, 0, 0, 0 ); + pTemp = Gia_ManDupAppendCones( p, &pNew, 1, 1 ); + Gia_ManStop( pNew ); + Gia_AigerWrite( pTemp, "miter3.aig", 0, 0 ); + return pTemp; +} + +/**Function************************************************************* + + Synopsis [Computes CE-induced network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Bmc_CexBuildNetwork2( Gia_Man_t * p, Abc_Cex_t * pCex, int fStart ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int fCompl0, fCompl1; + int i, k, iBit; + assert( pCex->nRegs == 0 ); + assert( pCex->nPis == Gia_ManCiNum(p) ); + assert( fStart <= pCex->iFrame ); + // start the manager + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( "unate" ); + // set const0 + Gia_ManConst0(p)->fMark0 = 0; // value + Gia_ManConst0(p)->fMark1 = 1; // care + Gia_ManConst0(p)->Value = ~0; + // set init state + Gia_ManForEachRi( p, pObj, k ) + { + pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k ); + pObj->fMark1 = 0; + pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 ); + } + Gia_ManHashAlloc( pNew ); + iBit = pCex->nRegs + fStart * Gia_ManCiNum(p); + for ( i = fStart; i <= pCex->iFrame; i++ ) + { + // primary inputs + Gia_ManForEachPi( p, pObj, k ) + { + pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ ); + pObj->fMark1 = 1; + pObj->Value = ~0; + } + iBit += Gia_ManRegNum(p); + // transfer + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + { + pObjRo->fMark0 = pObjRi->fMark0; + pObjRo->fMark1 = pObjRi->fMark1; + pObjRo->Value = pObjRi->Value; + } + // internal nodes + Gia_ManForEachAnd( p, pObj, k ) + { + fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj); + pObj->fMark0 = fCompl0 & fCompl1; + if ( pObj->fMark0 ) + pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1; + else if ( !fCompl0 && !fCompl1 ) + pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1; + else if ( !fCompl0 ) + pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1; + else if ( !fCompl1 ) + pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1; + else assert( 0 ); + pObj->Value = ~0; + if ( pObj->fMark1 ) + continue; + if ( pObj->fMark0 ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 && !fCompl1 ) + pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 ) + pObj->Value = Gia_ObjFanin0(pObj)->Value; + else if ( !fCompl1 ) + pObj->Value = Gia_ObjFanin1(pObj)->Value; + else assert( 0 ); + assert( pObj->Value > 0 ); + } + // combinational outputs + Gia_ManForEachCo( p, pObj, k ) + { + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1; + pObj->Value = Gia_ObjFanin0(pObj)->Value; + } + } + Gia_ManHashStop( pNew ); + assert( iBit == pCex->nBits ); + // create primary output + pObj = Gia_ManPo(p, pCex->iPo); + assert( pObj->fMark0 == 1 ); + assert( pObj->fMark1 == 0 ); + assert( pObj->Value > 0 ); + Gia_ManAppendCo( pNew, pObj->Value ); + // cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} +Gia_Man_t * Bmc_CexBuildNetwork2_( Gia_Man_t * p, Abc_Cex_t * pCex, int fStart ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int fCompl0, fCompl1; + int i, k, iBit; + assert( pCex->nRegs == 0 ); + assert( pCex->nPis == Gia_ManCiNum(p) ); + assert( fStart <= pCex->iFrame ); + // start the manager + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( "unate" ); + // set const0 + Gia_ManConst0(p)->fMark0 = 0; // value + Gia_ManConst0(p)->Value = 1; + // set init state + Gia_ManForEachRi( p, pObj, k ) + { + pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k ); + pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 ); + } + Gia_ManHashAlloc( pNew ); + iBit = pCex->nRegs + fStart * Gia_ManCiNum(p); + for ( i = fStart; i <= pCex->iFrame; i++ ) + { + // primary inputs + Gia_ManForEachPi( p, pObj, k ) + { + pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ ); + pObj->Value = 1; + } + iBit += Gia_ManRegNum(p); + // transfer + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + { + pObjRo->fMark0 = pObjRi->fMark0; + pObjRo->Value = pObjRi->Value; + } + // internal nodes + Gia_ManForEachAnd( p, pObj, k ) + { + fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj); + pObj->fMark0 = fCompl0 & fCompl1; + if ( pObj->fMark0 ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 && !fCompl1 ) + pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 ) + pObj->Value = Gia_ObjFanin0(pObj)->Value; + else if ( !fCompl1 ) + pObj->Value = Gia_ObjFanin1(pObj)->Value; + else assert( 0 ); + } + // combinational outputs + Gia_ManForEachCo( p, pObj, k ) + { + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + pObj->Value = Gia_ObjFanin0(pObj)->Value; + } + } + Gia_ManHashStop( pNew ); + assert( iBit == pCex->nBits ); + // create primary output + pObj = Gia_ManPo(p, pCex->iPo); + assert( pObj->fMark0 == 1 ); + assert( pObj->Value > 0 ); + Gia_ManAppendCo( pNew, pObj->Value ); + // cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFramesMax ) +{ + Gia_Man_t * pNew, * pTemp; + Vec_Ptr_t * vCones; + clock_t clk = clock(); + int i; + nFramesMax = Abc_MinInt( nFramesMax, pCex->iFrame ); + printf( "Processing CEX in frame %d (max frames %d).\n", pCex->iFrame, nFramesMax ); + vCones = Vec_PtrAlloc( nFramesMax ); + for ( i = pCex->iFrame; i > pCex->iFrame - nFramesMax; i-- ) + { + printf( "Frame %5d : ", i ); + pNew = Bmc_CexBuildNetwork2_( p, pCex, i ); + Gia_ManPrintStats( pNew, 0, 0, 0 ); + Vec_PtrPush( vCones, pNew ); + } + pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 ); + Gia_AigerWrite( pNew, "miter2.aig", 0, 0 ); +//Bmc_CexDumpAogStats( pNew, clock() - clk ); + Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i ) + Gia_ManStop( pTemp ); + Vec_PtrFree( vCones ); + printf( "GIA with additional properties is written into \"miter2.aig\".\n" ); +// printf( "CE-induced network is written into file \"unate.aig\".\n" ); + Abc_PrintTime( 1, "Time", clock() - clk ); +// Gia_ManStop( pNew ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int fVerbose ) +{ + Gia_Man_t * pNew; + clock_t clk = clock(); + Abc_Cex_t * pCexImpl = NULL; + Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose ); + Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose ); +// Abc_Cex_t * pCexEss, * pCexMin; + + if ( !Bmc_CexVerify( p, pCex, pCexCare ) ) + printf( "Counter-example care-set verification has failed.\n" ); + +// pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose ); +// pCexMin = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose ); + +// if ( !Bmc_CexVerify( p, pCex, pCexMin ) ) +// printf( "Counter-example min-set verification has failed.\n" ); + +// Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, clock() - clk ); + + Abc_PrintTime( 1, "Time", clock() - clk ); + pNew = Bmc_CexBuildNetwork2Test( p, pCexStates, nFrames ); +// Bmc_CexPerformUnrollingTest( p, pCex ); + + Abc_CexFreeP( &pCexStates ); + Abc_CexFreeP( &pCexImpl ); + Abc_CexFreeP( &pCexCare ); +// Abc_CexFreeP( &pCexEss ); +// Abc_CexFreeP( &pCexMin ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index fd50ec23..1ac04203 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -2,6 +2,7 @@ SRC += src/sat/bmc/bmcBmc.c \ src/sat/bmc/bmcBmc2.c \ src/sat/bmc/bmcBmc3.c \ src/sat/bmc/bmcCexCut.c \ + src/sat/bmc/bmcCexDepth.c \ src/sat/bmc/bmcCexMin1.c \ src/sat/bmc/bmcCexMin2.c \ src/sat/bmc/bmcCexTools.c \ |