From 2140c5d980cafc6d3daece9e6f2e04dc3cc1fb44 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 1 May 2011 15:36:39 -0700 Subject: Updating testcext to ignore the diff in register count and other things. --- src/aig/cec/cecSeq.c | 4 ++-- src/aig/gia/giaUtil.c | 8 ++++--- src/aig/saig/saig.h | 1 + src/aig/saig/saigBmc3.c | 59 +++++++++++++++++++++++++++++++++++++++++++++---- src/base/abci/abc.c | 41 +++++++++++++++++++++++++--------- 5 files changed, 93 insertions(+), 20 deletions(-) diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c index 0e49cd7c..e9f3df37 100644 --- a/src/aig/cec/cecSeq.c +++ b/src/aig/cec/cecSeq.c @@ -242,8 +242,8 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Abc_Cex 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" ); +// if ( RetValue && pPars->fCheckMiter ) +// Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" ); return RetValue; } diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 125f3592..d94a0412 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1191,9 +1191,11 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) { Gia_Obj_t * pObj, * pObjRi, * pObjRo; int RetValue, i, k, iBit = 0; + assert( Gia_ManPiNum(pAig) == p->nPis ); Gia_ManCleanMark0(pAig); - Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); +// Gia_ManForEachRo( pAig, pObj, i ) +// pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + iBit = p->nRegs; for ( i = 0; i <= p->iFrame; i++ ) { Gia_ManForEachPi( pAig, pObj, k ) @@ -1207,7 +1209,7 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) pObjRo->fMark0 = pObjRi->fMark0; } assert( iBit == p->nBits ); - // remember the number of failed output + // figure out the number of failed output RetValue = -1; for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- ) { diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 62ac35ac..c21ac625 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -62,6 +62,7 @@ struct Saig_ParBmc_t_ int nFramesMax; // maximum number of timeframes int nConfLimit; // maximum number of conflicts at a node int nTimeOut; // approximate timeout in seconds + int nPisAbstract; // the number of PIs to abstract int fSolveAll; // does not stop at the first SAT output int fDropSatOuts; // replace sat outputs by constant 0 int fVerbose; // verbose diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index e038d7a0..d82b4c39 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -551,10 +551,6 @@ void Saig_ManBmcMappingTest( Aig_Man_t * p ) - - - - /**Function************************************************************* Synopsis [Create manager.] @@ -613,6 +609,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig ) ***********************************************************************/ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) { + Aig_ManCleanMarkA( p->pAig ); if ( p->vCexes ) { assert( p->pAig->pSeqModelVec == NULL ); @@ -1000,6 +997,58 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) +/**Function************************************************************* + + Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeCompareRefsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) +{ + int Diff = Aig_ObjRefs(*pp1) - Aig_ObjRefs(*pp2); + if ( Diff > 0 ) + return -1; + if ( Diff < 0 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Mark PIs to be skipped based on nPisAbstract.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract ) +{ + Vec_Ptr_t * vPis; + Aig_Obj_t * pObj; + int i; + if ( nPisAbstract < 1 ) + return; + // sort PIs by the number of their fanouts +// Saig_ManForEachPi( pAig, pObj, i ) +// printf( "%d=%d ", i, Aig_ObjRefs(pObj) ); +// printf( "\n" ); + vPis = Vec_PtrAlloc( 100 ); + Saig_ManForEachPi( pAig, pObj, i ) + Vec_PtrPush( vPis, pObj ); + Vec_PtrSort( vPis, (int (*)(void))Aig_NodeCompareRefsDecrease ); + Vec_PtrForEachEntry( Aig_Obj_t *, vPis, pObj, i ) + if ( i > Saig_ManPiNum(pAig) - nPisAbstract ) + pObj->fMarkA = 1; +} + /**Function************************************************************* Synopsis [This procedure sets default parameters.] @@ -1018,6 +1067,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ) p->nFramesMax = 2000; // maximum number of timeframes p->nConfLimit = 2000; // maximum number of conflicts at a node p->nTimeOut = 0; // approximate timeout in seconds + p->nPisAbstract = 0; // the number of PIs to abstract p->fSolveAll = 0; // stops on the first SAT instance p->fDropSatOuts = 0; // replace sat outputs by constant 0 p->fVerbose = 0; // verbose @@ -1058,6 +1108,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) if ( p->pPars->nTimeOut ) sat_solver_set_runtime_limit( p->pSat, clock() + p->pPars->nTimeOut * CLOCKS_PER_SEC ); // perform frames +// Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract ); for ( f = 0; f < pPars->nFramesMax; f++ ) { pPars->iFrame = f; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1f15592d..10360809 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8544,7 +8544,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut ); // Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" ); // Ssm_ManExperiment( "m\\big3.ssim", "m\\big3_.ssim" ); - Ssm_ManExperiment( "m\\tb.ssim", "m\\tb_.ssim" ); +// Ssm_ManExperiment( "m\\tb.ssim", "m\\tb_.ssim" ); + Ssm_ManExperiment( "m\\simp.ssim", "m\\simp_.ssim" ); +} +*/ +/* +{ + Gia_Man_t * pGia = Abc_ManReadAig( "bug\\61\\tmp.out", "aig:" ); + Gia_ManStop( pGia ); } */ return 0; @@ -18340,7 +18347,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Saig_ParBmcSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCLsdrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCILsdrvh" ) ) != EOF ) { switch ( c ) { @@ -18388,6 +18395,17 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nConfLimit < 0 ) goto usage; break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nPisAbstract = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nPisAbstract < 0 ) + goto usage; + break; case 'L': if ( globalUtilOptind >= argc ) { @@ -18454,12 +18472,13 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: bmc3 [-SFTC num] [-L file] [-sdvh]\n" ); + Abc_Print( -2, "usage: bmc3 [-SFTCI num] [-L file] [-sdvh]\n" ); Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" ); Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nConfLimit ); + Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); Abc_Print( -2, "\t-s : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-d : drops (replaces by 0) satisfiable outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" ); @@ -19831,10 +19850,10 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Main AIG: The current network is not an AIG.\n"); else if ( Abc_NtkPiNum(pNtk) != pAbc->pCex->nPis ) Abc_Print( 1, "Main AIG: The number of PIs (%d) is different from cex (%d).\n", Abc_NtkPiNum(pNtk), pAbc->pCex->nPis ); - else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs ) - Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs ); - else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo ) - Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo ); +// else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs ) +// Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs ); +// else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo ) +// Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo ); else { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); @@ -19860,10 +19879,10 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "And AIG: There is no current network.\n"); else if ( Gia_ManPiNum(pAbc->pGia) != pAbc->pCex->nPis ) Abc_Print( 1, "And AIG: The number of PIs (%d) is different from cex (%d).\n", Gia_ManPiNum(pAbc->pGia), pAbc->pCex->nPis ); - else if ( Gia_ManRegNum(pAbc->pGia) != pAbc->pCex->nRegs ) - Abc_Print( 1, "And AIG: The number of registers (%d) is different from cex (%d).\n", Gia_ManRegNum(pAbc->pGia), pAbc->pCex->nRegs ); - else if ( Gia_ManPoNum(pAbc->pGia) <= pAbc->pCex->iPo ) - Abc_Print( 1, "And AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo ); +// else if ( Gia_ManRegNum(pAbc->pGia) != pAbc->pCex->nRegs ) +// Abc_Print( 1, "And AIG: The number of registers (%d) is different from cex (%d).\n", Gia_ManRegNum(pAbc->pGia), pAbc->pCex->nRegs ); +// else if ( Gia_ManPoNum(pAbc->pGia) <= pAbc->pCex->iPo ) +// Abc_Print( 1, "And AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo ); else { // if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) ) -- cgit v1.2.3