luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network.

This commit is contained in:
Alan Mishchenko 2016-01-14 20:42:22 -08:00
parent f30facfec8
commit c4446189a9
15 changed files with 457 additions and 68 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/base/abci/abc.c
View File

@ -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 <num>] [-axrmsipdgvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCDRTHG <num>] [-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 );

2
src/base/main/main.h
View File

@ -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 );

4
src/base/main/mainFrame.c
View File

@ -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;
}

2
src/base/main/mainInt.h
View File

@ -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;

1
src/base/wlc/module.make
View File

@ -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 \

154
src/base/wlc/wlcAbc.c Normal file
View File

@ -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

46
src/base/wlc/wlcBlast.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

67
src/base/wlc/wlcCom.c
View File

@ -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;

1
src/proof/pdr/pdr.h
View File

@ -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

24
src/proof/pdr/pdrCore.c
View File

@ -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--;

6
src/proof/pdr/pdrInt.h
View File

@ -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 );

150
src/proof/pdr/pdrInv.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

1
src/proof/pdr/pdrMan.c
View File

@ -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 )

11
src/proof/pdr/pdrSat.c
View File

@ -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 )
{

40
src/proof/pdr/pdrUtil.c
View File

@ -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.]