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

Multi-output property solver.

This commit is contained in:
Alan Mishchenko 2013-10-26 23:05:13 -07:00
parent 9437664596
commit 3b30fb2a11
6 changed files with 79 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -32346,16 +32346,15 @@ usage:
***********************************************************************/
int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose );
Vec_Int_t * vStatuses;
int TimeOutGlo = 30;
int TimeOutLoc = 2;
int TimeOutInc = 2;
int fUseSyn = 0;
int c, fVerbose = 0;
int fVeryVerbose = 0;
extern int Gia_ManMultiProve( Gia_Man_t * p, Bmc_MulPar_t * pPars );
Vec_Int_t * vStatuses; int c;
Bmc_MulPar_t Pars, * pPars = &Pars;
memset( pPars, 0, sizeof(Bmc_MulPar_t) );
pPars->TimeOutGlo = 30;
pPars->TimeOutLoc = 2;
pPars->TimeOutInc = 100;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsdvwh" ) ) != EOF )
{
switch ( c )
{
@ -32365,9 +32364,9 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
TimeOutGlo = atoi(argv[globalUtilOptind]);
pPars->TimeOutGlo = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( TimeOutGlo < 0 )
if ( pPars->TimeOutGlo < 0 )
goto usage;
break;
case 'L':
@ -32376,9 +32375,9 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
TimeOutLoc = atoi(argv[globalUtilOptind]);
pPars->TimeOutLoc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( TimeOutLoc <= 0 )
if ( pPars->TimeOutLoc <= 0 )
goto usage;
break;
case 'M':
@ -32387,19 +32386,22 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
TimeOutInc = atoi(argv[globalUtilOptind]);
pPars->TimeOutInc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( TimeOutInc <= 0 )
if ( pPars->TimeOutInc <= 0 )
goto usage;
break;
case 's':
fUseSyn ^= 1;
pPars->fUseSyn ^= 1;
break;
case 'd':
pPars->fDumpFinal ^= 1;
break;
case 'v':
fVerbose ^= 1;
pPars->fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
@ -32412,21 +32414,22 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" );
return 1;
}
pAbc->Status = Gia_ManMultiProve( pAbc->pGia, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
pAbc->Status = Gia_ManMultiProve( pAbc->pGia, pPars );
vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec );
Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
return 0;
usage:
Abc_Print( -2, "usage: &mprove [-TLM num] [-svwh]\n" );
Abc_Print( -2, "usage: &mprove [-TLM num] [-sdvwh]\n" );
Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" );
Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", TimeOutGlo );
Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", TimeOutLoc );
Abc_Print( -2, "\t-M num : approximate multiple of the local runtime limit [default = %d]\n", TimeOutInc );
Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", fUseSyn? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing additional verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", pPars->TimeOutGlo );
Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", pPars->TimeOutLoc );
Abc_Print( -2, "\t-M num : percentage of local runtime limit increase [default = %d]\n", pPars->TimeOutInc );
Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", pPars->fUseSyn? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping invariant into a file [default = %s]\n", pPars->fDumpFinal? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing additional verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}

7
src/base/abci/abcDar.c
View File

@ -2174,16 +2174,17 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
{
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 );
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 );
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, ". " );
}
Abc_Print( 1, " after %d frames", pPars->iFrame );
Abc_Print( 1, ". " );
}
}
ABC_PRT( "Time", Abc_Clock() - clk );

2
src/proof/ssw/sswRarity.c
View File

@ -1112,12 +1112,14 @@ 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 )
{

12
src/sat/bmc/bmc.h
View File

@ -91,6 +91,18 @@ struct Bmc_AndPar_t_
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of dropped outputs
};
typedef struct Bmc_MulPar_t_ Bmc_MulPar_t;
struct Bmc_MulPar_t_
{
int TimeOutGlo;
int TimeOutLoc;
int TimeOutInc;
int fUseSyn;
int fDumpFinal;
int fVerbose;
int fVeryVerbose;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///

2
src/sat/bmc/bmcBmc3.c
View File

@ -1353,7 +1353,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
goto finish;
}
// consider the next timeframe
if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
if ( (RetValue == -1 || pPars->fSolveAll) && pPars->nStart == 0 && !nJumpFrame )
pPars->iFrame = f-1;
// map nodes of this section
Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );

52
src/sat/bmc/bmcMulti.c
View File

@ -20,7 +20,9 @@
#include "bmc.h"
#include "proof/ssw/ssw.h"
#include "misc/extra/extra.h"
#include "aig/gia/giaAig.h"
#include "aig/ioa/ioa.h"
ABC_NAMESPACE_IMPL_START
@ -128,7 +130,7 @@ Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
{
Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim;
Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
@ -136,12 +138,12 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Vec_Ptr_t * vCexes;
Aig_Man_t * pTemp;
abctime clkStart = Abc_Clock();
int nTimeToStop = TimeOutGlo ? TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
int nTimeToStop = pPars->TimeOutGlo ? pPars->TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
int nTotalPo = Saig_ManPoNum(p);
int nTotalSize = Aig_ManObjNum(p);
int i, RetValue = -1;
if ( fVerbose )
printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d.\n", TimeOutGlo, TimeOutLoc, TimeOutInc );
if ( pPars->fVerbose )
printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
// create output map
vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
vCexes = Vec_PtrStart( Saig_ManPoNum(p) ); // maps solved outputs into their CEXes (or markers)
@ -151,8 +153,8 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Ssw_RarSetDefaultParams( pParsSim );
pParsSim->fSolveAll = 1;
pParsSim->fNotVerbose = 1;
pParsSim->fSilent = !fVeryVerbose;
pParsSim->TimeOut = TimeOutLoc;
pParsSim->fSilent = !pPars->fVeryVerbose;
pParsSim->TimeOut = pPars->TimeOutLoc;
pParsSim->nRandSeed = (i * 17) % 500;
RetValue *= Ssw_RarSimulate( p, pParsSim );
// sort outputs
@ -166,13 +168,13 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Vec_IntFree( vLeftOver );
Aig_ManStop( pTemp );
}
if ( fVerbose )
if ( pPars->fVerbose )
Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
// check timeout
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
if ( nTimeToStop && pPars->TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
{
printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
}
@ -180,9 +182,12 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Saig_ParBmcSetDefaultParams( pParsBmc );
pParsBmc->fSolveAll = 1;
pParsBmc->fNotVerbose = 1;
pParsBmc->fSilent = !fVeryVerbose;
pParsBmc->nTimeOut = TimeOutLoc;
pParsBmc->fSilent = !pPars->fVeryVerbose;
pParsBmc->nTimeOut = pPars->TimeOutLoc;
RetValue *= Saig_ManBmcScalable( p, pParsBmc );
if ( pPars->fVeryVerbose )
Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n",
Saig_ManPoNum(p) - Vec_PtrCountZero(p->vSeqModelVec), Saig_ManPoNum(p), pParsBmc->iFrame );
// sort outputs
if ( p->vSeqModelVec )
{
@ -194,41 +199,46 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc,
Vec_IntFree( vLeftOver );
Aig_ManStop( pTemp );
}
if ( fVerbose )
if ( pPars->fVerbose )
Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
// check timeout
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
if ( nTimeToStop && pPars->TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
{
printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
}
// synthesize
if ( fUseSyn )
if ( pPars->fUseSyn )
{
p = Gia_ManMultiProveSyn( pTemp = p, fVerbose, fVeryVerbose );
p = Gia_ManMultiProveSyn( pTemp = p, pPars->fVerbose, pPars->fVeryVerbose );
Aig_ManStop( pTemp );
if ( fVerbose )
if ( pPars->fVerbose )
Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
}
// increase timeout
TimeOutLoc *= TimeOutInc;
pPars->TimeOutLoc += pPars->TimeOutLoc * pPars->TimeOutInc / 100;
}
Vec_IntFree( vOutMap );
if ( pPars->fDumpFinal )
{
char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );
Ioa_WriteAiger( p, pFileName, 0, 0 );
printf( "Final AIG was dumped into file \"%s\".\n", pFileName );
}
Aig_ManStop( p );
return vCexes;
}
int Gia_ManMultiProve( Gia_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fUseSyn, int fVerbose, int fVeryVerbose )
int Gia_ManMultiProve( Gia_Man_t * p, Bmc_MulPar_t * pPars )
{
Aig_Man_t * pAig;
if ( p->vSeqModelVec )
Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL;
pAig = Gia_ManToAig( p, 0 );
p->vSeqModelVec = Gia_ManMultiProveAig( pAig, TimeOutGlo, TimeOutLoc, TimeOutInc, fUseSyn, fVerbose, fVeryVerbose );
p->vSeqModelVec = Gia_ManMultiProveAig( pAig, pPars ); // deletes pAig
assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) );
// Aig_ManStop( pAig );
return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0;
}