diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-11-02 17:35:47 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-11-02 17:35:47 -0800 |
commit | b4cf2f7448f1bd85c7f4f33daeed14a5f7cac602 (patch) | |
tree | 9ad178acb6aaab6e00a62541f01e5363ef201b99 /src | |
parent | 91885a6298e9df317f18658422f856bd4070a3b3 (diff) | |
download | abc-b4cf2f7448f1bd85c7f4f33daeed14a5f7cac602.tar.gz abc-b4cf2f7448f1bd85c7f4f33daeed14a5f7cac602.tar.bz2 abc-b4cf2f7448f1bd85c7f4f33daeed14a5f7cac602.zip |
Added switches '-c' and '-n' to 'init'.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/saig/saigDup.c | 64 | ||||
-rw-r--r-- | src/base/abci/abc.c | 60 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 2 |
3 files changed, 113 insertions, 13 deletions
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index cd978717..dabdf539 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -315,6 +315,70 @@ int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ) SeeAlso [] ***********************************************************************/ +int Saig_ManVerifyCexNoClear( Aig_Man_t * pAig, Abc_Cex_t * p ) +{ + Aig_Obj_t * pObj, * pObjRi, * pObjRo; + int RetValue, i, k, iBit = 0; + Aig_ManCleanMarkB(pAig); + Aig_ManConst1(pAig)->fMarkB = 1; + Saig_ManForEachLo( pAig, pObj, i ) + pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++); + for ( i = 0; i <= p->iFrame; i++ ) + { + Saig_ManForEachPi( pAig, pObj, k ) + pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++); + Aig_ManForEachNode( pAig, pObj, k ) + pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & + (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); + Aig_ManForEachCo( pAig, pObj, k ) + pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); + if ( i == p->iFrame ) + break; + Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k ) + pObjRo->fMarkB = pObjRi->fMarkB; + } + assert( iBit == p->nBits ); + RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB; + //Aig_ManCleanMarkB(pAig); + return RetValue; +} +Vec_Int_t * Saig_ManReturnFailingState( Aig_Man_t * pAig, Abc_Cex_t * p, int fNextOne ) +{ + Aig_Obj_t * pObj; + Vec_Int_t * vState; + int i, RetValue = Saig_ManVerifyCexNoClear( pAig, p ); + if ( RetValue == 0 ) + { + Aig_ManCleanMarkB(pAig); + printf( "CEX does fail the given sequential miter.\n" ); + return NULL; + } + vState = Vec_IntAlloc( Aig_ManRegNum(pAig) ); + if ( fNextOne ) + { + Saig_ManForEachLi( pAig, pObj, i ) + Vec_IntPush( vState, pObj->fMarkB ); + } + else + { + Saig_ManForEachLo( pAig, pObj, i ) + Vec_IntPush( vState, pObj->fMarkB ); + } + Aig_ManCleanMarkB(pAig); + return vState; +} + +/**Function************************************************************* + + Synopsis [Resimulates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p ) { Abc_Cex_t * pNew; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1f10be14..37d96dcc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -16493,20 +16493,17 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); Abc_Obj_t * pObj; + char * pInitStr = NULL; + int fZeros = 0; + int fOnes = 0; + int fRandom = 0; + int fDontCare = 0; + int fUseCexCs = 0; + int fUseCexNs = 0; int c, i; - int fZeros; - int fOnes; - int fRandom; - int fDontCare; - char * pInitStr; // set defaults - fZeros = 0; - fOnes = 0; - fRandom = 0; - fDontCare = 0; - pInitStr = NULL; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Szordh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Szordcnh" ) ) != EOF ) { switch ( c ) { @@ -16531,6 +16528,12 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': fDontCare ^= 1; break; + case 'c': + fUseCexCs ^= 1; + break; + case 'n': + fUseCexNs ^= 1; + break; case 'h': goto usage; default: @@ -16591,17 +16594,50 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj ); } + else if ( fUseCexCs || fUseCexNs ) + { + extern Vec_Int_t * Saig_ManReturnFailingState( Aig_Man_t * pMan, Abc_Cex_t * p, int fNextOne ); + Aig_Man_t * pMan; + Vec_Int_t * vFailState; + if ( fUseCexCs && fUseCexNs ) + { + Abc_Print( -1, "The two options (-c and -n) are incompatible.\n" ); + return 0; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "The current network should be an AIG.\n" ); + return 0; + } + if ( pAbc->pCex == NULL ) + { + Abc_Print( -1, "The current CEX is not available.\n" ); + return 0; + } + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + vFailState = Saig_ManReturnFailingState( pMan, pAbc->pCex, fUseCexNs ); + //Vec_IntPrint( vFailState ); + Aig_ManStop( pMan ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( Vec_IntEntry( vFailState, i ) ) + Abc_LatchSetInit1( pObj ); + else + Abc_LatchSetInit0( pObj ); + Vec_IntFree( vFailState ); + } else Abc_Print( -1, "The initial states remain unchanged.\n" ); return 0; usage: - Abc_Print( -2, "usage: init [-zordh] [-S <init_string>]\n" ); + Abc_Print( -2, "usage: init [-zordcnh] [-S <init_string>]\n" ); Abc_Print( -2, "\t resets initial states of all latches\n" ); Abc_Print( -2, "\t-z : set zeros initial states [default = %s]\n", fZeros? "yes": "no" ); Abc_Print( -2, "\t-o : set ones initial states [default = %s]\n", fOnes? "yes": "no" ); Abc_Print( -2, "\t-d : set don't-care initial states [default = %s]\n", fDontCare? "yes": "no" ); Abc_Print( -2, "\t-r : set random initial states [default = %s]\n", fRandom? "yes": "no" ); + Abc_Print( -2, "\t-c : set failure current state from the CEX (and run \"zero\") [default = %s]\n", fUseCexCs? "yes": "no" ); + Abc_Print( -2, "\t-n : set next state after failure from the CEX (and run \"zero\") [default = %s]\n", fUseCexNs? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-S str : (optional) initial state [default = unused]\n" ); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 1214e7b2..d2b74beb 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2307,7 +2307,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp ) if ( pPars->nDropOuts ) Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs ); } - Abc_Print( 1, " after %d frames", pPars->iFrame ); + Abc_Print( 1, " after %d frames", pPars->iFrame+2 ); Abc_Print( 1, ". " ); } } |