Skip to content

A
abc
Commit 760c1f60 by Alan Mishchenko
Options

Adding new command &mprove for proving groups of properties.

parent 1dd80e1c
Showing with 238 additions and 24 deletions
src/aig/gia/gia.h
......@@ -372,6 +372,9 @@ static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) {
static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1; }
static inline int Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); }
static inline int Gia_ManPoIsConst0( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst0Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
static inline int Gia_ManPoIsConst1( Gia_Man_t * p, int iPoIndex ) { return Gia_ManIsConst1Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
static inline Gia_Obj_t * Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ManObj( p, Abc_Lit2Var(pObj->Value) ); }
static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); }
......
src/aig/gia/giaUtil.c
......@@ -1393,6 +1393,95 @@ void Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues )
pObj->Value = Vec_IntEntry(vValues, i);
}
#include "base/main/mainInt.h"
/**Function*************************************************************
Synopsis [Proving multi-output properties.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
{
Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame();
Gia_Man_t * p = Gia_ManDup( pInit );
Gia_Man_t * pGroup;
Vec_Int_t * vOuts;
Vec_Int_t * vOutMap;
Vec_Ptr_t * vCexes;
int i, k, nGroupCur, nGroups;
clock_t clk, timeComm = 0;
clock_t timeStart = clock();
// pre-conditions
assert( nGroupSize > 0 );
assert( pCommLine != NULL );
assert( p->nConstrs == 0 );
Abc_Print( 1, "RUNNING MultiProve: Group size = %d. Command line = \"%s\".\n", nGroupSize, pCommLine );
// create output map
vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) );
vOutMap = Vec_IntAlloc( Gia_ManPoNum(p) );
vCexes = Vec_PtrAlloc( Gia_ManPoNum(p) );
nGroups = Gia_ManPoNum(p) / nGroupSize + (int)((Gia_ManPoNum(p) % nGroupSize) > 0);
for ( i = 0; i < nGroups; i++ )
{
// derive the group
nGroupCur = ((i + 1) * nGroupSize < Gia_ManPoNum(p)) ? nGroupSize : Gia_ManPoNum(p) - i * nGroupSize;
pGroup = Gia_ManDupCones( p, Vec_IntArray(vOuts) + i * nGroupSize, nGroupCur, 0 );
Abc_Print( 1, "GROUP %4d : %4d <= PoId < %4d : ", i, i * nGroupSize, i * nGroupSize + nGroupCur );
// set the current GIA
Abc_FrameUpdateGia( pAbc, pGroup );
// solve the group
clk = clock();
Cmd_CommandExecute( pAbc, pCommLine );
timeComm += clock() - clk;
// get the solution status
if ( nGroupSize == 1 )
{
Vec_IntPush( vOutMap, Abc_FrameReadProbStatus(pAbc) );
Vec_PtrPush( vCexes, Abc_FrameReadCex(pAbc) );
}
else // if ( nGroupSize > 1 )
{
Vec_Int_t * vStatusCur = Abc_FrameReadPoStatuses( pAbc );
Vec_Ptr_t * vCexesCur = Abc_FrameReadCexVec( pAbc );
assert( vStatusCur != NULL ); // only works for "bmc3" and "pdr"
assert( vCexesCur != NULL );
for ( k = 0; k < nGroupCur; k++ )
{
Vec_IntPush( vOutMap, Vec_IntEntry(vStatusCur, k) );
Vec_PtrPush( vCexes, Vec_PtrEntry(vCexesCur, k) );
}
}
}
assert( Vec_PtrSize(vCexes) == Gia_ManPoNum(p) );
assert( Vec_IntSize(vOutMap) == Gia_ManPoNum(p) );
// set CEXes
if ( Vec_PtrCountZero(vCexes) < Vec_PtrSize(vCexes) )
Abc_FrameReplaceCexVec( pAbc, &vCexes );
else // there is no CEXes
Vec_PtrFree( vCexes );
// report the result
Abc_Print( 1, "SUMMARY: " );
Abc_Print( 1, "Properties = %6d. ", Gia_ManPoNum(p) );
Abc_Print( 1, "UNSAT = %6d. ", Vec_IntCountEntry(vOutMap, 1) );
Abc_Print( 1, "SAT = %6d. ", Vec_IntCountEntry(vOutMap, 0) );
Abc_Print( 1, "UNDEC = %6d. ", Vec_IntCountEntry(vOutMap, -1) );
Abc_Print( 1, "\n" );
Abc_PrintTime( 1, "Command time", timeComm );
Abc_PrintTime( 1, "Total time ", clock() - timeStart );
// cleanup
Vec_IntFree( vOuts );
Gia_ManStop( p );
return vOutMap;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abci/abc.c
......@@ -382,6 +382,7 @@ static int Abc_CommandAbc9CexInfo ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Cycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -474,7 +475,6 @@ void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec )
***********************************************************************/
void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs )
{
// update the array vector
if ( pAbc->vPoEquivs )
Vec_VecFree( (Vec_Vec_t *)pAbc->vPoEquivs );
pAbc->vPoEquivs = *pvPoEquivs;
......@@ -492,6 +492,51 @@ void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs )
SeeAlso []
***********************************************************************/
void Abc_FrameReplacePoStatuses( Abc_Frame_t * pAbc, Vec_Int_t ** pvStatuses )
{
if ( pAbc->vStatuses )
Vec_IntFree( pAbc->vStatuses );
pAbc->vStatuses = *pvStatuses;
*pvStatuses = NULL;
}
/**Function*************************************************************
Synopsis [Derives array of statuses from the array of CEXes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_FrameDeriveStatusArray( Vec_Ptr_t * vCexes )
{
Vec_Int_t * vStatuses;
Abc_Cex_t * pCex;
int i;
if ( vCexes == NULL )
return NULL;
vStatuses = Vec_IntAlloc( Vec_PtrSize(vCexes) );
Vec_IntFill( vStatuses, Vec_PtrSize(vCexes), -1 ); // assume UNDEC
Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i )
if ( pCex != NULL )
Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
return vStatuses;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_FrameClearDesign()
{
}
......@@ -882,6 +927,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&cycle", Abc_CommandAbc9Cycle, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cone", Abc_CommandAbc9Cone, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&popart", Abc_CommandAbc9PoPart, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
......@@ -21194,6 +21240,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Saig_ParBmc_t Pars, * pPars = &Pars;
Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc);
Vec_Ptr_t * vSeqModelVec = NULL;
Vec_Int_t * vStatuses = NULL;
char * pLogFileName = NULL;
int fOrDecomp = 0;
int c;
......@@ -21356,7 +21403,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp );
pAbc->nFrames = pPars->iFrame;
pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
if ( pLogFileName )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" );
......@@ -21380,11 +21427,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
}
if ( vSeqModelVec )
{
vStatuses = Abc_FrameDeriveStatusArray( vSeqModelVec );
Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec );
pAbc->nFrames = -1;
}
return 0;
usage:
......@@ -22929,14 +22974,10 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// run the procedure
pAbc->Status = Abc_NtkDarPdr( pNtk, pPars );
pAbc->nFrames = pPars->iFrame;
pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
if ( pNtk->vSeqModelVec )
{
Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
pAbc->nFrames = -1;
}
ABC_FREE( pPars->pOutMap ); // cleanup after PDR
Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap );
return 0;
usage:
......@@ -30470,6 +30511,75 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose );
Vec_Int_t * vStatus;
char * pCommLine = NULL;
int c, nGroupSize = 1, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "GSvh" ) ) != EOF )
{
switch ( c )
{
case 'G':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
goto usage;
}
nGroupSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nGroupSize <= 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" );
goto usage;
}
pCommLine = argv[globalUtilOptind];
globalUtilOptind++;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
return 1;
}
vStatus = Gia_ManMultiProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose );
Vec_IntFree( vStatus );
return 0;
usage:
Abc_Print( -2, "usage: &mprove [-GS num] [-vh]\n" );
Abc_Print( -2, "\t proves multi-output testcase by splitting outputs into groups\n" );
Abc_Print( -2, "\t (currently, group size more than one works only for \"bmc3\" and \"pdr\")\n" );
Abc_Print( -2, "\t-G num : the size of one group [default = %d]\n", nGroupSize );
Abc_Print( -2, "\t-S str : the command line to be executed for each group [default = %s]\n", pCommLine ? pCommLine : "none" );
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*************************************************************
src/base/main/main.h
......@@ -116,6 +116,7 @@ extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p );
extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p );
extern ABC_DLL Vec_Int_t * Abc_FrameReadPoStatuses( Abc_Frame_t * p );
extern ABC_DLL Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadCexPiNum( Abc_Frame_t * p );
......@@ -138,6 +139,11 @@ extern ABC_DLL void Abc_FrameSetStatus( int Status );
extern ABC_DLL int Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
extern ABC_DLL void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex );
extern ABC_DLL void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec );
extern ABC_DLL void Abc_FrameReplacePoEquivs( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvPoEquivs );
extern ABC_DLL void Abc_FrameReplacePoStatuses( Abc_Frame_t * pAbc, Vec_Int_t ** pvStatuses );
ABC_NAMESPACE_HEADER_END
#endif
......
src/base/main/mainFrame.c
......@@ -65,6 +65,7 @@ int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFr
Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; }
Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; }
Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; }
Vec_Int_t * Abc_FrameReadPoStatuses( Abc_Frame_t * p ) { return s_GlobalFrame->vStatuses; }
Vec_Int_t * Abc_FrameReadObjIds( Abc_Frame_t * p ) { return s_GlobalFrame->vAbcObjIds; }
int Abc_FrameReadCexPiNum( Abc_Frame_t * p ) { return s_GlobalFrame->pCex->nPis; }
......@@ -177,6 +178,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
if ( p->vAbcObjIds) Vec_IntFree( p->vAbcObjIds );
if ( p->vCexVec ) Vec_PtrFreeFree( p->vCexVec );
if ( p->vPoEquivs ) Vec_VecFree( (Vec_Vec_t *)p->vPoEquivs );
if ( p->vStatuses ) Vec_IntFree( p->vStatuses );
if ( p->pLibVer ) Abc_LibFree( (Abc_Lib_t *)p->pLibVer, NULL );
if ( p->pManDec ) Dec_ManStop( (Dec_Man_t *)p->pManDec );
if ( p->dd ) Extra_StopManager( p->dd );
......
src/base/main/mainInt.h
......@@ -101,6 +101,7 @@ struct Abc_Frame_t_
Abc_Cex_t * pCex2; // copy of the above
Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails
Vec_Ptr_t * vPoEquivs; // equivalence classes of isomorphic primary outputs
Vec_Int_t * vStatuses; // problem status for each output
Vec_Int_t * vAbcObjIds; // object IDs
int Status; // the status of verification problem (proved=1, disproved=0, undecided=-1)
int nFrames; // the number of time frames completed by BMC
......
src/proof/pdr/pdr.h
......@@ -67,7 +67,7 @@ struct Pdr_Par_t_
int(*pFuncStop)(int); // callback to terminate
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
clock_t timeLastSolved; // the time when the last output was solved
int * pOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
};
////////////////////////////////////////////////////////////////////////
......
src/proof/pdr/pdrCore.c
......@@ -592,7 +592,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // SAT
}
p->pPars->nFailOuts++;
if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
if ( p->vCexes == NULL )
......@@ -684,7 +684,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // SAT
}
p->pPars->nFailOuts++;
if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
......@@ -719,7 +719,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pTime4Outs[p->iOutCur] == 0 && p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL )
{
p->pPars->nDropOuts++;
if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = -1;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
// printf( "Dropping output %d.\n", p->iOutCur );
}
}
......@@ -765,10 +765,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
// count the number of UNSAT outputs
p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
// convert previously 'unknown' into 'unsat'
if ( p->pPars->pOutMap )
if ( p->pPars->vOutMap )
for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
if ( p->pPars->pOutMap[k] == -2 ) // unknown
p->pPars->pOutMap[k] = 1; // unsat
if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown
Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
return p->vCexes ? 0 : 1; // UNSAT
}
if ( p->pPars->fVerbose )
......@@ -836,7 +836,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
{
Pdr_Man_t * p;
int RetValue;
int k, RetValue;
clock_t clk = clock();
if ( pPars->nTimeOutOne )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
......@@ -871,6 +871,11 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
p->tTotal += clock() - clk;
Pdr_ManStop( p );
pPars->iFrame--;
// convert all -2 (unknown) entries into -1 (undec)
if ( pPars->vOutMap )
for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
return RetValue;
}
......
src/proof/pdr/pdrMan.c
......@@ -83,10 +83,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
}
if ( pPars->fSolveAll )
{
int i;
pPars->pOutMap = ABC_ALLOC( int, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
pPars->pOutMap[i] = -2; // unknown
p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
}
return p;
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment