diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 191 | ||||
-rw-r--r-- | src/base/main/mainFrame.c | 1 | ||||
-rw-r--r-- | src/base/main/mainInt.h | 1 | ||||
-rw-r--r-- | src/sat/bmc/bmc.h | 10 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmc.c | 1 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmc2.c | 1 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmc3.c | 1 | ||||
-rw-r--r-- | src/sat/bmc/bmcCexCut.c | 6 | ||||
-rw-r--r-- | src/sat/bmc/bmcCexMin1.c | 1 |
9 files changed, 201 insertions, 12 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 028dddcc..09e1c94e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -294,7 +294,9 @@ static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandTestCex ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPdr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandCexMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCexSave ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCexLoad ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandCexMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDualRail ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBlockPo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIso ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -362,7 +364,8 @@ static int Abc_CommandAbc9ReachN ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9ReachY ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Iso ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9CexMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +//static int Abc_CommandAbc9CexMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -749,7 +752,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 ); Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 ); Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 ); - Cmd_CommandAdd( pAbc, "Verification", "cexmin", Abc_CommandCexMin, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "cexsave", Abc_CommandCexSave, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "cexload", Abc_CommandCexLoad, 0 ); +// Cmd_CommandAdd( pAbc, "Verification", "cexmin", Abc_CommandCexMin, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dualrail", Abc_CommandDualRail, 1 ); Cmd_CommandAdd( pAbc, "Verification", "blockpo", Abc_CommandBlockPo, 1 ); Cmd_CommandAdd( pAbc, "Verification", "iso", Abc_CommandIso, 1 ); @@ -814,7 +819,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&reachy", Abc_CommandAbc9ReachY, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&iso", Abc_CommandAbc9Iso, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&cexmin", Abc_CommandAbc9CexMin, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); +// Cmd_CommandAdd( pAbc, "ABC9", "&cexmin", Abc_CommandAbc9CexMin, 0 ); Cmd_CommandAdd( pAbc, "Abstraction", "&abs_derive", Abc_CommandAbc9AbsDerive, 0 ); Cmd_CommandAdd( pAbc, "Abstraction", "&abs_refine", Abc_CommandAbc9AbsRefine, 0 ); @@ -22480,6 +22486,90 @@ usage: return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandCexSave( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pCex == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + ABC_FREE( pAbc->pCex2 ); + pAbc->pCex2 = Abc_CexDup( pAbc->pCex, -1 ); + return 0; + +usage: + Abc_Print( -2, "usage: cexsave [-h]\n" ); + Abc_Print( -2, "\t saves the current CEX into the internal storage\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandCexLoad( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pCex == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + ABC_FREE( pAbc->pCex ); + pAbc->pCex = Abc_CexDup( pAbc->pCex2, -1 ); + return 0; + +usage: + Abc_Print( -2, "usage: cexload [-h]\n" ); + Abc_Print( -2, "\t loads the current CEX from the internal storage\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + + /**Function************************************************************* Synopsis [] @@ -28514,6 +28604,99 @@ usage: SeeAlso [] ***********************************************************************/ +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; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + iFrStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iFrStart < 0 ) + goto usage; + break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + iFrStop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iFrStop < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + Abc_Print( -2, "Unknown switch.\n"); + goto usage; + } + } + + if ( pAbc->pCex == NULL ) + { + Abc_Print( 1, "There is no current cex.\n"); + return 0; + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( 1, "There is no AIG in the &-space.\n"); + return 0; + } + if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) ) + { + Abc_Print( 1, "Current counter-example is not a valid counter-example for &-space AIG \"%s\".\n", Gia_ManName(pAbc->pGia) ); + return 0; + } + if ( iFrStop == ABC_INFINITY ) + iFrStop = pAbc->pCex->iFrame; + + pGiaNew = Bmc_GiaTargetStates( pAbc->pGia, pAbc->pCex, iFrStart, iFrStop, fVerbose ); + if ( pGiaNew == NULL ) + { + Abc_Print( 1, "Command has failed.\n"); + return 0; + } + Abc_CommandUpdate9( pAbc, pGiaNew ); + return 0; + +usage: + Abc_Print( -2, "usage: &cexcut [-FG num] [-vh]\n" ); + Abc_Print( -2, "\t extract logic representation of bad states\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-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9CexMin( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int nRealPis, int fJustMax, int fUseAll, int fVerbose ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 809056c9..deb0ddca 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -190,6 +190,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) } Vec_PtrFreeP( &p->vLTLProperties_global ); Abc_FrameDeleteAllNetworks( p ); + ABC_FREE( p->pCex2 ); ABC_FREE( p->pCex ); ABC_FREE( p ); s_GlobalFrame = NULL; diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index f30a13e5..9450462d 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -97,6 +97,7 @@ struct Abc_Frame_t_ Gia_Man_t * pGia; // alternative current network as a light-weight AIG Gia_Man_t * pGia2; // copy of the above Abc_Cex_t * pCex; // a counter-example to fail the current network + Abc_Cex_t * pCex2; // copy of the above Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails Vec_Ptr_t * vPoEquivs; // equivalence classes of isomorphic primary outputs int Status; // the status of verification problem (proved=1, disproved=0, undecided=-1) diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 633dc205..e1841bbc 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -27,6 +27,7 @@ //////////////////////////////////////////////////////////////////////// #include "aig/saig/saig.h" +#include "aig/gia/gia.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -66,13 +67,16 @@ struct Saig_ParBmc_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== saigBmc.c ==========================================================*/ +/*=== bmcBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); +/*=== bmcBmc2.c ==========================================================*/ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); -/*=== saigBmc3.c ==========================================================*/ +/*=== bmcBmc3.c ==========================================================*/ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); -/*=== saigCexMin.c ==========================================================*/ +/*=== bmcCexCut.c ==========================================================*/ +extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose ); +/*=== bmcCexMin.c ==========================================================*/ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex ); diff --git a/src/sat/bmc/bmcBmc.c b/src/sat/bmc/bmcBmc.c index 56bb7ca6..7a7c8940 100644 --- a/src/sat/bmc/bmcBmc.c +++ b/src/sat/bmc/bmcBmc.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "aig/saig/saig.h" #include "proof/fra/fra.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" diff --git a/src/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c index 778fe8e0..0f55f7ce 100644 --- a/src/sat/bmc/bmcBmc2.c +++ b/src/sat/bmc/bmcBmc2.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "aig/saig/saig.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #include "proof/ssw/ssw.h" diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index a29be146..7ca5c7ba 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "aig/saig/saig.h" #include "proof/fra/fra.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c index 3cc81d97..79944097 100644 --- a/src/sat/bmc/bmcCexCut.c +++ b/src/sat/bmc/bmcCexCut.c @@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* - Synopsis [] + Synopsis [Generate GIA for target bad states.] Description [] @@ -42,6 +42,10 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ +Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd ) +{ + return NULL; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/bmc/bmcCexMin1.c b/src/sat/bmc/bmcCexMin1.c index 3b0a0274..23133ac0 100644 --- a/src/sat/bmc/bmcCexMin1.c +++ b/src/sat/bmc/bmcCexMin1.c @@ -18,7 +18,6 @@ ***********************************************************************/ -#include "aig/saig/saig.h" #include "aig/ioa/ioa.h" #include "bmc.h" |