From c4446189a9ca5a187a2ede26a7102866d2c5ae8e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 14 Jan 2016 20:42:22 -0800 Subject: Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network. --- src/base/abci/abc.c | 16 ++++- src/base/main/main.h | 2 + src/base/main/mainFrame.c | 4 ++ src/base/main/mainInt.h | 2 + src/base/wlc/module.make | 1 + src/base/wlc/wlcAbc.c | 154 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/wlc/wlcBlast.c | 46 -------------- src/base/wlc/wlcCom.c | 67 +++++++++++++++++++- src/proof/pdr/pdr.h | 1 + src/proof/pdr/pdrCore.c | 24 ++++---- src/proof/pdr/pdrInt.h | 6 +- src/proof/pdr/pdrInv.c | 150 ++++++++++++++++++++++++++++++++++++++++++-- src/proof/pdr/pdrMan.c | 1 + src/proof/pdr/pdrSat.c | 11 +++- src/proof/pdr/pdrUtil.c | 40 ++++++++++++ 15 files changed, 457 insertions(+), 68 deletions(-) create mode 100644 src/base/wlc/wlcAbc.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a860a5a9..cd5f6e98 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -24985,7 +24985,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTHGaxrmsipdgvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGaxrmsipdgvwzh" ) ) != EOF ) { switch ( c ) { @@ -25022,6 +25022,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 'R': if ( globalUtilOptind >= argc ) { @@ -25134,13 +25145,14 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: pdr [-MFCRTHG ] [-axrmsipdgvwzh]\n" ); + Abc_Print( -2, "usage: pdr [-MFCDRTHG ] [-axrmsipdgvwzh]\n" ); Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" ); Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\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-R 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 ); diff --git a/src/base/main/main.h b/src/base/main/main.h index 44ec1c57..4fc2f87a 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -143,6 +143,8 @@ extern ABC_DLL void Abc_FrameSetStatus( int Status ); extern ABC_DLL void Abc_FrameSetManDsd( void * pMan ); extern ABC_DLL void Abc_FrameSetManDsd2( void * pMan ); extern ABC_DLL void Abc_FrameSetInv( Vec_Int_t * vInv ); +extern ABC_DLL void Abc_FrameSetCnf( Vec_Int_t * vInv ); +extern ABC_DLL void Abc_FrameSetStr( Vec_Str_t * vInv ); extern ABC_DLL int Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 54c97854..16c11288 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -93,6 +93,8 @@ void Abc_FrameSetStatus( int Status ) { ABC_FREE( s_Globa void Abc_FrameSetManDsd( void * pMan ) { if (s_GlobalFrame->pManDsd && s_GlobalFrame->pManDsd != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd, 0); s_GlobalFrame->pManDsd = pMan; } void Abc_FrameSetManDsd2( void * pMan ) { if (s_GlobalFrame->pManDsd2 && s_GlobalFrame->pManDsd2 != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd2, 0); s_GlobalFrame->pManDsd2 = pMan; } void Abc_FrameSetInv( Vec_Int_t * vInv ) { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; } +void Abc_FrameSetCnf( Vec_Int_t * vCnf ) { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcCnf); s_GlobalFrame->pAbcWlcCnf = vCnf; } +void Abc_FrameSetStr( Vec_Str_t * vStr ) { Vec_StrFreeP(&s_GlobalFrame->pAbcWlcStr); s_GlobalFrame->pAbcWlcStr = vStr; } int Abc_FrameIsBatchMode() { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0; } @@ -221,6 +223,8 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) ABC_FREE( p->pCex2 ); ABC_FREE( p->pCex ); Vec_IntFreeP( &p->pAbcWlcInv ); + Vec_IntFreeP( &p->pAbcWlcCnf ); + Vec_StrFreeP( &p->pAbcWlcStr ); ABC_FREE( p ); s_GlobalFrame = NULL; } diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index c7535c74..4082bab0 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -129,6 +129,8 @@ struct Abc_Frame_t_ void * pAbc85Delay; void * pAbcWlc; Vec_Int_t * pAbcWlcInv; + Vec_Int_t * pAbcWlcCnf; + Vec_Str_t * pAbcWlcStr; void * pAbcBac; void * pAbcCba; void * pAbcPla; diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make index f3aa6871..7bc7aa39 100644 --- a/src/base/wlc/module.make +++ b/src/base/wlc/module.make @@ -1,4 +1,5 @@ SRC += src/base/wlc/wlcAbs.c \ + src/base/wlc/wlcAbc.c \ src/base/wlc/wlcBlast.c \ src/base/wlc/wlcCom.c \ src/base/wlc/wlcNtk.c \ diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c new file mode 100644 index 00000000..0bf27f7b --- /dev/null +++ b/src/base/wlc/wlcAbc.c @@ -0,0 +1,154 @@ +/**CFile**************************************************************** + + FileName [wlcAbc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Verilog parser.] + + Synopsis [Parses several flavors of word-level Verilog.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - August 22, 2014.] + + Revision [$Id: wlcAbc.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "wlc.h" +#include "base/abc/abc.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose ) +{ + Wlc_Obj_t * pObj; + int i, k, nNum, nRange, nBits = 0; + Wlc_NtkForEachCi( pNtk, pObj, i ) + { + if ( pObj->Type != WLC_OBJ_FO ) + continue; + nRange = Wlc_ObjRange(pObj); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry(vInv, nBits + k); + if ( nNum ) + break; + } + if ( k == nRange ) + { + nBits += nRange; + continue; + } + printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg ); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry( vInv, nBits + k ); + if ( nNum == 0 ) + continue; + printf( " [%d] -> %d", k, nNum ); + } + printf( "\n"); + nBits += nRange; + } + //printf( "%d %d\n", Vec_IntSize(vInv), nBits ); + assert( Vec_IntSize(vInv) == nBits ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose ) +{ + Wlc_Obj_t * pObj; + int i, k, nNum, nRange, nBits = 0; + Abc_Ntk_t * pMainNtk = NULL; + Abc_Obj_t * pMainObj, * pMainTemp; + char Buffer[5000]; + // start the network + pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); + // duplicate the name and the spec + pMainNtk->pName = Extra_UtilStrsav(pNtk->pName); + // create primary inputs + Wlc_NtkForEachCi( pNtk, pObj, i ) + { + if ( pObj->Type != WLC_OBJ_FO ) + continue; + nRange = Wlc_ObjRange(pObj); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry(vInv, nBits + k); + if ( nNum ) + break; + } + if ( k == nRange ) + { + nBits += nRange; + continue; + } + //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg ); + for ( k = 0; k < nRange; k++ ) + { + nNum = Vec_IntEntry( vInv, nBits + k ); + if ( nNum == 0 ) + continue; + //printf( " [%d] -> %d", k, nNum ); + pMainObj = Abc_NtkCreatePi( pMainNtk ); + sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k ); + Abc_ObjAssignName( pMainObj, Buffer, NULL ); + + } + //printf( "\n"); + nBits += nRange; + } + //printf( "%d %d\n", Vec_IntSize(vInv), nBits ); + assert( Vec_IntSize(vInv) == nBits ); + // create node + pMainObj = Abc_NtkCreateNode( pMainNtk ); + Abc_NtkForEachPi( pMainNtk, pMainTemp, i ) + Abc_ObjAddFanin( pMainObj, pMainTemp ); + pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) ); + // create PO + pMainTemp = Abc_NtkCreatePo( pMainNtk ); + Abc_ObjAddFanin( pMainTemp, pMainObj ); + Abc_ObjAssignName( pMainTemp, "inv", NULL ); + return pMainNtk; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 426d9bbf..f3e0af8a 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1111,52 +1111,6 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds ) return pNew; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose ) -{ - Wlc_Obj_t * pObj; - int i, k, nNum, nRange, nBits = 0; - Wlc_NtkForEachCi( pNtk, pObj, i ) - { - if ( pObj->Type != WLC_OBJ_FO ) - continue; - nRange = Wlc_ObjRange(pObj); - for ( k = 0; k < nRange; k++ ) - { - nNum = Vec_IntEntry(vInv, nBits + k); - if ( nNum ) - break; - } - if ( k == nRange ) - { - nBits += nRange; - continue; - } - printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg ); - for ( k = 0; k < nRange; k++ ) - { - nNum = Vec_IntEntry( vInv, nBits + k ); - if ( nNum == 0 ) - continue; - printf( " [%d] -> %d", k, nNum ); - } - printf( "\n"); - nBits += nRange; - } - //printf( "%d %d\n", Vec_IntSize(vInv), nBits ); - assert( Vec_IntSize(vInv) == nBits ); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 3f8cc492..1584e346 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_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPsInv ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandGetInv ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; } @@ -40,6 +41,8 @@ static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; } static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcInv; } +static inline Vec_Int_t * Wlc_AbcGetCnf( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcCnf; } +static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcStr; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -63,6 +66,7 @@ void Wlc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%psinv", Abc_CommandPsInv, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%getinv", Abc_CommandGetInv, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 ); } @@ -421,7 +425,68 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: Abc_Print( -2, "usage: %%psinv [-vh]\n" ); - Abc_Print( -2, "\t prints inductive invariant statistics\n" ); + Abc_Print( -2, "\t prints statistics for inductive invariant\n" ); + Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose ); + Abc_Ntk_t * pMainNtk; + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandGetInv(): There is no current design.\n" ); + return 0; + } + if ( Wlc_AbcGetNtk(pAbc) == NULL ) + { + Abc_Print( 1, "Abc_CommandGetInv(): There is no saved invariant.\n" ); + return 0; + } + if ( Wlc_AbcGetInv(pAbc) == NULL ) + { + Abc_Print( 1, "Abc_CommandGetInv(): Invariant is not available.\n" ); + return 0; + } + // derive the network + pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), Wlc_AbcGetStr(pAbc), fVerbose ); + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk ); + return 0; + usage: + Abc_Print( -2, "usage: %%getinv [-vh]\n" ); + Abc_Print( -2, "\t places invariant found by PDR as the current network in the main-space\n" ); + Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index adbdafca..e4b764a1 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -44,6 +44,7 @@ struct Pdr_Par_t_ int nRecycle; // limit on vars for recycling int nFrameMax; // limit on frame count int nConfLimit; // limit on SAT solver conflicts + int nConfGenLimit; // limit on SAT solver conflicts during generalization int nRestLimit; // limit on the number of proof-obligations int nTimeOut; // timeout in seconds int nTimeOutGap; // approximate timeout in seconds since the last change diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 78cc16c1..8e81795b 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -55,6 +55,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->nTimeOut = 0; // timeout in seconds pPars->nTimeOutGap = 0; // timeout in seconds since the last solved pPars->nConfLimit = 0; // limit on SAT solver conflicts + pPars->nConfGenLimit = 0; // limit on SAT solver conflicts during generalization pPars->nRestLimit = 0; // limit on the number of proof-obligations pPars->fTwoRounds = 0; // use two rounds for generalization pPars->fMonoCnf = 0; // monolythic CNF @@ -115,7 +116,7 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) // make sure the cube works { int RetValue; - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 ); assert( RetValue ); } */ @@ -162,7 +163,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) } // check if the clause can be moved to the next frame - RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 ); + RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0 ); if ( RetValue2 == -1 ) return -1; if ( !RetValue2 ) @@ -310,7 +311,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP int * pOrder; // if there is no induction, return *ppCubeMin = NULL; - RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit ); + RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 ); if ( RetValue == -1 ) return -1; if ( RetValue == 0 ) @@ -343,7 +344,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP continue; // try removing this literal Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 ); if ( RetValue == -1 ) { Pdr_SetDeref( pCubeMin ); @@ -381,7 +382,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP continue; // try removing this literal Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0 ); if ( RetValue == -1 ) { Pdr_SetDeref( pCubeMin ); @@ -494,7 +495,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) assert( pPred == NULL ); for ( k = pThis->iFrame; k < kMax; k++ ) { - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 ); if ( RetValue == -1 ) { Pdr_OblDeref( pThis ); @@ -659,7 +660,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->pPars->iFrame = k; return -1; } - RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit ); + RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit, 0 ); if ( RetValue == 1 ) break; if ( RetValue == -1 ) @@ -911,10 +912,6 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) RetValue = Pdr_ManSolveInt( p ); if ( RetValue == 0 ) assert( pAig->pSeqModel != NULL || p->vCexes != NULL ); - if ( RetValue == 1 ) - Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) ); - else - Abc_FrameSetInv( NULL ); if ( p->vCexes ) { assert( p->pAig->vSeqModelVec == NULL ); @@ -922,7 +919,12 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) p->vCexes = NULL; } if ( p->pPars->fDumpInv ) + { + Abc_FrameSetCnf( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) ); + Abc_FrameSetStr( Pdr_ManDumpString(p) ); + Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) ); Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 ); + } p->tTotal += Abc_Clock() - clk; Pdr_ManStop( p ); pPars->iFrame--; diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index bd9fe87c..6a08a150 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -101,6 +101,7 @@ struct Pdr_Man_t_ Vec_Int_t * vSuppLits; // support literals Pdr_Set_t * pCubeJust; // justification abctime * pTime4Outs;// timeout per output + Vec_Ptr_t * vInfCubes; // infinity clauses/cubes // statistics int nBlocks; // the number of times blockState was called int nObligs; // the number of proof obligations derived @@ -167,8 +168,10 @@ extern Vec_Int_t * Pdr_ManCountFlopsInv( Pdr_Man_t * p ); extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ); extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart ); extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ); +extern Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p ); extern void Pdr_ManReportInvariant( Pdr_Man_t * p ); extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p ); +extern Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ); /*=== pdrMan.c ==========================================================*/ extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit ); extern void Pdr_ManStop( Pdr_Man_t * p ); @@ -182,7 +185,7 @@ extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, in extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues ); extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); -extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit ); +extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf ); /*=== pdrTsim.c ==========================================================*/ extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ); /*=== pdrUtil.c ==========================================================*/ @@ -197,6 +200,7 @@ extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew ); extern int Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew ); extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove ); extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); +extern void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ); extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 ); extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext ); extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p ); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 860462c3..b548cf68 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -110,11 +110,15 @@ Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) int i, n; vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) ); Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) + continue; for ( n = 0; n < pCube->nLits; n++ ) { assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) ); Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 ); } + } return vFlopCount; } @@ -202,7 +206,10 @@ int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart ) Vec_Int_t * vFlopCounts; Vec_Ptr_t * vCubes; int i, Entry, Counter = 0; - vCubes = Pdr_ManCollectCubes( p, kStart ); + if ( p->vInfCubes == NULL ) + vCubes = Pdr_ManCollectCubes( p, kStart ); + else + vCubes = Vec_PtrDup( p->vInfCubes ); vFlopCounts = Pdr_ManCountFlops( p, vCubes ); Vec_IntForEachEntry( vFlopCounts, Entry, i ) Counter += (Entry > 0); @@ -338,7 +345,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) Vec_Ptr_t * vCubes; Pdr_Set_t * pCube; char ** pNamesCi; - int i, kStart; + int i, kStart, Count = 0; // create file pFile = fopen( pFileName, "w" ); if ( pFile == NULL ) @@ -348,9 +355,20 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) } // collect cubes kStart = Pdr_ManFindInvariantStart( p ); - vCubes = Pdr_ManCollectCubes( p, kStart ); + if ( fProved ) + vCubes = Pdr_ManCollectCubes( p, kStart ); + else + vCubes = Vec_PtrDup( p->vInfCubes ); Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare ); // Pdr_ManDumpAig( p->pAig, vCubes ); + // count cubes + Count = 0; + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) + continue; + Count++; + } // collect variable appearances vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; // output the header @@ -361,7 +379,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() ); fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) ); fprintf( pFile, ".o 1\n" ); - fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) ); + fprintf( pFile, ".p %d\n", Count ); // output flop names pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 ); if ( pNamesCi ) @@ -377,6 +395,8 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) // output cubes Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { + if ( pCube->nRefs == -1 ) + continue; Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); fprintf( pFile, " 1\n" ); } @@ -390,6 +410,48 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved ) Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p ) +{ + int fUseSupp = 1; + Vec_Str_t * vStr; + Vec_Int_t * vFlopCounts; + Vec_Ptr_t * vCubes; + Pdr_Set_t * pCube; + int i, kStart; + vStr = Vec_StrAlloc( 1000 ); + // collect cubes + kStart = Pdr_ManFindInvariantStart( p ); + if ( p->vInfCubes == NULL ) + vCubes = Pdr_ManCollectCubes( p, kStart ); + else + vCubes = Vec_PtrDup( p->vInfCubes ); + Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare ); + // collect variable appearances + vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; + // output cubes + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) + continue; + Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts ); + } + Vec_IntFreeP( &vFlopCounts ); + Vec_PtrFree( vCubes ); + Vec_StrPush( vStr, '\0' ); + return vStr; +} + /**Function************************************************************* @@ -469,6 +531,86 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p ) Vec_PtrFree( vCubes ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes ) +{ + sat_solver * pSat; + Vec_Int_t * vLits; + Pdr_Set_t * pCube; + int i, kThis, RetValue, fChanges = 0, Counter = 0; + // create solver with the cubes + kThis = Vec_PtrSize(p->vSolvers); + pSat = Pdr_ManCreateSolver( p, kThis ); + // add the clauses + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) // skip non-inductive + continue; + vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 ); + RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + assert( RetValue ); + sat_solver_compress( pSat ); + } + // check each clause + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) // skip non-inductive + continue; + vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 ); + RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); + if ( RetValue != l_False ) // mark as non-inductive + { + pCube->nRefs = -1; + fChanges = 1; + } + else + Counter++; + } + //printf( "Clauses = %d.\n", Counter ); + //sat_solver_delete( pSat ); + return fChanges; +} +Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce ) +{ + Vec_Int_t * vResult; + Vec_Ptr_t * vCubes; + Pdr_Set_t * pCube; + int i, v, kStart; + abctime clk = Abc_Clock(); + // collect cubes used in the inductive invariant + kStart = Pdr_ManFindInvariantStart( p ); + vCubes = Pdr_ManCollectCubes( p, kStart ); + // refine as long as there are changes + if ( fReduce ) + while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) ); + // collect remaining clauses + vResult = Vec_IntAlloc( 1000 ); + Vec_IntPush( vResult, 0 ); + Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) + { + if ( pCube->nRefs == -1 ) // skip non-inductive + continue; + Vec_IntAddToEntry( vResult, 0, 1 ); + Vec_IntPush( vResult, pCube->nLits ); + for ( v = 0; v < pCube->nLits; v++ ) + Vec_IntPush( vResult, pCube->Lits[v] ); + } + //Vec_PtrFree( vCubes ); + Vec_PtrFreeP( &p->vInfCubes ); + p->vInfCubes = vCubes; + return vResult; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 9a73b697..b58c479b 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -163,6 +163,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) Vec_IntFree( p->vCi2Rem ); // CIs to be removed Vec_IntFree( p->vRes ); // final result Vec_IntFree( p->vSuppLits ); // support literals + Vec_PtrFreeP( &p->vInfCubes ); ABC_FREE( p->pCubeJust ); ABC_FREE( p->pTime4Outs ); if ( p->vCexes ) diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index 244d0311..f3681adb 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -283,7 +283,7 @@ int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) SeeAlso [] ***********************************************************************/ -int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit ) +int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf ) { int fUseLit = 1; int fLitUsed = 0; @@ -329,10 +329,15 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr // solve clk = Abc_Clock(); Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) ); - RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 ); + RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), fTryConf ? p->pPars->nConfGenLimit : nConfLimit, 0, 0, 0 ); sat_solver_set_runtime_limit( pSat, Limit ); if ( RetValue == l_Undef ) - return -1; + { + if ( fTryConf && p->pPars->nConfGenLimit ) + RetValue = l_True; + else + return -1; + } /* if ( RetValue == l_True ) { diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index 1536c1cc..53a8a54a 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -249,6 +249,46 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun ABC_FREE( pBuff ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts ) +{ + char * pBuff; + int i, k = 0, Entry; + pBuff = ABC_ALLOC( char, nRegs + 1 ); + for ( i = 0; i < nRegs; i++ ) + pBuff[i] = '-'; + pBuff[i] = 0; + for ( i = 0; i < p->nLits; i++ ) + { + if ( p->Lits[i] == -1 ) + continue; + pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1'); + } + if ( vFlopCounts ) + { + // skip some literals + Vec_IntForEachEntry( vFlopCounts, Entry, i ) + if ( Entry ) + pBuff[k++] = pBuff[i]; + pBuff[k] = 0; + } + Vec_StrPushBuffer( vStr, pBuff, k ); + Vec_StrPush( vStr, ' ' ); + Vec_StrPush( vStr, '0' ); + Vec_StrPush( vStr, '\n' ); + ABC_FREE( pBuff ); +} + /**Function************************************************************* Synopsis [Return 1 if pOld set-theoretically contains pNew.] -- cgit v1.2.3