diff options
Diffstat (limited to 'src/base/abci/abcDar.c')
| -rw-r--r-- | src/base/abci/abcDar.c | 69 |
1 files changed, 56 insertions, 13 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index d2022e37..d4771989 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1202,10 +1202,10 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fVerbose ) +int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose ) { Aig_Man_t * pMan; - int clk = clock(); + int RetValue, clk = clock(); // derive the AIG manager pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) @@ -1214,16 +1214,35 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, in return -1; } assert( pMan->nRegs > 0 ); + pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); + pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); // perform verification - Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose ); - pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - if ( pNtk->pSeqModel ) + if ( fNewAlgo ) { - Fra_Cex_t * pCex = pNtk->pSeqModel; - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame ); + int iFrame; + RetValue = Saig_ManBmcSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose, &iFrame ); + if ( RetValue == 1 ) + printf( "No output was asserted in %d frames. ", nFrames ); + else if ( RetValue == -1 ) + printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit ); + else // if ( RetValue == 0 ) + { + Fra_Cex_t * pCex = pNtk->pSeqModel; + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame ); + } } else - printf( "No output was asserted after BMC with %d frames. ", nFrames ); + { + Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose ); + pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; + if ( pNtk->pSeqModel ) + { + Fra_Cex_t * pCex = pNtk->pSeqModel; + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame ); + } + else + printf( "No output was asserted in %d frames. ", nFrames ); + } PRT( "Time", clock() - clk ); Aig_ManStop( pMan ); return 1; @@ -1240,7 +1259,7 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) +int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose ) { Aig_Man_t * pMan; int RetValue, Depth, clk = clock(); @@ -1254,7 +1273,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) assert( pMan->nRegs > 0 ); pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); - RetValue = Saig_Interpolate( pMan, nConfLimit, fVerbose, &Depth ); + RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fVerbose, &Depth ); if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) @@ -1892,7 +1911,7 @@ timeInt = 0; /**Function************************************************************* - Synopsis [Interplates two networks.] + Synopsis [] Description [] @@ -1915,7 +1934,32 @@ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose ) /**Function************************************************************* - Synopsis [Interplates two networks.] + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk ) +{ + extern void Saig_ManPrintCones( Aig_Man_t * pAig ); + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return; + assert( Aig_ManRegNum(pMan) > 0 ); + pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); + pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); + Saig_ManPrintCones( pMan ); + Aig_ManStop( pMan ); +} + +/**Function************************************************************* + + Synopsis [] Description [] @@ -1947,7 +1991,6 @@ Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose return pNtkAig; } - /**Function************************************************************* Synopsis [Performs phase abstraction.] |