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

Adding features for invariant minimization.

This commit is contained in:
Alan Mishchenko 2017-01-24 20:02:19 -08:00
parent cf539dcca4
commit 51f4dab475
7 changed files with 686 additions and 165 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -95,8 +95,6 @@ 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; }
void Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs ) { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
void Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs ) { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
@ -227,8 +225,6 @@ 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_NamDeref( s_GlobalFrame->pJsonStrs );
Vec_WecFreeP(&s_GlobalFrame->vJsonObjs );
ABC_FREE( p );

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

@ -129,8 +129,6 @@ 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;

155
src/base/wlc/wlcAbc.c
View File

@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
{
Wlc_Obj_t * pObj;
int i, k, nNum, nRange, nBits = 0;
@ -53,7 +53,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
nRange = Wlc_ObjRange(pObj);
for ( k = 0; k < nRange; k++ )
{
nNum = Vec_IntEntry(vInv, nBits + k);
nNum = Vec_IntEntry(vCounts, nBits + k);
if ( nNum )
break;
}
@ -65,7 +65,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
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 );
nNum = Vec_IntEntry( vCounts, nBits + k );
if ( nNum == 0 )
continue;
printf( " [%d] -> %d", k, nNum );
@ -73,8 +73,8 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
printf( "\n");
nBits += nRange;
}
//printf( "%d %d\n", Vec_IntSize(vInv), nBits );
assert( Vec_IntSize(vInv) == nBits );
//printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
assert( Vec_IntSize(vCounts) == nBits );
}
/**Function*************************************************************
@ -88,8 +88,14 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )
Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
{
extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts );
Wlc_Obj_t * pObj;
int i, k, nNum, nRange, nBits = 0;
Abc_Ntk_t * pMainNtk = NULL;
@ -98,46 +104,69 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
// 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);
pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv");
// create primary inputs
Wlc_NtkForEachCi( pNtk, pObj, i )
if ( pNtk == NULL )
{
if ( pObj->Type != WLC_OBJ_FO )
continue;
nRange = Wlc_ObjRange(pObj);
for ( k = 0; k < nRange; k++ )
int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) );
Vec_IntForEachEntry( vCounts, Entry, i )
{
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 )
if ( Entry == 0 )
continue;
//printf( " [%d] -> %d", k, nNum );
pMainObj = Abc_NtkCreatePi( pMainNtk );
sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
sprintf( Buffer, "pi%d", i );
Abc_ObjAssignName( pMainObj, Buffer, NULL );
}
//printf( "\n");
nBits += nRange;
if ( Abc_NtkPiNum(pMainNtk) != nInputs )
{
printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );
Abc_NtkDelete( pMainNtk );
return NULL;
}
}
//printf( "%d %d\n", Vec_IntSize(vInv), nBits );
assert( Vec_IntSize(vInv) == nBits );
else
{
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(vCounts, 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( vCounts, 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(vCounts), nBits );
assert( pNtk == NULL || Vec_IntSize(vCounts) == 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) );
Vec_IntFree( vCounts );
Vec_StrFree( vSop );
// create PO
pMainTemp = Abc_NtkCreatePo( pMainNtk );
Abc_ObjAddFanin( pMainTemp, pMainObj );
@ -145,6 +174,66 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
return pMainNtk;
}
/**Function*************************************************************
Synopsis [Translate current network into an interpolant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs )
{
Vec_Int_t * vRes = NULL;
if ( Abc_NtkPoNum(pNtk) != 1 )
printf( "The number of outputs is other than 1.\n" );
else if ( Abc_NtkNodeNum(pNtk) != 1 )
printf( "The number of internal nodes is other than 1.\n" );
else
{
Abc_Obj_t * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
char * pName, * pCube, * pSop = (char *)pNode->pData;
Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
Abc_Obj_t * pFanin; int i, k, Value, nLits;
Abc_ObjForEachFanin( pNode, pFanin, i )
{
assert( Abc_ObjIsCi(pFanin) );
pName = Abc_ObjName(pFanin);
for ( k = (int)strlen(pName)-1; k >= 0; k-- )
if ( pName[k] < '0' || pName[k] > '9' )
break;
if ( k == (int)strlen(pName)-1 )
{
printf( "Cannot read input name of fanin %d.\n", i );
Value = i;
}
else
Value = atoi(pName + k + 1);
Vec_IntPush( vFanins, Value );
}
assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) );
vRes = Vec_IntAlloc( 1000 );
Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) );
Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube )
{
nLits = 0;
Abc_CubeForEachVar( pCube, Value, k )
if ( Value != '-' )
nLits++;
Vec_IntPush( vRes, nLits );
Abc_CubeForEachVar( pCube, Value, k )
if ( Value != '-' )
Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') );
}
Vec_IntPush( vRes, nRegs );
Vec_IntFree( vFanins );
}
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -32,18 +32,21 @@ static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
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_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInvPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInvPrint ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInvCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInvGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInvPut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInvMin ( 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; }
static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(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 ///
@ -66,10 +69,15 @@ void Wlc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 );
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", "%profile", Abc_CommandProfile, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 );
Cmd_CommandAdd( pAbc, "Word level", "inv_ps", Abc_CommandInvPs, 0 );
Cmd_CommandAdd( pAbc, "Word level", "inv_print", Abc_CommandInvPrint, 0 );
Cmd_CommandAdd( pAbc, "Word level", "inv_check", Abc_CommandInvCheck, 0 );
Cmd_CommandAdd( pAbc, "Word level", "inv_get", Abc_CommandInvGet, 0 );
Cmd_CommandAdd( pAbc, "Word level", "inv_put", Abc_CommandInvPut, 0 );
Cmd_CommandAdd( pAbc, "Word level", "inv_min", Abc_CommandInvMin, 0 );
}
/**Function********************************************************************
@ -429,122 +437,6 @@ usage:
return 1;
}
/**Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose );
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_CommandPsInv(): There is no current design.\n" );
return 0;
}
if ( Wlc_AbcGetNtk(pAbc) == NULL )
{
Abc_Print( 1, "Abc_CommandPsInv(): There is no saved invariant.\n" );
return 0;
}
if ( Wlc_AbcGetInv(pAbc) == NULL )
{
Abc_Print( 1, "Abc_CommandPsInv(): Invariant is not available.\n" );
return 0;
}
Wlc_NtkPrintInvStats( pNtk, Wlc_AbcGetInv(pAbc), fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: %%psinv [-vh]\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;
}
/**Function********************************************************************
Synopsis []
@ -641,6 +533,326 @@ usage:
return 1;
}
/**Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int Abc_CommandInvPs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose );
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
Vec_Int_t * vCounts;
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_CommandInvPs(): There is no current design.\n" );
return 0;
}
if ( Wlc_AbcGetInv(pAbc) == NULL )
{
Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
return 0;
}
vCounts = Pdr_InvCounts( Wlc_AbcGetInv(pAbc) );
Wlc_NtkPrintInvStats( pNtk, vCounts, fVerbose );
Vec_IntFree( vCounts );
return 0;
usage:
Abc_Print( -2, "usage: inv_ps [-vh]\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_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Pdr_InvPrint( Vec_Int_t * vInv );
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 ( Wlc_AbcGetInv(pAbc) == NULL )
{
Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
return 0;
}
Pdr_InvPrint( Wlc_AbcGetInv(pAbc) );
return 0;
usage:
Abc_Print( -2, "usage: inv_print [-vh]\n" );
Abc_Print( -2, "\t prints the current 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_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv );
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 ( pAbc->pGia == NULL )
{
Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
return 0;
}
if ( Wlc_AbcGetInv(pAbc) == NULL )
{
Abc_Print( 1, "Abc_CommandInvMin(): There is no saved invariant.\n" );
return 0;
}
if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(Wlc_AbcGetInv(pAbc)) )
{
Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
return 0;
}
Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc) );
return 0;
usage:
Abc_Print( -2, "usage: inv_check [-vh]\n" );
Abc_Print( -2, "\t checks that the invariant is indeed an inductive invariant\n" );
Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\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_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv );
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 ( Wlc_AbcGetInv(pAbc) == NULL )
{
Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" );
return 0;
}
// derive the network
pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) );
// replace the current network
if ( pMainNtk )
Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
return 0;
usage:
Abc_Print( -2, "usage: inv_get [-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;
}
/**Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, int nRegs );
Vec_Int_t * vInv = NULL;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(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_CommandInvPut(): There is no current design.\n" );
return 0;
}
if ( pAbc->pGia == NULL )
{
Abc_Print( 1, "Abc_CommandInvPut(): There is no current AIG.\n" );
return 0;
}
// derive the network
vInv = Wlc_NtkGetPut( pNtk, Gia_ManRegNum(pAbc->pGia) );
if ( vInv )
Abc_FrameSetInv( vInv );
return 0;
usage:
Abc_Print( -2, "usage: inv_put [-vh]\n" );
Abc_Print( -2, "\t inputs the current network in the main-space as an invariant\n" );
Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\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_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv );
Vec_Int_t * vInv, * vInv2;
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 ( pAbc->pGia == NULL )
{
Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
return 0;
}
if ( Wlc_AbcGetInv(pAbc) == NULL )
{
Abc_Print( 1, "Abc_CommandInvMin(): Invariant is not available.\n" );
return 0;
}
vInv = Wlc_AbcGetInv(pAbc);
if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(vInv) )
{
Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
return 0;
}
vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv );
if ( vInv2 )
Abc_FrameSetInv( vInv2 );
return 0;
usage:
Abc_Print( -2, "usage: inv_min [-vh]\n" );
Abc_Print( -2, "\t minimizes the number of clauses in the current invariant\n" );
Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\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;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -923,9 +923,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
if ( p->pPars->fDumpInv )
{
char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
Abc_FrameSetCnf( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
Abc_FrameSetStr( Pdr_ManDumpString(p) );
Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
}
p->tTotal += Abc_Clock() - clk;

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

@ -605,9 +605,237 @@ Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
//Vec_PtrFree( vCubes );
Vec_PtrFreeP( &p->vInfCubes );
p->vInfCubes = vCubes;
Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) );
return vResult;
}
/**Function*************************************************************
Synopsis [Remove clauses while maintaining the invariant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#define Pdr_ForEachCube( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 )
extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts )
{
int i, k = 0, Count;
Vec_Int_t * vMap = Vec_IntStart( Vec_IntSize(vCounts) );
Vec_IntForEachEntry( vCounts, Count, i )
if ( Count )
Vec_IntWriteEntry( vMap, i, k++ );
return vMap;
}
Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv )
{
int i, k, * pCube, * pList = Vec_IntArray(vInv);
Vec_Int_t * vCounts = Vec_IntStart( Vec_IntEntryLast(vInv) );
Pdr_ForEachCube( pList, pCube, i )
for ( k = 0; k < pCube[0]; k++ )
Vec_IntAddToEntry( vCounts, Abc_Lit2Var(pCube[k+1]), 1 );
return vCounts;
}
int Pdr_InvUsedFlopNum( Vec_Int_t * vInv )
{
Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
int nZeros = Vec_IntCountZero( vCounts );
Vec_IntFree( vCounts );
return Vec_IntEntryLast(vInv) - nZeros;
}
Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts )
{
Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
Vec_Int_t * vMap = Pdr_InvMap( vCounts );
int nVars = Vec_IntSize(vCounts) - Vec_IntCountZero(vCounts);
int i, k, * pCube, * pList = Vec_IntArray(vInv);
char * pBuffer = ABC_ALLOC( char, nVars );
for ( i = 0; i < nVars; i++ )
pBuffer[i] = '-';
Pdr_ForEachCube( pList, pCube, i )
{
for ( k = 0; k < pCube[0]; k++ )
pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '0' + !Abc_LitIsCompl(pCube[k+1]);
for ( k = 0; k < nVars; k++ )
Vec_StrPush( vStr, pBuffer[k] );
Vec_StrPush( vStr, ' ' );
Vec_StrPush( vStr, '1' );
Vec_StrPush( vStr, '\n' );
for ( k = 0; k < pCube[0]; k++ )
pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '-';
}
Vec_StrPush( vStr, '\0' );
ABC_FREE( pBuffer );
Vec_IntFree( vMap );
return vStr;
}
void Pdr_InvPrint( Vec_Int_t * vInv )
{
Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts );
printf( "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) );
printf( "%s", Vec_StrArray( vStr ) );
Vec_IntFree( vCounts );
Vec_StrFree( vStr );
}
void Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
{
int nBTLimit = 0;
int i, k, status, nFailed = 0;
// create SAT solver
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
// collect cubes
int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
// create variables
Vec_Int_t * vLits = Vec_IntAlloc(100);
int nVars = Gia_ManRegNum(p);
int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
int iFiVarBeg = 1 + Gia_ManPoNum(p);
assert( Gia_ManPoNum(p) == 1 );
// add cubes
Pdr_ForEachCube( pList, pCube, i )
{
// collect literals
Vec_IntClear( vLits );
for ( k = 0; k < pCube[0]; k++ )
Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
// add it to the solver
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
assert( status == 1 );
}
// iterate through cubes in the direct order
Pdr_ForEachCube( pList, pCube, i )
{
// collect cube
Vec_IntClear( vLits );
for ( k = 0; k < pCube[0]; k++ )
Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
// check if this cube intersects with the complement of other cubes in the solver
// if it does not intersect, then it is redundant and can be skipped
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
if ( status == l_Undef ) // timeout
break;
if ( status == l_False ) // unsat -- correct
continue;
assert( status == l_True );
nFailed++;
}
if ( nFailed )
printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, nCubes );
else
printf( "Invariant verification passes.\n" );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Vec_IntFree( vLits );
}
Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv )
{
int nBTLimit = 0;
int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0;
Vec_Int_t * vRes = NULL;
// create SAT solver
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
// create variables
Vec_Int_t * vLits = Vec_IntAlloc(100);
Vec_Bit_t * vRemoved = Vec_BitStart( nCubes );
int nVars = Gia_ManRegNum(p);
int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
int iFiVarBeg = 1 + Gia_ManPoNum(p);
int iAuxVarBeg = sat_solver_nvars(pSat);
assert( Gia_ManPoNum(p) == 1 );
// allocate auxiliary variables
sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + nCubes );
// add clauses
Pdr_ForEachCube( pList, pCube, i )
{
// collect literals
Vec_IntFill( vLits, 1, Abc_Var2Lit(iAuxVarBeg + i, 1) ); // neg aux literal
for ( k = 0; k < pCube[0]; k++ )
Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
// add it to the solver
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
assert( status == 1 );
}
// iterate through clauses
Pdr_ForEachCube( pList, pCube, i )
{
if ( Vec_BitEntry(vRemoved, i) )
continue;
// collect aux literals for remaining clauses
Vec_IntClear( vLits );
for ( k = 0; k < nCubes; k++ )
if ( k != i && !Vec_BitEntry(vRemoved, k) ) // skip this cube and already removed cubes
Vec_IntPush( vLits, Abc_Var2Lit(iAuxVarBeg + k, 0) ); // pos aux literal
nLits = Vec_IntSize( vLits );
// try removing other clauses
fCannot = 0;
Pdr_ForEachCube( pList, pCube, n )
{
if ( Vec_BitEntry(vRemoved, n) || n == i )
continue;
// collect cube
Vec_IntShrink( vLits, nLits );
for ( k = 0; k < pCube[0]; k++ )
Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
// check if this cube intersects with the complement of other cubes in the solver
// if it does not intersect, then it is redundant and can be skipped
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
if ( status == l_Undef ) // timeout
{
fFailed = 1;
break;
}
if ( status == l_False ) // unsat -- correct
continue;
assert( status == l_True );
// cannot remove
fCannot = 1;
break;
}
if ( fFailed )
break;
if ( fCannot )
continue;
printf( "Removing clause %d.\n", i );
Vec_BitWriteEntry( vRemoved, i, 1 );
nRemoved++;
}
if ( nRemoved )
printf( "Invariant minimization reduced %d clauses (out of %d).\n", nRemoved, nCubes );
else
printf( "Invariant minimization did not change the invariant.\n" );
// cleanup cover
if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes
{
vRes = Vec_IntAlloc( 1000 );
Vec_IntPush( vRes, nCubes-nRemoved );
Pdr_ForEachCube( pList, pCube, i )
if ( !Vec_BitEntry(vRemoved, i) )
for ( k = 0; k <= pCube[0]; k++ )
Vec_IntPush( vRes, pCube[k] );
Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
}
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Vec_BitFree( vRemoved );
Vec_IntFree( vLits );
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -284,7 +284,7 @@ void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vF
}
Vec_StrPushBuffer( vStr, pBuff, k );
Vec_StrPush( vStr, ' ' );
Vec_StrPush( vStr, '0' );
Vec_StrPush( vStr, '1' );
Vec_StrPush( vStr, '\n' );
ABC_FREE( pBuff );
}