diff options
Diffstat (limited to 'src/sat/bmc/bmcMulti.c')
-rw-r--r-- | src/sat/bmc/bmcMulti.c | 52 |
1 files changed, 48 insertions, 4 deletions
diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c index 35029034..cf04ab62 100644 --- a/src/sat/bmc/bmcMulti.c +++ b/src/sat/bmc/bmcMulti.c @@ -75,6 +75,34 @@ Vec_Int_t * Gia_ManProcessOutputs( Vec_Ptr_t * vCexesIn, Vec_Ptr_t * vCexesOut, /**Function************************************************************* + Synopsis [Counts the number of constant 0 POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCountConst0PosGia( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, Counter = 0; + Gia_ManForEachPo( p, pObj, i ) + Counter += (Gia_ObjFaninLit0p(p, pObj) == 0); + return Counter; +} +int Gia_ManCountConst0Pos( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, Counter = 0; + Saig_ManForEachPo( p, pObj, i ) + Counter += (Aig_ObjChild0(pObj) == Aig_ManConst0(p)); + return Counter; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -138,18 +166,23 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) Vec_Ptr_t * vCexes; Aig_Man_t * pTemp; abctime clkStart = Abc_Clock(); - int nTimeToStop = pPars->TimeOutGlo ? pPars->TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0; + abctime nTimeToStop = pPars->TimeOutGlo ? Abc_Clock() + pPars->TimeOutGlo * CLOCKS_PER_SEC : 0; int nTotalPo = Saig_ManPoNum(p); int nTotalSize = Aig_ManObjNum(p); int TimeOutLoc = pPars->TimeOutLoc; int i, RetValue = -1; if ( pPars->fVerbose ) - printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc ); + printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n", + pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc ); + if ( pPars->fVerbose ) + printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n", + pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose ); // create output map vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs vCexes = Vec_PtrStart( Saig_ManPoNum(p) ); // maps solved outputs into their CEXes (or markers) for ( i = 0; i < 1000; i++ ) { + int nSolved = Vec_PtrCountZero(vCexes); // perform SIM3 Ssw_RarSetDefaultParams( pParsSim ); pParsSim->fSolveAll = 1; @@ -157,6 +190,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) pParsSim->fSilent = !pPars->fVeryVerbose; pParsSim->TimeOut = TimeOutLoc; pParsSim->nRandSeed = (i * 17) % 500; + pParsSim->nWords = 5; RetValue *= Ssw_RarSimulate( p, pParsSim ); // sort outputs if ( p->vSeqModelVec ) @@ -173,7 +207,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart ); // check timeout - if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop ) + if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop ) { printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo ); break; @@ -185,6 +219,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) pParsBmc->fNotVerbose = 1; pParsBmc->fSilent = !pPars->fVeryVerbose; pParsBmc->nTimeOut = TimeOutLoc; + pParsBmc->nTimeOutOne = pPars->TimePerOut; RetValue *= Saig_ManBmcScalable( p, pParsBmc ); if ( pPars->fVeryVerbose ) Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n", @@ -204,12 +239,19 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart ); // check timeout - if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop ) + if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop ) { printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo ); break; } + // check gap timeout + if ( pPars->TimeOutGap && pPars->TimeOutGap <= TimeOutLoc && nSolved == Vec_PtrCountZero(vCexes) ) + { + printf( "Gap timeout (%d sec) is reached.\n", pPars->TimeOutGap ); + break; + } + // synthesize if ( pPars->fUseSyn ) { @@ -223,6 +265,8 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars ) TimeOutLoc += TimeOutLoc * pPars->TimeOutInc / 100; } Vec_IntFree( vOutMap ); + if ( pPars->fVerbose ) + printf( "The number of POs proved UNSAT by synthesis = %d.\n", Gia_ManCountConst0Pos(p) ); if ( pPars->fDumpFinal ) { char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" ); |