Skip to content

A
abc
Commit 47afd0f4 by Alan Mishchenko
Options

Multi-output property solver.

parent 8ad1729a
Showing with 126 additions and 45 deletions
abclib.dsp
......@@ -1447,6 +1447,10 @@ SOURCE=.\src\sat\bmc\bmcLoad.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcMulti.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcUnroll.c
# End Source File
# End Group
......
src/aig/gia/gia.h
......@@ -133,6 +133,7 @@ struct Gia_Man_t_
Vec_Int_t * vLutConfigs; // LUT configurations
Abc_Cex_t * pCexComb; // combinational counter-example
Abc_Cex_t * pCexSeq; // sequential counter-example
Vec_Ptr_t * vSeqModelVec; // sequential counter-examples
int * pCopies; // intermediate copies
Vec_Int_t * vTruths; // used for truth table computation
Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc
......
src/aig/gia/giaMan.c
......@@ -72,6 +72,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax )
***********************************************************************/
void Gia_ManStop( Gia_Man_t * p )
{
if ( p->vSeqModelVec )
Vec_PtrFreeFree( p->vSeqModelVec );
Gia_ManStaticFanoutStop( p );
Tim_ManStopP( (Tim_Man_t **)&p->pManTime );
assert( p->pManTime == NULL );
......
src/aig/gia/giaUtil.c
......@@ -1716,7 +1716,7 @@ int Gia_ManHasChoices_very_old( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * pInit, char * pCommLine, int nGroupSize, int fVerbose )
{
Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame();
Gia_Man_t * p = Gia_ManDup( pInit );
......
src/base/abci/abc.c
......@@ -398,6 +398,7 @@ static int Abc_CommandAbc9Cycle ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Cone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Slice ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -961,6 +962,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&cone", Abc_CommandAbc9Cone, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&slice", Abc_CommandAbc9Slice, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&popart", Abc_CommandAbc9PoPart, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gprove", Abc_CommandAbc9GroupProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 );
......@@ -32259,9 +32261,9 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandAbc9GroupProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose );
extern Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose );
Vec_Int_t * vStatus;
char * pCommLine = NULL;
int c, nGroupSize = 1, fVerbose = 0;
......@@ -32300,15 +32302,15 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
Abc_Print( -1, "Abc_CommandAbc9GroupProve(): There is no AIG.\n" );
return 1;
}
vStatus = Gia_ManMultiProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose );
vStatus = Gia_ManGroupProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose );
Vec_IntFree( vStatus );
return 0;
usage:
Abc_Print( -2, "usage: &mprove [-GS num] [-vh]\n" );
Abc_Print( -2, "usage: &gprove [-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 );
......@@ -32329,6 +32331,56 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose );
Vec_Int_t * vStatuses;
char * pCommLine = NULL;
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_CommandAbc9PoPart(): There is no AIG.\n" );
return 1;
}
pAbc->Status = Gia_ManMultiProve( pAbc->pGia, fVerbose );
vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec );
Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
return 0;
usage:
Abc_Print( -2, "usage: &mprove [-vh]\n" );
Abc_Print( -2, "\t proves multi-output testcase by applying several engines\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_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c;
src/base/abci/abcDar.c
......@@ -2138,56 +2138,62 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 )
{
Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) );
}
else if ( RetValue == -1 )
if ( !pPars->fSilent )
{
if ( pPars->nFailOuts == 0 )
if ( RetValue == 1 )
{
Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
if ( nTimeOut && Abc_Clock() > nTimeOut )
Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
else
Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) );
}
else
else if ( RetValue == -1 )
{
Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
if ( Abc_Clock() > nTimeOut )
Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
if ( pPars->nFailOuts == 0 )
{
Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
if ( nTimeOut && Abc_Clock() > nTimeOut )
Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
else
Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
}
else
Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
}
}
else // if ( RetValue == 0 )
{
if ( !pPars->fSolveAll )
{
Abc_Cex_t * pCex = pNtk->pSeqModel;
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
{
Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
if ( Abc_Clock() > nTimeOut )
Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
else
Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
}
}
else
else // if ( RetValue == 0 )
{
int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs );
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
if ( !pPars->fSolveAll )
{
Abc_Cex_t * pCex = pNtk->pSeqModel;
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
}
else
{
Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
if ( pPars->nDropOuts )
Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
Abc_Print( 1, ". " );
int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs );
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
else
{
Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
if ( pPars->nDropOuts )
Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
Abc_Print( 1, ". " );
}
}
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
ABC_PRT( "Time", Abc_Clock() - clk );
}
if ( RetValue == 0 && pPars->fSolveAll )
{
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
ABC_PRT( "Time", Abc_Clock() - clk );
if ( pNtk->pSeqModel )
{
status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
......
src/proof/ssw/ssw.h
......@@ -101,6 +101,7 @@ struct Ssw_RarPars_t_
int fSetLastState;
int fVerbose;
int fNotVerbose;
int fSilent;
int fDropSatOuts;
int fMiter;
int fUseCex;
......
src/proof/ssw/sswRarity.c
......@@ -1051,16 +1051,22 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
// check timeout
if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
{
if ( !pPars->fSilent )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
}
goto finish;
}
if ( pPars->TimeOutGap && timeLastSolved && Abc_Clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
{
if ( !pPars->fSilent )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_Print( 1, "Reached gap timeout (%d sec).\n", pPars->TimeOutGap );
}
goto finish;
}
// check if all outputs are solved by now
......@@ -1106,15 +1112,21 @@ finish:
}
if ( pPars->nSolved )
{
if ( !pPars->fSilent )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
}
else if ( r == pPars->nRounds && f == pPars->nFrames )
{
if ( !pPars->fSilent )
{
if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
}
// cleanup
Ssw_RarManStop( p );
......
src/sat/bmc/bmc.h
......@@ -65,6 +65,7 @@ struct Saig_ParBmc_t_
int nLearnedPerce; // ratio of learned clause limit
int fVerbose; // verbose
int fNotVerbose; // skip line-by-line print-out
int fSilent; // completely silent
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of dropped outputs
......
src/sat/bmc/bmcBmc3.c
......@@ -1397,7 +1397,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
}
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
{
Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
if ( !pPars->fSilent )
Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
goto finish;
}
// skip solved outputs
......
src/sat/bmc/module.make
......@@ -8,4 +8,5 @@ SRC += src/sat/bmc/bmcBmc.c \
src/sat/bmc/bmcCexMin2.c \
src/sat/bmc/bmcCexTools.c \
src/sat/bmc/bmcLoad.c \
src/sat/bmc/bmcMulti.c \
src/sat/bmc/bmcUnroll.c
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