From 2eb2402b01541ed672ac2b7e742f1e1aa38542e8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 14 Nov 2012 20:50:18 -0800 Subject: Added command 'cexcut' and 'cexmerge'. --- src/base/abci/abc.c | 34 ++++++++++++++++++++++------------ src/sat/bmc/bmc.h | 4 ++-- src/sat/bmc/bmcCexCut.c | 23 +++++++++++++---------- 3 files changed, 37 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b02bcf09..9f072f5f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -22590,11 +22590,12 @@ usage: int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) { int c; - int iFrStart = 0; - int iFrStop = ABC_INFINITY; - int fVerbose = 0; + int iFrStart = 0; + int iFrStop = ABC_INFINITY; + int fCombOnly = 0; + int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FGcvh" ) ) != EOF ) { switch ( c ) { @@ -22620,6 +22621,9 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( iFrStop < 0 ) goto usage; break; + case 'c': + fCombOnly ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -22654,7 +22658,7 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); Abc_Ntk_t * pNtkNew; Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 ); - Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fVerbose ); + Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fCombOnly, fVerbose ); Aig_ManStop( pAig ); if ( pAigNew == NULL ) { @@ -22670,10 +22674,11 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: cexcut [-FG num] [-vh]\n" ); + Abc_Print( -2, "usage: cexcut [-FG num] [-cvh]\n" ); Abc_Print( -2, "\t creates logic for bad states using the current CEX\n" ); Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart ); Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop ); + Abc_Print( -2, "\t-c : toggle outputting combinational unate circuit [default = %s]\n", fCombOnly? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -28810,11 +28815,12 @@ int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pGiaNew; int c; - int iFrStart = 0; - int iFrStop = ABC_INFINITY; - int fVerbose = 0; + int iFrStart = 0; + int iFrStop = ABC_INFINITY; + int fCombOnly = 0; + int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FGcvh" ) ) != EOF ) { switch ( c ) { @@ -28840,6 +28846,9 @@ int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( iFrStop < 0 ) goto usage; break; + case 'c': + fCombOnly ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -28869,7 +28878,7 @@ int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( iFrStop == ABC_INFINITY ) iFrStop = pAbc->pCex->iFrame; - pGiaNew = Bmc_GiaTargetStates( pAbc->pGia, pAbc->pCex, iFrStart, iFrStop, fVerbose ); + pGiaNew = Bmc_GiaTargetStates( pAbc->pGia, pAbc->pCex, iFrStart, iFrStop, fCombOnly, fVerbose ); if ( pGiaNew == NULL ) { Abc_Print( 1, "Command has failed.\n"); @@ -28879,10 +28888,11 @@ int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &cexcut [-FG num] [-vh]\n" ); + Abc_Print( -2, "usage: &cexcut [-FG num] [-cvh]\n" ); Abc_Print( -2, "\t creates logic for bad states using the current CEX\n" ); Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart ); Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop ); + Abc_Print( -2, "\t-c : toggle producing combinational unate circuit [default = %s]\n", fCombOnly? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 5d789dcb..45caa3c5 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -75,8 +75,8 @@ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); /*=== bmcCexCut.c ==========================================================*/ -extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); -extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); +extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fVerbose ); +extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fVerbose ); /*=== bmcCexMin.c ==========================================================*/ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex ); diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c index bbb1bc73..98786620 100644 --- a/src/sat/bmc/bmcCexCut.c +++ b/src/sat/bmc/bmcCexCut.c @@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ) +Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fVerbose ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pObjRo, * pObjRi; @@ -141,13 +141,16 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); - // create new GIA - pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); - Gia_ManStop( pTemp ); + if ( !fCombOnly ) + { + // create new GIA + pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); + Gia_ManStop( pTemp ); - // create new initial state - pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) ); - Gia_ManStop( pTemp ); + // create new initial state + pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) ); + Gia_ManStop( pTemp ); + } Vec_BitFree( vInitNew ); return pNew; @@ -164,18 +167,18 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in SeeAlso [] ***********************************************************************/ -Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ) +Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fVerbose ) { Aig_Man_t * pAig; Gia_Man_t * pGia, * pRes; pGia = Gia_ManFromAigSimple( p ); if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) ) { - Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName ); + Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName ); Gia_ManStop( pGia ); return NULL; } - pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fVerbose ); + pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fVerbose ); pAig = Gia_ManToAigSimple( pRes ); Gia_ManStop( pGia ); Gia_ManStop( pRes ); -- cgit v1.2.3