From 1d3ff5338a0c98f2319578b25f9695c3a326dd9d Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Fri, 17 Feb 2017 18:55:00 -0800 Subject: added ipdr --- src/base/abci/abc.c | 268 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 268 insertions(+) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 52684f8c..af79a66d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -333,6 +333,7 @@ static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv ); 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_CommandIPdr ( Abc_Frame_t * pAbc, int argc, char ** argv ); #ifdef ABC_USE_CUDD static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv ); #endif @@ -983,6 +984,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 ); Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 ); Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "ipdr", Abc_CommandIPdr, 0 ); #ifdef ABC_USE_CUDD Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 ); #endif @@ -26415,6 +26417,272 @@ usage: + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); + Pdr_Par_t Pars, * pPars = &Pars; + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + int c; + Pdr_ManSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegjonctkvwzh" ) ) != EOF ) + { + switch ( c ) + { + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nRecycle = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nRecycle < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFrameMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFrameMax < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nConfLimit < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nConfGenLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nConfGenLimit < 0 ) + goto usage; + break; + case 'Q': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nRestLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nRestLimit < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTimeOut < 0 ) + goto usage; + break; + case 'H': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTimeOutOne = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTimeOutOne < 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; + } + pPars->nTimeOutGap = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTimeOutGap < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nRandomSeed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nRandomSeed < 0 ) + goto usage; + break; + case 'a': + pPars->fSolveAll ^= 1; + break; + case 'x': + pPars->fStoreCex ^= 1; + break; + case 'r': + pPars->fTwoRounds ^= 1; + break; + case 'm': + pPars->fMonoCnf ^= 1; + break; + case 'u': + pPars->fNewXSim ^= 1; + break; + case 'y': + pPars->fFlopPrio ^= 1; + break; + case 'f': + pPars->fFlopOrder ^= 1; + break; + case 's': + pPars->fShortest ^= 1; + break; + case 'i': + pPars->fShiftStart ^= 1; + break; + case 'p': + pPars->fReuseProofOblig ^= 1; + break; + case 'd': + pPars->fDumpInv ^= 1; + break; + case 'e': + pPars->fUseSupp ^= 1; + break; + case 'g': + pPars->fSkipGeneral ^= 1; + break; + case 'j': + pPars->fSimpleGeneral ^= 1; + break; + case 'o': + pPars->fUsePropOut ^= 1; + break; + case 'n': + pPars->fSkipDown ^= 1; + break; + case 'c': + pPars->fCtgs ^= 1; + break; + case 't': + pPars->fUseAbs ^= 1; + break; + case 'k': + pPars->fUseSimpleRef ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; + case 'z': + pPars->fNotVerbose ^= 1; + break; + case 'h': + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -2, "There is no current network.\n"); + return 0; + } + if ( Abc_NtkLatchNum(pNtk) == 0 ) + { + Abc_Print( 0, "The current network is combinational.\n"); + return 0; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); + return 0; + } + // run the procedure + pPars->fUseBridge = pAbc->fBridgeMode; + pAbc->Status = Abc_NtkDarPdr( pNtk, pPars ); + pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; + Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap ); + if ( pNtk->vSeqModelVec ) + Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); + else + Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); + return 0; + +usage: + Abc_Print( -2, "usage: ipdr [-MFCDQTHGS ] [-axrmuyfsipdegjonctkvwzh]\n" ); + Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); + Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" ); + Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); + Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle ); + Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax ); + Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit ); + Abc_Print( -2, "\t-D num : limit on conflicts during ind-generalization (0 = no limit) [default = %d]\n",pPars->nConfGenLimit ); + Abc_Print( -2, "\t-Q num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit ); + Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut ); + Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); + Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap ); + Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed ); + Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); + Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); + Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" ); + Abc_Print( -2, "\t-u : toggle updated X-valued simulation [default = %s]\n", pPars->fNewXSim? "yes": "no" ); + Abc_Print( -2, "\t-y : toggle using structural flop priorities [default = %s]\n", pPars->fFlopPrio? "yes": "no" ); + Abc_Print( -2, "\t-f : toggle ordering flops by cost before generalization [default = %s]\n", pPars->fFlopOrder? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" ); + Abc_Print( -2, "\t-i : toggle clause pushing from an intermediate timeframe [default = %s]\n", pPars->fShiftStart? "yes": "no" ); + Abc_Print( -2, "\t-p : toggle reusing proof-obligations in the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle dumping invariant (valid if init state is all-0) [default = %s]\n", pPars->fDumpInv? "yes": "no" ); + Abc_Print( -2, "\t-e : toggle using only support variables in the invariant [default = %s]\n", pPars->fUseSupp? "yes": "no" ); + Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" ); + Abc_Print( -2, "\t-j : toggle using simplified generalization step [default = %s]\n", pPars->fSimpleGeneral? "yes": "no" ); + Abc_Print( -2, "\t-o : toggle using property output as inductive hypothesis [default = %s]\n", pPars->fUsePropOut? "yes": "no" ); + Abc_Print( -2, "\t-n : * toggle skipping \'down\' in generalization [default = %s]\n", pPars->fSkipDown? "yes": "no" ); + Abc_Print( -2, "\t-c : * toggle handling CTGs in \'down\' [default = %s]\n", pPars->fCtgs? "yes": "no" ); + Abc_Print( -2, "\t-t : toggle using abstraction [default = %s]\n", pPars->fUseAbs? "yes": "no" ); + Abc_Print( -2, "\t-k : toggle using simplified refinement [default = %s]\n", pPars->fUseSimpleRef? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n\n"); + Abc_Print( -2, "\t* Implementation of switches -S, -n, and -c is contributed by Zyad Hassan.\n"); + Abc_Print( -2, "\t The theory and experiments supporting this work can be found in the following paper:\n"); + Abc_Print( -2, "\t Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, \"Better Generalization in IC3\", FMCAD 2013.\n"); + Abc_Print( -2, "\t (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/85-Better-Generalization-IC3.pdf)\n"); + + + return 1; } -- cgit v1.2.3 From 16fda0bd24f1d1e4bb6b39cd0f1a545fd096d6c3 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 18 Feb 2017 09:10:45 -0800 Subject: added a simple example; edited hgignore --- .hgignore | 5 +++++ fsm.v | 28 ++++++++++++++++++++++++++++ 2 files changed, 33 insertions(+) create mode 100644 fsm.v diff --git a/.hgignore b/.hgignore index b5fedc7a..f5d4784c 100644 --- a/.hgignore +++ b/.hgignore @@ -52,9 +52,14 @@ build/ *.rej *.orig +tags + syntax: regexp ^libabc.a$ ^abc$ ^arch_flags$ + +^cmake +^cscope diff --git a/fsm.v b/fsm.v new file mode 100644 index 00000000..272c4a89 --- /dev/null +++ b/fsm.v @@ -0,0 +1,28 @@ +module fsm (out); +output out; + +wire [2:0] ns; +wire [2:0] cs; + +always @( ns or cs ) +begin +case (cs) + 0 : ns = 3'b010; + 1 : ns = 3'b001; + 2 : ns = 3'b000; + 3 : ns = 3'b101; + 4 : ns = 3'b001; + 5 : ns = 3'b111; + 6 : ns = 3'b001; + 7 : ns = 3'b110; +endcase +end + +assign out = cs == 3'b001; + +wire [2:0] const0 = 3'h0; + + +CPL_FF#3 ff3 ( .q(cs), .qbar(), .d(ns), .clk(), .arst(), .arstval(const0) ); + +endmodule -- cgit v1.2.3 From 196b3591830e9fbe0877411b8053233c11d0f4ce Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 18 Feb 2017 09:51:54 -0800 Subject: started pdrIncr.c --- src/base/abci/abc.c | 2 ++ src/proof/pdr/module.make | 3 ++- src/proof/pdr/pdrIncr.c | 56 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 60 insertions(+), 1 deletion(-) create mode 100644 src/proof/pdr/pdrIncr.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index af79a66d..0e3a1d3a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26434,6 +26434,7 @@ usage: int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); + extern int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); Pdr_Par_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int c; @@ -26629,6 +26630,7 @@ int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // run the procedure + IPdr_ManSolve( pNtk, pPars ); pPars->fUseBridge = pAbc->fBridgeMode; pAbc->Status = Abc_NtkDarPdr( pNtk, pPars ); pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; diff --git a/src/proof/pdr/module.make b/src/proof/pdr/module.make index 2967aeb8..4c177a21 100644 --- a/src/proof/pdr/module.make +++ b/src/proof/pdr/module.make @@ -5,4 +5,5 @@ SRC += src/proof/pdr/pdrCnf.c \ src/proof/pdr/pdrSat.c \ src/proof/pdr/pdrTsim.c \ src/proof/pdr/pdrTsim2.c \ - src/proof/pdr/pdrUtil.c + src/proof/pdr/pdrUtil.c \ + src/proof/pdr/pdrIncr.c diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c new file mode 100644 index 00000000..a2329870 --- /dev/null +++ b/src/proof/pdr/pdrIncr.c @@ -0,0 +1,56 @@ +/**CFile**************************************************************** + + FileName [pdrIncr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Property driven reachability.] + + Synopsis [PDR with incremental solving.] + + Author [Yen-Sheng Ho, Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Feb. 17, 2017.] + + Revision [$Id: pdrIncr.c$] + +***********************************************************************/ + +#include "pdrInt.h" +#include "base/main/main.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ) +{ + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END -- cgit v1.2.3 From 91a0a0fc3b5dfd5aa71122106dbdacf6268e51fb Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 18 Feb 2017 10:28:16 -0800 Subject: copied pdr_mansolve --- src/base/abci/abc.c | 3 +-- src/proof/pdr/pdrIncr.c | 41 ++++++++++++++++++++++++++++++++++++++++- 2 files changed, 41 insertions(+), 3 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0e3a1d3a..f12e3727 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26630,9 +26630,8 @@ int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // run the procedure - IPdr_ManSolve( pNtk, pPars ); pPars->fUseBridge = pAbc->fBridgeMode; - pAbc->Status = Abc_NtkDarPdr( pNtk, pPars ); + pAbc->Status = IPdr_ManSolve( pNtk, pPars ); pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap ); if ( pNtk->vSeqModelVec ) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index a2329870..2276384c 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -27,6 +27,7 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -45,7 +46,45 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ) { - return 0; + int RetValue = -1; + abctime clk = Abc_Clock(); + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + + RetValue = Pdr_ManSolve( pMan, pPars ); + + if ( RetValue == 1 ) + Abc_Print( 1, "Property proved. " ); + else + { + if ( RetValue == 0 ) + { + if ( pMan->pSeqModel == NULL ) + Abc_Print( 1, "Counter-example is not available.\n" ); + else + { + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame ); + if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) ) + Abc_Print( 1, "Counter-example verification has FAILED.\n" ); + } + } + else if ( RetValue == -1 ) + Abc_Print( 1, "Property UNDECIDED. " ); + else + assert( 0 ); + } + ABC_PRT( "Time", Abc_Clock() - clk ); + + + ABC_FREE( pNtk->pSeqModel ); + pNtk->pSeqModel = pMan->pSeqModel; + pMan->pSeqModel = NULL; + if ( pNtk->vSeqModelVec ) + Vec_PtrFreeFree( pNtk->vSeqModelVec ); + pNtk->vSeqModelVec = pMan->vSeqModelVec; + pMan->vSeqModelVec = NULL; + Aig_ManStop( pMan ); + return RetValue; } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3 From b93a80512941e5039e48a7b74e625d7d6f9f720a Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 18 Feb 2017 12:43:03 -0800 Subject: copied some functions from pdr --- src/base/abci/abc.c | 4 +- src/proof/pdr/pdrIncr.c | 429 +++++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 429 insertions(+), 4 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f12e3727..0645c6e3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26434,7 +26434,7 @@ usage: int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); - extern int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); + extern int Abc_NtkDarIPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); Pdr_Par_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int c; @@ -26631,7 +26631,7 @@ int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) } // run the procedure pPars->fUseBridge = pAbc->fBridgeMode; - pAbc->Status = IPdr_ManSolve( pNtk, pPars ); + pAbc->Status = Abc_NtkDarIPdr( pNtk, pPars ); pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap ); if ( pNtk->vSeqModelVec ) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 2276384c..d33b45ac 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -28,6 +28,11 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); +extern int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ); +extern int Pdr_ManPushClauses( Pdr_Man_t * p ); +extern int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer ); +extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -44,14 +49,434 @@ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); SeeAlso [] ***********************************************************************/ -int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ) +int IPdr_ManSolveInt( Pdr_Man_t * p ) +{ + int fPrintClauses = 0; + Pdr_Set_t * pCube = NULL; + Aig_Obj_t * pObj; + Abc_Cex_t * pCexNew; + int iFrame, RetValue = -1; + int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); + abctime clkStart = Abc_Clock(), clkOne = 0; + p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; + assert( Vec_PtrSize(p->vSolvers) == 0 ); + // in the multi-output mode, mark trivial POs (those fed by const0) as solved + if ( p->pPars->fSolveAll ) + Saig_ManForEachPo( p->pAig, pObj, iFrame ) + if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) ) + { + Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat + p->pPars->nProveOuts++; + if ( p->pPars->fUseBridge ) + Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); + } + // create the first timeframe + p->pPars->timeLastSolved = Abc_Clock(); + Pdr_ManCreateSolver( p, (iFrame = 0) ); + while ( 1 ) + { + int fRefined = 0; + if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 1 ) + { +// int i, Prio; + assert( p->vAbsFlops == NULL ); + p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) ); + p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) ); + p->vMapPpi2Ff = Vec_IntAlloc( 100 ); +// Vec_IntForEachEntry( p->vPrio, Prio, i ) +// if ( Prio >> p->nPrioShift ) +// Vec_IntWriteEntry( p->vAbsFlops, i, 1 ); + } + //if ( p->pPars->fUseAbs && p->vAbsFlops ) + // printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) ); + p->nFrames = iFrame; + assert( iFrame == Vec_PtrSize(p->vSolvers)-1 ); + p->iUseFrame = Abc_MaxInt(iFrame, 1); + Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) + { + // skip disproved outputs + if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) ) + continue; + // skip output whose time has run out + if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 ) + continue; + // check if the output is trivially solved + if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) ) + continue; + // check if the output is trivially solved + if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) ) + { + if ( !p->pPars->fSolveAll ) + { + pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ); + p->pAig->pSeqModel = pCexNew; + return 0; // SAT + } + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + p->pPars->nFailOuts++; + if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); + if ( !p->pPars->fNotVerbose ) + Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n", + nOutDigits, p->iOutCur, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); + if ( p->pPars->fUseBridge ) + Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); + Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); + if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; + return -1; + } + if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) ) + return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC + p->pPars->timeLastSolved = Abc_Clock(); + continue; + } + // try to solve this output + if ( p->pTime4Outs ) + { + assert( p->pTime4Outs[p->iOutCur] > 0 ); + clkOne = Abc_Clock(); + p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock(); + } + while ( 1 ) + { + if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); + p->pPars->iFrame = iFrame; + return -1; + } + RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0, 1 ); + if ( RetValue == 1 ) + break; + if ( RetValue == -1 ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( p->timeToStop && Abc_Clock() > p->timeToStop ) + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); + else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); + else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne ) + { + Pdr_QueueClean( p ); + pCube = NULL; + break; // keep solving + } + else if ( p->pPars->nConfLimit ) + Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame ); + else if ( p->pPars->fVerbose ) + Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; + return -1; + } + if ( RetValue == 0 ) + { + RetValue = Pdr_ManBlockCube( p, pCube ); + if ( RetValue == -1 ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( p->timeToStop && Abc_Clock() > p->timeToStop ) + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); + else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); + else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne ) + { + Pdr_QueueClean( p ); + pCube = NULL; + break; // keep solving + } + else if ( p->pPars->nConfLimit ) + Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame ); + else if ( p->pPars->fVerbose ) + Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; + return -1; + } + if ( RetValue == 0 ) + { + if ( fPrintClauses ) + { + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); + Pdr_ManPrintClauses( p, 0 ); + } + if ( p->pPars->fVerbose && !p->pPars->fUseAbs ) + Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart ); + p->pPars->iFrame = iFrame; + if ( !p->pPars->fSolveAll ) + { + abctime clk = Abc_Clock(); + Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p); + p->tAbs += Abc_Clock() - clk; + if ( pCex == NULL ) + { + assert( p->pPars->fUseAbs ); + Pdr_QueueClean( p ); + pCube = NULL; + fRefined = 1; + break; // keep solving + } + p->pAig->pSeqModel = pCex; + return 0; // SAT + } + p->pPars->nFailOuts++; + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1; + if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); + assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); + if ( p->pPars->fUseBridge ) + Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); + Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); + if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; + return -1; + } + if ( !p->pPars->fNotVerbose ) + Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n", + nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) + return 0; // all SAT + Pdr_QueueClean( p ); + pCube = NULL; + break; // keep solving + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart ); + } + } + if ( fRefined ) + break; + if ( p->pTime4Outs ) + { + abctime timeSince = Abc_Clock() - clkOne; + assert( p->pTime4Outs[p->iOutCur] > 0 ); + p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0; + if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided + { + p->pPars->nDropOuts++; + if ( p->pPars->vOutMap ) + Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); + if ( !p->pPars->fNotVerbose ) + Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame ); + } + p->timeToStopOne = 0; + } + } + if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined ) + { + int i, Used; + Vec_IntForEachEntry( p->vAbsFlops, Used, i ) + if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 ) + Vec_IntWriteEntry( p->vAbsFlops, i, 0 ); + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart ); + if ( fRefined ) + continue; + //if ( p->pPars->fUseAbs && p->vAbsFlops ) + // printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) ); + // open a new timeframe + p->nQueLim = p->pPars->nRestLimit; + assert( pCube == NULL ); + Pdr_ManSetPropertyOutput( p, iFrame ); + Pdr_ManCreateSolver( p, ++iFrame ); + if ( fPrintClauses ) + { + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); + Pdr_ManPrintClauses( p, 0 ); + } + // push clauses into this timeframe + RetValue = Pdr_ManPushClauses( p ); + if ( RetValue == -1 ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( !p->pPars->fSilent ) + { + if ( p->timeToStop && Abc_Clock() > p->timeToStop ) + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); + else + Abc_Print( 1, "Reached conflict limit (%d) in frame.\n", p->pPars->nConfLimit, iFrame ); + } + p->pPars->iFrame = iFrame; + return -1; + } + if ( RetValue ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( !p->pPars->fSilent ) + Pdr_ManReportInvariant( p ); + if ( !p->pPars->fSilent ) + Pdr_ManVerifyInvariant( p ); + p->pPars->iFrame = iFrame; + // count the number of UNSAT outputs + p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts; + // convert previously 'unknown' into 'unsat' + if ( p->pPars->vOutMap ) + for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ ) + if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown + { + Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat + if ( p->pPars->fUseBridge ) + Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); + } + if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) ) + return 1; // UNSAT + if ( p->pPars->nFailOuts > 0 ) + return 0; // SAT + return -1; + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart ); + + // check termination + if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) ) + { + p->pPars->iFrame = iFrame; + return -1; + } + if ( p->timeToStop && Abc_Clock() > p->timeToStop ) + { + if ( fPrintClauses ) + { + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); + Pdr_ManPrintClauses( p, 0 ); + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); + p->pPars->iFrame = iFrame; + return -1; + } + if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) + { + if ( fPrintClauses ) + { + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); + Pdr_ManPrintClauses( p, 0 ); + } + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); + p->pPars->iFrame = iFrame; + return -1; + } + if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + if ( !p->pPars->fSilent ) + Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax ); + p->pPars->iFrame = iFrame; + return -1; + } + } + assert( 0 ); + return -1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) +{ + Pdr_Man_t * p; + int k, RetValue; + abctime clk = Abc_Clock(); + if ( pPars->nTimeOutOne && !pPars->fSolveAll ) + pPars->nTimeOutOne = 0; + if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 ) + pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0); + if ( pPars->fVerbose ) + { +// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); + Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ", + pPars->nRecycle, + pPars->nFrameMax, + pPars->nRestLimit, + pPars->nTimeOut ); + Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n", + pPars->fMonoCnf ? "yes" : "no", + pPars->fSkipGeneral ? "yes" : "no", + pPars->fSolveAll ? "yes" : "no" ); + } + ABC_FREE( pAig->pSeqModel ); + p = Pdr_ManStart( pAig, pPars, NULL ); + RetValue = IPdr_ManSolveInt( p ); + if ( RetValue == 0 ) + assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); + if ( p->vCexes ) + { + assert( p->pAig->vSeqModelVec == NULL ); + p->pAig->vSeqModelVec = p->vCexes; + p->vCexes = NULL; + } + if ( p->pPars->fDumpInv ) + { + char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla"); + Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); + Pdr_ManDumpClauses( p, pFileName, RetValue==1 ); + } + else if ( RetValue == 1 ) + Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); + p->tTotal += Abc_Clock() - clk; + Pdr_ManStop( p ); + pPars->iFrame--; + // convert all -2 (unknown) entries into -1 (undec) + if ( pPars->vOutMap ) + for ( k = 0; k < Saig_ManPoNum(pAig); k++ ) + if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown + Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec + if ( pPars->fUseBridge ) + Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" ); + return RetValue; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarIPdr ( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ) { int RetValue = -1; abctime clk = Abc_Clock(); Aig_Man_t * pMan; pMan = Abc_NtkToDar( pNtk, 0, 1 ); - RetValue = Pdr_ManSolve( pMan, pPars ); + RetValue = IPdr_ManSolve( pMan, pPars ); if ( RetValue == 1 ) Abc_Print( 1, "Property proved. " ); -- cgit v1.2.3 From fdc0b471e5b9a20d4bf5f603f58369aba17326c3 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 18 Feb 2017 14:38:08 -0800 Subject: working on incremental pdr --- src/proof/pdr/pdrIncr.c | 149 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 146 insertions(+), 3 deletions(-) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index d33b45ac..c4f384f5 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -38,6 +38,121 @@ extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, in /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ) +{ + Vec_Ptr_t * vArrayK; + Pdr_Set_t * pCube; + int i, k, Counter = 0; + Vec_VecForEachLevelStart( vClauses, vArrayK, k, kStart ) + { + Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare ); + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i ) + { + Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k ); + Pdr_SetPrint( stdout, pCube, nRegs, NULL ); + Abc_Print( 1, "\n" ); + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p ) +{ + int i, k; + Vec_Vec_t * vClausesSaved; + Pdr_Set_t * pCla; + + // Note that the last frame is empty + vClausesSaved = Vec_VecStart(Vec_VecSize(p->vClauses)-1); + Vec_VecForEachEntryStartStop( Pdr_Set_t *, p->vClauses, pCla, i, k, 0, Vec_VecSize(vClausesSaved) ) + Vec_VecPush(vClausesSaved, i, Pdr_SetDup(pCla)); + + return vClausesSaved; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k ) +{ + sat_solver * pSat; + Vec_Ptr_t * vArrayK; + Pdr_Set_t * pCube; + int i, j; + + assert( Vec_PtrSize(p->vSolvers) == k ); + assert( Vec_IntSize(p->vActVars) == k ); + + pSat = zsat_solver_new_seed(p->pPars->nRandomSeed); + pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) ); + Vec_PtrPush( p->vSolvers, pSat ); + Vec_IntPush( p->vActVars, 0 ); + + // set the property output + Pdr_ManSetPropertyOutput( p, k ); + // add the clauses + Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k ) + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j ) + Pdr_ManSolverAddClause( p, k, pCube ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) +{ + int i; + + assert(vClauses); + + Vec_VecFree(p->vClauses); + p->vClauses = vClauses; + + for ( i = 0; i < Vec_VecSize(p->vClauses); ++i ) + IPdr_ManSetSolver(p, i); + + return 0; +} + /**Function************************************************************* Synopsis [] @@ -59,7 +174,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p ) int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); abctime clkStart = Abc_Clock(), clkOne = 0; p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; - assert( Vec_PtrSize(p->vSolvers) == 0 ); + // assert( Vec_PtrSize(p->vSolvers) == 0 ); // in the multi-output mode, mark trivial POs (those fed by const0) as solved if ( p->pPars->fSolveAll ) Saig_ManForEachPo( p->pAig, pObj, iFrame ) @@ -72,7 +187,13 @@ int IPdr_ManSolveInt( Pdr_Man_t * p ) } // create the first timeframe p->pPars->timeLastSolved = Abc_Clock(); - Pdr_ManCreateSolver( p, (iFrame = 0) ); + + if ( Vec_VecSize(p->vClauses) == 0 ) + Pdr_ManCreateSolver( p, (iFrame = 0) ); + else { + iFrame = Vec_VecSize(p->vClauses); + Pdr_ManCreateSolver( p, iFrame ); + } while ( 1 ) { int fRefined = 0; @@ -406,6 +527,9 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) { Pdr_Man_t * p; int k, RetValue; + int i, nRegs; + Vec_Vec_t * vClausesSaved; + abctime clk = Abc_Clock(); if ( pPars->nTimeOutOne && !pPars->fSolveAll ) pPars->nTimeOutOne = 0; @@ -444,6 +568,26 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) else if ( RetValue == 1 ) Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); p->tTotal += Abc_Clock() - clk; + + if (pPars->iFrame == pPars->nFrameMax) + { + vClausesSaved = IPdr_ManSaveClauses(p); + nRegs = Aig_ManRegNum(p->pAig); + + Pdr_ManStop( p ); + + printf("PDR reached the max frame: %d\n", pPars->iFrame); + IPdr_ManPrintClauses(vClausesSaved, 0, nRegs); + + p = Pdr_ManStart( pAig, pPars, NULL ); + IPdr_ManRestore( p, vClausesSaved ); + + // Solve again + pPars->nFrameMax = pPars->nFrameMax + 1; + RetValue = IPdr_ManSolveInt(p); + IPdr_ManPrintClauses(p->vClauses, 0, nRegs); + } + Pdr_ManStop( p ); pPars->iFrame--; // convert all -2 (unknown) entries into -1 (undec) @@ -457,7 +601,6 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) } - /**Function************************************************************* Synopsis [] -- cgit v1.2.3 From fc0f3b8d0dbd15b57f2159a1119b1dcf5db0aa68 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sat, 18 Feb 2017 21:22:26 -0800 Subject: working on incremental pdr --- src/proof/pdr/pdrIncr.c | 70 +++++++++++++++++++++++++------------------------ 1 file changed, 36 insertions(+), 34 deletions(-) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index c4f384f5..aa07b668 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -527,7 +527,6 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) { Pdr_Man_t * p; int k, RetValue; - int i, nRegs; Vec_Vec_t * vClausesSaved; abctime clk = Abc_Clock(); @@ -549,46 +548,49 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) pPars->fSolveAll ? "yes" : "no" ); } ABC_FREE( pAig->pSeqModel ); + + p = Pdr_ManStart( pAig, pPars, NULL ); - RetValue = IPdr_ManSolveInt( p ); - if ( RetValue == 0 ) - assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); - if ( p->vCexes ) - { - assert( p->pAig->vSeqModelVec == NULL ); - p->pAig->vSeqModelVec = p->vCexes; - p->vCexes = NULL; - } - if ( p->pPars->fDumpInv ) - { - char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla"); - Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); - Pdr_ManDumpClauses( p, pFileName, RetValue==1 ); - } - else if ( RetValue == 1 ) - Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); - p->tTotal += Abc_Clock() - clk; + while ( 1 ) { + RetValue = IPdr_ManSolveInt( p ); - if (pPars->iFrame == pPars->nFrameMax) - { - vClausesSaved = IPdr_ManSaveClauses(p); - nRegs = Aig_ManRegNum(p->pAig); + if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) { + vClausesSaved = IPdr_ManSaveClauses( p ); - Pdr_ManStop( p ); + Pdr_ManStop( p ); - printf("PDR reached the max frame: %d\n", pPars->iFrame); - IPdr_ManPrintClauses(vClausesSaved, 0, nRegs); + p = Pdr_ManStart( pAig, pPars, NULL ); + IPdr_ManRestore( p, vClausesSaved ); - p = Pdr_ManStart( pAig, pPars, NULL ); - IPdr_ManRestore( p, vClausesSaved ); + pPars->nFrameMax = pPars->nFrameMax << 1; - // Solve again - pPars->nFrameMax = pPars->nFrameMax + 1; - RetValue = IPdr_ManSolveInt(p); - IPdr_ManPrintClauses(p->vClauses, 0, nRegs); - } + continue; + } + + if ( RetValue == 0 ) + assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); + if ( p->vCexes ) + { + assert( p->pAig->vSeqModelVec == NULL ); + p->pAig->vSeqModelVec = p->vCexes; + p->vCexes = NULL; + } + if ( p->pPars->fDumpInv ) + { + char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla"); + Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); + Pdr_ManDumpClauses( p, pFileName, RetValue==1 ); + } + else if ( RetValue == 1 ) + Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); - Pdr_ManStop( p ); + p->tTotal += Abc_Clock() - clk; + Pdr_ManStop( p ); + + break; + } + + pPars->iFrame--; // convert all -2 (unknown) entries into -1 (undec) if ( pPars->vOutMap ) -- cgit v1.2.3 From 24fdcecb2d034af4d7f7c26ec083f6baf1434018 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Feb 2017 09:20:44 -0800 Subject: started %pdra --- src/base/wlc/wlcCom.c | 117 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 117 insertions(+) diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 97717b09..6b542b94 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -33,6 +33,7 @@ static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ) static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPdrAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbs2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -75,6 +76,7 @@ void Wlc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%cone", Abc_CommandCone, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%abs", Abc_CommandAbs, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%pdra", Abc_CommandPdrAbs, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%abs2", Abc_CommandAbs2, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 ); @@ -442,6 +444,121 @@ usage: return 1; } +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + Wlc_Par_t Pars, * pPars = &Pars; + int c; + Wlc_ManSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsAdd < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMul = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMul < 0 ) + goto usage; + break; + case 'X': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMux = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMux < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsFlop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsFlop < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nIterMax < 0 ) + goto usage; + break; + case 'x': + pPars->fXorOutput ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fPdrVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); + return 0; + } + Wlc_NtkAbsCore( pNtk, pPars ); + return 0; +usage: + Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-xvwh]\n" ); + Abc_Print( -2, "\t abstraction for word-level networks\n" ); + Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); + Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); + Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); + Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); + Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + + /**Function******************************************************************** Synopsis [] -- cgit v1.2.3 From 6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Feb 2017 09:55:58 -0800 Subject: working on pdr with wla --- src/base/wlc/wlc.h | 1 + src/base/wlc/wlcAbs.c | 111 ++++++++++++++++++++++++++++++++++++++++++++++++ src/base/wlc/wlcCom.c | 2 +- src/proof/pdr/pdrIncr.c | 11 +++-- 4 files changed, 120 insertions(+), 5 deletions(-) diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 91dc0573..9ca56917 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -277,6 +277,7 @@ static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId ) /*=== wlcAbs.c ========================================================*/ extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); +extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcAbs2.c ========================================================*/ extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcBlast.c ========================================================*/ diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 318df4dd..cfd1155d 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -283,6 +283,117 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec return nNodes; } +/**Function************************************************************* + + Synopsis [Performs PDR with word-level abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +{ + abctime clk = Abc_Clock(); + int nIters, nNodes, nDcFlops, RetValue = -1; + // start the bitmap to mark objects that cannot be abstracted because of refinement + // currently, this bitmap is empty because abstraction begins without refinement + Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) ); + // set up parameters to run PDR + Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; + Pdr_ManSetDefaultParams( pPdrPars ); + pPdrPars->fVerbose = pPars->fPdrVerbose; + + // perform refinement iterations + for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) + { + Aig_Man_t * pAig; + Abc_Cex_t * pCex; + Vec_Int_t * vPisNew, * vRefine; + Gia_Man_t * pGia, * pTemp; + Wlc_Ntk_t * pAbs; + + if ( pPars->fVerbose ) + printf( "\nIteration %d:\n", nIters ); + + // get abstracted GIA and the set of pseudo-PIs (vPisNew) + pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose ); + pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 ); + + // if the abstraction has flops with DC-init state, + // new PIs were introduced by bit-blasting at the end of the PI list + // here we move these variables to be *before* PPIs, because + // PPIs are supposed to be at the end of the PI list for refinement + nDcFlops = Wlc_NtkDcFlopNum(pAbs); + if ( nDcFlops > 0 ) // DC-init flops are present + { + pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops ); + Gia_ManStop( pTemp ); + } + // if the word-level outputs have to be XORs, this is a place to do it + if ( pPars->fXorOutput ) + { + pGia = Gia_ManTransformMiter2( pTemp = pGia ); + Gia_ManStop( pTemp ); + } + if ( pPars->fVerbose ) + { + printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); + Gia_ManPrintStats( pGia, NULL ); + } + Wlc_NtkFree( pAbs ); + + // try to prove abstracted GIA by converting it to AIG and calling PDR + pAig = Gia_ManToAigSimple( pGia ); + RetValue = Pdr_ManSolve( pAig, pPdrPars ); + pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; + Aig_ManStop( pAig ); + + // consider outcomes + if ( pCex == NULL ) + { + assert( RetValue ); // proved or undecided + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + break; + } + + // perform refinement + vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + Gia_ManStop( pGia ); + Vec_IntFree( vPisNew ); + if ( vRefine == NULL ) // real CEX + { + Abc_CexFree( pCex ); // return CEX in the future + break; + } + + // update the set of objects to be un-abstracted + nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); + if ( pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); + Vec_IntFree( vRefine ); + Abc_CexFree( pCex ); + } + + Vec_BitFree( vUnmark ); + // report the result + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "Abstraction " ); + if ( RetValue == 0 ) + printf( "resulted in a real CEX" ); + else if ( RetValue == 1 ) + printf( "is successfully proved" ); + else + printf( "timed out" ); + printf( " after %d iterations. ", nIters ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return RetValue; +} + /**Function************************************************************* Synopsis [Performs abstraction.] diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 6b542b94..e980752b 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -541,7 +541,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); return 0; } - Wlc_NtkAbsCore( pNtk, pPars ); + Wlc_NtkPdrAbs( pNtk, pPars ); return 0; usage: Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-xvwh]\n" ); diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index aa07b668..2a718577 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -77,14 +77,17 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ) SeeAlso [] ***********************************************************************/ -Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p ) +Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ) { int i, k; Vec_Vec_t * vClausesSaved; Pdr_Set_t * pCla; - // Note that the last frame is empty - vClausesSaved = Vec_VecStart(Vec_VecSize(p->vClauses)-1); + if ( fDropLast ) + vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 ); + else + vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses) ); + Vec_VecForEachEntryStartStop( Pdr_Set_t *, p->vClauses, pCla, i, k, 0, Vec_VecSize(vClausesSaved) ) Vec_VecPush(vClausesSaved, i, Pdr_SetDup(pCla)); @@ -555,7 +558,7 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) RetValue = IPdr_ManSolveInt( p ); if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) { - vClausesSaved = IPdr_ManSaveClauses( p ); + vClausesSaved = IPdr_ManSaveClauses( p, 1 ); Pdr_ManStop( p ); -- cgit v1.2.3 From 840f5d1ca8d8d51fa28c2ac3cd7bc9dd2e245f29 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Feb 2017 10:22:15 -0800 Subject: working on pdr with wla --- src/base/wlc/wlcAbs.c | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index cfd1155d..b6571e53 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -20,6 +20,7 @@ #include "wlc.h" #include "proof/pdr/pdr.h" +#include "proof/pdr/pdrInt.h" #include "aig/gia/giaAig.h" #include "sat/bmc/bmc.h" @@ -29,6 +30,10 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ); +extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ); +extern int IPdr_ManSolveInt( Pdr_Man_t * p ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -297,6 +302,8 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { abctime clk = Abc_Clock(); + Pdr_Man_t * pPdr; + Vec_Vec_t * vClauses = NULL; int nIters, nNodes, nDcFlops, RetValue = -1; // start the bitmap to mark objects that cannot be abstracted because of refinement // currently, this bitmap is empty because abstraction begins without refinement @@ -347,9 +354,14 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) // try to prove abstracted GIA by converting it to AIG and calling PDR pAig = Gia_ManToAigSimple( pGia ); - RetValue = Pdr_ManSolve( pAig, pPdrPars ); + + pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); + if (vClauses) + IPdr_ManRestore(pPdr, vClauses); + + RetValue = IPdr_ManSolveInt( pPdr ); + pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; - Aig_ManStop( pAig ); // consider outcomes if ( pCex == NULL ) @@ -357,6 +369,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) assert( RetValue ); // proved or undecided Gia_ManStop( pGia ); Vec_IntFree( vPisNew ); + Pdr_ManStop( pPdr ); + Aig_ManStop( pAig ); break; } @@ -367,15 +381,22 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) if ( vRefine == NULL ) // real CEX { Abc_CexFree( pCex ); // return CEX in the future + Pdr_ManStop( pPdr ); + Aig_ManStop( pAig ); break; } + // spurious CEX, continue solving + vClauses = IPdr_ManSaveClauses( pPdr, 0 ); + Pdr_ManStop( pPdr ); + // update the set of objects to be un-abstracted nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); if ( pPars->fVerbose ) printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); Vec_IntFree( vRefine ); Abc_CexFree( pCex ); + Aig_ManStop( pAig ); } Vec_BitFree( vUnmark ); -- cgit v1.2.3 From 2732cbc1ee3b82fa7f609ef4c7156132058612dc Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Feb 2017 12:31:28 -0800 Subject: working on pdr with wla --- src/base/wlc/wlcAbs.c | 30 +++++++++++++++++++++++++----- src/proof/pdr/pdrIncr.c | 3 +++ 2 files changed, 28 insertions(+), 5 deletions(-) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index b6571e53..342d667f 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -133,6 +133,17 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * Wlc_NtkCleanMarks( p ); Wlc_NtkForEachCo( p, pObj, i ) Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops ); + + + Vec_IntClear(vFlops); + Wlc_NtkForEachCi( p, pObj, i ) { + if ( !Wlc_ObjIsPi(pObj) ) { + Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) ); + pObj->Mark = 1; + } + } + + Wlc_NtkForEachObjVec( vFlops, p, pObj, i ) Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops ); Wlc_NtkForEachObj( p, pObj, i ) @@ -312,6 +323,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; Pdr_ManSetDefaultParams( pPdrPars ); pPdrPars->fVerbose = pPars->fPdrVerbose; + pPdrPars->fVeryVerbose = 1; // perform refinement iterations for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) @@ -356,8 +368,15 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pAig = Gia_ManToAigSimple( pGia ); pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); - if (vClauses) - IPdr_ManRestore(pPdr, vClauses); + if ( vClauses ) { + if ( Vec_VecSize( vClauses) == 1 ) { + Vec_VecFree( vClauses ); + vClauses = NULL; + } else { + assert( Vec_VecSize( vClauses) >= 2 ); + IPdr_ManRestore(pPdr, vClauses); + } + } RetValue = IPdr_ManSolveInt( pPdr ); @@ -441,11 +460,12 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) // set up parameters to run PDR Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; Pdr_ManSetDefaultParams( pPdrPars ); - pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction) - pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization) - pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) + //pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction) + //pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization) + //pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this pPdrPars->fVerbose = pPars->fPdrVerbose; + pPdrPars->fVeryVerbose = 1; // perform refinement iterations for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) { diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 2a718577..b1f126f4 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -147,6 +147,9 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) assert(vClauses); + printf( "IPdr restore:\n" ); + IPdr_ManPrintClauses( vClauses, 0, Aig_ManRegNum( p->pAig ) ); + Vec_VecFree(p->vClauses); p->vClauses = vClauses; -- cgit v1.2.3 From 2d1792040a8c09a12d70413ceb99bd11bb145c2b Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Feb 2017 15:57:13 -0800 Subject: working on pdr with wla --- src/base/wlc/wlcAbs.c | 16 ++++++---------- src/proof/pdr/pdrIncr.c | 47 ++++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 48 insertions(+), 15 deletions(-) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 342d667f..8cc79722 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -323,7 +323,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; Pdr_ManSetDefaultParams( pPdrPars ); pPdrPars->fVerbose = pPars->fPdrVerbose; - pPdrPars->fVeryVerbose = 1; + pPdrPars->fVeryVerbose = 0; // perform refinement iterations for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) @@ -368,14 +368,10 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pAig = Gia_ManToAigSimple( pGia ); pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); + if ( vClauses ) { - if ( Vec_VecSize( vClauses) == 1 ) { - Vec_VecFree( vClauses ); - vClauses = NULL; - } else { - assert( Vec_VecSize( vClauses) >= 2 ); - IPdr_ManRestore(pPdr, vClauses); - } + assert( Vec_VecSize( vClauses) >= 2 ); + IPdr_ManRestore( pPdr, vClauses ); } RetValue = IPdr_ManSolveInt( pPdr ); @@ -406,7 +402,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } // spurious CEX, continue solving - vClauses = IPdr_ManSaveClauses( pPdr, 0 ); + vClauses = IPdr_ManSaveClauses( pPdr, 1 ); Pdr_ManStop( pPdr ); // update the set of objects to be un-abstracted @@ -465,7 +461,7 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) //pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this pPdrPars->fVerbose = pPars->fPdrVerbose; - pPdrPars->fVeryVerbose = 1; + pPdrPars->fVeryVerbose = 0; // perform refinement iterations for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) { diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index b1f126f4..4f66eeb4 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -66,6 +66,41 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ) } } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IPdr_ManCheckClauses( Pdr_Man_t * p ) +{ + Pdr_Set_t * pCubeK; + Vec_Ptr_t * vArrayK; + int j, k, RetValue, kMax = Vec_PtrSize(p->vSolvers)-1; + int iStartFrame = 1; + + Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax ) + { + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) + { + RetValue = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 ); + + if ( !RetValue ) { + printf( "Cube[%d][%d] not inductive!\n", k, j ); + } + + assert( RetValue == 1 ); + } + } + + return 1; +} + /**Function************************************************************* Synopsis [] @@ -83,6 +118,11 @@ Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ) Vec_Vec_t * vClausesSaved; Pdr_Set_t * pCla; + if ( Vec_VecSize( p->vClauses ) == 1 ) + return NULL; + if ( Vec_VecSize( p->vClauses ) == 2 && fDropLast ) + return NULL; + if ( fDropLast ) vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 ); else @@ -147,9 +187,6 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) assert(vClauses); - printf( "IPdr restore:\n" ); - IPdr_ManPrintClauses( vClauses, 0, Aig_ManRegNum( p->pAig ) ); - Vec_VecFree(p->vClauses); p->vClauses = vClauses; @@ -197,8 +234,8 @@ int IPdr_ManSolveInt( Pdr_Man_t * p ) if ( Vec_VecSize(p->vClauses) == 0 ) Pdr_ManCreateSolver( p, (iFrame = 0) ); else { - iFrame = Vec_VecSize(p->vClauses); - Pdr_ManCreateSolver( p, iFrame ); + iFrame = Vec_VecSize(p->vClauses) - 1; + IPdr_ManCheckClauses( p ); } while ( 1 ) { -- cgit v1.2.3 From 1a66a5823a37123c099e63cb94bba1fd844487d1 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Feb 2017 16:09:59 -0800 Subject: working on pdr with wla --- src/base/wlc/wlcAbs.c | 2 +- src/proof/pdr/pdrIncr.c | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 8cc79722..47bd9a3f 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -402,7 +402,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } // spurious CEX, continue solving - vClauses = IPdr_ManSaveClauses( pPdr, 1 ); + vClauses = IPdr_ManSaveClauses( pPdr, 0 ); Pdr_ManStop( pPdr ); // update the set of objects to be un-abstracted diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 4f66eeb4..9f7dfd90 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -81,14 +81,16 @@ int IPdr_ManCheckClauses( Pdr_Man_t * p ) { Pdr_Set_t * pCubeK; Vec_Ptr_t * vArrayK; - int j, k, RetValue, kMax = Vec_PtrSize(p->vSolvers)-1; + int j, k, RetValue, kMax = Vec_PtrSize(p->vSolvers); int iStartFrame = 1; + int counter = 0; Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax ) { Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) { - RetValue = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 ); + ++counter; + RetValue = Pdr_ManCheckCube( p, k - 1, pCubeK, NULL, 0, 0, 1 ); if ( !RetValue ) { printf( "Cube[%d][%d] not inductive!\n", k, j ); @@ -97,6 +99,7 @@ int IPdr_ManCheckClauses( Pdr_Man_t * p ) assert( RetValue == 1 ); } } + printf( "XXX: Pass check clauses! %d frames and %d clauses checked\n", k, counter ); return 1; } -- cgit v1.2.3 From 25ecc3d42973cd832d78b00cbed188171892325d Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Feb 2017 19:57:44 -0800 Subject: fixed a tricky bug: property should not be assumed true in the last frame --- src/proof/pdr/pdrIncr.c | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 9f7dfd90..09a06a27 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -99,7 +99,6 @@ int IPdr_ManCheckClauses( Pdr_Man_t * p ) assert( RetValue == 1 ); } } - printf( "XXX: Pass check clauses! %d frames and %d clauses checked\n", k, counter ); return 1; } @@ -149,7 +148,7 @@ Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ) SeeAlso [] ***********************************************************************/ -sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k ) +sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int nTotal ) { sat_solver * pSat; Vec_Ptr_t * vArrayK; @@ -165,7 +164,12 @@ sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k ) Vec_IntPush( p->vActVars, 0 ); // set the property output - Pdr_ManSetPropertyOutput( p, k ); + if ( k < nTotal - 1 ) + Pdr_ManSetPropertyOutput( p, k ); + + if (k == 0) + return pSat; + // add the clauses Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k ) Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j ) @@ -194,7 +198,7 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) p->vClauses = vClauses; for ( i = 0; i < Vec_VecSize(p->vClauses); ++i ) - IPdr_ManSetSolver(p, i); + IPdr_ManSetSolver( p, i, Vec_VecSize( p->vClauses ) ); return 0; } -- cgit v1.2.3 From 222b3741a40af2913132ef385936b955bbc19b4d Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Mon, 20 Feb 2017 10:13:18 -0800 Subject: fixed time profiling in pdr --- src/base/wlc/wlcAbs.c | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 47bd9a3f..902c060d 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -313,6 +313,7 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { abctime clk = Abc_Clock(); + abctime pdrClk; Pdr_Man_t * pPdr; Vec_Vec_t * vClauses = NULL; int nIters, nNodes, nDcFlops, RetValue = -1; @@ -368,6 +369,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pAig = Gia_ManToAigSimple( pGia ); pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); + pdrClk = Abc_Clock(); if ( vClauses ) { assert( Vec_VecSize( vClauses) >= 2 ); @@ -375,6 +377,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } RetValue = IPdr_ManSolveInt( pPdr ); + pPdr->tTotal += Abc_Clock() - pdrClk; pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; @@ -403,6 +406,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) // spurious CEX, continue solving vClauses = IPdr_ManSaveClauses( pPdr, 0 ); + Pdr_ManStop( pPdr ); // update the set of objects to be un-abstracted -- cgit v1.2.3 From 19510bd38e46fd913bf6dc29393938e50fd717ee Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Mon, 20 Feb 2017 11:07:12 -0800 Subject: added datastructure for %pdra options --- src/base/wlc/wlc.h | 18 +++++++++++++++++- src/base/wlc/wlcAbs.c | 27 ++++++++++++++++++++++++++- src/base/wlc/wlcCom.c | 4 ++-- 3 files changed, 45 insertions(+), 4 deletions(-) diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 9ca56917..cf8bdab4 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -174,6 +174,21 @@ struct Wlc_Par_t_ int fPdrVerbose; // verbose output }; + +typedef struct WlcPdr_Par_t_ WlcPdr_Par_t; +struct WlcPdr_Par_t_ +{ + int nBitsAdd; // adder bit-width + int nBitsMul; // multiplier bit-widht + int nBitsMux; // MUX bit-width + int nBitsFlop; // flop bit-width + int nIterMax; // the max number of iterations + int fXorOutput; // XOR outputs of word-level miter + int fVerbose; // verbose output + int fPdrVerbose; // verbose output +}; + + static inline int Wlc_NtkObjNum( Wlc_Ntk_t * p ) { return p->iObj - 1; } static inline int Wlc_NtkObjNumMax( Wlc_Ntk_t * p ) { return p->iObj; } static inline int Wlc_NtkPiNum( Wlc_Ntk_t * p ) { return Vec_IntSize(&p->vPis); } @@ -277,7 +292,7 @@ static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId ) /*=== wlcAbs.c ========================================================*/ extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); -extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); +extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars ); /*=== wlcAbs2.c ========================================================*/ extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcBlast.c ========================================================*/ @@ -286,6 +301,7 @@ extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int i extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ); /*=== wlcNtk.c ========================================================*/ extern void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ); +extern void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ); extern char * Wlc_ObjTypeName( Wlc_Obj_t * p ); extern Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc ); extern int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg ); diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 902c060d..8fde7f56 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -38,6 +38,31 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p ); /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ) +{ + memset( pPars, 0, sizeof(WlcPdr_Par_t) ); + pPars->nBitsAdd = ABC_INFINITY; // adder bit-width + pPars->nBitsMul = ABC_INFINITY; // multiplier bit-width + pPars->nBitsMux = ABC_INFINITY; // MUX bit-width + pPars->nBitsFlop = ABC_INFINITY; // flop bit-width + pPars->nIterMax = 1000; // the max number of iterations + pPars->fXorOutput = 1; // XOR outputs of word-level miter + pPars->fVerbose = 0; // verbose output + pPars->fPdrVerbose = 0; // show verbose PDR output +} + /**Function************************************************************* Synopsis [Mark operators that meet the abstraction criteria.] @@ -310,7 +335,7 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec SeeAlso [] ***********************************************************************/ -int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars ) { abctime clk = Abc_Clock(); abctime pdrClk; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index e980752b..d30b376e 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -458,9 +458,9 @@ usage: int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); - Wlc_Par_t Pars, * pPars = &Pars; + WlcPdr_Par_t Pars, * pPars = &Pars; int c; - Wlc_ManSetDefaultParams( pPars ); + WlcPdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) { -- cgit v1.2.3 From 9f43c84501cf8c5a8ae74cc5bebea63dafc3a714 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Mon, 20 Feb 2017 12:51:04 -0800 Subject: added options of checking and pushing to %pdra --- src/base/wlc/wlc.h | 2 ++ src/base/wlc/wlcAbs.c | 10 ++++++---- src/base/wlc/wlcCom.c | 12 ++++++++++-- src/proof/pdr/pdrIncr.c | 37 +++++++++++++++++++++++++++++++++---- 4 files changed, 51 insertions(+), 10 deletions(-) diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index cf8bdab4..9cb34bf3 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -184,6 +184,8 @@ struct WlcPdr_Par_t_ int nBitsFlop; // flop bit-width int nIterMax; // the max number of iterations int fXorOutput; // XOR outputs of word-level miter + int fCheckClauses; // Check clauses in the reloaded trace + int fPushClauses; // Push clauses in the reloaded trace int fVerbose; // verbose output int fPdrVerbose; // verbose output }; diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 8fde7f56..fbaa1b8a 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -32,7 +32,7 @@ ABC_NAMESPACE_IMPL_START extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ); extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ); -extern int IPdr_ManSolveInt( Pdr_Man_t * p ); +extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -59,6 +59,8 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ) pPars->nBitsFlop = ABC_INFINITY; // flop bit-width pPars->nIterMax = 1000; // the max number of iterations pPars->fXorOutput = 1; // XOR outputs of word-level miter + pPars->fCheckClauses = 1; // Check clauses in the reloaded trace + pPars->fPushClauses = 0; // Push clauses in the reloaded trace pPars->fVerbose = 0; // verbose output pPars->fPdrVerbose = 0; // show verbose PDR output } @@ -76,7 +78,7 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) +static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) { Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) ); Wlc_Obj_t * pObj; int i, Count[4] = {0}; @@ -197,7 +199,7 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * SeeAlso [] ***********************************************************************/ -static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose ) +static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose ) { Wlc_Ntk_t * pNtkNew = NULL; Vec_Int_t * vPisOld = Vec_IntAlloc( 100 ); @@ -401,7 +403,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars ) IPdr_ManRestore( pPdr, vClauses ); } - RetValue = IPdr_ManSolveInt( pPdr ); + RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses ); pPdr->tTotal += Abc_Clock() - pdrClk; pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index d30b376e..7801abc6 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; WlcPdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF ) { switch ( c ) { @@ -524,6 +524,12 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'x': pPars->fXorOutput ^= 1; break; + case 'c': + pPars->fCheckClauses ^= 1; + break; + case 'p': + pPars->fPushClauses ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -544,7 +550,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_NtkPdrAbs( pNtk, pPars ); return 0; usage: - Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-xvwh]\n" ); + Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" ); Abc_Print( -2, "\t abstraction for word-level networks\n" ); Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); @@ -552,6 +558,8 @@ usage: Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" ); + Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 09a06a27..85403a7d 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -68,7 +68,9 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ) /**Function************************************************************* - Synopsis [] + Synopsis [ Check if each cube c_k in frame k satisfies the query + R_{k-1} && T && !c_k && c_k' (must be UNSAT). + Return True if all cubes pass the check. ] Description [] @@ -214,7 +216,7 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) SeeAlso [] ***********************************************************************/ -int IPdr_ManSolveInt( Pdr_Man_t * p ) +int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) { int fPrintClauses = 0; Pdr_Set_t * pCube = NULL; @@ -242,7 +244,34 @@ int IPdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManCreateSolver( p, (iFrame = 0) ); else { iFrame = Vec_VecSize(p->vClauses) - 1; - IPdr_ManCheckClauses( p ); + + if ( fCheckClauses ) + { + if ( p->pPars->fVerbose ) + Abc_Print( 1, "IPDR: Checking the reloaded length-%d trace...", iFrame + 1 ) ; + IPdr_ManCheckClauses( p ); + if ( p->pPars->fVerbose ) + Abc_Print( 1, " Passed!\n" ) ; + } + + if ( fPushClauses ) + { + p->iUseFrame = Abc_MaxInt(iFrame, 1); + + if ( p->pPars->fVerbose ) + { + Abc_Print( 1, "IPDR: Pushing the reloaded clauses. Before:\n" ); + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + } + + RetValue = Pdr_ManPushClauses( p ); + + if ( p->pPars->fVerbose ) + { + Abc_Print( 1, "IPDR: Finished pushing. After:\n" ); + Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); + } + } } while ( 1 ) { @@ -602,7 +631,7 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) p = Pdr_ManStart( pAig, pPars, NULL ); while ( 1 ) { - RetValue = IPdr_ManSolveInt( p ); + RetValue = IPdr_ManSolveInt( p, 1, 0 ); if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) { vClausesSaved = IPdr_ManSaveClauses( p, 1 ); -- cgit v1.2.3 From c5e9506f5d5a5303b9df453fce7f313147799276 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Mon, 20 Feb 2017 12:58:20 -0800 Subject: small tweaks in %pdra -p --- src/proof/pdr/pdrIncr.c | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 85403a7d..6de86c18 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -271,6 +271,13 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ) Abc_Print( 1, "IPDR: Finished pushing. After:\n" ); Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); } + + if ( RetValue ) + { + Pdr_ManReportInvariant( p ); + Pdr_ManVerifyInvariant( p ); + return 1; + } } } while ( 1 ) -- cgit v1.2.3 From 01e6beea8e617eb5ef4f9b621b009eded9498a1f Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Tue, 21 Feb 2017 20:06:13 -0800 Subject: clean up --- fsm.v | 28 ---------------------------- src/base/wlc/wlc.h | 18 +----------------- src/base/wlc/wlcAbs.c | 33 +++------------------------------ src/base/wlc/wlcCom.c | 4 ++-- src/base/wlc/wlcNtk.c | 2 ++ 5 files changed, 8 insertions(+), 77 deletions(-) delete mode 100644 fsm.v diff --git a/fsm.v b/fsm.v deleted file mode 100644 index 272c4a89..00000000 --- a/fsm.v +++ /dev/null @@ -1,28 +0,0 @@ -module fsm (out); -output out; - -wire [2:0] ns; -wire [2:0] cs; - -always @( ns or cs ) -begin -case (cs) - 0 : ns = 3'b010; - 1 : ns = 3'b001; - 2 : ns = 3'b000; - 3 : ns = 3'b101; - 4 : ns = 3'b001; - 5 : ns = 3'b111; - 6 : ns = 3'b001; - 7 : ns = 3'b110; -endcase -end - -assign out = cs == 3'b001; - -wire [2:0] const0 = 3'h0; - - -CPL_FF#3 ff3 ( .q(cs), .qbar(), .d(ns), .clk(), .arst(), .arstval(const0) ); - -endmodule diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 9cb34bf3..686d9f00 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -163,20 +163,6 @@ struct Wlc_Ntk_t_ typedef struct Wlc_Par_t_ Wlc_Par_t; struct Wlc_Par_t_ -{ - int nBitsAdd; // adder bit-width - int nBitsMul; // multiplier bit-widht - int nBitsMux; // MUX bit-width - int nBitsFlop; // flop bit-width - int nIterMax; // the max number of iterations - int fXorOutput; // XOR outputs of word-level miter - int fVerbose; // verbose output - int fPdrVerbose; // verbose output -}; - - -typedef struct WlcPdr_Par_t_ WlcPdr_Par_t; -struct WlcPdr_Par_t_ { int nBitsAdd; // adder bit-width int nBitsMul; // multiplier bit-widht @@ -190,7 +176,6 @@ struct WlcPdr_Par_t_ int fPdrVerbose; // verbose output }; - static inline int Wlc_NtkObjNum( Wlc_Ntk_t * p ) { return p->iObj - 1; } static inline int Wlc_NtkObjNumMax( Wlc_Ntk_t * p ) { return p->iObj; } static inline int Wlc_NtkPiNum( Wlc_Ntk_t * p ) { return Vec_IntSize(&p->vPis); } @@ -294,7 +279,7 @@ static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId ) /*=== wlcAbs.c ========================================================*/ extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); -extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars ); +extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcAbs2.c ========================================================*/ extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcBlast.c ========================================================*/ @@ -303,7 +288,6 @@ extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int i extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ); /*=== wlcNtk.c ========================================================*/ extern void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ); -extern void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ); extern char * Wlc_ObjTypeName( Wlc_Obj_t * p ); extern Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc ); extern int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg ); diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index fbaa1b8a..1e5df918 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -38,33 +38,6 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ) -{ - memset( pPars, 0, sizeof(WlcPdr_Par_t) ); - pPars->nBitsAdd = ABC_INFINITY; // adder bit-width - pPars->nBitsMul = ABC_INFINITY; // multiplier bit-width - pPars->nBitsMux = ABC_INFINITY; // MUX bit-width - pPars->nBitsFlop = ABC_INFINITY; // flop bit-width - pPars->nIterMax = 1000; // the max number of iterations - pPars->fXorOutput = 1; // XOR outputs of word-level miter - pPars->fCheckClauses = 1; // Check clauses in the reloaded trace - pPars->fPushClauses = 0; // Push clauses in the reloaded trace - pPars->fVerbose = 0; // verbose output - pPars->fPdrVerbose = 0; // show verbose PDR output -} - /**Function************************************************************* Synopsis [Mark operators that meet the abstraction criteria.] @@ -78,7 +51,7 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) +static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) { Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) ); Wlc_Obj_t * pObj; int i, Count[4] = {0}; @@ -199,7 +172,7 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * SeeAlso [] ***********************************************************************/ -static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose ) +static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose ) { Wlc_Ntk_t * pNtkNew = NULL; Vec_Int_t * vPisOld = Vec_IntAlloc( 100 ); @@ -337,7 +310,7 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec SeeAlso [] ***********************************************************************/ -int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars ) +int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { abctime clk = Abc_Clock(); abctime pdrClk; diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 7801abc6..df736e70 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -458,9 +458,9 @@ usage: int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); - WlcPdr_Par_t Pars, * pPars = &Pars; + Wlc_Par_t Pars, * pPars = &Pars; int c; - WlcPdr_ManSetDefaultParams( pPars ); + Wlc_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF ) { diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index e6ab0739..c8fc15a7 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -114,6 +114,8 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) pPars->nBitsFlop = ABC_INFINITY; // flop bit-width pPars->nIterMax = 1000; // the max number of iterations pPars->fXorOutput = 1; // XOR outputs of word-level miter + pPars->fCheckClauses = 1; // Check clauses in the reloaded trace + pPars->fPushClauses = 0; // Push clauses in the reloaded trace pPars->fVerbose = 0; // verbose output` pPars->fPdrVerbose = 0; // show verbose PDR output } -- cgit v1.2.3 From fb2fbd70bd31eb08dd50c66788d5165697ca6925 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Tue, 21 Feb 2017 20:10:11 -0800 Subject: clean up --- src/base/abci/abc.c | 269 ---------------------------------------------------- 1 file changed, 269 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0645c6e3..52684f8c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -333,7 +333,6 @@ static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv ); 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_CommandIPdr ( Abc_Frame_t * pAbc, int argc, char ** argv ); #ifdef ABC_USE_CUDD static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, char ** argv ); #endif @@ -984,7 +983,6 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 ); Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 ); Cmd_CommandAdd( pAbc, "Verification", "pdr", Abc_CommandPdr, 0 ); - Cmd_CommandAdd( pAbc, "Verification", "ipdr", Abc_CommandIPdr, 0 ); #ifdef ABC_USE_CUDD Cmd_CommandAdd( pAbc, "Verification", "reconcile", Abc_CommandReconcile, 1 ); #endif @@ -26417,273 +26415,6 @@ usage: - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); - extern int Abc_NtkDarIPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars ); - Pdr_Par_t Pars, * pPars = &Pars; - Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); - int c; - Pdr_ManSetDefaultParams( pPars ); - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegjonctkvwzh" ) ) != EOF ) - { - switch ( c ) - { - case 'M': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nRecycle = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nRecycle < 0 ) - goto usage; - break; - case 'F': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nFrameMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nFrameMax < 0 ) - goto usage; - break; - case 'C': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nConfLimit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nConfLimit < 0 ) - goto usage; - break; - case 'D': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nConfGenLimit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nConfGenLimit < 0 ) - goto usage; - break; - case 'Q': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nRestLimit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nRestLimit < 0 ) - goto usage; - break; - case 'T': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nTimeOut = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nTimeOut < 0 ) - goto usage; - break; - case 'H': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nTimeOutOne = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nTimeOutOne < 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; - } - pPars->nTimeOutGap = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nTimeOutGap < 0 ) - goto usage; - break; - case 'S': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nRandomSeed = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nRandomSeed < 0 ) - goto usage; - break; - case 'a': - pPars->fSolveAll ^= 1; - break; - case 'x': - pPars->fStoreCex ^= 1; - break; - case 'r': - pPars->fTwoRounds ^= 1; - break; - case 'm': - pPars->fMonoCnf ^= 1; - break; - case 'u': - pPars->fNewXSim ^= 1; - break; - case 'y': - pPars->fFlopPrio ^= 1; - break; - case 'f': - pPars->fFlopOrder ^= 1; - break; - case 's': - pPars->fShortest ^= 1; - break; - case 'i': - pPars->fShiftStart ^= 1; - break; - case 'p': - pPars->fReuseProofOblig ^= 1; - break; - case 'd': - pPars->fDumpInv ^= 1; - break; - case 'e': - pPars->fUseSupp ^= 1; - break; - case 'g': - pPars->fSkipGeneral ^= 1; - break; - case 'j': - pPars->fSimpleGeneral ^= 1; - break; - case 'o': - pPars->fUsePropOut ^= 1; - break; - case 'n': - pPars->fSkipDown ^= 1; - break; - case 'c': - pPars->fCtgs ^= 1; - break; - case 't': - pPars->fUseAbs ^= 1; - break; - case 'k': - pPars->fUseSimpleRef ^= 1; - break; - case 'v': - pPars->fVerbose ^= 1; - break; - case 'w': - pPars->fVeryVerbose ^= 1; - break; - case 'z': - pPars->fNotVerbose ^= 1; - break; - case 'h': - default: - goto usage; - } - } - if ( pNtk == NULL ) - { - Abc_Print( -2, "There is no current network.\n"); - return 0; - } - if ( Abc_NtkLatchNum(pNtk) == 0 ) - { - Abc_Print( 0, "The current network is combinational.\n"); - return 0; - } - if ( !Abc_NtkIsStrash(pNtk) ) - { - Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n"); - return 0; - } - // run the procedure - pPars->fUseBridge = pAbc->fBridgeMode; - pAbc->Status = Abc_NtkDarIPdr( pNtk, pPars ); - pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; - Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap ); - if ( pNtk->vSeqModelVec ) - Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); - else - Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); - return 0; - -usage: - Abc_Print( -2, "usage: ipdr [-MFCDQTHGS ] [-axrmuyfsipdegjonctkvwzh]\n" ); - Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); - Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" ); - Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" ); - Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle ); - Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax ); - Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit ); - Abc_Print( -2, "\t-D num : limit on conflicts during ind-generalization (0 = no limit) [default = %d]\n",pPars->nConfGenLimit ); - Abc_Print( -2, "\t-Q num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit ); - Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); - Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap ); - Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed ); - Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); - Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); - Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" ); - Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" ); - Abc_Print( -2, "\t-u : toggle updated X-valued simulation [default = %s]\n", pPars->fNewXSim? "yes": "no" ); - Abc_Print( -2, "\t-y : toggle using structural flop priorities [default = %s]\n", pPars->fFlopPrio? "yes": "no" ); - Abc_Print( -2, "\t-f : toggle ordering flops by cost before generalization [default = %s]\n", pPars->fFlopOrder? "yes": "no" ); - Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" ); - Abc_Print( -2, "\t-i : toggle clause pushing from an intermediate timeframe [default = %s]\n", pPars->fShiftStart? "yes": "no" ); - Abc_Print( -2, "\t-p : toggle reusing proof-obligations in the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" ); - Abc_Print( -2, "\t-d : toggle dumping invariant (valid if init state is all-0) [default = %s]\n", pPars->fDumpInv? "yes": "no" ); - Abc_Print( -2, "\t-e : toggle using only support variables in the invariant [default = %s]\n", pPars->fUseSupp? "yes": "no" ); - Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" ); - Abc_Print( -2, "\t-j : toggle using simplified generalization step [default = %s]\n", pPars->fSimpleGeneral? "yes": "no" ); - Abc_Print( -2, "\t-o : toggle using property output as inductive hypothesis [default = %s]\n", pPars->fUsePropOut? "yes": "no" ); - Abc_Print( -2, "\t-n : * toggle skipping \'down\' in generalization [default = %s]\n", pPars->fSkipDown? "yes": "no" ); - Abc_Print( -2, "\t-c : * toggle handling CTGs in \'down\' [default = %s]\n", pPars->fCtgs? "yes": "no" ); - Abc_Print( -2, "\t-t : toggle using abstraction [default = %s]\n", pPars->fUseAbs? "yes": "no" ); - Abc_Print( -2, "\t-k : toggle using simplified refinement [default = %s]\n", pPars->fUseSimpleRef? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); - Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n\n"); - Abc_Print( -2, "\t* Implementation of switches -S, -n, and -c is contributed by Zyad Hassan.\n"); - Abc_Print( -2, "\t The theory and experiments supporting this work can be found in the following paper:\n"); - Abc_Print( -2, "\t Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, \"Better Generalization in IC3\", FMCAD 2013.\n"); - Abc_Print( -2, "\t (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/85-Better-Generalization-IC3.pdf)\n"); - - - return 1; } -- cgit v1.2.3