diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 17:46:48 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 17:46:48 -0800 |
commit | 71cbf17e7f0352556af12ccccf9051e02c773e58 (patch) | |
tree | 002afb74b25be94e512e4869d328959046529766 /src/aig/fra | |
parent | 686d38d66754027cd29c64f1dc2975248eab7796 (diff) | |
download | abc-71cbf17e7f0352556af12ccccf9051e02c773e58.tar.gz abc-71cbf17e7f0352556af12ccccf9051e02c773e58.tar.bz2 abc-71cbf17e7f0352556af12ccccf9051e02c773e58.zip |
Unified the use of counter-examples in three packages.
Diffstat (limited to 'src/aig/fra')
-rw-r--r-- | src/aig/fra/fra.h | 6 | ||||
-rw-r--r-- | src/aig/fra/fraBmc.c | 4 | ||||
-rw-r--r-- | src/aig/fra/fraSec.c | 14 | ||||
-rw-r--r-- | src/aig/fra/fraSim.c | 222 |
4 files changed, 16 insertions, 230 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index aee38d08..a0073ca1 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -376,12 +376,6 @@ extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); extern Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ); extern Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); -extern void Fra_SmlFreeCounterExample( Abc_Cex_t * p ); -extern Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ); -extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); -extern int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p ); -extern Abc_Cex_t * Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo ); - ABC_NAMESPACE_HEADER_END diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c index ae9e4bc5..3907fcdd 100644 --- a/src/aig/fra/fraBmc.c +++ b/src/aig/fra/fraBmc.c @@ -417,7 +417,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew clk = clock(); iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames ); if ( iOutput >= 0 ) - pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput ); + pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); else { pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 ); @@ -428,7 +428,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew ABC_FREE( pBmc->pAigFraig->pData ); } else if ( iOutput >= 0 ) - pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput ); + pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); } if ( fVerbose ) { diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 7608791f..4b893cb2 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -203,14 +203,14 @@ clk = clock(); if ( pTemp->pSeqModel ) { - if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) ) + if ( !Saig_ManVerifyCex( pTemp, pTemp->pSeqModel ) ) printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" ); if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) ) printf( "The counter-example is invalid because of phase abstraction.\n" ); else { ABC_FREE( p->pSeqModel ); - p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) ); + p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) ); ABC_FREE( pTemp->pSeqModel ); } } @@ -443,7 +443,7 @@ ABC_PRT( "Time", clock() - clk ); else { ABC_FREE( p->pSeqModel ); - p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) ); + p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) ); ABC_FREE( pNew->pSeqModel ); } @@ -505,7 +505,7 @@ clk = clock(); RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth ); if ( pTemp->pSeqModel ) { - pCex = p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) ); + pCex = p->pSeqModel = Abc_CexDup( pTemp->pSeqModel, Aig_ManRegNum(p) ); pCex->iPo = i; Aig_ManStop( pTemp ); break; @@ -548,7 +548,7 @@ clk = clock(); { Abc_Cex_t * pCex; pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL; - pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel ); + pCex->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel ); } Aig_ManStop( pNewOrpos ); } @@ -598,7 +598,7 @@ ABC_PRT( "Time", clock() - clk ); printf( "Running property directed reachability...\n" ); RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex ); if ( pCex ) - pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pCex ); + pCex->iPo = Saig_ManFindFailedPoCex( pNew, pCex ); Aig_ManStop( pNewOrpos ); pNew->pSeqModel = pCex; } @@ -665,7 +665,7 @@ ABC_PRT( "Time", clock() - clkTotal ); else { ABC_FREE( p->pSeqModel ); - p->pSeqModel = Ssw_SmlDupCounterExample( pNew->pSeqModel, Aig_ManRegNum(p) ); + p->pSeqModel = Abc_CexDup( pNew->pSeqModel, Aig_ManRegNum(p) ); ABC_FREE( pNew->pSeqModel ); } } diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 25c30989..37620a16 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "fra.h" +#include "saig.h" ABC_NAMESPACE_IMPL_START @@ -879,45 +880,6 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW /**Function************************************************************* - Synopsis [Allocates a counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ) -{ - Abc_Cex_t * pCex; - int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames ); - pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); - pCex->nRegs = nRegs; - pCex->nPis = nRealPis; - pCex->nBits = nRegs + nRealPis * nFrames; - return pCex; -} - -/**Function************************************************************* - - Synopsis [Frees the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_SmlFreeCounterExample( Abc_Cex_t * pCex ) -{ - ABC_FREE( pCex ); -} - -/**Function************************************************************* - Synopsis [Creates sequential counter-example from the simulation info.] Description [] @@ -960,7 +922,7 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ) assert( iBit < 32 * p->nWordsFrame ); // allocate the counter example - pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; @@ -981,10 +943,10 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ) } } // verify the counter example - if ( !Fra_SmlRunCounterExample( p->pAig, pCex ) ) + if ( !Saig_ManVerifyCex( p->pAig, pCex ) ) { printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" ); - Fra_SmlFreeCounterExample( pCex ); + Abc_CexFree( pCex ); pCex = NULL; } return pCex; @@ -1026,7 +988,7 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in } assert( iPo >= 0 ); // allocate the counter example - pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; @@ -1040,186 +1002,16 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in } // verify the counter example - if ( !Fra_SmlRunCounterExample( pAig, pCex ) ) + if ( !Saig_ManVerifyCex( pAig, pCex ) ) { printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" ); - Fra_SmlFreeCounterExample( pCex ); + Abc_CexFree( pCex ); pCex = NULL; } return pCex; } -/**Function************************************************************* - - Synopsis [Make the trivial counter-example for the trivially asserted output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ) -{ - Abc_Cex_t * pCex; - int nTruePis, nTruePos, iPo, iFrame; - assert( Aig_ManRegNum(pAig) > 0 ); - nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); - nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig); - iPo = iFrameOut % nTruePos; - iFrame = iFrameOut / nTruePos; - // allocate the counter example - pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 ); - pCex->iPo = iPo; - pCex->iFrame = iFrame; - return pCex; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ) -{ - Fra_Sml_t * pSml; - Aig_Obj_t * pObj; - int RetValue, i, k, iBit; - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); - // start a new sequential simulator - pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 ); - // assign simulation info for the registers - iBit = 0; - Aig_ManForEachLoSeq( pAig, pObj, i ) - Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); - // assign simulation info for the primary inputs - for ( i = 0; i <= p->iFrame; i++ ) - Aig_ManForEachPiSeq( pAig, pObj, k ) - Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); - assert( iBit == p->nBits ); - // run random simulation - Fra_SmlSimulateOne( pSml ); - // check if the given output has failed - RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); - Fra_SmlStop( pSml ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Make the trivial counter-example for the trivially asserted output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Fra_SmlSimpleCounterExample( Aig_Man_t * pAig, int * pModel, int iFrame, int iPo ) -{ - Abc_Cex_t * pCex; - int iBit; - pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), iFrame + 1 ); - pCex->iPo = iPo; - pCex->iFrame = iFrame; - for ( iBit = Aig_ManRegNum(pAig); iBit < pCex->nBits; iBit++ ) - if ( pModel[iBit-Aig_ManRegNum(pAig)] ) - Aig_InfoSetBit( pCex->pData, iBit ); -/* - if ( !Fra_SmlRunCounterExample( pAig, pCex ) ) - { - printf( "Fra_SmlSimpleCounterExample(): Counter-example is invalid.\n" ); -// Fra_SmlFreeCounterExample( pCex ); -// pCex = NULL; - } -*/ - return pCex; -} - -/**Function************************************************************* - - Synopsis [Resimulates the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p ) -{ - Fra_Sml_t * pSml; - Aig_Obj_t * pObj; - int RetValue, i, k, iBit; - unsigned * pSims; - assert( Aig_ManRegNum(pAig) > 0 ); - assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); - // start a new sequential simulator - pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 ); - // assign simulation info for the registers - iBit = 0; - Aig_ManForEachLoSeq( pAig, pObj, i ) -// Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 ); - Fra_SmlAssignConst( pSml, pObj, 0, 0 ); - // assign simulation info for the primary inputs - iBit = p->nRegs; - for ( i = 0; i <= p->iFrame; i++ ) - Aig_ManForEachPiSeq( pAig, pObj, k ) - Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i ); - assert( iBit == p->nBits ); - // run random simulation - Fra_SmlSimulateOne( pSml ); - // check if the given output has failed - RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) ); - - // write the output file - for ( i = 0; i <= p->iFrame; i++ ) - { -/* - Aig_ManForEachLoSeq( pAig, pObj, k ) - { - pSims = Fra_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } - fprintf( pFile, " " ); -*/ - Aig_ManForEachPiSeq( pAig, pObj, k ) - { - pSims = Fra_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } -/* - fprintf( pFile, " " ); - Aig_ManForEachPoSeq( pAig, pObj, k ) - { - pSims = Fra_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } - fprintf( pFile, " " ); - Aig_ManForEachLiSeq( pAig, pObj, k ) - { - pSims = Fra_ObjSim(pSml, pObj->Id); - fprintf( pFile, "%d", (int)(pSims[i] != 0) ); - } -*/ - fprintf( pFile, "\n" ); - } - - Fra_SmlStop( pSml ); - return RetValue; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |